English
The congruence between the new and old uniform structures is maintained under the core-based replacement, ensuring the same metric behavior.
Русский
Сохранение эквивалентности между новой и старой униформностью под заменой ядра сохраняет поведение метрики.
LaTeX
$$$$\text{congruent} :\;\mathcal{U}_{new}=\mathcal{U}_{old}.$$$$
Lean4
/-- Produces a `SeminormedAddCommGroup 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 ofCoreReplaceUniformity {𝕜 : Type*} {E : Type*} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E]
[U : UniformSpace E] (core : SeminormedSpace.Core 𝕜 E)
(H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace (self := PseudoEMetricSpace.ofSeminormedSpaceCore core)]) :
SeminormedAddCommGroup E :=
{ PseudoMetricSpace.ofSeminormedSpaceCoreReplaceUniformity core H with }
