term_add — Mathlib

English

The map s ↦ term(f+g) s is the sum of term f s and term g s; i.e., term is linear in the first argument.

Русский

Функция s ↦ term(f+g) s равна сумме term f s и term g s; то есть term линейна по первому аргументу.

LaTeX

$$$$ \operatorname{term}(f+g)(s) = \operatorname{term}(f)(s) + \operatorname{term}(g)(s). $$$$

Lean4

theorem term_add (f g : ℕ → ℂ) (s : ℂ) : term (f + g) s = term f s + term g s := by ext ⟨- | n⟩ <;> simp [add_div]

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