English
Equivalence between the range of Sum.inl and α; toFun maps ⟨inl x, _⟩ to x; invFun maps x to ⟨inl x, mem_range_self⟩.
Русский
Эквивалентность между множеством образов Sum.inl и α; отображение toFun отправляет ⟨inl x, _⟩ в x; обратное — x в ⟨inl x, mem_range_self⟩.
LaTeX
$$$\\mathrm{rangeInl}(\\alpha,\\beta) : \\mathrm{Set.range}(\\mathrm{Sum.inl}) \\simeq \\alpha$$$
Lean4
/-- Equivalence between the range of `Sum.inl : α → α ⊕ β` and `α`. -/
@[simps symm_apply_coe]
def rangeInl (α β : Type*) : Set.range (Sum.inl : α → α ⊕ β) ≃ α
where
toFun
| ⟨.inl x, _⟩ => x
| ⟨.inr _, h⟩ => False.elim <| by rcases h with ⟨x, h'⟩; cases h'
invFun x := ⟨.inl x, mem_range_self _⟩
left_inv := fun ⟨_, _, rfl⟩ => rfl
