sumIsLeft — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The left summand of `α ⊕ β` is equivalent to `α`. -/
@[simps (attr := grind =)]
def sumIsLeft : { x : α ⊕ β // x.isLeft } ≃ α
    where
  toFun x := x.1.getLeft x.2
  invFun a := ⟨.inl a, Sum.isLeft_inl⟩
  left_inv
    | ⟨.inl _a, _⟩ => rfl

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