norm_sub_mul_self — Mathlib

English

For x, y ∈ E, ‖x − y‖^2 = ‖x‖^2 − 2 Re ⟪x, y⟫ + ‖y‖^2.

Русский

Для x, y в пространстве: ‖x − y‖^2 = ‖x‖^2 − 2 Re ⟪x, y⟫ + ‖y‖^2.

LaTeX

$$$\|x - y\|^2 = \|x\|^2 - 2 \Re\langle x, y\rangle + \|y\|^2$$$

Lean4

/-- Expand the square -/
theorem norm_sub_mul_self (x y : E) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖ :=
  by
  repeat' rw [← sq (M := ℝ)]
  exact norm_sub_sq _ _

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