English
Construct a new metric space by replacing its uniform structure with a given uniform structure, while preserving the distance relation.
Русский
Построение нового метрического пространства путём замены равномерной структуры на заданную, сохранив при этом отношение расстояний.
LaTeX
$$ReplaceUniformity\;{γ} [U: UniformSpace\ γ] (m: MetricSpace\ γ) (H: 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : MetricSpace γ$$
Lean4
/-- 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].
-/
abbrev replaceUniformity {γ} [U : UniformSpace γ] (m : MetricSpace γ)
(H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : MetricSpace γ
where
toPseudoMetricSpace := PseudoMetricSpace.replaceUniformity m.toPseudoMetricSpace H
eq_of_dist_eq_zero := @eq_of_dist_eq_zero _ _
