Equivalences for option α
#
We define
equiv.option_congr
: theoption α ≃ option β
constructed frome : α ≃ β
by sendingnone
tonone
, and applying ae
elsewhere.equiv.remove_none
: theα ≃ β
constructed fromoption α ≃ option β
by removingnone
from both sides.
A universe-polymorphic version of equiv_functor.map_equiv option e
.
Equations
- e.option_congr = {to_fun := option.map ⇑e, inv_fun := option.map ⇑(e.symm), left_inv := _, right_inv := _}
@[simp]
theorem
equiv.option_congr_apply
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
(o : option α) :
⇑(e.option_congr) o = option.map ⇑e o
@[simp]
theorem
equiv.option_congr_refl
{α : Type u_1} :
(equiv.refl α).option_congr = equiv.refl (option α)
@[simp]
@[simp]
theorem
equiv.option_congr_trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(e₁ : α ≃ β)
(e₂ : β ≃ γ) :
e₁.option_congr.trans e₂.option_congr = (e₁.trans e₂).option_congr
When α
and β
are in the same universe, this is the same as the result of
equiv_functor.map_equiv
.
Given an equivalence between two option
types, eliminate none
from that equivalence by
mapping e.symm none
to e none
.
@[simp]
theorem
equiv.remove_none_symm
{α : Type u_1}
{β : Type u_2}
(e : option α ≃ option β) :
e.remove_none.symm = e.symm.remove_none
theorem
equiv.remove_none_some
{α : Type u_1}
{β : Type u_2}
(e : option α ≃ option β)
{x : α}
(h : ∃ (x' : β), ⇑e (option.some x) = option.some x') :
option.some (⇑(e.remove_none) x) = ⇑e (option.some x)
theorem
equiv.remove_none_none
{α : Type u_1}
{β : Type u_2}
(e : option α ≃ option β)
{x : α}
(h : ⇑e (option.some x) = option.none) :
option.some (⇑(e.remove_none) x) = ⇑e option.none
@[simp]
theorem
equiv.some_remove_none_iff
{α : Type u_1}
{β : Type u_2}
(e : option α ≃ option β)
{x : α} :
option.some (⇑(e.remove_none) x) = ⇑e option.none ↔ ⇑(e.symm) option.none = option.some x
@[simp]
theorem
equiv.remove_none_option_congr
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β) :
e.option_congr.remove_none = e