Equivalences for Option α

We define

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

ink

@[simp]

theorem Equiv.optionCongr_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) : ∀ (a : Option α), ↑(Equiv.optionCongr e) a = Option.map (↑e) a

ink

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

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

Equations

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

ink

@[simp]

theorem Equiv.optionCongr_refl {α : Type u_1} : Equiv.optionCongr (Equiv.refl α) = Equiv.refl (Option α)

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Equiv.optionCongr_eq_equivFunctor_mapEquiv {α : Type u_1} {β : Type u_1} (e : α ≃ β) : Equiv.optionCongr e = EquivFunctor.mapEquiv Option e

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

ink

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

• Equiv.removeNone_aux e x = if h : Option.isSome (↑e (some x)) = true then Option.get (↑e (some x)) h else Option.get (↑e none) (_ : Option.isSome (↑e none) = true)

ink

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

ink

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

ink

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

ink

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

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

theorem Equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) : ↑(Equiv.symm e) none = none ↔ ↑e none = none

ink

theorem Equiv.some_removeNone_iff {α : Type u_2} {β : Type u_1} (e : Option α ≃ Option β) {x : α} : some (↑(Equiv.removeNone e) x) = ↑e none ↔ ↑(Equiv.symm e) none = some x

ink

@[simp]

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

ink

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

ink

def Equiv.optionSubtype {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (x : β) : { e // ↑e none = x } ≃ (α ≃ { y // y ≠ x })

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

Equations

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

ink

@[simp]

theorem Equiv.optionSubtype_apply_apply {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : { e // ↑e none = x }) (a : α) (h : ↑↑e (some a) ≠ x) : ↑(↑(Equiv.optionSubtype x) e) a = { val := ↑↑e (some a), property := h }

ink

@[simp]

theorem Equiv.coe_optionSubtype_apply_apply {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : { e // ↑e none = x }) (a : α) : ↑(↑(↑(Equiv.optionSubtype x) e) a) = ↑↑e (some a)

ink

@[simp]

theorem Equiv.optionSubtype_apply_symm_apply {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : { e // ↑e none = x }) (b : { y // y ≠ x }) : some (↑(Equiv.symm (↑(Equiv.optionSubtype x) e)) b) = ↑(Equiv.symm ↑e) ↑b

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem Equiv.optionSubtype_symm_apply_apply_none {α : Type u_2} {β : Type u_1} [inst : DecidableEq β] (x : β) (e : α ≃ { y // y ≠ x }) : ↑↑(↑(Equiv.symm (Equiv.optionSubtype x)) e) none = x

ink

@[simp]

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