linearCombination_option — Mathlib

English

For v: Option α → M and f: Option α →₀ R, linearCombination_R(v) f equals f none • v none plus linearCombination_R(v ∘ Option.some) f.some.

Русский

Для $v: Option α → M$ и $f: Option α →₀ R$ выполняется: линейная комбинация через $v$ на $f$ равна $f none$ умноженному на $v none$ плюс линейная комбинация через $v ∘ ext{Option.some}$ на $f.some$.

LaTeX

$$$\operatorname{linearCombination}_R(v)\, f = f\,\text{none} \cdot v\text{ none} + \operatorname{linearCombination}_R(v\circ\text{Option.some})\, f\text{some}$$$

Lean4

theorem linearCombination_option (v : Option α → M) (f : Option α →₀ R) :
    linearCombination R v f = f none • v none + linearCombination R (v ∘ Option.some) f.some := by
  rw [linearCombination_apply, sum_option_index_smul, linearCombination_apply]; simp

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