norm_sub_eq_norm_add — Mathlib

English

If ⟪v,w⟫ = 0, then ||w−v|| = ||w+v||.

Русский

Если ⟪v,w⟫ = 0, то ||w−v|| = ||w+v||.

LaTeX

$$$\|w-v\| = \|w+v\|$$$

Lean4

/-- Given two orthogonal vectors, their sum and difference have equal norms. -/
theorem norm_sub_eq_norm_add {v w : E} (h : ⟪v, w⟫ = 0) : ‖w - v‖ = ‖w + v‖ :=
  by
  rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]
  simp only [h, ← @inner_self_eq_norm_mul_norm 𝕜, sub_neg_eq_add, sub_zero, map_sub, zero_re, zero_sub, add_zero,
    map_add, inner_add_right, inner_sub_left, inner_sub_right, inner_re_symm, zero_add]

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