English
From a NormedSpace.Core on E one obtains a NormedSpace 𝕜 E; the norm is defined by restricting to core-bound structure.
Русский
Из NormedSpace.Core на E получают NormedSpace 𝕜 E; норма задаётся через ядро/структуру.
LaTeX
$$$$\|x\|_{E}=\|x\|_{core}.$$$$
Lean4
/-- Produces a `NormedSpace 𝕜 E` instance from a `NormedSpace.Core`. This is meant to be used
on types where the `NormedAddCommGroup E` instance has also been defined using `core`.
See note [reducible non-instances]. -/
abbrev ofCore {𝕜 : Type*} {E : Type*} [NormedField 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E]
(core : NormedSpace.Core 𝕜 E) : NormedSpace 𝕜 E where norm_smul_le r x := by rw [core.norm_smul r x]
