English
If fbc semiconjugates gb to gc and fab semiconjugates ga to gb, then fbc ∘ fab semiconjugates ga to gc.
Русский
Если fbc полуприводит gb к gc, а fab полуприводит ga к gb, то fbc ∘ fab полуприводит ga к gc.
LaTeX
$$$ (fbc \circ fab) \circ ga = gc \circ (fbc \circ fab) $$$
Lean4
/-- If `fbc : β → γ` semiconjugates `gb` to `gc` and `fab : α → β` semiconjugates `ga` to `gb`,
then `fbc ∘ fab` semiconjugates `ga` to `gc`.
See also `Function.Semiconj.trans` for a version with reversed arguments.
**Backward compatibility note:** before 2024-01-13,
this lemma used to have the same order of arguments that `Function.Semiconj.trans` has now. -/
theorem comp_left (hbc : Semiconj fbc gb gc) (hab : Semiconj fab ga gb) : Semiconj (fbc ∘ fab) ga gc :=
hab.trans hbc
