rangeInr — Mathlib

English

Equivalence between the range of Sum.inr and β.

Русский

Эквивалентность между образом Sum.inr и β.

LaTeX

$$$\\mathrm{rangeInr}(\\alpha,\\beta) : \\mathrm{Set.range}(\\mathrm{Sum.inr}) \\simeq \\beta$$$

Lean4

/-- Equivalence between the range of `Sum.inr : β → α ⊕ β` and `β`. -/
@[simps symm_apply_coe]
def rangeInr (α β : Type*) : Set.range (Sum.inr : β → α ⊕ β) ≃ β
    where
  toFun
    | ⟨.inl _, h⟩ => False.elim <| by rcases h with ⟨x, h'⟩; cases h'
    | ⟨.inr x, _⟩ => x
  invFun x := ⟨.inr x, mem_range_self _⟩
  left_inv := fun ⟨_, _, rfl⟩ => rfl

Похожие утверждения