English
Given f and a left inverse f_inv with LeftInverse hf, the Equiv built from left inverses equals the Equiv built from the injective f (up to empty/nonempty case).
Русский
Дано отображение f и семейство левых обратных f_inv с свойством LeftInverse hf; эквивалентность, построенная через левую обратную, эквивалентна эквивалентности, получаемой из инъекции f (с учётом пустоты/непустоты).
LaTeX
$$$\\mathrm{Equiv.ofLeftInverse}(f,f_{inv},hf) = \\mathrm{Equiv.ofInjective}(f)\\text{ (с учётом случая пустого множества)}$$$
Lean4
theorem ofLeftInverse_eq_ofInjective {α β : Type*} (f : α → β) (f_inv : Nonempty α → β → α)
(hf : ∀ h : Nonempty α, LeftInverse (f_inv h) f) :
ofLeftInverse f f_inv hf =
ofInjective f ((isEmpty_or_nonempty α).elim (fun _ _ _ _ => Subsingleton.elim _ _) (fun h => (hf h).injective)) :=
by
ext
simp
