English
Distance is preserved when passing to the multiplicative representation.
Русский
Расстояние сохраняется при переходе к умножаемой представимости.
LaTeX
$$$\\mathrm{edist}(a\\toMul, b\\toMul) = \\mathrm{edist}(a,b)$$$
Lean4
/-- Auxiliary function to replace the topology on an emetric space with
a topology which is equal to the original one, but maybe not defeq.
This is useful if one wants to construct an emetric space with a
specified topology. See Note [forgetful inheritance] explaining why having definitionally
the right topology is often important.
See note [reducible non-instances].
-/
abbrev replaceTopology {γ} [T : TopologicalSpace γ] (m : EMetricSpace γ) (H : T = m.toUniformSpace.toTopologicalSpace) :
EMetricSpace γ where
edist := @edist _ m.toEDist
edist_self := edist_self
eq_of_edist_eq_zero := @eq_of_edist_eq_zero _ _
edist_comm := edist_comm
edist_triangle := edist_triangle
toUniformSpace := m.toUniformSpace.replaceTopology H
uniformity_edist := PseudoEMetricSpace.uniformity_edist
