norm_smul_le — Mathlib

English

Let α and β be normed additive groups with a bounded scalar action of α on β. Then for all r ∈ α and x ∈ β, ‖r • x‖ ≤ ‖r‖ · ‖x‖.

Русский

Пусть α и β — нормированные аддитивные группы, и есть ограниченное действие скаляра: r • x. Тогда для всех r ∈ α и x ∈ β выполняется ‖r • x‖ ≤ ‖r‖ · ‖x‖.

LaTeX

$$$\\|r \\cdot x\\| \\le \\|r\\| \\cdot \\|x\\|$$$

Lean4

@[bound]
theorem norm_smul_le (r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖ := by simpa [smul_zero] using dist_smul_pair r 0 x

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