English
If the topology on E matches the uniformity-induced topology from the core, the replacement preserves the same seminormed structure.
Русский
Если топология на E совпадает с топологией, индуцированной униформностью ядра, замена сохраняет ту же полинормированную структуру.
LaTeX
$$$$\text{topology equality} : \; T = (\text{PseudoEMetricSpace.ofSeminormedSpaceCore(core)}).toUniformSpace.toTopologicalSpace.$$$$
Lean4
/-- Produces a `SeminormedAddCommGroup E` instance from a `SeminormedSpace.Core` on a type
that already has an existing topology. This requires a proof that the uniformity
induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances]. -/
abbrev ofCoreReplaceTopology {𝕜 : Type*} {E : Type*} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E]
[T : TopologicalSpace E] (core : SeminormedSpace.Core 𝕜 E)
(H : T = (PseudoEMetricSpace.ofSeminormedSpaceCore core).toUniformSpace.toTopologicalSpace) :
SeminormedAddCommGroup E :=
{ PseudoMetricSpace.ofSeminormedSpaceCoreReplaceTopology core H with }
