English
If we replace the uniform structure of a pseudometric space by the same uniform structure, we obtain the same space.
Русский
Если заменить равномерную структуру псевдометрического пространства на ту же самую структуру, получаем то же пространство.
LaTeX
$$$m\\replaceUniformity\\; H = m$ whenever $H$ expresses the equality of the given uniformity with the original one.$$
Lean4
/-- Build a new pseudometric 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 : PseudoMetricSpace α)
(H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : PseudoMetricSpace α :=
{ m with
toUniformSpace := U
uniformity_dist := H.trans PseudoMetricSpace.uniformity_dist }
