English
A construction that replaces the uniformity on a type with a given uniform structure, resulting in a PseudoEMetricSpace whose edist agrees with the original and whose uniformity matches the new one.
Русский
Построение, заменяющее униформность на заданную структуру, получающее псевдоэмитическое пространство, у которого евристика совпадает с исходной и униформность совпадает с новой.
LaTeX
$$$\text{Given } U\text{ a UniformSpace on }\alpha,\ m: PseudoEMetricSpace\alpha,\ H: 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]\ \Rightarrow\ replaceUniformity\, (\alpha)\ U\ m\ H \text{ yields a PseudoEMetricSpace with } edist' = edist_m \text{ and } uniformity' = U.$$$
Lean4
/-- Auxiliary function to replace the uniformity on a pseudoemetric space with
a uniformity which is equal to the original one, but maybe not defeq.
This is useful if one wants to construct a pseudoemetric 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 : PseudoEMetricSpace α)
(H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : PseudoEMetricSpace α
where
edist := @edist _ m.toEDist
edist_self := edist_self
edist_comm := edist_comm
edist_triangle := edist_triangle
toUniformSpace := U
uniformity_edist := H.trans (@PseudoEMetricSpace.uniformity_edist α _)
