Theorems · Definition · general topology

MetricSpace.replaceUniformity

{γ : Type u_3} → [U : UniformSpace γ] → (m : MetricSpace γ) → uniformity γ = uniformity γ → MetricSpace γ

Build a new metric 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.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace