norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero

English

If ⟪x,y⟫ = 0, then ||x−y||^2 = ||x||^2 + ||y||^2.

Русский

Если ⟪x,y⟫ = 0, то ||x−y||^2 = ||x||^2 + ||y||^2.

LaTeX

$$$\|x-y\|^2 = \|x\|^2 + \|y\|^2 \quad\text{when } ⟪x,y⟫ = 0$$$

Lean4

/-- Pythagorean theorem, subtracting vectors, if-and-only-if vector
inner product form. -/
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero (x y : F) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0 :=
  by
  rw [@norm_sub_mul_self ℝ, add_right_cancel_iff, sub_eq_add_neg, add_eq_left, neg_eq_zero, mul_eq_zero]
  simp

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