iterate_restrict — Mathlib

English

For h: MapsTo f s s, the n-th iterate of the restricted map equals the restriction of the n-th iterate of f.

Русский

Для h: MapsTo f s s, n-й итерат ограниченного отображения равен ограничению n-й итерации f.

LaTeX

$$$ (MapsTo\\ restrict\\ f\\ s\\ s)^{[n]} = (MapsTo\\ iterate\\ f\\ n)\\ restrict\\ s\\ s $$$

Lean4

theorem iterate_restrict {f : α → α} {s : Set α} (h : MapsTo f s s) (n : ℕ) :
    (h.restrict f s s)^[n] = (h.iterate n).restrict _ _ _ :=
  by
  funext x
  rw [Subtype.ext_iff, MapsTo.val_restrict_apply]
  induction n generalizing x with
  | zero => rfl
  | succ n ihn => simp [Nat.iterate, ihn]

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