psumEquivSum — Mathlib

English

There is an equivalence between PSum α β and Sum α β; PSum is isomorphic to Sum with inl and inr.

Русский

Существует эквивалентность между PSum α β и Sum α β; PSum изоморфен Sum.

LaTeX

$$PSum α β ≃ Sum α β$$

Lean4

/-- `PSum` is equivalent to `Sum`. -/
def psumEquivSum (α β) : α ⊕' β ≃ α ⊕ β where
  toFun s := PSum.casesOn s inl inr
  invFun := Sum.elim PSum.inl PSum.inr
  left_inv s := by cases s <;> rfl
  right_inv s := by cases s <;> rfl

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