le_of_lt_minimalPeriod_of_iterate_eq

English

If m < minimalPeriod f x and f^[m] x = f^[n] x, then m ≤ n.

Русский

Если m < минимального периода f x и f^m(x) = f^n(x), то m ≤ n.

LaTeX

$$$$ m < \\operatorname{minimalPeriod}(f,x) \\land f^{[m]}(x) = f^{[n]}(x) \\Rightarrow m \\le n. $$$$

Lean4

theorem le_of_lt_minimalPeriod_of_iterate_eq {m n : ℕ} (hm : m < minimalPeriod f x) (hmn : f^[m] x = f^[n] x) : m ≤ n :=
  by
  by_contra! hmn'
  rw [← Nat.add_sub_of_le hmn'.le, add_comm, iterate_add_apply] at hmn
  exact
    ((IsPeriodicPt.minimalPeriod_le (tsub_pos_of_lt hmn')
              (isPeriodicPt_of_mem_periodicPts_of_isPeriodicPt_iterate
                (minimalPeriod_pos_iff_mem_periodicPts.1 ((zero_le m).trans_lt hm)) hmn)).trans
          (Nat.sub_le m n)).not_gt
      hm

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