rightInverse_rangeSplitting — Mathlib

English

If f is injective, then rangeFactorization f and rangeSplitting f form a right inverse pair: rangeFactorization f followed by rangeSplitting f returns the identity on range.

Русский

Если f инъективна, то rangeFactorization f и rangeSplitting f образуют правый обратный пары: применение rangeFactorization f затем rangeSplitting f возвращает тождество на диапазоне.

LaTeX

$$$$ \\text{RightInverse}(\\operatorname{rangeFactorization} f, \\operatorname{rangeSplitting} f) $$$$

Lean4

theorem rightInverse_rangeSplitting {f : α → β} (h : Injective f) :
    RightInverse (rangeFactorization f) (rangeSplitting f) :=
  (leftInverse_rangeSplitting f).rightInverse_of_injective fun _ _ hxy => h <| Subtype.ext_iff.1 hxy

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