English
The SeminormedAddCommGroup E has a topology compatible with the core-induced seminorm, provided the topologies agree.
Русский
SeminormedAddCommGroup E совместима с ядром, если топологии совпадают.
LaTeX
$$$$T = (\text{PseudoEMetricSpace.ofSeminormedSpaceCore(core)}).toUniformSpace.toTopologicalSpace.$$$$
Lean4
/-- Produces a `NormedAddCommGroup E` instance from a `NormedSpace.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 [T : TopologicalSpace E] (core : NormedSpace.Core 𝕜 E)
(H : T = (PseudoEMetricSpace.ofSeminormedSpaceCore core.toCore).toUniformSpace.toTopologicalSpace) :
NormedAddCommGroup E :=
{ SeminormedAddCommGroup.ofCoreReplaceTopology core.toCore H with
eq_of_dist_eq_zero := by
intro x y h
rw [← sub_eq_zero, ← core.norm_eq_zero_iff]
exact h }
