iterate_fixed

Mathlib.Logic.Function.Iterate

URI: https://scilib.ai/kg/mathlib#Function.iterate_fixed

English

If f maps x to itself, then all its iterates fix x: f^{[n]}(x) = x for all n.

Русский

Если f(x) = x, то все продолжения итерации держат x фиксированным: f^{[n]}(x) = x.

LaTeX

$$$$\text{If } f(x) = x, \text{ then } f^{[n]}(x) = x \text{ for all } n.$$$$

Lean4

theorem iterate_fixed {x} (h : f x = x) (n : ℕ) : f^[n] x = x :=
  Nat.recOn n rfl fun n ihn ↦ by rw [iterate_succ_apply, h, ihn]

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

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

Разделы

Аффилиация

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