iterate

Mathlib.Dynamics.PeriodicPts.Defs

URI: https://scilib.ai/kg/mathlib#Function.IsPeriodicPt.iterate

← MathLib Explorer

English

If x is periodic with period n, then f^{m mod n}(x) = f^{m}(x) for any m.

Русский

Если x имеет период n, то для любого m выполняется f^{m mod n}(x) = f^{m}(x).

LaTeX

$$$IsPeriodicPt f n x \to \forall m, f^{m \% n}(x) = f^{m}(x)$$$

Lean4

protected theorem iterate (hf : IsPeriodicPt f n x) (m : ℕ) : IsPeriodicPt f^[m] n x :=
  by
  rw [IsPeriodicPt, ← iterate_mul, mul_comm, iterate_mul]
  exact hf.isFixedPt.iterate m

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

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

Разделы

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

Аффилиация

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