Mathlib Map

Theorems · Definition · general topology

TopologicalSpace.generateFrom

{α : Type u} → Set (Set α) → TopologicalSpace α

The smallest topological space containing the collection g of basic sets

Defined in
Mathlib.Topology.Order
Cited by
62 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

TopologicalSpace.vietoris · cited by 34TopologicalSpace.vietorisPreorder.topology · cited by 24Preorder.topologyTopologicalSpace.nhds_generateFrom · cited by 15TopologicalSpace.nhds_gen…TopologicalSpace.isOpen_generateFrom_of_mem · cited by 11TopologicalSpace.isOpen_g…le_generateFrom · cited by 10le_generateFromTopologicalSpace.IsTopologicalBasis.eq_generateFrom · cited by 10IsTopologicalBasis.eq_gen…TopologicalSpace.exists_countable_basis · cited by 9TopologicalSpace.exists_c…TopologicalSpace.gciGenerateFrom · cited by 9TopologicalSpace.gciGener…Ctop.toTopsp · cited by 8Ctop.toTopspTopology.lower · cited by 7Topology.lowercontinuous_generateFrom_iff · cited by 7continuous_generateFrom_i…TopologicalSpace.generateFrom_anti · cited by 6TopologicalSpace.generate…TopologicalSpace.isTopologicalBasis_of_subbasis · cited by 6TopologicalSpace.isTopolo…TopologicalSpace.gc_generateFrom · cited by 6TopologicalSpace.gc_gener…Topology.upper · cited by 5Topology.upperSet · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceTopologicalSpace.GenerateOpen · cited by 12TopologicalSpace.Generate…TopologicalSpace.generateFromCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by74

Results whose statement or proof uses this declaration.