self_iterate

Mathlib.Logic.Function.Iterate

URI: https://scilib.ai/kg/mathlib#Function.Commute.self_iterate

English

For any f: α → α and any n ∈ ℕ, f commutes with its n-th iterate: f ∘ f^{[n]} = f^{[n]} ∘ f.

Русский

Для любой функции f: α → α и любого n ∈ ℕ, f commute с своей n-й итерацией: f ∘ f^{[n]} = f^{[n]} ∘ f.

LaTeX

$$$$\forall f:\alpha\to\alpha,\forall n\in\mathbb{N},\ f\circ f^{[n]} = f^{[n]}\circ f. $$$$

Lean4

theorem self_iterate (n : ℕ) : Commute f f^[n] :=
  (refl f).iterate_right n

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

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

Разделы

Аффилиация

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