English
There is a bijection between the range of Sum.inl : α → α ⊕ β and α, given by projecting away the right component: toFun(⟨inl x, _⟩) = x; inverse maps x ↦ ⟨inl x, mem_range_self _⟩.
Русский
Существует биекция между образом Sum.inl : α → α ⊕ β и α, задаваемая проекцией на левую компоненту: toFun(⟨inl x⟩) = x; обратное отображение x ↦ ⟨inl x, доказательство⟩.
LaTeX
$$$\\operatorname{range}(\\mathrm{Sum.inl}) \\cong α$$$
Lean4
/-- If `f : α → β` has a left-inverse, then `α` is computably equivalent to the range of `f`.
Note that if `α` is empty, no such `f_inv` exists and so this definition can't be used, unlike
the stronger but less convenient `ofLeftInverse`. -/
abbrev ofLeftInverse' {α β : Sort _} (f : α → β) (f_inv : β → α) (hf : LeftInverse f_inv f) : α ≃ range f :=
ofLeftInverse f (fun _ => f_inv) fun _ => hf
