mapsTo_fixedPoints — Mathlib

English

The set of fixed points of f is contained in the range of f.

Русский

Множество фиксированных точек f вложено в образ функции f.

LaTeX

$$$fixedPoints f \subseteq Set.range f$$$

Lean4

/-- If `g` semiconjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
of `fb`. -/
theorem mapsTo_fixedPoints {g : α → β} (h : Semiconj g fa fb) : Set.MapsTo g (fixedPoints fa) (fixedPoints fb) :=
  fun _ hx => hx.map h

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