birkhoffSum_one'

Mathlib.Dynamics.BirkhoffSum.Basic

URI: https://scilib.ai/kg/mathlib#birkhoffSum_one'

English

A simp lemma asserting birkhoffSum f g 1 = g, as a direct corollary of the previous.

Русский

Упрощенная лемма: birkhoffSum f g 1 = g.

LaTeX

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

Lean4

@[simp]
theorem birkhoffSum_one' (f : α → α) (g : α → M) : birkhoffSum f g 1 = g :=
  funext <| birkhoffSum_one f g

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru