eq_of_apply_eq — Mathlib

English

If x and y are periodic with periods m and n (with m,n > 0) and f x = f y, then x = y.

Русский

Если x и y периодичны с периодами m и n (m,n > 0) и f x = f y, тогда x = y.

LaTeX

$$$IsPeriodicPt f m x \to IsPeriodicPt f n y \to 0 < m \to 0 < n \to f x = f y \Rightarrow x = y$$$

Lean4

/-- If `f` sends two periodic points `x` and `y` of positive periods to the same point,
then `x = y`. -/
theorem eq_of_apply_eq (hx : IsPeriodicPt f m x) (hy : IsPeriodicPt f n y) (hm : 0 < m) (hn : 0 < n) (h : f x = f y) :
    x = y :=
  (hx.mul_const n).eq_of_apply_eq_same (hy.const_mul m) (Nat.mul_pos hm hn) h

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