iterate — Mathlib

English

If g is a left inverse of f (g ∘ f = id), then for every n ∈ ℕ, g^{[n]} is a left inverse of f^{[n]}.

Русский

Если g — левообратная к f (g ∘ f = id), то для каждого n ∈ ℕ g^{[n]} — левообратная к f^{[n]}.

LaTeX

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

Lean4

theorem iterate {g : α → α} (hg : LeftInverse g f) (n : ℕ) : LeftInverse g^[n] f^[n] :=
  Nat.recOn n (fun _ ↦ rfl) fun n ihn ↦ by
    rw [iterate_succ', iterate_succ]
    exact ihn.comp hg

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