birkhoffAverage_neg — Mathlib

English

A reiteration that birkhoffAverage with respect to R equals birkhoffAverage with respect to S; a restatement of 113249/113250 in a taut form.

Русский

Повторение того, что среднее Биркхоффа не зависит от кольца – эквивалентность для разных колец.

LaTeX

$$$\mathrm{birkhoffAverage}(R,f,g,n,x) = \mathrm{birkhoffAverage}(S,f,g,n,x).$$$

Lean4

theorem birkhoffAverage_neg {f : α → α} {g : α → M} : birkhoffAverage R f (-g) = -birkhoffAverage R f g :=
  by
  funext _ x
  simp [birkhoffAverage, birkhoffSum]

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