mem_periodicPts — Mathlib

English

If α is finite and f is injective, then every x ∈ α is a periodic point of f, i.e., x ∈ periodicPts f for all x.

Русский

Если множество α конечно и отображение f инъективно, то каждый элемент x ∈ α является периодической точкой, то есть x ∈ periodicPts f для любого x.

LaTeX

$$$\forall x, x \in \mathrm{periodicPts}(f)$$$

Lean4

theorem mem_periodicPts [Finite α] (h : Injective f) (x : α) : x ∈ periodicPts f :=
  by
  obtain ⟨m, n, heq, hne⟩ : ∃ m n, f^[m] x = f^[n] x ∧ m ≠ n := by
    simpa [Injective] using not_injective_infinite_finite (f^[·] x)
  rcases lt_or_gt_of_ne hne with hlt | hlt
  · exact mk_mem_periodicPts (by cutsat) (iterate_cancel h heq.symm)
  · exact mk_mem_periodicPts (by cutsat) (iterate_cancel h heq)

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