English
There exists a way to transport a seminorm-based uniform structure through a replacement of the uniformity, yielding a new consistent pseudo-metric structure on the same underlying type whenever the uniformities agree.
Русский
Существует способ перенести структуру по униформности через замену униформности, получая новую последовательную псевдометрическую структуру на том же базовом типе при согласии униформностей.
LaTeX
$$$$\mathcal{U}=\mathcal{U}_{\text{new}},$$$$
Lean4
/-- Produces a `PseudoEMetricSpace E` instance from a `SeminormedSpace.Core` on a type that
already has an existing uniform space structure. This requires a proof that the uniformity induced
by the norm is equal to the preexisting uniformity. See note [reducible non-instances]. -/
abbrev ofSeminormedSpaceCoreReplaceUniformity {𝕜 E : Type*} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E]
[U : UniformSpace E] (core : SeminormedSpace.Core 𝕜 E)
(H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace (self := PseudoEMetricSpace.ofSeminormedSpaceCore core)]) :
PseudoMetricSpace E :=
.replaceUniformity (.ofSeminormedSpaceCore core) H
