iterate_cancel — Mathlib

English

If f is injective and f^{[m]}(a) = f^{[n]}(a), then f^{[m-n]}(a) = a, where subtraction is the natural subtraction with the usual interpretation when m≥n.

Русский

Если f инъективна и f^{[m]}(a) = f^{[n]}(a), тогда f^{[m-n]}(a) = a (с учётом обычного определения m-n).

LaTeX

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

Lean4

theorem iterate_cancel (hf : Injective f) (ha : f^[m] a = f^[n] a) : f^[m - n] a = a :=
  by
  obtain h | h := Nat.le_total m n
  { simp [Nat.sub_eq_zero_of_le h]
  }
  { exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h])
  }

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