English
From a SeminormedSpace.Core on E one obtains a SeminormedAddCommGroup E; the induced distance coincides with the core-induced norm distance.
Русский
Из ядра SeminormedSpace на E получают SeminormedAddCommGroup E; полученное расстояние совпадает с расстоянием, заданным ядром/нормой.
LaTeX
$$$$d(x,y)=\|x-y\|.$$$$
Lean4
/-- Produces a `SeminormedAddCommGroup E` instance from a `SeminormedSpace.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 or topology.
See note [reducible non-instances]. -/
abbrev ofCore {𝕜 : Type*} {E : Type*} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E]
(core : SeminormedSpace.Core 𝕜 E) : SeminormedAddCommGroup E :=
{ PseudoMetricSpace.ofSeminormedSpaceCore core with }
