English
If a collection s of subsets equals the collection of sets that are open in the topology they generate, then the structure with IsOpen(U) defined by U ∈ s is a topology on α.
Русский
Если множество подмножеств s совпадает с множеством подмножеств, открытых в топологии, которая порождается s, то структура, задаваемая IsOpen(U) ⇔ U ∈ s, является топологией на α.
LaTeX
$$$\\text{If } \\{U : \\mathcal P(\\alpha) : \\IsOpen[t](U) \\} = s \\text{, then } \\TopologicalSpace.mkOfClosure\\;s\\;hs \\text{ defines a topology on } \\alpha.$$$
Lean4
/-- If `s` equals the collection of open sets in the topology it generates, then `s` defines a
topology. -/
protected def mkOfClosure (s : Set (Set α)) (hs : {u | GenerateOpen s u} = s) : TopologicalSpace α
where
IsOpen u := u ∈ s
isOpen_univ := hs ▸ TopologicalSpace.GenerateOpen.univ
isOpen_inter := hs ▸ TopologicalSpace.GenerateOpen.inter
isOpen_sUnion := hs ▸ TopologicalSpace.GenerateOpen.sUnion
