English
From a SeminormedSpace.Core on a type E with a preexisting topology, one obtains a PseudoEMetricSpace structure on E by the same norm-driven distance, compatible with the topology.
Русский
Из ядра SeminormedSpace на E с существующей топологией получается структура PseudoEMetricSpace, заданная той же нормой расстояния.
LaTeX
$$$$\text{Let } core: \text{SeminormedSpace.Core} \; 𝕜\; E. \ d(x,y)=\|x-y\|.$$$$
Lean4
/-- Produces a `PseudoEMetricSpace E` instance from a `SeminormedSpace.Core`. Note that
if this is used to define an instance on a type, it also provides a new uniformity and
topology on the type. See note [reducible non-instances]. -/
abbrev ofSeminormedSpaceCore {𝕜 E : Type*} [NormedField 𝕜] [AddCommGroup E] [Norm E] [Module 𝕜 E]
(core : SeminormedSpace.Core 𝕜 E) : PseudoEMetricSpace E :=
(PseudoMetricSpace.ofSeminormedSpaceCore core).toPseudoEMetricSpace
