English
There is a Galois coinsertion between the lattice of topologies on α and the dual lattice of subsets of α, with lower part sending a topology to its open-sets and upper part sending a collection to the topology they generate.
Русский
Существует кофункция Гальуа между решеткой топологий на α и двойственной решеткой подмножеств α: нижняя часть отправляет топологию в её множество открытых, верхняя — множество порождающих топологию.
LaTeX
$$GaloisCoinsertion (\\lambda t : TopologicalSpace α => OrderDual.toDual {s | IsOpen s}) (generateFrom ∘ OrderDual.ofDual)$$
Lean4
/-- The Galois coinsertion between `TopologicalSpace α` and `(Set (Set α))ᵒᵈ` whose lower part sends
a topology to its collection of open subsets, and whose upper part sends a collection of subsets
of `α` to the topology they generate. -/
def gciGenerateFrom (α : Type*) :
GaloisCoinsertion (fun t : TopologicalSpace α => OrderDual.toDual {s | IsOpen[t] s})
(generateFrom ∘ OrderDual.ofDual)
where
gc := gc_generateFrom α
u_l_le _ s hs := TopologicalSpace.GenerateOpen.basic s hs
choice g hg := TopologicalSpace.mkOfClosure g (Subset.antisymm hg <| le_generateFrom_iff_subset_isOpen.1 <| le_rfl)
choice_eq _ _ := mkOfClosure_sets
