English
Let fab: α → β semiconjugate ga to gb, and fbc: β → γ semiconjugate gb to gc. Then their composition fbc ∘ fab semiconjugates ga to gc.
Русский
Пусть fab: α → β полуприводит ga к gb, а fbc: β → γ полуприводит gb к gc. Тогда композиция fbc ∘ fab полуприводит ga к gc.
LaTeX
$$$ (fbc \circ fab) \circ ga = gc \circ (fbc \circ fab) $$$
Lean4
/-- If `fab : α → β` semiconjugates `ga` to `gb` and `fbc : β → γ` semiconjugates `gb` to `gc`,
then `fbc ∘ fab` semiconjugates `ga` to `gc`.
See also `Function.Semiconj.comp_left` for a version with reversed arguments. -/
protected theorem trans (hab : Semiconj fab ga gb) (hbc : Semiconj fbc gb gc) : Semiconj (fbc ∘ fab) ga gc := fun x ↦ by
simp only [comp_apply, hab.eq, hbc.eq]
