term_sub_apply — Mathlib

English

For any f,g and s,n, the subtraction identity holds on the term: term(f−g) s n = term f s n − term g s n.

Русский

Для любых f,g и s,n выполняется тождество на члене: term(f−g) s n = term f s n − term g s n.

LaTeX

$$$$ \operatorname{term}(f-g)\; s\; n = \operatorname{term} f\; s\; n - \operatorname{term} g\; s\; n. $$$$

Lean4

theorem term_sub_apply (f g : ℕ → ℂ) (s : ℂ) (n : ℕ) : term (f - g) s n = term f s n - term g s n := by
  rw [term_sub, Pi.sub_apply]

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