preimage_iterate — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem preimage_iterate {s : Set α} (h : IsFixedPt (Set.preimage f) s) (n : ℕ) : IsFixedPt (Set.preimage f^[n]) s :=
  by
  rw [Set.preimage_iterate_eq]
  exact h.iterate n

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