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