mathlib3 documentation

logic.equiv.option

Equivalences for option α #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
@[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) :
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 : α β) :
def equiv.option_subtype {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) :
{e // e option.none = x} {y // y x})

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

Equations
@[simp]
theorem equiv.option_subtype_apply_apply {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : {e // e option.none = x}) (a : α) (h : e a x) :
@[simp]
theorem equiv.coe_option_subtype_apply_apply {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : {e // e option.none = x}) (a : α) :
@[simp]
theorem equiv.option_subtype_apply_symm_apply {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : {e // e option.none = x}) (b : {y // y x}) :
@[simp]
theorem equiv.option_subtype_symm_apply_apply_coe {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : α {y // y x}) (a : α) :
@[simp]
theorem equiv.option_subtype_symm_apply_apply_some {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : α {y // y x}) (a : α) :
@[simp]
theorem equiv.option_subtype_symm_apply_apply_none {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : α {y // y x}) :
@[simp]
theorem equiv.option_subtype_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : α {y // y x}) (b : {y // y x}) :