English
For all x,y ∈ E, ‖x+y‖ ≤ ‖x‖ + ‖y‖.
Русский
Для любых x,y ∈ E: ‖x+y‖ ≤ ‖x‖ + ‖y‖.
LaTeX
$$$\\\\|x + y\\\\| \\\\leq \\\\|x\\\\| + \\\\|y\\\\|$$$
Lean4
protected theorem norm_triangle (x y : E) : ‖x + y‖ ≤ ‖x‖ + ‖y‖ :=
by
have h : ‖x + y‖ ^ 2 ≤ (‖x‖ + ‖y‖) ^ 2 := by
calc
_ ≤ ‖⟪x, x⟫ + ⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ :=
by
simp only [norm_eq_sqrt_norm_inner_self (A := A), inner_add_right, inner_add_left, ← add_assoc, norm_nonneg,
Real.sq_sqrt]
exact norm_add₃_le
_ ≤ ‖⟪x, x⟫‖ + ‖⟪y, x⟫‖ + ‖⟪x, y⟫‖ + ‖⟪y, y⟫‖ := by gcongr; exact norm_add_le _ _
_ ≤ ‖⟪x, x⟫‖ + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖⟪y, y⟫‖ := by gcongr <;> exact norm_inner_le E
_ = ‖x‖ ^ 2 + ‖y‖ * ‖x‖ + ‖x‖ * ‖y‖ + ‖y‖ ^ 2 := by simp [norm_eq_sqrt_norm_inner_self (A := A)]
_ = (‖x‖ + ‖y‖) ^ 2 := by simp only [add_pow_two, add_left_inj]; ring
refine (pow_le_pow_iff_left₀ (CStarModule.norm_nonneg A) ?_ (by simp)).mp h
exact add_nonneg (CStarModule.norm_nonneg A) (CStarModule.norm_nonneg A)
