iterate_injOn_Iio_minimalPeriod — Mathlib

English

The map t ↦ f^t(x) is injective on the interval 0 ≤ t < minimalPeriod f x.

Русский

Функция t ↦ f^t(x) инъективна на интервале 0 ≤ t < минимального периода f x.

LaTeX

$$$$ \\text{The function } t \\mapsto f^{t}(x) \\text{ is injective on } \\bigl(0, \\operatorname{minimalPeriod}(f,x)\\bigr). $$$$

Lean4

theorem iterate_injOn_Iio_minimalPeriod : (Iio <| minimalPeriod f x).InjOn (f^[·] x) := fun _m hm _n hn hmn ↦
  (le_of_lt_minimalPeriod_of_iterate_eq hm hmn).antisymm (le_of_lt_minimalPeriod_of_iterate_eq hn hmn.symm)

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