image_iterate — Mathlib

English

If s is fixed by Set.image f, then it is fixed by all iterates Set.image f^[n].

Русский

Если множество s фиксировано образом Set.image f, то оно фиксировано и образами Set.image f^[n] для всех n.

LaTeX

$$$IsFixedPt (Set.image f) s \rightarrow \forall n:\mathbb{N}, IsFixedPt (Set.image (f^{n})) s$$$

Lean4

theorem image_iterate {s : Set α} (h : IsFixedPt (Set.image f) s) (n : ℕ) : IsFixedPt (Set.image f^[n]) s :=
  Set.image_iterate_eq ▸ h.iterate n

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