eq_zero_of_lt_minimalPeriod — Mathlib

English

If x is a periodic point with period n under f, then the minimal period of x divides n.

Русский

Если x является периодической точкой с периодом n относительно f, то минимальный период x делится на n.

LaTeX

$$$\\operatorname{IsPeriodicPt}(f,n,x) \\Rightarrow \\operatorname{minimalPeriod}(f,x) \\mid n$$$

Lean4

theorem eq_zero_of_lt_minimalPeriod (hx : IsPeriodicPt f n x) (hn : n < minimalPeriod f x) : n = 0 :=
  Eq.symm <| (eq_or_lt_of_le <| n.zero_le).resolve_right fun hn0 => not_lt.2 (hx.minimalPeriod_le hn0) hn

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