real_inner_sub_sub_self — Mathlib

English

For x,y ∈ F (real), ⟪x - y, x - y⟫_ℝ = ⟪x,x⟫_ℝ - 2⟪x,y⟫_ℝ + ⟪y,y⟫_ℝ.

Русский

Для x,y ∈ F (вещественное), ⟪x - y, x - y⟫_ℝ = ⟪x,x⟫_ℝ - 2⟪x,y⟫_ℝ + ⟪y,y⟫_ℝ.

LaTeX

$$$\langle x - y, x - y \rangle_\mathbb{R} = \langle x,x \rangle_\mathbb{R} - 2 \langle x,y \rangle_\mathbb{R} + \langle y,y \rangle_\mathbb{R}$$$

Lean4

/-- Expand `⟪x - y, x - y⟫_ℝ` -/
theorem real_inner_sub_sub_self (x y : F) : ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ :=
  by
  have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl
  simp only [inner_sub_sub_self, this, add_left_inj]
  ring

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