Theorems · Definition · general topology
TopologicalSpace.pseudoMetrizableSpaceUniformity
(X : Type u_5) → [inst : TopologicalSpace X] → [h : TopologicalSpace.PseudoMetrizableSpace X] → UniformSpace X
Construct on a pseudometrizable space a countably generated uniformity
compatible with the topology. Use pseudoMetrizableSpaceUniformity_countably_generated for a proof
that this uniformity is countably generated.
- Defined in
- Mathlib.Topology.Metrizable.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound
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
- TopologicalSpace.PseudoMetrizableSpacestatement and proof · cited by 245
- UniformSpace.replaceTopologyproof · cited by 2
- TopologicalSpace.PseudoMetrizableSpace.exists_countably_generatedproof · cited by 1
Cited by6
Results whose statement or proof uses this declaration.
- TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generatedstatement · cited by 5
- TopologicalSpace.IsSeparable.secondCountableTopologyproof · cited by 4
- IsGδ.setOfPred_continuousAtproof · cited by 2
- TopologicalSpace.IsSeparable.exists_countable_dense_subsetproof · cited by 2
- Topology.IsInducing.isSeparable_preimageproof · cited by 1
- Topology.IsInducing.pseudoMetrizableSpaceproof · cited by 1