periodicPts_subset_range — Mathlib

English

Every periodic point of f lies in the image of f, i.e., periodic points are contained in the range of f.

Русский

Каждая периодическая точка f лежит в образе f, то есть периодические точки ⊆ образ f.

LaTeX

$$$$ \\operatorname{periodicPts}(f) \\subseteq \\operatorname{range}(f). $$$$

Lean4

theorem periodicPts_subset_range : periodicPts f ⊆ range f :=
  by
  intro x h
  rw [mem_periodicPts] at h
  rcases h with ⟨n, _, h⟩
  use f^[n - 1] x
  nth_rw 1 [← iterate_one f]
  rw [← iterate_add_apply, Nat.add_sub_cancel' (by cutsat)]
  exact h

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