English
No positive integer n smaller than the minimal period of x can be a period of x; i.e., if n ≠ 0 and n < minimalPeriod f x, then x is not periodic with period n.
Русский
Никакой положительный n меньше минимального периода x не может являться периодом x; то есть если n ≠ 0 и n < minimalPeriod f x, то x не периодично по f с периодом n.
LaTeX
$$$\\forall f,x,n:\\ n \\neq 0 \\land n < \\operatorname{minimalPeriod}(f,x) \\Rightarrow \\neg \\operatorname{IsPeriodicPt}(f,n,x)$$$
Lean4
theorem not_isPeriodicPt_of_pos_of_lt_minimalPeriod :
∀ {n : ℕ} (_ : n ≠ 0) (_ : n < minimalPeriod f x), ¬IsPeriodicPt f n x
| 0, n0, _ => (n0 rfl).elim
| _ + 1, _, hn => fun hp => Nat.succ_ne_zero _ (hp.eq_zero_of_lt_minimalPeriod hn)