feat: add Stone duality theorem for clopen sets in complete types

Author: NoneMore

Mathlib/ModelTheory/Topology/Types.lean

@@ -95,6 +95,27 @@ instance : CompactSpace (T.CompleteType α) := by
       obtain ⟨_, rfl⟩ := h.2
       exact h.1
 
-instance : BaireSpace (T.CompleteType α) := BaireSpace.of_t2Space_locallyCompactSpace
+/--
+Stone Duality:
+Every clopen set in the Stone space of types corresponds to the set of types
+consistent with some sentence φ.
+-/
+theorem exists_sentence_of_isClopen (U : Set (CompleteType T α)) :
+    IsClopen U → ∃ (φ : L[[α]].Sentence), U = typesWith (T := T) φ := by
+  intro hU
+  obtain ⟨ι,S,hUS,hS⟩ := IsTopologicalBasis.open_eq_iUnion typesWith_basis hU.2
+  obtain ⟨F,hF⟩ := IsCompact.elim_finite_subcover hU.1.isCompact S
+    (fun i => IsTopologicalBasis.isOpen typesWith_basis (hS i))
+    (hUS.subset)
+  replace hF : U = ⋃ i ∈ F, S i := Subset.antisymm hF (by
+    rw [hUS]
+    exact iUnion₂_subset_iUnion (Membership.mem F) S
+  )
+  choose φs hφs using hS
+  exists Formula.iSup (fun (x : F) => φs x.1)
+  simp [typesWith_iSup, hF, hφs]
+  exact Eq.symm (iUnion_subtype (Membership.mem F) fun x ↦ S ↑x)
+
+instance {n : ℕ} : BaireSpace (T.CompleteType (Fin n)) := BaireSpace.of_t2Space_locallyCompactSpace
 
 end CompleteType

Mathlib/ModelTheory/Types.lean

@@ -193,6 +193,17 @@ lemma typesWith_inf (φ ψ : L[[α]].Sentence)
   simp only [p.isMaximal.mem_iff_models, ModelsBoundedFormula, ←forall_and]
   exact forall₃_congr fun _ _ _ ↦ BoundedFormula.realize_inf
 
+lemma typesWith_iSup {β : Type*} [Finite β] (f : β → L[[α]].Sentence) :
+    typesWith (T := T) (Formula.iSup f) = ⋃ (i : β), typesWith (f i) := by
+  ext p
+  simp only [typesWith, Set.mem_setOf_eq, Set.mem_iUnion]
+  obtain ⟨M⟩ := p.isMaximal'.1
+  have : ∀ φ, φ ∈ ↑p ↔ φ.Realize M.Carrier := by
+    intro φ
+    simp [←SetLike.mem_coe, p.isMaximal.mem_iff_models]
+    exact (p.isMaximal.isComplete.realize_sentence_iff φ M).symm
+  simp only [this, Sentence.Realize, Formula.realize_iSup]
+
 lemma typesWith_mem {φ} (hφ : φ ∈ (L.lhomWithConstants α).onTheory T)
     : typesWith (T := T) φ = Set.univ
   := univ_subset_iff.mp fun p _ ↦ p.subset hφ