norm_smul_of_nonneg

Mathlib.Analysis.Normed.Module.RCLike.Real

URI: https://scilib.ai/kg/mathlib#norm_smul_of_nonneg

English

For a real t ≥ 0 and any vector x, the norm of t•x equals t times the norm of x.

Русский

Для действительного t ≥ 0 и любого вектора x имеет место ||t•x|| = t||x||.

LaTeX

$$$\\|t \\cdot x\\| = t \\|x\\|$$$

Lean4

theorem norm_smul_of_nonneg {t : ℝ} (ht : 0 ≤ t) (x : E) : ‖t • x‖ = t * ‖x‖ := by
  rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg ht]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru