birkhoffAverage_one' — Mathlib

English

A simp variant: birkhoffAverage_one' asserts birkhoffAverage_R f g 1 = g for all f,g,x; it follows from the previous result.

Русский

Дополнительная упрощенная формулировка: birkhoffAverage_one' утверждает то же равенство для n = 1.

LaTeX

$$$\mathrm{birkhoffAverage}(R,f,g,1) = g$$$

Lean4

@[simp]
theorem birkhoffAverage_one' (f : α → α) (g : α → M) : birkhoffAverage R f g 1 = g :=
  funext <| birkhoffAverage_one R f g

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