mathlib documentation

logic.equiv.option

Equivalences for option α #

We define

source
def equiv.option_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
option α ≃ option β

A universe-polymorphic version of equiv_functor.map_equiv option e.

Equations
source
@[simp]
theorem equiv.option_congr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (o : option α) :
⇑(e.option_congr) o = option.map ⇑e o
source
@[simp]
theorem equiv.option_congr_refl {α : Type u_1} :
(equiv.refl α).option_congr = equiv.refl (option α)
source
@[simp]
theorem equiv.option_congr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.option_congr.symm = e.symm.option_congr
source
@[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
source
theorem equiv.option_congr_eq_equiv_function_map_equiv {α β : Type u_1} (e : α ≃ β) :
e.option_congr = equiv_functor.map_equiv option e

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

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_option_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :
e.option_congr.remove_none = e
source
theorem equiv.option_congr_injective {α : Type u_1} {β : Type u_2} :
function.injective equiv.option_congr