English
A topology on X can be defined by a collection T of closed sets that contains ∅, is closed under arbitrary intersections and under finite unions; then a set is open exactly when its complement lies in T.
Русский
Топология на X задаётся коллекцией T замкнутых множеств, содержащей ∅, замкнутой относительно произвольных пересечений и конечных объединений; тогда множество открыто тогда и только тогда, когда его комплемент принадлежит T.
LaTeX
$$$\text{IsOpen}(s) \iff s^{c} \in T$$$
Lean4
/-- A constructor for topologies by specifying the closed sets,
and showing that they satisfy the appropriate conditions. -/
def ofClosed {X : Type u} (T : Set (Set X)) (empty_mem : ∅ ∈ T) (sInter_mem : ∀ A, A ⊆ T → ⋂₀ A ∈ T)
(union_mem : ∀ A, A ∈ T → ∀ B, B ∈ T → A ∪ B ∈ T) : TopologicalSpace X
where
IsOpen X := Xᶜ ∈ T
isOpen_univ := by simp [empty_mem]
isOpen_inter s t hs ht := by simpa only [compl_inter] using union_mem sᶜ hs tᶜ ht
isOpen_sUnion s
hs := by
simp only [Set.compl_sUnion]
exact sInter_mem (compl '' s) fun z ⟨y, hy, hz⟩ => hz ▸ hs y hy
