Equivalences for `Option α` #

We define

Equiv.optionCongr: the Option α ≃ Option β constructed from e : α ≃ β by sending none to none, and applying e elsewhere.
Equiv.removeNone: the α ≃ β constructed from Option α ≃ Option β by removing none from both sides.

source

def Equiv.optionCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

Option α ≃ Option β

A universe-polymorphic version of EquivFunctor.mapEquiv Option e.

Equations

e.optionCongr = { toFun := Option.map ⇑e, invFun := Option.map ⇑e.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem Equiv.optionCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (a✝ : Option α) :

e.optionCongr a✝ = Option.map (⇑e) a✝

source

@[simp]

theorem Equiv.optionCongr_refl {α : Type u_1} :

(Equiv.refl α).optionCongr = Equiv.refl (Option α)

source

@[simp]

theorem Equiv.optionCongr_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

e.symm.optionCongr = e.optionCongr.symm

source

@[simp]

theorem Equiv.optionCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α ≃ β) (e₂ : β ≃ γ) :

(e₁.trans e₂).optionCongr = e₁.optionCongr.trans e₂.optionCongr

source

theorem Equiv.optionCongr_eq_equivFunctor_mapEquiv {α β : Type u} (e : α ≃ β) :

e.optionCongr = EquivFunctor.mapEquiv Option e

When α and β are in the same universe, this is the same as the result of EquivFunctor.mapEquiv.

source

def Equiv.removeNoneAux {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) (x : α) :

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

Equations

e.removeNoneAux x = if h : (e (some x)).isSome = true then (e (some x)).get h else (e none).get ⋯

Instances For

source

theorem Equiv.removeNoneAux_some {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α} (h : ∃ (x' : β), e (some x) = some x') :

some (e.removeNoneAux x) = e (some x)

source

theorem Equiv.removeNoneAux_none {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α} (h : e (some x) = none) :

some (e.removeNoneAux x) = e none

source

theorem Equiv.removeNoneAux_inv {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) (x : α) :

e.symm.removeNoneAux (e.removeNoneAux x) = x

source

@[deprecated Equiv.removeNoneAux (since := "2026-06-06")]

def Equiv.removeNone_aux {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) (x : α) :

Alias of Equiv.removeNoneAux.

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

Equations

@Equiv.removeNone_aux = @Equiv.removeNoneAux

Instances For

source

@[deprecated Equiv.removeNoneAux_none (since := "2026-06-06")]

theorem Equiv.removeNone_aux_none {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α} (h : e (some x) = none) :

some (e.removeNoneAux x) = e none

Alias of Equiv.removeNoneAux_none.

source

@[deprecated Equiv.removeNoneAux_some (since := "2026-06-06")]

theorem Equiv.removeNone_aux_some {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α} (h : ∃ (x' : β), e (some x) = some x') :

some (e.removeNoneAux x) = e (some x)

Alias of Equiv.removeNoneAux_some.

source

@[deprecated Equiv.removeNoneAux_inv (since := "2026-06-06")]

theorem Equiv.removeNone_aux_inv {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) (x : α) :

e.symm.removeNoneAux (e.removeNoneAux x) = x

Alias of Equiv.removeNoneAux_inv.

source

def Equiv.removeNone {α : 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

e.removeNone = { toFun := e.removeNoneAux, invFun := e.symm.removeNoneAux, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem Equiv.removeNone_symm {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) :

e.removeNone.symm = e.symm.removeNone

source

theorem Equiv.removeNone_some {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α} (h : ∃ (x' : β), e (some x) = some x') :

some (e.removeNone x) = e (some x)

source

theorem Equiv.removeNone_none {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α} (h : e (some x) = none) :

some (e.removeNone x) = e none

source

@[simp]

theorem Equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) :

e.symm none = none ↔ e none = none

source

theorem Equiv.some_removeNone_iff {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α} :

some (e.removeNone x) = e none ↔ e.symm none = some x

source

@[simp]

theorem Equiv.removeNone_optionCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

e.optionCongr.removeNone = e

source

theorem Equiv.optionCongr_injective {α : Type u_1} {β : Type u_2} :

Function.Injective optionCongr

source

def Equiv.optionSubtype {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) :

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

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Equiv.optionSubtype_apply_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x }) (a : α) (h : ↑e (some a) ≠ x) :

((optionSubtype x) e) a = ⟨↑e (some a), h⟩

source

@[simp]

theorem Equiv.coe_optionSubtype_apply_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x }) (a : α) :

↑(((optionSubtype x) e) a) = ↑e (some a)

source

@[simp]

theorem Equiv.optionSubtype_apply_symm_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : { e : Option α ≃ β // e none = x }) (b : { y : β // y ≠ x }) :

some (((optionSubtype x) e).symm b) = (↑e).symm ↑b

source

@[simp]

theorem Equiv.optionSubtype_symm_apply_apply_coe {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) (a : α) :

↑((optionSubtype x).symm e) (some a) = ↑(e a)

source

@[simp]

theorem Equiv.optionSubtype_symm_apply_apply_some {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) (a : α) :

↑((optionSubtype x).symm e) (some a) = ↑(e a)

source

@[simp]

theorem Equiv.optionSubtype_symm_apply_apply_none {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) :

↑((optionSubtype x).symm e) none = x

source

@[simp]

theorem Equiv.optionSubtype_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α ≃ { y : β // y ≠ x }) (b : { y : β // y ≠ x }) :

(↑((optionSubtype x).symm e)).symm ↑b = some (e.symm b)

source

def Equiv.optionSubtypeNe {α : Type u_1} [DecidableEq α] (a : α) :

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

Any type with a distinguished element is equivalent to an Option type on the subtype excluding that element.

Equations

Equiv.optionSubtypeNe a = ↑((Equiv.optionSubtype a).symm (Equiv.refl { y : α // y ≠ a }))

Instances For

source

@[simp]

theorem Equiv.optionSubtypeNe_symm_apply {α : Type u_1} [DecidableEq α] (a b : α) :

(optionSubtypeNe a).symm b = if h : b = a then none else some ⟨b, h⟩

source

@[simp]

theorem Equiv.optionSubtypeNe_apply {α : Type u_1} [DecidableEq α] (a : α) (a✝ : Option { y : α // y ≠ a }) :

(optionSubtypeNe a) a✝ = a✝.casesOn' a Subtype.val

source

theorem Equiv.optionSubtypeNe_symm_self {α : Type u_1} [DecidableEq α] (a : α) :

(optionSubtypeNe a).symm a = none

source

theorem Equiv.optionSubtypeNe_symm_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (hba : b ≠ a) :

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

source

@[simp]

theorem Equiv.optionSubtypeNe_none {α : Type u_1} [DecidableEq α] (a : α) :

(optionSubtypeNe a) none = a

source

@[simp]

theorem Equiv.optionSubtypeNe_some {α : Type u_1} [DecidableEq α] (a : α) (b : { b : α // b ≠ a }) :

(optionSubtypeNe a) (some b) = ↑b

source

def Equiv.optionEquivSumPUnit (α : Type w) :

Option α ≃ α ⊕ PUnit

Option α is equivalent to α ⊕ PUnit

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Equiv.optionEquivSumPUnit_none {α : Type u_4} :

(optionEquivSumPUnit α) none = Sum.inr PUnit.unit

source

@[simp]

theorem Equiv.optionEquivSumPUnit_some {α : Type u_4} (a : α) :

(optionEquivSumPUnit α) (some a) = Sum.inl a

source

@[simp]

theorem Equiv.optionEquivSumPUnit_coe {α : Type u_4} (a : α) :

(optionEquivSumPUnit α) (some a) = Sum.inl a

source

@[simp]

theorem Equiv.optionEquivSumPUnit_symm_inl {α : Type u_4} (a : α) :

(optionEquivSumPUnit α).symm (Sum.inl a) = some a

source

@[simp]

theorem Equiv.optionEquivSumPUnit_symm_inr {α : Type u_4} (a : PUnit) :

(optionEquivSumPUnit α).symm (Sum.inr a) = none

source

def Equiv.optionIsSomeEquiv (α : Type u_4) :

{ x : Option α // x.isSome = true } ≃ α

The set of x : Option α such that isSome x is equivalent to α.

Equations

Equiv.optionIsSomeEquiv α = { toFun := fun (o : { x : Option α // x.isSome = true }) => (↑o).get ⋯, invFun := fun (x : α) => ⟨some x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem Equiv.optionIsSomeEquiv_symm_apply_coe (α : Type u_4) (x : α) :

↑((optionIsSomeEquiv α).symm x) = some x

source

@[simp]

theorem Equiv.optionIsSomeEquiv_apply (α : Type u_4) (o : { x : Option α // x.isSome = true }) :

(optionIsSomeEquiv α) o = (↑o).get ⋯

Documentation

Mathlib.Logic.Equiv.Option

Equivalences for `Option α` #

Equivalences for Option α #

Equivalences for `Option α` #