Theorems · Inductive type · general topology
TopologicalSpace.GenerateOpen
{α : Type u} → Set (Set α) → Set α → PropThe open sets of the least topology containing a collection of basic sets.
- Defined in
- Mathlib.Topology.Order
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
Cited by18
Results whose statement or proof uses this declaration.
- TopologicalSpace.generateFromproof · cited by 62
- TopologicalSpace.nhds_generateFromproof · cited by 15
- TopologicalSpace.le_generateFrom_iff_subset_isOpenproof · cited by 5
- Topology.IsLower.isLowerSet_of_isOpenproof · cited by 4
- borel_eq_generateFrom_of_subbasisproof · cited by 2
- generateFrom_insert_of_generateOpenstatement and proof · cited by 2
- IndiscreteTopology.isOpen_iffproof · cited by 2
- TopologicalSpace.mkOfClosurestatement and proof · cited by 1
- Topology.IsLower.isOpen_iff_generate_Ici_complstatement and proof · cited by 1
- isOpen_iff_generate_intervalsstatement and proof · cited by 1
- TopologicalSpace.GenerateOpen.belowstatement · cited by 1
- TopologicalSpace.GenerateOpen.recOnstatement and proof · cited by 1