Theorems · Theorem · general topology
TopologicalSpace.gc_generateFrom
∀ (α : Type u_1),
GaloisConnection (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)- Defined in
- Mathlib.Topology.Order
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Equivstatement · cited by 8,337
- Set.ofPredstatement · cited by 6,101
- IsOpenstatement · cited by 2,400
- OrderDualstatement and proof · cited by 927
- OrderDual.toDualstatement · cited by 481
- OrderDual.ofDualstatement · cited by 400
- GaloisConnectionstatement · cited by 253
- TopologicalSpace.generateFromstatement · cited by 62
- TopologicalSpace.le_generateFrom_iff_subset_isOpenproof · cited by 5
Cited by7
Results whose statement or proof uses this declaration.
- TopologicalSpace.gciGenerateFromproof · cited by 9
- TopologicalSpace.generateFrom_antiproof · cited by 6
- setOfPred_isOpen_iSupproof · cited by 2
- generateFrom_iUnionproof · cited by 1
- setOfPred_isOpen_sSupproof · cited by 1
- generateFrom_sUnionproof · cited by 0
- generateFrom_unionproof · cited by 0