iterate_eq_pow — Mathlib

English

Let f be a permutation of α and n a natural number. The n-th iterate of f equals the function underlying the n-th power of f: f^{[n]} = ⇑(f^n).

Русский

Пусть f — перестановка α и n — натуральное число. n-я итерация f равна функции, лежащей в основе f^n: f^{[n]} = ⇑(f^n).

LaTeX

$$$\\\\forall \\\\alpha, (f : \\\\mathrm{Perm} \\\\alpha), (n : \\\\mathbb{N}), f^{[n]} = \\\\operatorname{toFun}(f^n)$$$

Lean4

@[simp]
theorem iterate_eq_pow (f : Perm α) (n : ℕ) : f^[n] = ⇑(f ^ n) :=
  rfl

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