mathlib documentation

lean_problem_sheets / 2019.solutions.sheet3

source
theorem question5 (X Y Z : Type) (f : X → Z) (g : Y → Z) (hf : function.injective f) (hg : function.injective g) :
(∃ (h : X → Y), function.bijective h ∧ f = g ∘ h) ↔ set.range f = set.range g