toNormedSpace — Mathlib

English

A submodule carries a normed space structure from its ambient space via the restricted norm; the norm satisfies the usual bounds.

Русский

Подмодуль несёт структуру нормированного пространства от внешнего пространства с помощью ограниченной нормы; норма удовлетворяет обычным неравенствам.

LaTeX

$$$\\|c\\cdot x\\|_{s} \\leq \\|c\\| \\|x\\|_{s}$ for scalars c and x ∈ s$$

Lean4

instance (priority := 75) toNormedSpace : NormedSpace 𝕜 s where norm_smul_le c x := norm_smul_le c (x : E)

Похожие утверждения