mathlib documentation

logic.equiv.option

Equivalences for option α #

We define

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

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

Equations
@[simp]
theorem equiv.option_congr_apply {α : Type u_1} {β : Type u_2} (e : α β) (o : option α) :
@[simp]
theorem equiv.option_congr_refl {α : Type u_1} :
@[simp]
theorem equiv.option_congr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
@[simp]
theorem equiv.option_congr_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 equiv_functor.map_equiv.

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
@[simp]
theorem equiv.remove_none_symm {α : Type u_1} {β : Type u_2} (e : option α option β) :
theorem equiv.remove_none_some {α : Type u_1} {β : Type u_2} (e : option α option β) {x : α} (h : ∃ (x' : β), e (option.some x) = 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) :
@[simp]
theorem equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : option α option β) :
theorem equiv.some_remove_none_iff {α : Type u_1} {β : Type u_2} (e : option α option β) {x : α} :
@[simp]
theorem equiv.remove_none_option_congr {α : Type u_1} {β : Type u_2} (e : α β) :
theorem equiv.option_congr_injective {α : Type u_1} {β : Type u_2} :