inverses_right — Mathlib

English

If f semiconjugates ga to gb, ga' is a right inverse of ga, and gb' is a left inverse of gb, then f semiconjugates ga' to gb'.

Русский

Если f полуприводит ga к gb, ga' является правой обратной к ga, а gb' — левой обратной к gb, то f полуприводит ga' к gb'.

LaTeX

$$$ f(ga'(x)) = gb'(f(x)) \quad \text{for all } x $$$

Lean4

/-- If `f : α → β` semiconjugates `ga : α → α` to `gb : β → β`,
`ga'` is a right inverse of `ga`, and `gb'` is a left inverse of `gb`,
then `f` semiconjugates `ga'` to `gb'` as well. -/
theorem inverses_right (h : Semiconj f ga gb) (ha : RightInverse ga' ga) (hb : LeftInverse gb' gb) :
    Semiconj f ga' gb' := fun x ↦ by rw [← hb (f (ga' x)), ← h.eq, ha x]

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