wInner_zero_left — Mathlib

English

The weighted inner product is additive in the first argument: ⟪f1+f2, g⟫ = ⟪f1, g⟫ + ⟪f2, g⟫.

Русский

Весовое скалярное произведение аддитивно по первому аргументу: ⟪f1+f2, g⟫ = ⟪f1, g⟫ + ⟪f2, g⟫.

LaTeX

$$$ \\langle f_1 + f_2, g \\rangle_{𝕜,[w]} = \\langle f_1, g \\rangle_{𝕜,[w]} + \\langle f_2, g \\rangle_{𝕜,[w]} $$$

Lean4

@[simp]
theorem wInner_zero_left (w : ι → ℝ) (g : ∀ i, E i) : ⟪0, g⟫_[𝕜, w] = 0 := by simp [wInner]

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