norm_le_mul_norm_add' — Mathlib

English

For all u, v ∈ E, ‖v‖ ≤ ‖u v‖ + ‖u‖.

Русский

Для любых u, v ∈ E выполняется ‖v‖ ≤ ‖u v‖ + ‖u‖.

LaTeX

$$$$ \|v\| \le \|u v\| + \|u\|. $$$$

Lean4

/-- An analogue of `norm_le_mul_norm_add` for the multiplication from the left. -/
@[to_additive /-- An analogue of `norm_le_add_norm_add` for the addition from the left. -/
    ]
theorem norm_le_mul_norm_add' (u v : E) : ‖v‖ ≤ ‖u * v‖ + ‖u‖ :=
  calc
    ‖v‖ = ‖u⁻¹ * (u * v)‖ := by rw [← mul_assoc, inv_mul_cancel, one_mul]
    _ ≤ ‖u⁻¹‖ + ‖u * v‖ := (norm_mul_le' u⁻¹ (u * v))
    _ = ‖u * v‖ + ‖u‖ := by rw [norm_inv', add_comm]

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