norm_add_eq_norm_sub_iff_angle_eq_pi_div_two

English

For all x,y, ‖x + y‖ = ‖x − y‖ if and only if angle x y = π/2.

Русский

Для любых x,y: ‖x + y‖ = ‖x − y‖ тогда и только тогда, когда угол x y равен π/2.

LaTeX

$$$‖x + y‖ = ‖x - y‖ \\;\\leftrightarrow\\; angle x y = \\pi/2$$$

Lean4

/-- The norm of the sum of two vectors equals the norm of their difference if and only if
the angle between them is π/2. -/
theorem norm_add_eq_norm_sub_iff_angle_eq_pi_div_two (x y : V) : ‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2 :=
  by
  rw [← sq_eq_sq₀ (norm_nonneg (x + y)) (norm_nonneg (x - y)), ← inner_eq_zero_iff_angle_eq_pi_div_two x y,
    norm_add_pow_two_real, norm_sub_pow_two_real]
  constructor <;> intro h <;> linarith

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