iterate — Mathlib

English

If g is a right inverse of f, then for every n ∈ ℕ, g^{[n]} is a right inverse of f^{[n]}.

Русский

Если g — правый обратный к f, то для каждого n ∈ ℕ g^{[n]} является правым обратным к f^{[n]}.

LaTeX

$$$$\forall f,g:\alpha\to\alpha,\ g\text{ is right inverse of } f \Rightarrow \forall n:\mathbb{N},\ g^{[n]} \text{ is right inverse of } f^{[n]}. $$$$

Lean4

theorem iterate {g : α → α} (hg : RightInverse g f) (n : ℕ) : RightInverse g^[n] f^[n] :=
  LeftInverse.iterate hg n

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