iterate_invariant — Mathlib

English

If f is injective, then every iterate f^{[n]} is injective.

Русский

Если f инъективна, то каждая итерация f^{[n]} инъективна.

LaTeX

$$$$\text{If } \mathrm{Injective}(f), \; \forall n, \mathrm{Injective}(f^{[n]}).$$$$

Lean4

/-- If a function `g` is invariant under composition with a function `f` (i.e., `g ∘ f = g`), then
`g` is invariant under composition with any iterate of `f`. -/
theorem iterate_invariant {g : α → β} (h : g ∘ f = g) (n : ℕ) : g ∘ f^[n] = g :=
  match n with
  | 0 => by rw [iterate_zero, comp_id]
  | m + 1 => by rwa [iterate_succ, ← comp_assoc, iterate_invariant h m]

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