is_periodic_id

Mathlib.Dynamics.PeriodicPts.Defs

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

← MathLib Explorer

English

For the identity map, every point is periodic with any period.

Русский

Для тождественной карты cada точка периодична для любого периода.

LaTeX

$$$ \text{IsPeriodicPt}(\operatorname{id}, n, x). $$$

Lean4

/-- For the identity map, all points are periodic. -/
theorem is_periodic_id (n : ℕ) (x : α) : IsPeriodicPt id n x :=
  (isFixedPt_id x).isPeriodicPt n

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

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

Разделы

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

Аффилиация

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