Equivalences for option α #
We define
equiv.option_congr: theoption α ≃ option βconstructed frome : α ≃ βby sendingnonetonone, and applying aeelsewhere.equiv.remove_none: theα ≃ βconstructed fromoption α ≃ option βby removingnonefrom both sides.
A universe-polymorphic version of equiv_functor.map_equiv option e.
Equations
- e.option_congr = {to_fun := option.map ⇑e, inv_fun := option.map ⇑(e.symm), left_inv := _, right_inv := _}
@[simp]
theorem
equiv.option_congr_apply
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β)
(o : option α) :
⇑(e.option_congr) o = option.map ⇑e o
@[simp]
theorem
equiv.option_congr_refl
{α : Type u_1} :
(equiv.refl α).option_congr = equiv.refl (option α)
@[simp]
@[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
When α and β are in the same universe, this is the same as the result of
equiv_functor.map_equiv.
Given an equivalence between two option types, eliminate none from that equivalence by
mapping e.symm none to e none.
@[simp]
theorem
equiv.remove_none_symm
{α : Type u_1}
{β : Type u_2}
(e : option α ≃ option β) :
e.remove_none.symm = e.symm.remove_none
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)
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
@[simp]
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
@[simp]
theorem
equiv.remove_none_option_congr
{α : Type u_1}
{β : Type u_2}
(e : α ≃ β) :
e.option_congr.remove_none = e
Equivalences between option α and β that send none to x are equivalent to
equivalences between α and {y : β // y ≠ x}.
Equations
- equiv.option_subtype x = {to_fun := λ (e : {e // ⇑e option.none = x}), {to_fun := λ (a : α), ⟨⇑e ↑a, _⟩, inv_fun := λ (b : {y // y ≠ x}), option.get _, left_inv := _, right_inv := _}, inv_fun := λ (e : α ≃ {y // y ≠ x}), ⟨{to_fun := λ (a : option α), a.cases_on' x (coe ∘ ⇑e), inv_fun := λ (b : β), dite (b = x) (λ (h : b = x), option.none) (λ (h : ¬b = x), ↑(⇑(e.symm) ⟨b, h⟩)), left_inv := _, right_inv := _}, _⟩, left_inv := _, right_inv := _}
@[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 : α) :
⇑(⇑((equiv.option_subtype x).symm) e) (option.some a) = ↑(⇑e a)
@[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