norm_sub_sq_eq_norm_sq_add_norm_sq_real

English

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

Русский

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

LaTeX

$$$\|x-y\|^2 = \|x\|^2 + \|y\|^2 \quad\text{when } \operatorname{Re}\langle x,y\rangle = 0$$$

Lean4

/-- Pythagorean theorem, subtracting vectors, vector inner product
form. -/
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_real {x y : F} (h : ⟪x, y⟫_ℝ = 0) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ :=
  (norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero x y).2 h

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