inner_sub_sub_self — Mathlib

English

For x,y ∈ E, ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫.

Русский

Для любых x,y ∈ E имеем ⟪x - y, x - y⟫ = ⟪x,x⟫ - ⟪x,y⟫ - ⟪y,x⟫ + ⟪y,y⟫.

LaTeX

$$$\langle x - y, x - y \rangle = \langle x, x \rangle - \langle x, y \rangle - \langle y, x \rangle + \langle y, y \rangle$$$

Lean4

theorem inner_sub_sub_self (x y : E) : ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫ := by
  simp only [inner_sub_left, inner_sub_right]; ring

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