Documentation

Mathlib.Logic.Equiv.Option

Equivalences for Option α #

We define

@[simp]
theorem Equiv.optionCongr_apply {α : Type u_1} {β : Type u_2} (e : α β) :
∀ (a : Option α), ↑(Equiv.optionCongr e) 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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Equiv.optionCongr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
@[simp]
theorem Equiv.optionCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α β) (e₂ : β γ) :

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 : Option α Option β) (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
theorem Equiv.removeNone_aux_some {α : Type u_2} {β : Type u_1} (e : Option α Option β) {x : α} (h : x', e (some x) = some x') :
theorem Equiv.removeNone_aux_none {α : Type u_2} {β : Type u_1} (e : Option α Option β) {x : α} (h : e (some x) = none) :
some (Equiv.removeNone_aux e x) = e none
theorem Equiv.removeNone_aux_inv {α : Type u_1} {β : Type u_2} (e : Option α Option β) (x : α) :
def Equiv.removeNone {α : Type u_1} {β : Type u_2} (e : Option α Option β) :
α β

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

Equations
  • One or more equations did not get rendered due to their size.
theorem Equiv.removeNone_some {α : Type u_2} {β : Type u_1} (e : Option α Option β) {x : α} (h : x', e (some x) = some x') :
some (↑(Equiv.removeNone e) x) = e (some x)
theorem Equiv.removeNone_none {α : Type u_2} {β : Type u_1} (e : Option α Option β) {x : α} (h : e (some x) = none) :
some (↑(Equiv.removeNone e) x) = e none
@[simp]
theorem Equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : Option α Option β) :
↑(Equiv.symm e) none = none e none = none
theorem Equiv.some_removeNone_iff {α : Type u_2} {β : Type u_1} (e : Option α Option β) {x : α} :
some (↑(Equiv.removeNone e) x) = e none ↑(Equiv.symm e) none = some x
@[simp]
theorem Equiv.removeNone_optionCongr {α : Type u_1} {β : Type u_2} (e : α β) :
theorem Equiv.optionCongr_injective {α : Type u_1} {β : Type u_2} :
Function.Injective Equiv.optionCongr
def Equiv.optionSubtype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (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}≠ x}.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Equiv.optionSubtype_apply_apply {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : { e // e none = x }) (a : α) (h : e (some a) x) :
↑(↑(Equiv.optionSubtype x) e) a = { val := e (some a), property := h }
@[simp]
theorem Equiv.coe_optionSubtype_apply_apply {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : { e // e none = x }) (a : α) :
↑(↑(↑(Equiv.optionSubtype x) e) a) = e (some a)
@[simp]
theorem Equiv.optionSubtype_apply_symm_apply {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : { e // e none = x }) (b : { y // y x }) :
some (↑(Equiv.symm (↑(Equiv.optionSubtype x) e)) b) = ↑(Equiv.symm e) b
@[simp]
theorem Equiv.optionSubtype_symm_apply_apply_coe {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : α { y // y x }) (a : α) :
↑(↑(Equiv.symm (Equiv.optionSubtype x)) e) (some a) = ↑(e a)
@[simp]
theorem Equiv.optionSubtype_symm_apply_apply_some {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : α { y // y x }) (a : α) :
↑(↑(Equiv.symm (Equiv.optionSubtype x)) e) (some a) = ↑(e a)
@[simp]
theorem Equiv.optionSubtype_symm_apply_apply_none {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : α { y // y x }) :
↑(↑(Equiv.symm (Equiv.optionSubtype x)) e) none = x
@[simp]
theorem Equiv.optionSubtype_symm_apply_symm_apply {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : α { y // y x }) (b : { y // y x }) :
↑(Equiv.symm ↑(↑(Equiv.symm (Equiv.optionSubtype x)) e)) b = some (↑(Equiv.symm e) b)