real_inner_add_sub_eq_zero_iff — Mathlib

English

The sum and difference x+y and x−y are orthogonal iff ‖x‖ = ‖y‖.

Русский

Сумма и разность x+y и x−y ортогональны тогда и только тогда, когда ‖x‖ = ‖y‖.

LaTeX

$$$\langle x+y, x-y\rangle_\mathbb{R} = 0 \iff \|x\| = \|y\|$$$

Lean4

/-- The sum and difference of two vectors are orthogonal if and only
if they have the same norm. -/
theorem real_inner_add_sub_eq_zero_iff (x y : F) : ⟪x + y, x - y⟫_ℝ = 0 ↔ ‖x‖ = ‖y‖ :=
  by
  conv_rhs => rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]
  simp only [← @inner_self_eq_norm_mul_norm ℝ, inner_add_left, inner_sub_right, real_inner_comm y x, sub_eq_zero,
    re_to_real]
  grind

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