English
Under uniformity and bornology replacement, the resulting NormedAddCommGroup has a norm compatible with core.
Русский
При замене униформности и борологии нормированная аддитивная коммогруппа сохраняет совместную норму.
LaTeX
$$$$\text{norm}_{new}(x) = \text{norm}_{old}(x) $$$$
Lean4
/-- Produces a `NormedAddCommGroup E` instance from a `NormedSpace.Core`. Note that if this is
used to define an instance on a type, it also provides a new distance measure from the norm.
it must therefore not be used on a type with a preexisting distance measure.
See note [reducible non-instances]. -/
abbrev ofCore (core : NormedSpace.Core 𝕜 E) : NormedAddCommGroup E :=
{ SeminormedAddCommGroup.ofCore core.toCore with
eq_of_dist_eq_zero := by
intro x y h
rw [← sub_eq_zero, ← core.norm_eq_zero_iff]
exact h }
