inner_eq_tsum — Mathlib

English

For f,g in lp G 2, the lp inner product equals the sum of the coordinate inner products: ⟪f,g⟫ = ∑' i ⟪f(i), g(i)⟫.

Русский

Для f,g в lp G 2 скалярное произведение равно сумме поперечных координат: ⟪f,g⟫ = ∑' i ⟪f(i), g(i)⟫.

LaTeX

$$$ \\langle f,g \\rangle = \\sum\\_' i \\langle f(i), g(i) \\rangle $$$

Lean4

theorem inner_eq_tsum (f g : lp G 2) : ⟪f, g⟫ = ∑' i, ⟪f i, g i⟫ :=
  rfl

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