sumIsRight — Mathlib

English

The right summand of α ⊕ β is equivalent to β.

Русский

Правая часть суммы α ⊕ β эквивалентна β.

LaTeX

$$$\\{ x : \\alpha \\oplus \\beta \\;\\text{and}\\\\ x.\\mathrm{isRight} \\} \\cong \\beta$$$

Lean4

/-- The right summand of `α ⊕ β` is equivalent to `β`. -/
@[simps (attr := grind =)]
def sumIsRight : { x : α ⊕ β // x.isRight } ≃ β
    where
  toFun x := x.1.getRight x.2
  invFun b := ⟨.inr b, Sum.isRight_inr⟩
  left_inv
    | ⟨.inr _b, _⟩ => rfl

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