norm_sub_sq_eq_norm_sq_add_norm_sq'

English

The squared norm of x−y equals the sum of squared norms iff angle x y = π/2.

Русский

Квадрат нормы разности равен сумме квадратов норм тогда и только тогда, когда угол x y = π/2.

LaTeX

$$‖x - y‖^2 = ‖x‖^2 + ‖y‖^2 ↔ angle x y = π/2$$

Lean4

/-- Pythagorean theorem, subtracting vectors, vector angle form. -/
theorem norm_sub_sq_eq_norm_sq_add_norm_sq' (x y : V) (h : angle x y = π / 2) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ :=
  (norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two x y).2 h

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