fixedPoints — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The set of fixed points of a map `f : α → α`. -/
def fixedPoints (f : α → α) : Set α :=
  {x : α | IsFixedPt f x}

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