optionEquivSumPUnit_coe — Mathlib

English

There is a natural bijection between the type Option α and the sum α ⊕ PUnit; under this bijection, the forward map sends some a to inl a.

Русский

Существуют естественный биекция между типом Option α и суммой α ⊕ PUnit; переход в прямом направлении отправляет Some a в inl a.

LaTeX

$$$\forall \alpha\, (a:\alpha), \operatorname{optionEquivSumPUnit} \alpha\ a = \mathrm{Sum.inl}\ a$$$

Lean4

@[simp]
theorem optionEquivSumPUnit_coe {α} (a : α) : optionEquivSumPUnit α a = Sum.inl a :=
  rfl

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