comp_right — Mathlib

English

If f semiconjugates ga to gb and ga' to gb', then it also semiconjugates ga ∘ ga' to gb ∘ gb'.

Русский

Если f полусопряжает ga к gb и ga' к gb', то оно инвариантно по композиции ga ∘ ga' к gb ∘ gb'.

LaTeX

$$$ \forall {\alpha} {\beta} {\gamma} {f} {ga} {ga'} {gb} {gb'} (h : \operatorname{Semiconj} f ga gb) (h' : \operatorname{Semiconj} f ga' gb') : \operatorname{Semiconj} f (ga \circ ga') (gb \circ gb')$$$

Lean4

/-- If `f` semiconjugates `ga` to `gb` and `ga'` to `gb'`,
then it semiconjugates `ga ∘ ga'` to `gb ∘ gb'`. -/
theorem comp_right (h : Semiconj f ga gb) (h' : Semiconj f ga' gb') : Semiconj f (ga ∘ ga') (gb ∘ gb') := fun x ↦ by
  simp only [comp_apply, h.eq, h'.eq]

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