minimalPeriod_eq_zero_of_notMem_periodicPts

Mathlib.Dynamics.PeriodicPts.Defs

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

English

If x is not a periodic point, then minimalPeriod f x = 0.

Русский

Если x не периодична, то minimalPeriod f x = 0.

LaTeX

$$$$ x \\notin \\operatorname{periodicPts}(f) \\Rightarrow \\operatorname{minimalPeriod}(f,x) = 0. $$$$

Lean4

theorem minimalPeriod_eq_zero_of_notMem_periodicPts (hx : x ∉ periodicPts f) : minimalPeriod f x = 0 := by
  simp only [minimalPeriod, dif_neg hx]

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

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

Разделы

Аффилиация

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