Theorems · Theorem · general topology
TopologicalSpace.exists_countable_basis
∀ (α : Type u) [t : TopologicalSpace α] [SecondCountableTopology α], ∃ b, b.Countable ∧ ∅ ∉ b ∧ TopologicalSpace.IsTopologicalBasis b
- Defined in
- Mathlib.Topology.Bases
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
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.ofPredproof · cited by 6,101
- Set.imageproof · cited by 5,609
- Set.Finiteproof · cited by 1,814
- SecondCountableTopologystatement and proof · cited by 750
- Set.Countablestatement and proof · cited by 545
- Set.sInterproof · cited by 225
- Set.sdiff_subsetproof · cited by 156
- TopologicalSpace.IsTopologicalBasisstatement · cited by 126
- TopologicalSpace.generateFromproof · cited by 62
- Set.Countable.imageproof · cited by 47
Cited by10
Results whose statement or proof uses this declaration.
- TopologicalSpace.countableBasisproof · cited by 14
- TopologicalSpace.isBasis_countableBasisproof · cited by 10
- TopologicalSpace.countable_countableBasisproof · cited by 8
- Measurable.exists_continuousproof · cited by 2
- Topology.IsQuotientMap.secondCountableTopologyproof · cited by 1
- MeasureTheory.measurableSet_range_of_continuous_injectiveproof · cited by 1
- TopologicalSpace.empty_notMem_countableBasisproof · cited by 1
- exists_countable_union_perfect_of_isClosedproof · cited by 1
- TopologicalSpace.exists_isInducing_l_inftyproof · cited by 1
- TopologicalSpace.exists_seq_basisproof · cited by 0