exists_iterate_apply_eq_of_mem_periodicPts

Mathlib.Dynamics.PeriodicPts.Defs

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

← MathLib Explorer

English

If x is periodic under f, there exists n with f^n x = x.

Русский

Если x периодична по f, существует n, такое что f^n x = x.

LaTeX

$$$\\exists n:\\mathbb{N},\\ f^{n}(x) = x$$$

Lean4

@[simp]
theorem exists_iterate_apply_eq_of_mem_periodicPts (hx : x ∈ periodicPts f) : ∃ n, f^[n] x = x := by
  simpa only [← mem_periodicOrbit_iff hx] using iterate_mem_periodicOrbit hx 0

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

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

Разделы

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

Аффилиация

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