Theorems · Definition · general topology

PseudoMetricSpace.replaceUniformity

{α : Type u_3} → [U : UniformSpace α] → (m : PseudoMetricSpace α) → uniformity α = uniformity α → PseudoMetricSpace α

Build a new pseudometric space from an old one where the bundled uniform structure is provably (but typically non-definitionaly) equal to some given uniform structure. See Note [forgetful inheritance]. See Note [reducible non-instances].

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Cited by

1 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpace