eq_of_apply_eq_same — Mathlib

English

If x has period m for f, then for any n, x has period n · m.

Русский

Если x имеет период m для f, то для любого n точка x имеет период n · m.

LaTeX

$$$IsPeriodicPt f m x \to IsPeriodicPt f (n * m) x$$$

Lean4

/-- If `f` sends two periodic points `x` and `y` of the same positive period to the same point,
then `x = y`. For a similar statement about points of different periods see `eq_of_apply_eq`. -/
theorem eq_of_apply_eq_same (hx : IsPeriodicPt f n x) (hy : IsPeriodicPt f n y) (hn : 0 < n) (h : f x = f y) : x = y :=
  by rw [← hx.eq, ← hy.eq, ← iterate_pred_comp_of_pos f hn, comp_apply, comp_apply, h]

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