Theorems · Definition · general topology
TopologicalSpace.Opens.IsBasis
{α : Type u_2} → [inst : TopologicalSpace α] → Set (TopologicalSpace.Opens α) → PropA set of opens α is a basis if the set of corresponding sets is a topological basis.
- Defined in
- Mathlib.Topology.Sets.Opens
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- SetLike.coeproof · cited by 8,199
- Set.imageproof · cited by 5,609
- TopologicalSpace.Opensstatement and proof · cited by 2,040
- TopologicalSpace.IsTopologicalBasisproof · cited by 126
Cited by32
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.isBasis_affineOpensstatement · cited by 37
- PrimeSpectrum.isBasis_basic_opensstatement · cited by 16
- TopologicalSpace.Opens.isBasis_iff_nbhdstatement and proof · cited by 10
- TopologicalSpace.Opens.isBasis_iff_coverstatement and proof · cited by 4
- TopCat.Sheaf.restrictHomEquivHomstatement and proof · cited by 4
- TopologicalSpace.Opens.IsBasis.exists_finite_of_isCompactstatement and proof · cited by 3
- AlgebraicGeometry.isBasis_basicOpenstatement and proof · cited by 3
- AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpenstatement · cited by 2
- TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnionstatement and proof · cited by 2
- TopologicalSpace.Opens.IsBasis.of_isInducingstatement and proof · cited by 2
- TopCat.Sheaf.extend_hom_appstatement and proof · cited by 2