norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero

English

If the real inner product is zero, then ||x+y||^2 = ||x||^2 + ||y||^2.

Русский

Если вещественное скалярное произведение равно нулю, то ||x+y||^2 = ||x||^2 + ||y||^2.

LaTeX

$$$\langle x,y\rangle_\mathbb{R} = 0 \Rightarrow \|x+y\|^2 = \|x\|^2 + \|y\|^2$$$

Lean4

/-- Pythagorean theorem, vector inner product form. -/
theorem norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (x y : E) (h : ⟪x, y⟫ = 0) :
    ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ :=
  by
  rw [@norm_add_mul_self 𝕜, add_right_cancel_iff, add_eq_left, mul_eq_zero]
  apply Or.inr
  simp only [h, zero_re]

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