map — Mathlib

English

If g semiconjugates fa to fb, then it maps fixed points of fa to fixed points of fb.

Русский

Если g полуподражает fa к fb, то фиксированные точки fa отображаются в фиксированные точки fb.

LaTeX

$$$\text{IsFixedPt fa x} \rightarrow \text{Semiconj } g\ fa\ fb \rightarrow \text{IsFixedPt fb (g x)}$$$

Lean4

/-- If `g` (semi)conjugates `fa` to `fb`, then it sends fixed points of `fa` to fixed points
of `fb`. -/
protected theorem map {x : α} (hx : IsFixedPt fa x) {g : α → β} (h : Semiconj g fa fb) : IsFixedPt fb (g x) :=
  calc
    fb (g x) = g (fa x) := (h.eq x).symm
    _ = g x := congr_arg g hx

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