iterate_add_apply

Mathlib.Logic.Function.Iterate

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

← MathLib Explorer

English

For all m,n and x, f^{[m+n]}(x) = f^{[m]}(f^{[n]}(x)).

Русский

Для всех m,n и x: f^{[m+n]}(x) = f^{[m]}(f^{[n]}(x)).

LaTeX

$$$$f^{[m+n]}(x) = f^{[m]}(f^{[n]}(x))$$$$

Lean4

theorem iterate_add_apply (m n : ℕ) (x : α) : f^[m + n] x = f^[m] (f^[n] x) :=
  by
  rw [iterate_add f m n]
  rfl
    -- can be proved by simp but this is shorter and more natural

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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