English
The distance is preserved under certain multiplicative embeddings: edist(a,b) = edist(ofMul a, ofMul b).
Русский
Расстояние сохраняется под определёнными умножающими вложениями: edist(a,b) = edist(ofMul a, ofMul b).
LaTeX
$$$\\mathrm{edist}(a,b) = \\mathrm{edist}(\\mathrm{ofMul}\\ a, \\mathrm{ofMul}\\ b)$$$
Lean4
/-- Auxiliary function to replace the uniformity on an emetric space with
a uniformity 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 uniformity. See Note [forgetful inheritance] explaining why having definitionally
the right uniformity is often important.
See note [reducible non-instances].
-/
abbrev replaceUniformity {γ} [U : UniformSpace γ] (m : EMetricSpace γ)
(H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : 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 := U
uniformity_edist := H.trans (@PseudoEMetricSpace.uniformity_edist γ _)
