English
There is a Galois connection between the maps t ↦ {s | IsOpen[t] s} and generateFrom, given by the duality between topologies and generated topologies.
Русский
Существует связь Гальуа между отображениями, отправляющими топологию в множество открытых, и порождающим топологию, с учетом дуальности между топологиями и порождаемыми топологиями.
LaTeX
$$GaloisConnection (\\lambda t : TopologicalSpace α => OrderDual.toDual {s | IsOpen[s of t] s}) (Function.comp TopologicalSpace.generateFrom (OrderDual.ofDual))$$
Lean4
theorem mono (h : t₁ ≤ t₂) : closure[t₁] s ⊆ closure[t₂] s :=
@closure_minimal _ t₁ s (@closure _ t₂ s) subset_closure (IsClosed.mono isClosed_closure h)
