coe_iterate_restrict — Mathlib

English

Iterating the restricted map corresponds to iterating the original map on the underlying element.

Русский

Итерация ограниченного отображения эквивалентна итерации исходного отображения на базовом элементе.

LaTeX

$$$\\text{coe}_\\text{iterate} (h) (x) (k) : h.restrict^[k] x = f^[k] x$$$

Lean4

theorem coe_iterate_restrict {f : α → α} (h : MapsTo f s s) (x : s) (k : ℕ) : h.restrict^[k] x = f^[k] x := by
  induction k with
  | zero => simp
  | succ k ih => simp only [iterate_succ', comp_apply, val_restrict_apply, ih]

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