MathlibAnnex/Topology/ClosureSpace/Basic.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6module78public import Mathlib.Order.Closure9public import Mathlib.Data.Set.Lattice1011/-!12# Closure spaces without finite-union preservation1314A `ClosureSpace` is explicit data, not a topology or a typeclass. Its order-theoretic15part is Mathlib's `ClosureOperator (Set α)`. Only preservation of the empty set is16added. No finite-union axiom is imposed.1718This implements the basic definitions in Section 3 of arXiv:2504.05551v1.19-/2021@[expose] public section2223set_option autoImplicit false2425universe u2627/-- An extensive, monotone, idempotent set closure that preserves the empty set. -/28structure ClosureSpace (α : Type u) where29  toClosureOperator : ClosureOperator (Set α)30  map_empty' : toClosureOperator ∅ = ∅3132namespace ClosureSpace3334variable {α : Type u}3536/-- The underlying set closure. -/37def closure (c : ClosureSpace α) : Set α → Set α := c.toClosureOperator3839/-- Closedness uses the predicate of the underlying Mathlib closure operator. -/40abbrev IsClosed (c : ClosureSpace α) (s : Set α) : Prop :=41  c.toClosureOperator.IsClosed s4243@[simp]44theorem closure_empty (c : ClosureSpace α) : c.closure ∅ = ∅ := c.map_empty'4546theorem subset_closure (c : ClosureSpace α) (s : Set α) : s ⊆ c.closure s :=47  c.toClosureOperator.le_closure s4849theorem closure_mono (c : ClosureSpace α) {s t : Set α} (h : s ⊆ t) :50    c.closure s ⊆ c.closure t := c.toClosureOperator.monotone h5152@[simp]53theorem closure_closure (c : ClosureSpace α) (s : Set α) :54    c.closure (c.closure s) = c.closure s := c.toClosureOperator.idempotent s5556@[simp]57theorem closure_univ (c : ClosureSpace α) : c.closure Set.univ = Set.univ :=58  c.toClosureOperator.closure_top5960theorem isClosed_iff (c : ClosureSpace α) (s : Set α) :61    c.IsClosed s ↔ c.closure s = s := c.toClosureOperator.isClosed_iff6263theorem isClosed_iff_closure_subset (c : ClosureSpace α) (s : Set α) :64    c.IsClosed s ↔ c.closure s ⊆ s := ClosureOperator.isClosed_iff_closure_le6566@[simp]67theorem isClosed_closure (c : ClosureSpace α) (s : Set α) : c.IsClosed (c.closure s) :=68  c.toClosureOperator.isClosed_closure s6970@[simp]71theorem isClosed_empty (c : ClosureSpace α) : c.IsClosed ∅ :=72  (c.isClosed_iff ∅).2 c.closure_empty7374@[simp]75theorem isClosed_univ (c : ClosureSpace α) : c.IsClosed Set.univ :=76  (c.isClosed_iff Set.univ).2 c.closure_univ7778theorem closure_min (c : ClosureSpace α) {s t : Set α}79    (hst : s ⊆ t) (ht : c.IsClosed t) : c.closure s ⊆ t :=80  ClosureOperator.closure_min hst ht8182theorem isClosed_sInter (c : ClosureSpace α) {S : Set (Set α)}83    (hS : ∀ s ∈ S, c.IsClosed s) : c.IsClosed (⋂₀ S) := by84  apply (c.isClosed_iff_closure_subset _).285  intro x hx86  apply Set.mem_sInter.287  intro s hs88  exact c.closure_min (Set.sInter_subset_of_mem hs) (hS s hs) hx8990/-- The closure is the intersection of all closed supersets; no topology is used. -/91theorem closure_eq_sInter (c : ClosureSpace α) (s : Set α) :92    c.closure s = ⋂₀ {t : Set α | s ⊆ t ∧ c.IsClosed t} := by93  apply Set.Subset.antisymm94  · intro x hx95    apply Set.mem_sInter.296    intro t ht97    exact c.closure_min ht.1 ht.2 hx98  · intro x hx99    exact Set.mem_sInter.1 hx (c.closure s) ⟨c.subset_closure s, c.isClosed_closure s⟩100101/-- Finite-union preservation, the extra condition for a topological closure. -/102def IsTopologizable (c : ClosureSpace α) : Prop :=103  ∀ s t : Set α, c.closure (s ∪ t) = c.closure s ∪ c.closure t104105theorem isTopologizable_iff (c : ClosureSpace α) :106    c.IsTopologizable ↔ ∀ s t : Set α, c.closure (s ∪ t) ⊆ c.closure s ∪ c.closure t := by107  constructor108  · intro h s t109    exact (h s t).subset110  · intro h s t111    apply Set.Subset.antisymm (h s t)112    intro x hx113    rcases hx with hx | hx114    · exact c.closure_mono Set.subset_union_left hx115    · exact c.closure_mono Set.subset_union_right hx116117/-- The specialization preorder of an arbitrary closure space is antisymmetric. -/118def IsT0 (c : ClosureSpace α) : Prop :=119  ∀ x y : α, x ∈ c.closure {y} → y ∈ c.closure {x} → x = y120121/-- Every singleton is closed. -/122def IsT1 (c : ClosureSpace α) : Prop := ∀ x : α, c.IsClosed {x}123124theorem IsT1.isT0 {c : ClosureSpace α} (h : c.IsT1) : c.IsT0 := by125  intro x y hxy _126  have hy := (c.isClosed_iff {y}).1 (h y)127  rw [hy] at hxy128  exact Set.mem_singleton_iff.1 hxy129130end ClosureSpace