minimalPeriod_le — Mathlib

English

minimalPeriod f x = 0 if and only if x ∉ periodicPts f.

Русский

minimalPeriod f x = 0 тогда и только тогда, когда x ∉ periodicPts f.

LaTeX

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

Lean4

theorem minimalPeriod_le (hn : 0 < n) (hx : IsPeriodicPt f n x) : minimalPeriod f x ≤ n := by
  classical
  rw [minimalPeriod, dif_pos (mk_mem_periodicPts hn hx)]
  exact Nat.find_min' (mk_mem_periodicPts hn hx) ⟨hn, hx⟩

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