norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two

English

The squared norm of x+y equals 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, if-and-only-if vector angle form. -/
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two (x y : V) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2 :=
  by
  rw [norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
  exact inner_eq_zero_iff_angle_eq_pi_div_two x y

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