mathlib 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

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 (option.some x) = option.some x') :
option.some (⇑(e.remove_none) x) = ⇑e (option.some x)
source
theorem equiv.remove_none_none {α : Type u_1} {β : Type u_2} (e : option α ≃ option β) {x : α} (h : ⇑e (option.some x) = option.none) :
option.some (⇑(e.remove_none) x) = ⇑e option.none
source
@[simp]
theorem equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : option α ≃ option β) :
⇑(e.symm) option.none = option.none ↔ ⇑e option.none = option.none
source
theorem equiv.some_remove_none_iff {α : Type u_1} {β : Type u_2} (e : option α ≃ option β) {x : α} :
option.some (⇑(e.remove_none) x) = ⇑e option.none ↔ ⇑(e.symm) option.none = option.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
source
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
source
@[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) :
⇑(⇑(equiv.option_subtype x) e) a = ⟨⇑↑e ↑a, h⟩
source
@[simp]
theorem equiv.coe_option_subtype_apply_apply {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : {e // ⇑e option.none = x}) (a : α) :
↑(⇑(⇑(equiv.option_subtype x) e) a) = ⇑↑e ↑a
source
@[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}) :
↑(⇑((⇑(equiv.option_subtype x) e).symm) b) = ⇑(↑e.symm) ↑b
source
@[simp]
theorem equiv.option_subtype_symm_apply_apply_coe {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : α ≃ {y // y ≠ x}) (a : α) :
⇑(⇑((equiv.option_subtype x).symm) e) ↑a = ↑(⇑e a)
source
@[simp]
theorem equiv.option_subtype_symm_apply_apply_some {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : α ≃ {y // y ≠ x}) (a : α) :
⇑(⇑((equiv.option_subtype x).symm) e) (option.some a) = ↑(⇑e a)
source
@[simp]
theorem equiv.option_subtype_symm_apply_apply_none {α : Type u_1} {β : Type u_2} [decidable_eq β] (x : β) (e : α ≃ {y // y ≠ x}) :
⇑(⇑((equiv.option_subtype x).symm) e) option.none = x
source
@[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}) :
⇑(↑(⇑((equiv.option_subtype x).symm) e).symm) ↑b = ↑(⇑(e.symm) b)