iterate_add_eq_iterate — Mathlib

English

If f is injective and f^{[m]}(a) = f^{[n]}(a), then f^{[m+n]}(a) = f^{[n]}(a) implies f^{[m]}(a) = a.

Русский

Если f инъективна и f^{[m]}(a) = f^{[n]}(a), то f^{[m+n]}(a) = f^{[n]}(a) эквивалентно f^{[m]}(a) = a.

LaTeX

$$$$\forall f:\alpha\to\alpha,\forall m,n:\mathbb{N},\ hf:\text{Injective}(f)\Rightarrow \bigl(f^{[m+n]}(a)=f^{[n]}(a) \iff f^{[m]}(a)=a\bigr). $$$$

Lean4

theorem iterate_add_eq_iterate (hf : Injective f) : f^[m + n] a = f^[n] a ↔ f^[m] a = a :=
  Iff.trans (by rw [← iterate_add_apply, Nat.add_comm]) (hf.iterate n).eq_iff

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