English
There is a Galois connection between the poset of topologies on α and the dual of the set-of-open-sets operator, given by t ↦ {s | IsOpen[t] s} and g ↦ generateFrom g.
Русский
Между частично упорядованными множествами топологий на α и двойственным порядком операции 'множество открытых', существует связь Гальуа: t ↦ {s | IsOpen[t] s}, g ↦ generateFrom g.
LaTeX
$$GaloisConnection (\\lambda t : TopologicalSpace α. => OrderDual.toDual {s | IsOpen[t] s}) (generateFrom ∘ OrderDual.ofDual)$$
Lean4
theorem gc_generateFrom (α) :
GaloisConnection (fun t : TopologicalSpace α => OrderDual.toDual {s | IsOpen[t] s})
(generateFrom ∘ OrderDual.ofDual) :=
fun _ _ => le_generateFrom_iff_subset_isOpen.symm
