birkhoffSum_sub — Mathlib

English

For all f: α→α and g,g': α→G with G AddCommGroup, birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x for all n and x.

Русский

Для любых f: α→α и наблюдаемых g,g': α→G, где G — AddCommGroup, выполняется birkhoffSum(f, g - g', n, x) = birkhoffSum(f, g, n, x) - birkhoffSum(f, g', n, x).

LaTeX

$$$\\mathrm{birkhoffSum}(f,g-g',n,x)=\\mathrm{birkhoffSum}(f,g,n,x)-\\mathrm{birkhoffSum}(f,g',n,x)$$$

Lean4

theorem birkhoffSum_sub (f : α → α) (g g' : α → G) (n : ℕ) (x : α) :
    birkhoffSum f (g - g') n x = birkhoffSum f g n x - birkhoffSum f g' n x := by simp [birkhoffSum]

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