not_isPeriodicPt_of_pos_of_lt_minimalPeriod

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)

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