preimage_rangeSplitting — Mathlib

English

If f is injective, then the preimage of rangeSplitting f equals the image of rangeFactorization f.

Русский

Если f инъективна, то предобраз rangeSplitting f равен образу rangeFactorization f.

LaTeX

$$$$ \\operatorname{preimage}(\\operatorname{rangeSplitting} f) = \\operatorname{image}(\\operatorname{rangeFactorization} f) $$$$

Lean4

theorem preimage_rangeSplitting {f : α → β} (hf : Injective f) :
    preimage (rangeSplitting f) = image (rangeFactorization f) :=
  (image_eq_preimage_of_inverse (rightInverse_rangeSplitting hf) (leftInverse_rangeSplitting f)).symm

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