Mathlib.Logic.Equiv.Option

Equiv.optionCongr definition

(e : α ≃ β) : Option α ≃ Option β

Full source

/-- A universe-polymorphic version of `EquivFunctor.mapEquiv Option e`. -/
@[simps apply]
def optionCongr (e : α ≃ β) : OptionOption α ≃ Option β where
  toFun := Option.map e
  invFun := Option.map e.symm
  left_inv x := (Option.map_map _ _ _).trans <| e.symm_comp_self.symm ▸ congr_fun Option.map_id x
  right_inv x := (Option.map_map _ _ _).trans <| e.self_comp_symm.symm ▸ congr_fun Option.map_id x

Equivalence of Option types induced by an equivalence

Informal description

Given an equivalence $e : \alpha \simeq \beta$, the function constructs an equivalence $\text{Option } \alpha \simeq \text{Option } \beta$ by mapping $\text{none}$ to $\text{none}$ and applying $e$ to the values inside $\text{some}$.

Equiv.optionCongr_refl theorem

: optionCongr (Equiv.refl α) = Equiv.refl _

Full source

@[simp]
theorem optionCongr_refl : optionCongr (Equiv.refl α) = Equiv.refl _ :=
  ext <| congr_fun Option.map_id

Identity Equivalence Preserved by `optionCongr`

Informal description

The equivalence `optionCongr` applied to the identity equivalence on a type $\alpha$ yields the identity equivalence on $\text{Option } \alpha$, i.e., $\text{optionCongr}(\text{id}_\alpha) = \text{id}_{\text{Option } \alpha}$.

Equiv.optionCongr_symm theorem

(e : α ≃ β) : (optionCongr e).symm = optionCongr e.symm

Full source

@[simp]
theorem optionCongr_symm (e : α ≃ β) : (optionCongr e).symm = optionCongr e.symm :=
  rfl

Inverse of Option Equivalence Induced by Equivalence

Informal description

For any equivalence $e : \alpha \simeq \beta$, the inverse of the induced equivalence $\text{Option } \alpha \simeq \text{Option } \beta$ (constructed by mapping $\text{none}$ to $\text{none}$ and applying $e$ to $\text{some}$ values) is equal to the equivalence induced by the inverse of $e$, i.e., $(\text{optionCongr } e)^{-1} = \text{optionCongr } e^{-1}$.

Equiv.optionCongr_trans theorem

(e₁ : α ≃ β) (e₂ : β ≃ γ) : (optionCongr e₁).trans (optionCongr e₂) = optionCongr (e₁.trans e₂)

Full source

@[simp]
theorem optionCongr_trans (e₁ : α ≃ β) (e₂ : β ≃ γ) :
    (optionCongr e₁).trans (optionCongr e₂) = optionCongr (e₁.trans e₂) :=
  ext <| Option.map_map _ _

Composition of Option Equivalences via Composition of Underlying Equivalences

Informal description

Given equivalences $e₁ : α ≃ β$ and $e₂ : β ≃ γ$, the composition of the induced option equivalences $(e₁.\text{optionCongr}) \circ (e₂.\text{optionCongr})$ is equal to the option equivalence induced by the composition $e₁ \circ e₂$, i.e., $$(e₁.\text{optionCongr}) \circ (e₂.\text{optionCongr}) = (e₁ \circ e₂).\text{optionCongr}.$$

Equiv.optionCongr_eq_equivFunctor_mapEquiv theorem

{α β : Type u} (e : α ≃ β) : optionCongr e = EquivFunctor.mapEquiv Option e

Full source

/-- When `α` and `β` are in the same universe, this is the same as the result of
`EquivFunctor.mapEquiv`. -/
theorem optionCongr_eq_equivFunctor_mapEquiv {α β : Type u} (e : α ≃ β) :
    optionCongr e = EquivFunctor.mapEquiv Option e :=
  rfl

Equality of Option Equivalence Constructions: $\text{optionCongr } e = \text{mapEquiv Option } e$

Informal description

For any types $\alpha$ and $\beta$ in the same universe and any equivalence $e : \alpha \simeq \beta$, the equivalence $\text{optionCongr } e$ between $\text{Option } \alpha$ and $\text{Option } \beta$ is equal to the result of applying the functorial map of $\text{Option}$ to $e$, i.e., $\text{optionCongr } e = \text{EquivFunctor.mapEquiv Option } e$.

Equiv.removeNone_aux definition

(x : α) : β

Full source

/-- If we have a value on one side of an `Equiv` of `Option`
    we also have a value on the other side of the equivalence
-/
def removeNone_aux (x : α) : β :=
  if h : (e (some x)).isSome then Option.get _ h
  else
    Option.get _ <|
      show (e none).isSome by
        rw [← Option.ne_none_iff_isSome]
        intro hn
        rw [Option.not_isSome_iff_eq_none, ← hn] at h
        exact Option.some_ne_none _ (e.injective h)

Auxiliary function for removing `none` in an equivalence of options

Informal description

Given an equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$ and an element $x \in \alpha$, the function returns the element $y \in \beta$ such that $e(\text{some } x) = \text{some } y$ if such $y$ exists, otherwise it returns the element $y' \in \beta$ such that $e(\text{none}) = \text{some } y'$.

Equiv.removeNone_aux_some theorem

{x : α} (h : ∃ x', e (some x) = some x') : some (removeNone_aux e x) = e (some x)

Full source

theorem removeNone_aux_some {x : α} (h : ∃ x', e (some x) = some x') :
    some (removeNone_aux e x) = e (some x) := by
  simp [removeNone_aux, Option.isSome_iff_exists.mpr h]

Auxiliary Some Preservation Property for Option Equivalence

Informal description

For any element $x \in \alpha$ and equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, if there exists $x' \in \beta$ such that $e(\text{some } x) = \text{some } x'$, then $\text{some } (\text{removeNone\_aux } e x) = e(\text{some } x)$.

Equiv.removeNone_aux_none theorem

{x : α} (h : e (some x) = none) : some (removeNone_aux e x) = e none

Full source

theorem removeNone_aux_none {x : α} (h : e (some x) = none) :
    some (removeNone_aux e x) = e none := by
  simp [removeNone_aux, Option.not_isSome_iff_eq_none.mpr h]

Auxiliary None Removal Property for Option Equivalence

Informal description

For any element $x \in \alpha$ and equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, if $e(\text{some } x) = \text{none}$, then $\text{some } (\text{removeNone\_aux } e x) = e(\text{none})$.

Equiv.removeNone_aux_inv theorem

(x : α) : removeNone_aux e.symm (removeNone_aux e x) = x

Full source

theorem removeNone_aux_inv (x : α) : removeNone_aux e.symm (removeNone_aux e x) = x :=
  Option.some_injective _
    (by
      cases h1 : e.symm (some (removeNone_aux e x)) <;> cases h2 : e (some x)
      · rw [removeNone_aux_none _ h1]
        exact (e.eq_symm_apply.mpr h2).symm

      · rw [removeNone_aux_some _ ⟨_, h2⟩] at h1
        simp at h1

      · rw [removeNone_aux_none _ h2] at h1
        simp at h1

      · rw [removeNone_aux_some _ ⟨_, h1⟩]
        rw [removeNone_aux_some _ ⟨_, h2⟩]
        simp)

Inverse Property of `removeNone_aux` for Option Equivalence

Informal description

For any element $x \in \alpha$ and equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, applying the auxiliary function $\text{removeNone\_aux}$ with $e$ and then with its inverse $e^{-1}$ recovers the original element $x$, i.e., $\text{removeNone\_aux } e^{-1} (\text{removeNone\_aux } e x) = x$.

Equiv.removeNone definition

: α ≃ β

Full source

/-- Given an equivalence between two `Option` types, eliminate `none` from that equivalence by
mapping `e.symm none` to `e none`. -/
def removeNone : α ≃ β where
  toFun := removeNone_aux e
  invFun := removeNone_aux e.symm
  left_inv := removeNone_aux_inv e
  right_inv := removeNone_aux_inv e.symm

Equivalence between $\alpha$ and $\beta$ by removing $\text{none}$ from an option equivalence

Informal description

Given an equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, the equivalence $\text{removeNone } e : \alpha \simeq \beta$ is constructed by eliminating the $\text{none}$ cases from $e$. Specifically, it maps $x \in \alpha$ to the unique $y \in \beta$ such that $e(\text{some } x) = \text{some } y$, and if no such $y$ exists (i.e., $e(\text{some } x) = \text{none}$), it maps $x$ to the unique $y' \in \beta$ such that $e(\text{none}) = \text{some } y'$. The inverse function is similarly constructed using the inverse equivalence $e^{-1}$.

Equiv.removeNone_symm theorem

: (removeNone e).symm = removeNone e.symm

Full source

@[simp]
theorem removeNone_symm : (removeNone e).symm = removeNone e.symm :=
  rfl

Inverse of $\text{removeNone}$ Equivalence

Informal description

For any equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, the inverse of the equivalence $\text{removeNone } e : \alpha \simeq \beta$ is equal to the equivalence obtained by applying $\text{removeNone}$ to the inverse of $e$, i.e., $(\text{removeNone } e)^{-1} = \text{removeNone } (e^{-1})$.

Equiv.removeNone_some theorem

{x : α} (h : ∃ x', e (some x) = some x') : some (removeNone e x) = e (some x)

Full source

theorem removeNone_some {x : α} (h : ∃ x', e (some x) = some x') :
    some (removeNone e x) = e (some x) :=
  removeNone_aux_some e h

Preservation of Some under Equivalence Removal: $\text{some } (\text{removeNone } e x) = e(\text{some } x)$ when $e(\text{some } x) = \text{some } x'$

Informal description

For any element $x \in \alpha$ and equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, if there exists $x' \in \beta$ such that $e(\text{some } x) = \text{some } x'$, then $\text{some } (\text{removeNone } e x) = e(\text{some } x)$.

Equiv.removeNone_none theorem

{x : α} (h : e (some x) = none) : some (removeNone e x) = e none

Full source

theorem removeNone_none {x : α} (h : e (some x) = none) : some (removeNone e x) = e none :=
  removeNone_aux_none e h

None Removal Property for Option Equivalence: $\text{some } (\text{removeNone } e x) = e(\text{none})$ when $e(\text{some } x) = \text{none}$

Informal description

For any element $x \in \alpha$ and equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, if $e(\text{some } x) = \text{none}$, then $\text{some } (\text{removeNone } e x) = e(\text{none})$.

Equiv.option_symm_apply_none_iff theorem

: e.symm none = none ↔ e none = none

Full source

@[simp]
theorem option_symm_apply_none_iff : e.symm none = none ↔ e none = none :=
  ⟨fun h => by simpa using (congr_arg e h).symm, fun h => by simpa using (congr_arg e.symm h).symm⟩

Inverse Equivalence Preserves None: $e^{-1}(\text{none}) = \text{none} \leftrightarrow e(\text{none}) = \text{none}$

Informal description

For any equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, the inverse equivalence $e^{-1}$ maps `none` to `none` if and only if $e$ maps `none` to `none$. In other words, $e^{-1}(\text{none}) = \text{none} \leftrightarrow e(\text{none}) = \text{none}$.

Equiv.some_removeNone_iff theorem

{x : α} : some (removeNone e x) = e none ↔ e.symm none = some x

Full source

theorem some_removeNone_iff {x : α} : somesome (removeNone e x) = e none ↔ e.symm none = some x := by
  rcases h : e (some x) with a | a
  · rw [removeNone_none _ h]
    simpa using (congr_arg e.symm h).symm
  · rw [removeNone_some _ ⟨a, h⟩]
    have h1 := congr_arg e.symm h
    rw [symm_apply_apply] at h1
    simp only [apply_eq_iff_eq, reduceCtorEq]
    simp [h1, apply_eq_iff_eq]

Equivalence between $\text{some } (\text{removeNone } e x) = e(\text{none})$ and $e^{-1}(\text{none}) = \text{some } x$

Informal description

For any element $x \in \alpha$ and equivalence $e : \text{Option } \alpha \simeq \text{Option } \beta$, the following are equivalent: 1. $\text{some } (\text{removeNone } e x) = e(\text{none})$ 2. The inverse equivalence $e^{-1}$ maps $\text{none}$ to $\text{some } x$ (i.e., $e^{-1}(\text{none}) = \text{some } x$).

Equiv.removeNone_optionCongr theorem

(e : α ≃ β) : removeNone e.optionCongr = e

Full source

@[simp]
theorem removeNone_optionCongr (e : α ≃ β) : removeNone e.optionCongr = e :=
  Equiv.ext fun x => Option.some_injective _ <| removeNone_some _ ⟨e x, by simp [EquivFunctor.map]⟩

Equivalence Preservation under Option Construction and Removal: $\text{removeNone}(e.\text{optionCongr}) = e$

Informal description

For any equivalence $e : \alpha \simeq \beta$, the equivalence obtained by removing the `none` cases from the option equivalence `e.optionCongr` is equal to $e$ itself. That is, $\text{removeNone}(e.\text{optionCongr}) = e$.

Equiv.optionCongr_injective theorem

: Function.Injective (optionCongr : α ≃ β → Option α ≃ Option β)

Full source

theorem optionCongr_injective : Function.Injective (optionCongr : α ≃ β → OptionOption α ≃ Option β) :=
  Function.LeftInverse.injective removeNone_optionCongr

Injectivity of Option Equivalence Construction: $\text{optionCongr}$ is injective

Informal description

The function $\text{optionCongr} : (\alpha \simeq \beta) \to (\text{Option } \alpha \simeq \text{Option } \beta)$ is injective. That is, for any two equivalences $e_1, e_2 : \alpha \simeq \beta$, if $\text{optionCongr } e_1 = \text{optionCongr } e_2$, then $e_1 = e_2$.

Equiv.optionSubtype definition

[DecidableEq β] (x : β) : { e : Option α ≃ β // e none = x } ≃ (α ≃ { y : β // y ≠ x })

Full source

/-- Equivalences between `Option α` and `β` that send `none` to `x` are equivalent to
equivalences between `α` and `{y : β // y ≠ x}`. -/
def optionSubtype [DecidableEq β] (x : β) :
    { e : Option α ≃ β // e none = x }{ e : Option α ≃ β // e none = x } ≃ (α ≃ { y : β // y ≠ x }) where
  toFun e :=
    { toFun := fun a =>
        ⟨(e : Option α ≃ β) a, ((EquivLike.injective _).ne_iff' e.property).2 (some_ne_none _)⟩,
      invFun := fun b =>
        get _
          (ne_none_iff_isSome.1
            (((EquivLike.injective _).ne_iff'
              ((apply_eq_iff_eq_symm_apply _).1 e.property).symm).2 b.property)),
      left_inv := fun a => by
        rw [← some_inj, some_get]
        exact symm_apply_apply (e : OptionOption α ≃ β) a,
      right_inv := fun b => by
        ext
        simp }
  invFun e :=
    ⟨{  toFun := fun a => casesOn' a x (Subtype.val ∘ e),
        invFun := fun b => if h : b = x then none else e.symm ⟨b, h⟩,
        left_inv := fun a => by
          cases a with
          | none => simp
          | some a =>
            simp only [casesOn'_some, Function.comp_apply, Subtype.coe_eta,
              symm_apply_apply, dite_eq_ite]
            exact if_neg (e a).property,
        right_inv := fun b => by
          by_cases h : b = x <;> simp [h] },
      rfl⟩
  left_inv e := by
    ext a
    cases a
    · simpa using e.property.symm
    · simp
  right_inv e := by
    ext a
    rfl

Equivalence between Option α ≃ β fixing none and α ≃ {y | y ≠ x}

Informal description

Given a type $\beta$ with decidable equality and an element $x \in \beta$, there is a natural equivalence between: 1. The type of equivalences $e : \text{Option } \alpha \simeq \beta$ that map $\text{none}$ to $x$, and 2. The type of equivalences $\alpha \simeq \{ y \in \beta \mid y \neq x \}$. The forward direction of this equivalence takes an equivalence $e : \text{Option } \alpha \simeq \beta$ with $e(\text{none}) = x$ and restricts it to $\alpha \to \{ y \in \beta \mid y \neq x \}$. The inverse direction constructs an equivalence $\text{Option } \alpha \simeq \beta$ from an equivalence $\alpha \simeq \{ y \in \beta \mid y \neq x \}$ by mapping $\text{none}$ to $x$ and using the given equivalence for the remaining elements.

Equiv.optionSubtype_apply_apply theorem

 [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x }) (a : α) (h) :
  optionSubtype x e a = ⟨(e : Option α ≃ β) a, h⟩

Full source

@[simp]
theorem optionSubtype_apply_apply
    [DecidableEq β] (x : β)
    (e : { e : Option α ≃ β // e none = x })
    (a : α)
    (h) : optionSubtype x e a = ⟨(e : Option α ≃ β) a, h⟩ := rfl

Application of `optionSubtype` Equivalence Preserves Mapping

Informal description

Given a type $\beta$ with decidable equality, an element $x \in \beta$, and an equivalence $e : \text{Option } \alpha \simeq \beta$ such that $e(\text{none}) = x$, then for any $a \in \alpha$ and any proof $h$ that $e(a) \neq x$, the application of the equivalence $\text{optionSubtype } x \ e$ to $a$ yields the pair $\langle e(a), h \rangle$.

Equiv.coe_optionSubtype_apply_apply theorem

 [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x }) (a : α) :
  ↑(optionSubtype x e a) = (e : Option α ≃ β) a

Full source

@[simp]
theorem coe_optionSubtype_apply_apply
    [DecidableEq β] (x : β)
    (e : { e : Option α ≃ β // e none = x })
    (a : α) : ↑(optionSubtype x e a) = (e : OptionOption α ≃ β) a := rfl

Coefficient of Option Subtype Application Equals Original Equivalence

Informal description

Given a type $\beta$ with decidable equality, an element $x \in \beta$, and an equivalence $e : \text{Option } \alpha \simeq \beta$ such that $e(\text{none}) = x$, then for any $a \in \alpha$, the underlying value of $\text{optionSubtype}(x, e)(a)$ is equal to $e(a)$.

Equiv.optionSubtype_apply_symm_apply theorem

 [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x }) (b : { y : β // y ≠ x }) :
  ↑((optionSubtype x e).symm b) = (e : Option α ≃ β).symm b

Full source

@[simp]
theorem optionSubtype_apply_symm_apply
    [DecidableEq β] (x : β)
    (e : { e : Option α ≃ β // e none = x })
    (b : { y : β // y ≠ x }) : ↑((optionSubtype x e).symm b) = (e : OptionOption α ≃ β).symm b := by
  dsimp only [optionSubtype]
  simp

Inverse Image Preservation in Option Subtype Equivalence

Informal description

Given a type $\beta$ with decidable equality, an element $x \in \beta$, and an equivalence $e : \text{Option } \alpha \simeq \beta$ satisfying $e(\text{none}) = x$, for any element $b \in \{ y \in \beta \mid y \neq x \}$, the underlying value of the inverse image of $b$ under the restricted equivalence $\text{optionSubtype}(x, e)^{-1}$ equals the inverse image of $b$ under $e$.

Equiv.optionSubtype_symm_apply_apply_coe theorem

 [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) (a : α) : ((optionSubtype x).symm e : Option α ≃ β) a = e a

Full source

@[simp]
theorem optionSubtype_symm_apply_apply_coe [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x })
    (a : α) : ((optionSubtype x).symm e : OptionOption α ≃ β) a = e a :=
  rfl

Equivalence Construction Preserves Mapping on $\alpha$ in Option Subtype Inverse

Informal description

Given a type $\beta$ with decidable equality, an element $x \in \beta$, and an equivalence $e : \alpha \simeq \{ y \in \beta \mid y \neq x \}$, the constructed equivalence $(\text{optionSubtype } x)^{-1} e : \text{Option } \alpha \simeq \beta$ satisfies $((\text{optionSubtype } x)^{-1} e)(a) = e(a)$ for any $a \in \alpha$.

Equiv.optionSubtype_symm_apply_apply_some theorem

 [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) (a : α) : ((optionSubtype x).symm e : Option α ≃ β) (some a) = e a

Full source

@[simp]
theorem optionSubtype_symm_apply_apply_some
    [DecidableEq β]
    (x : β)
    (e : α ≃ { y : β // y ≠ x })
    (a : α) : ((optionSubtype x).symm e : OptionOption α ≃ β) (some a) = e a :=
  rfl

Image of $\text{some } a$ under inverse of $\text{optionSubtype}$ equivalence equals $e(a)$

Informal description

Given a type $\beta$ with decidable equality, an element $x \in \beta$, and an equivalence $e : \alpha \simeq \{ y \in \beta \mid y \neq x \}$, the constructed equivalence $\text{Option } \alpha \simeq \beta$ maps $\text{some } a$ to $e(a)$ for any $a \in \alpha$. In other words, for any $a \in \alpha$, we have $((\text{optionSubtype } x)^{-1} e)(\text{some } a) = e(a)$.

Equiv.optionSubtype_symm_apply_apply_none theorem

[DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) : ((optionSubtype x).symm e : Option α ≃ β) none = x

Full source

@[simp]
theorem optionSubtype_symm_apply_apply_none
    [DecidableEq β]
    (x : β)
    (e : α ≃ { y : β // y ≠ x }) : ((optionSubtype x).symm e : OptionOption α ≃ β) none = x :=
  rfl

Inverse of `optionSubtype` maps `none` to specified element

Informal description

Given a type $\beta$ with decidable equality, an element $x \in \beta$, and an equivalence $e : \alpha \simeq \{ y \in \beta \mid y \neq x \}$, the inverse of the `optionSubtype` construction applied to $e$ maps $\text{none}$ to $x$. That is, $((\text{optionSubtype } x)^{-1} e) (\text{none}) = x$.

Equiv.optionSubtype_symm_apply_symm_apply theorem

 [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) (b : { y : β // y ≠ x }) :
  ((optionSubtype x).symm e : Option α ≃ β).symm b = e.symm b

Full source

@[simp]
theorem optionSubtype_symm_apply_symm_apply [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x })
    (b : { y : β // y ≠ x }) : ((optionSubtype x).symm e : OptionOption α ≃ β).symm b = e.symm b := by
  simp only [optionSubtype, coe_fn_symm_mk, Subtype.coe_mk,
             Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
  exact fun h => False.elim (b.property h)

Inverse of Option Subtype Equivalence Construction

Informal description

Given a type $\beta$ with decidable equality, an element $x \in \beta$, and an equivalence $e : \alpha \simeq \{ y \in \beta \mid y \neq x \}$, the inverse of the constructed equivalence $\text{Option } \alpha \simeq \beta$ (from `optionSubtype x`) satisfies the following property: for any $b \in \{ y \in \beta \mid y \neq x \}$, the inverse equivalence maps $b$ to $e^{-1}(b)$. In other words, if $E = (\text{optionSubtype } x)^{-1}(e) : \text{Option } \alpha \simeq \beta$, then $E^{-1}(b) = e^{-1}(b)$ for all $b \neq x$.

Equiv.optionSubtypeNe definition

(a : α) : Option { b // b ≠ a } ≃ α

Full source

/-- Any type with a distinguished element is equivalent to an `Option` type on the subtype excluding
that element. -/
@[simps!]
def optionSubtypeNe (a : α) : OptionOption {b // b ≠ a} ≃ α := optionSubtype a |>.symm (.refl _) |>.1

Equivalence between Option {b ≠ a} and α fixing none to a

Informal description

For any element $a$ in a type $\alpha$, there is a natural equivalence between the type $\text{Option } \{ b \in \alpha \mid b \neq a \}$ and $\alpha$ itself. This equivalence maps $\text{none}$ to $a$ and applies the identity function to all other elements.

Equiv.optionSubtypeNe_symm_self theorem

(a : α) : (optionSubtypeNe a).symm a = none

Full source

lemma optionSubtypeNe_symm_self (a : α) : (optionSubtypeNe a).symm a = none := by simp

Inverse of Option Subtype Equivalence Maps $a$ to None

Informal description

For any element $a$ in a type $\alpha$, the inverse of the equivalence $\text{optionSubtypeNe } a$ maps $a$ to $\text{none}$.

Equiv.optionSubtypeNe_symm_of_ne theorem

(hba : b ≠ a) : (optionSubtypeNe a).symm b = some ⟨b, hba⟩

Full source

lemma optionSubtypeNe_symm_of_ne (hba : b ≠ a) : (optionSubtypeNe a).symm b = some ⟨b, hba⟩ := by
  simp [hba]

Inverse of Option Subtype Equivalence for Non-Equal Elements

Informal description

For any element $b$ in a type $\alpha$ such that $b \neq a$, the inverse of the equivalence $\text{optionSubtypeNe } a$ maps $b$ to $\text{some } \langle b, hba \rangle$, where $hba$ is the proof that $b \neq a$.

Equiv.optionSubtypeNe_none theorem

(a : α) : optionSubtypeNe a none = a

Full source

@[simp] lemma optionSubtypeNe_none (a : α) : optionSubtypeNe a none = a := rfl

$\text{optionSubtypeNe}$ maps none to $a$

Informal description

For any element $a$ in a type $\alpha$, the equivalence $\text{optionSubtypeNe}$ maps $\text{none}$ to $a$, i.e., $\text{optionSubtypeNe}(a)(\text{none}) = a$.

Equiv.optionSubtypeNe_some theorem

(a : α) (b) : optionSubtypeNe a (some b) = b

Full source

@[simp] lemma optionSubtypeNe_some (a : α) (b) : optionSubtypeNe a (some b) = b := rfl

Mapping of `some` under Option-Subtype Equivalence

Informal description

For any element $a$ in a type $\alpha$ and any element $b$ of the subtype $\{b \in \alpha \mid b \neq a\}$, the equivalence `optionSubtypeNe a` maps `some b` to $b$ itself.

Equiv.optionEquivSumPUnit definition

(α : Type w) : Option α ≃ α ⊕ PUnit.{v + 1}

Full source

/-- `Option α` is equivalent to `α ⊕ PUnit` -/
def optionEquivSumPUnit.{v, w} (α : Type w) : OptionOption α ≃ α ⊕ PUnit.{v+1} :=
  ⟨fun o => o.elim (inr PUnit.unit) inl, fun s => s.elim some fun _ => none,
    fun o => by cases o <;> rfl,
    fun s => by rcases s with (_ | ⟨⟨⟩⟩) <;> rfl⟩

Equivalence between Option and Direct Sum with Unit

Informal description

The equivalence between `Option α` and the direct sum `α ⊕ PUnit` maps `none` to the right summand `PUnit.unit` and `some a` to the left summand `a`.

Equiv.optionEquivSumPUnit_none theorem

{α} : optionEquivSumPUnit α none = Sum.inr PUnit.unit

Full source

@[simp]
theorem optionEquivSumPUnit_none {α} : optionEquivSumPUnit α none = Sum.inr PUnit.unit :=
  rfl

Mapping of `none` under Option-Sum Equivalence

Informal description

For any type $\alpha$, the equivalence `optionEquivSumPUnit` maps the `none` value of `Option α` to the right summand `PUnit.unit` in the direct sum $\alpha \oplus \text{PUnit}$.

Equiv.optionEquivSumPUnit_some theorem

{α} (a) : optionEquivSumPUnit α (some a) = Sum.inl a

Full source

@[simp]
theorem optionEquivSumPUnit_some {α} (a) : optionEquivSumPUnit α (some a) = Sum.inl a :=
  rfl

Mapping of Some Element under Option-Sum Equivalence

Informal description

For any type $\alpha$ and element $a \in \alpha$, the equivalence $\text{optionEquivSumPUnit} \alpha$ maps the element $\text{some } a$ in $\text{Option } \alpha$ to the left summand $\text{Sum.inl}(a)$ in the direct sum $\alpha \oplus \text{PUnit}$.

Equiv.optionEquivSumPUnit_coe theorem

{α} (a : α) : optionEquivSumPUnit α a = Sum.inl a

Full source

@[simp]
theorem optionEquivSumPUnit_coe {α} (a : α) : optionEquivSumPUnit α a = Sum.inl a :=
  rfl

Mapping of Some Element under Option-Sum Equivalence

Informal description

For any type $\alpha$ and element $a \in \alpha$, the equivalence $\text{optionEquivSumPUnit} \alpha$ maps the element $a$ (viewed as $\text{some } a$ in $\text{Option } \alpha$) to the left summand $\text{Sum.inl}(a)$ in the direct sum $\alpha \oplus \text{PUnit}$.

Equiv.optionEquivSumPUnit_symm_inl theorem

{α} (a) : (optionEquivSumPUnit α).symm (Sum.inl a) = a

Full source

@[simp]
theorem optionEquivSumPUnit_symm_inl {α} (a) : (optionEquivSumPUnit α).symm (Sum.inl a) = a :=
  rfl

Inverse of Option-Sum Equivalence Maps Left Summand to Original Element

Informal description

For any type $\alpha$ and element $a \in \alpha$, the inverse of the equivalence $\text{optionEquivSumPUnit} \alpha$ maps the left summand $\text{Sum.inl}(a)$ back to $a$.

Equiv.optionEquivSumPUnit_symm_inr theorem

{α} (a) : (optionEquivSumPUnit α).symm (Sum.inr a) = none

Full source

@[simp]
theorem optionEquivSumPUnit_symm_inr {α} (a) : (optionEquivSumPUnit α).symm (Sum.inr a) = none :=
  rfl

Inverse of Option-Sum Equivalence Maps Right Summand to None

Informal description

For any type $\alpha$ and element $a$ of the unit type $\text{PUnit}$, the inverse of the equivalence $\text{optionEquivSumPUnit} \alpha$ maps the right summand $\text{Sum.inr}(a)$ to $\text{none}$.

Equiv.optionIsSomeEquiv definition

(α) : { x : Option α // x.isSome } ≃ α

Full source

/-- The set of `x : Option α` such that `isSome x` is equivalent to `α`. -/
@[simps]
def optionIsSomeEquiv (α) : { x : Option α // x.isSome }{ x : Option α // x.isSome } ≃ α where
  toFun o := Option.get _ o.2
  invFun x := ⟨some x, rfl⟩
  left_inv _ := Subtype.eq <| Option.some_get _
  right_inv _ := Option.get_some _ _

Equivalence between non-none options and the base type

Informal description

The equivalence between the subtype of `Option α` consisting of elements `x` such that `x.isSome` (i.e., elements of the form `some a`) and the type `α` itself. The forward direction maps `some a` to `a`, while the inverse direction maps `a` to `some a`.