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