norm_sub_eq_sqrt_iff_real_inner_eq_zero

English

The equality ‖x−y‖ = √(‖x‖^2 + ‖y‖^2) holds iff ⟪x,y⟫ = 0 (in the real case).

Русский

Равенство ‖x−y‖ = √(‖x‖^2 + ‖y‖^2) верно тогда и только тогда, когда ⟪x,y⟫ = 0 (в вещественном случае).

LaTeX

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

Lean4

/-- Pythagorean theorem, subtracting vectors, if-and-if vector inner product form using square
roots. -/
theorem norm_sub_eq_sqrt_iff_real_inner_eq_zero {x y : F} : ‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0 := by
  rw [← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero, eq_comm, sqrt_eq_iff_mul_self_eq, eq_comm] <;>
    positivity

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