iterate_succ

Mathlib.Logic.Function.Iterate

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

English

The successor iterate is the previous iterate composed with the function: f^{[n+1]} = f^{[n]} ∘ f.

Русский

Следующая итерация — это композиция предыдущей итерации с функцией: f^{[n+1]} = f^{[n]} ∘ f.

LaTeX

$$$$f^{[n+1]} = f^{[n]} \circ f$$$$

Lean4

@[simp]
theorem iterate_succ (n : ℕ) : f^[n.succ] = f^[n] ∘ f :=
  rfl

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

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

Разделы

Аффилиация

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