norm_sub_mul_self_real — Mathlib

English

For x,y ∈ E, ‖x − y‖ · ‖x − y‖ = ‖x‖ · ‖x‖ − 2 Re ⟪x, y⟫_ℝ + ‖y‖ · ‖y‖.

Русский

Для x,y в E: ‖x − y‖·‖x − y‖ = ‖x‖·‖x‖ − 2 Re ⟪x,y⟫_ℝ + ‖y‖·‖y‖.

LaTeX

$$$\|x-y\| \cdot \|x-y\| = \|x\| \cdot \|x\| - 2 \Re\langle x, y\rangle_ℝ + \|y\| \cdot \|y\|$$$

Lean4

/-- Expand the square -/
theorem norm_sub_mul_self_real (x y : F) : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖ :=
  by
  have h := @norm_sub_mul_self ℝ _ _ _ _ x y
  simpa using h

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