diff --git a/.obsidian/appearance.json b/.obsidian/appearance.json
index 4ffdb128..f62f8e56 100644
--- a/.obsidian/appearance.json
+++ b/.obsidian/appearance.json
@@ -9,7 +9,6 @@
     "tabs_on_multiple_rown",
     "popup_preview_size",
     "checkboxes",
-    "custom_callouts",
     "darkmode",
     "breadcrumbs",
     "[ui] Ultra Compact Tab Header",
@@ -42,7 +41,8 @@
     "supercharged-links-gen",
     "stacked_tabs",
     "vertical_stacked_tabs",
-    "headers"
+    "headers",
+    "custom_callouts"
   ],
   "interfaceFontFamily": "CMU Bright,CMU Sans Serif,FiraCode Nerd Font",
   "textFontFamily": "CMU Sans Serif,FiraCode Nerd Font,CMU Serif",
diff --git a/famille filtrante.md b/famille filtrante.md
new file mode 100644
index 00000000..a4c0f3e4
--- /dev/null
+++ b/famille filtrante.md	
@@ -0,0 +1,21 @@
+---
+up:
+  - "[[filtre]]"
+tags:
+  - s/maths/logique
+  - s/maths/topologie
+aliases:
+---
+
+> [!definition] Définition
+> Un ensemble ordonné $(I, <)$ est **filtrant** si :
+> pour tout $i, j \in I$ il existe $k \in I$ tel que $i \leq k$ et $j \leq k$
+> $\forall i, j \in I,\quad \exists k \in I,\quad i \leq k \wedge j \leq k$
+>  - I tout paire d'éléments est majorée par au moins un élément
+>      - ! ne pas confondre avec la propriété des [[treillis]] qui affirme qu'il existe une borne supérieur (i.e. un plus petit majorant) : ici, on peut avoir plusieurs majorants indiscernables.
+^definition
+
+# Propriétés
+
+# Exemples
+
diff --git a/obsidian callouts.md b/obsidian callouts.md
index dc44b3c3..ea5d823d 100644
--- a/obsidian callouts.md	
+++ b/obsidian callouts.md	
@@ -47,7 +47,6 @@ Il existe 12 types par défaut :
 
 ### Exemples
 
-
 #### Callouts natifs
 Voici les types de callout natifs à obsidian :
 
diff --git a/théorie logique.md b/théorie logique.md
index 8cd477f1..59cc5649 100644
--- a/théorie logique.md	
+++ b/théorie logique.md	
@@ -6,6 +6,7 @@
 
 # Propriétés
 
+## Cohérence
 > [!proposition]+ Cohérence
 > une théorie est cohérente     
 > 
@@ -32,9 +33,36 @@
 > > > Soit $F \subseteq T$ une partie finie de $T$
 > > > On se demande si $F$ est cohérente
 > > > $f \in F \leadsto n_{f} \in \mathbb{N} \text{ tq } f \in T_{n_{f}}$
-> > > $\displaystyle n = min_{f \in F}(n_{f})$
-
+> > > $\displaystyle n = \min_{f \in F}(n_{f})$
+> > > $F \subseteq T_{n}$ cohérente par hypothèses 
+> > > Donc $F$ est cohérente
+>  
+> > [!corollaire] 
+> > Soit $(T_{i})_{i \in I}$ une **[[famille filtrante]]** de théories **cohérentes**
+> > Alors $\displaystyle \bigcup _{i \in I} T_{i}$ est cohérente
+> 
+> > [!corollaire] 
+> > Si $T$ est une théorie cohérente
+> > Il existe une théorie cohérente $T'$ telle que $T \subseteq T'$ et qui est maximale (parmi les théories cohérentes contenant $T$) :
+> > $\begin{cases} T \subseteq T' \\ T' \text{ est cohérente} \\ \text{si } f \not\subset T',\quad T' \cup \{  f  \} \text{ n'est pas cohérente} \end{cases}$
+> > 
+> > > [!démonstration]- Démonstration
+> > > Application du [[lemme de Zorn]] :
+> > > $\mathscr{C} = \{ \text{théories cohérentes} \}$ est inductif
+> > > toute famille filtrante d'éléments de $\mathscr{C}$ est donc majorée
 
+> [!proposition]+ Théorème de déduction
+> Soit $f$ un énoncé, soit $T$ une théorie
+> On a équivalence entre :
+>  - $T \cup \{ f \} \vdash g$
+>  - $T \vdash f \to g$
+> 
+> > [!démonstration]- Démonstration
+> > Soit $(g_1, \dots, g_{n})$ une démonstration formelle de $T \cup \{ f \} \vdash g$
+> > On obtient une démonstration formelle de $T \vdash f \to g$ en partant de la suite $(f \to g_1, \dots, f\to g_{n})$ et en insérant des formules supplémentaires :
+> > $T \vdash f \to g_1 \qquad T \cup \{ f \}$
+> > $\vdots$
+> > $T \vdash f \to g_{n-1}$