Theorems · Inductive type · general topology
TopologicalSpace.IsTopologicalBasis
{α : Type u} → [t : TopologicalSpace α] → Set (Set α) → PropA topological basis is one that satisfies the necessary conditions so that it suffices to take unions of the basis sets to get a topology (without taking finite intersections as well).
- Defined in
- Mathlib.Topology.Bases
- Cited by
- 126 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement · cited by 24,529
Cited by133
Results whose statement or proof uses this declaration.
- TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_openstatement and proof · cited by 58
- TopologicalSpace.IsTopologicalBasis.isOpenstatement and proof · cited by 31
- TopologicalSpace.Opens.IsBasisproof · cited by 30
- TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhdsstatement · cited by 22
- PrimeSpectrum.isBasis_basic_opensproof · cited by 16
- TopologicalSpace.IsTopologicalBasis.mem_nhds_iffstatement and proof · cited by 13
- AlgebraicGeometry.iSup_affineOpens_eq_topproof · cited by 13
- PrimeSpectrum.isTopologicalBasis_basic_opensstatement · cited by 11
- TopologicalSpace.isBasis_countableBasisstatement · cited by 10
- TopologicalSpace.IsTopologicalBasis.eq_generateFromstatement and proof · cited by 10
- TopologicalSpace.IsTopologicalBasis.nhds_hasBasisstatement and proof · cited by 10
- TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'statement and proof · cited by 9