Theorems · Theorem · general topology
TopologicalSpace.le_generateFrom_iff_subset_isOpen
∀ {α : Type u} {g : Set (Set α)} {t : TopologicalSpace α}, t ≤ TopologicalSpace.generateFrom g ↔ g ⊆ {s | IsOpen s}- Defined in
- Mathlib.Topology.Order
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Set.ofPredstatement and proof · cited by 6,101
- IsOpenstatement and proof · cited by 2,400
- isOpen_univproof · cited by 112
- IsOpen.interproof · cited by 98
- TopologicalSpace.generateFromstatement and proof · cited by 62
- isOpen_sUnionproof · cited by 15
- TopologicalSpace.GenerateOpenproof · cited by 12
- TopologicalSpace.GenerateOpen.recOnproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- le_generateFromproof · cited by 10
- continuous_generateFrom_iffproof · cited by 7
- TopologicalSpace.gc_generateFromproof · cited by 6
- TopologicalSpace.exists_countable_of_generateFromproof · cited by 1
- exists_countable_generateFrom_Ioi_Iioproof · cited by 0