iterate_eq_of_map_eq — Mathlib

English

Let f,g: α → α satisfy f ∘ g = g ∘ f. If f x = g x for some x, then for every n ∈ ℕ, the n-th iterate of f at x equals the n-th iterate of g at x.

Русский

Пусть f, g: α → α коммютируют (f ∘ g = g ∘ f). Если для некоторого x верно f x = g x, то для любого n ∈ ℕ выполняется f^[n] x = g^[n] x.

LaTeX

$$$$\forall f,g: \alpha \to \alpha,\ (f\circ g = g\circ f) \\Rightarrow \forall x:\alpha,\ f\ x = g\ x \Rightarrow \forall n:\mathbb{N},\ f^{[n]}(x) = g^{[n]}(x). $$$$

Lean4

theorem iterate_eq_of_map_eq (h : Commute f g) (n : ℕ) {x} (hx : f x = g x) : f^[n] x = g^[n] x :=
  Nat.recOn n rfl fun n ihn ↦ by
    simp only [iterate_succ_apply, hx, (h.iterate_left n).eq, ihn, ((refl g).iterate_right n).eq]

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