inverse_left — 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` and `f'` is both a left and a right inverse of `f`,
then `f'` semiconjugates `gb` to `ga`. -/
theorem inverse_left {f' : β → α} (h : Semiconj f ga gb) (hf₁ : LeftInverse f' f) (hf₂ : RightInverse f' f) :
    Semiconj f' gb ga := fun x ↦ by rw [← hf₁.injective.eq_iff, h, hf₂, hf₂]

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