Theorems · Definition · general topology

TopologicalSpace.gciGenerateFrom

(α : Type u_1) →
  GaloisCoinsertion (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)

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.

Defined in

Mathlib.Topology.Order

Cited by

9 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound