mathlib documentation

data.equiv.option

Equivalences for option α #

We define remove_none which acts to provide a e : α ≃ β if given a f : option α ≃ option β.

To construct an f : option α ≃ option β from e : α ≃ β such that f none = none and f (some x) = some (e x), use f = equiv_functor.map_equiv option e.

source
def equiv.remove_none {α : 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
source
@[simp]
theorem equiv.remove_none_symm {α : Type u_1} {β : Type u_2} (e : option α ≃ option β) :
e.remove_none.symm = e.symm.remove_none
source
theorem equiv.remove_none_some {α : Type u_1} {β : Type u_2} (e : option α ≃ option β) {x : α} (h : ∃ (x' : β), ⇑e (some x) = some x') :
some (⇑(e.remove_none) x) = ⇑e (some x)
source
theorem equiv.remove_none_none {α : Type u_1} {β : Type u_2} (e : option α ≃ option β) {x : α} (h : ⇑e (some x) = none) :
some (⇑(e.remove_none) x) = ⇑e none
source
@[simp]
theorem equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : option α ≃ option β) :
⇑(e.symm) none = none ↔ ⇑e none = none
source
theorem equiv.some_remove_none_iff {α : Type u_1} {β : Type u_2} (e : option α ≃ option β) {x : α} :
some (⇑(e.remove_none) x) = ⇑e none ↔ ⇑(e.symm) none = some x
source
@[simp]
theorem equiv.remove_none_map_equiv {α β : Type u_1} (e : α ≃ β) :
(equiv_functor.map_equiv option e).remove_none = e