# mathlib3documentation

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

• equiv.option_congr: the option α ≃ option β constructed from e : α ≃ β by sending none to none, and applying a e elsewhere.
• equiv.remove_none: the α ≃ β constructed from option α ≃ option β by removing none from both sides.
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₂ : β γ) :
= (e₁.trans e₂).option_congr
theorem equiv.option_congr_eq_equiv_function_map_equiv {α β : Type u_1} (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 : ) :
α β

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 : ) :
theorem equiv.remove_none_some {α : Type u_1} {β : Type u_2} (e : ) {x : α} (h : (x' : β), e (option.some x) = ) :
theorem equiv.remove_none_none {α : Type u_1} {β : Type u_2} (e : ) {x : α} (h : e (option.some x) = option.none) :
@[simp]
theorem equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : ) :
theorem equiv.some_remove_none_iff {α : Type u_1} {β : Type u_2} (e : ) {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} :
def equiv.option_subtype {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) :
{e // = 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 // = x}) (a : α) (h : e a x) :
e) a = e a, h⟩
@[simp]
theorem equiv.coe_option_subtype_apply_apply {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : {e // = x}) (a : α) :
( e) a) = e a
@[simp]
theorem equiv.option_subtype_apply_symm_apply {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : {e // = x}) (b : {y // y x}) :
((( e).symm) b) = (e.symm) b
@[simp]
theorem equiv.option_subtype_symm_apply_apply_coe {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : α {y // y x}) (a : α) :
(.symm) e) a = (e 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}) :
((.symm) e).symm) b = ((e.symm) b)