Theorems · Theorem · general topology
TopologicalSpace.PseudoMetrizableSpace.exists_countably_generated
∀ {X : Type u_5} {t : TopologicalSpace X} [self : TopologicalSpace.PseudoMetrizableSpace X],
∃ u, u.toTopologicalSpace = t ∧ (uniformity X).IsCountablyGenerated- Defined in
- Mathlib.Topology.Metrizable.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- UniformSpacestatement · cited by 2,040
- uniformitystatement · cited by 765
- TopologicalSpace.PseudoMetrizableSpacestatement and proof · cited by 245
- Filter.IsCountablyGeneratedstatement · cited by 220
Cited by2
Results whose statement or proof uses this declaration.
- TopologicalSpace.pseudoMetrizableSpaceUniformityproof · cited by 6
- TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generatedproof · cited by 5