Equivalences for Option α
#
We define
Equiv.optionCongr
: theOption α ≃ Option β
constructed frome : α ≃ β
by sendingnone
tonone
, and applyinge
elsewhere.Equiv.removeNone
: theα ≃ β
constructed fromOption α ≃ Option β
by removingnone
from both sides.
@[simp]
@[simp]
@[simp]
When α
and β
are in the same universe, this is the same as the result of
EquivFunctor.mapEquiv
.
@[simp]
@[simp]
theorem
Equiv.optionSubtype_symm_apply_apply_coe
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
(x : β)
(e : α ≃ { y : β // y ≠ x })
(a : α)
:
@[simp]
theorem
Equiv.optionSubtype_symm_apply_apply_some
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
(x : β)
(e : α ≃ { y : β // y ≠ x })
(a : α)
:
@[simp]
theorem
Equiv.optionSubtype_symm_apply_apply_none
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
(x : β)
(e : α ≃ { y : β // y ≠ x })
:
@[simp]
@[simp]
theorem
Equiv.optionSubtypeNe_apply
{α : Type u_1}
[DecidableEq α]
(a : α)
(a✝ : Option { y : α // y ≠ a })
:
@[simp]
@[simp]
theorem
Equiv.optionSubtypeNe_some
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : { b : α // b ≠ a })
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]