minimalPeriod_eq_zero_iff_notMem_periodicPts

Mathlib.Dynamics.PeriodicPts.Defs

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

← MathLib Explorer

English

0 < minimalPeriod f x iff x ∈ periodicPts f.

Русский

0 < минимальный период f x тогда и только тогда, когда x ∈ periodicPts f.

LaTeX

$$$$ 0 < \\operatorname{minimalPeriod}(f,x) \\iff x \\in \\operatorname{periodicPts}(f). $$$$

Lean4

theorem minimalPeriod_eq_zero_iff_notMem_periodicPts : minimalPeriod f x = 0 ↔ x ∉ periodicPts f := by
  rw [← minimalPeriod_pos_iff_mem_periodicPts, not_lt, nonpos_iff_eq_zero]

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

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

Разделы

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

Аффилиация

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