English
The finite-subspace e.finiteSubspace inherits a NormedSpace 𝕜-structure from the ambient space. In particular, the norm satisfies the standard inequality ‖c x‖ ≤ ‖c‖ ‖x‖ for all scalars c in 𝕜 and x in e.finiteSubspace.
Русский
Конечномерное подпространство e.finiteSubspace наследует структуру NormedSpace над полем 𝕜 из окружающего пространства. В частности, для всех скаляров c∈𝕜 и векторов x∈e.finiteSubspace выполняется неравенство ‖c x‖ ≤ ‖c‖ ‖x‖.
LaTeX
$$$\\|c x\\| \\le \\|c\\| \\cdot \\|x\\| \\quad (c \\in 𝕜, x \\in e.finiteSubspace)$$$
Lean4
/-- Normed space instance on `e.finiteSubspace`. -/
instance normedSpace : NormedSpace 𝕜 e.finiteSubspace where
norm_smul_le c x := le_of_eq <| by simp [finite_norm_eq, ENNReal.toReal_mul]
