# Equivalences for Option α#

We define

• Equiv.optionCongr: the Option α ≃ Option β constructed from e : α ≃ β by sending none to none, and applying e elsewhere.
• Equiv.removeNone: the α ≃ β constructed from Option α ≃ Option β by removing none from both sides.
@[simp]
theorem Equiv.optionCongr_apply {α : Type u_1} {β : Type u_2} (e : α β) :
∀ (a : ), e.optionCongr a = Option.map (e) a
def Equiv.optionCongr {α : Type u_1} {β : Type u_2} (e : α β) :

A universe-polymorphic version of EquivFunctor.mapEquiv Option e.

Equations
• e.optionCongr = { toFun := , invFun := Option.map e.symm, left_inv := , right_inv := }
Instances For
@[simp]
theorem Equiv.optionCongr_refl {α : Type u_1} :
().optionCongr = Equiv.refl ()
@[simp]
theorem Equiv.optionCongr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
e.optionCongr.symm = e.symm.optionCongr
@[simp]
theorem Equiv.optionCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α β) (e₂ : β γ) :
e₁.optionCongr.trans e₂.optionCongr = (e₁.trans e₂).optionCongr
theorem Equiv.optionCongr_eq_equivFunctor_mapEquiv {α : Type u} {β : Type u} (e : α β) :
e.optionCongr =

When α and β are in the same universe, this is the same as the result of EquivFunctor.mapEquiv.

def Equiv.removeNone_aux {α : Type u_1} {β : Type u_2} (e : ) (x : α) :
β

If we have a value on one side of an Equiv of Option we also have a value on the other side of the equivalence

Equations
• e.removeNone_aux x = if h : (e (some x)).isSome = true then (e (some x)).get h else (e none).get
Instances For
theorem Equiv.removeNone_aux_some {α : Type u_1} {β : Type u_2} (e : ) {x : α} (h : ∃ (x' : β), e (some x) = some x') :
some (e.removeNone_aux x) = e (some x)
theorem Equiv.removeNone_aux_none {α : Type u_1} {β : Type u_2} (e : ) {x : α} (h : e (some x) = none) :
some (e.removeNone_aux x) = e none
theorem Equiv.removeNone_aux_inv {α : Type u_1} {β : Type u_2} (e : ) (x : α) :
e.symm.removeNone_aux (e.removeNone_aux x) = x
def Equiv.removeNone {α : Type u_1} {β : Type u_2} (e : ) :
α β

Given an equivalence between two Option types, eliminate none from that equivalence by mapping e.symm none to e none.

Equations
• e.removeNone = { toFun := e.removeNone_aux, invFun := e.symm.removeNone_aux, left_inv := , right_inv := }
Instances For
@[simp]
theorem Equiv.removeNone_symm {α : Type u_1} {β : Type u_2} (e : ) :
e.removeNone.symm = e.symm.removeNone
theorem Equiv.removeNone_some {α : Type u_1} {β : Type u_2} (e : ) {x : α} (h : ∃ (x' : β), e (some x) = some x') :
some (e.removeNone x) = e (some x)
theorem Equiv.removeNone_none {α : Type u_1} {β : Type u_2} (e : ) {x : α} (h : e (some x) = none) :
some (e.removeNone x) = e none
@[simp]
theorem Equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : ) :
e.symm none = none e none = none
theorem Equiv.some_removeNone_iff {α : Type u_1} {β : Type u_2} (e : ) {x : α} :
some (e.removeNone x) = e none e.symm none = some x
@[simp]
theorem Equiv.removeNone_optionCongr {α : Type u_1} {β : Type u_2} (e : α β) :
e.optionCongr.removeNone = e
theorem Equiv.optionCongr_injective {α : Type u_1} {β : Type u_2} :
Function.Injective Equiv.optionCongr
def Equiv.optionSubtype {α : Type u_1} {β : Type u_2} [] (x : β) :
{ e : β // e none = x } (α { y : β // y x })

Equivalences between Option α and β that send none to x are equivalent to equivalences between α and {y : β // y ≠ x}.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Equiv.optionSubtype_apply_apply {α : Type u_1} {β : Type u_2} [] (x : β) (e : { e : β // e none = x }) (a : α) (h : e (some a) x) :
( e) a = e (some a), h
@[simp]
theorem Equiv.coe_optionSubtype_apply_apply {α : Type u_1} {β : Type u_2} [] (x : β) (e : { e : β // e none = x }) (a : α) :
(( e) a) = e (some a)
@[simp]
theorem Equiv.optionSubtype_apply_symm_apply {α : Type u_1} {β : Type u_2} [] (x : β) (e : { e : β // e none = x }) (b : { y : β // y x }) :
some (( e).symm b) = (e).symm b
@[simp]
theorem Equiv.optionSubtype_symm_apply_apply_coe {α : Type u_1} {β : Type u_2} [] (x : β) (e : α { y : β // y x }) (a : α) :
(.symm e) (some a) = (e a)
@[simp]
theorem Equiv.optionSubtype_symm_apply_apply_some {α : Type u_1} {β : Type u_2} [] (x : β) (e : α { y : β // y x }) (a : α) :
(.symm e) (some a) = (e a)
@[simp]
theorem Equiv.optionSubtype_symm_apply_apply_none {α : Type u_1} {β : Type u_2} [] (x : β) (e : α { y : β // y x }) :
(.symm e) none = x
@[simp]
theorem Equiv.optionSubtype_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [] (x : β) (e : α { y : β // y x }) (b : { y : β // y x }) :
((.symm e)).symm b = some (e.symm b)
@[simp]
theorem Equiv.optionSubtypeNe_apply {α : Type u_1} [] (a : α) (a : Option { y : α // y a✝ }) :
a = a.casesOn' a✝ Subtype.val
@[simp]
theorem Equiv.optionSubtypeNe_symm_apply {α : Type u_1} [] (a : α) (b : α) :
.symm b = if h : b = a then none else some b, h
def Equiv.optionSubtypeNe {α : Type u_1} [] (a : α) :
Option { b : α // b a } α

Any type with a distinguished element is equivalent to an Option type on the subtype excluding that element.

Equations
Instances For
theorem Equiv.optionSubtypeNe_symm_self {α : Type u_1} [] (a : α) :
.symm a = none
theorem Equiv.optionSubtypeNe_symm_of_ne {α : Type u_1} [] {a : α} {b : α} (hba : b a) :
.symm b = some b, hba
@[simp]
theorem Equiv.optionSubtypeNe_none {α : Type u_1} [] (a : α) :
none = a
@[simp]
theorem Equiv.optionSubtypeNe_some {α : Type u_1} [] (a : α) (b : { b : α // b a }) :
(some b) = b