optionEquivSumPUnit — Mathlib

English

There is a canonical equivalence between Option α and α ⊕ PUnit, sending none to inr unit and some a to inl a.

Русский

Существует каноническая эквивалентость между Option α и α ⊕ PUnit, отправляющая none в inr unit, а some a в inl a.

LaTeX

$$$\mathrm{Option}\,\alpha \simeq \alpha \oplus \mathrm{PUnit}$ with the specified forward/backward maps.$$

Lean4

/-- `Option α` is equivalent to `α ⊕ PUnit` -/
def optionEquivSumPUnit.{v, w} (α : Type w) : Option α ≃ α ⊕ PUnit.{v + 1} :=
  ⟨fun o => o.elim (inr PUnit.unit) inl, fun s => s.elim some fun _ => none, fun o => by cases o <;> rfl, fun s => by
    rcases s with (_ | ⟨⟨⟩⟩) <;> rfl⟩

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