Documentation

Mathlib.Logic.Equiv.Option

Equivalences for Option α #

We define

@[simp]
theorem Equiv.optionCongr_apply {α : Type u_1} {β : Type u_2} (e : α β) :
∀ (a : Option α), (Equiv.optionCongr e) a = Option.map (e) a
def Equiv.optionCongr {α : Type u_1} {β : Type u_2} (e : α β) :

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Equiv.optionCongr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
    @[simp]
    theorem Equiv.optionCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α β) (e₂ : β γ) :
    (Equiv.optionCongr e₁).trans (Equiv.optionCongr e₂) = Equiv.optionCongr (e₁.trans e₂)

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

    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
    Instances For
      theorem Equiv.removeNone_aux_some {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} (h : ∃ (x' : β), e (some x) = some x') :
      theorem Equiv.removeNone_aux_none {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} (h : e (some x) = none) :
      theorem Equiv.removeNone_aux_inv {α : Type u_1} {β : Type u_2} (e : Option α Option β) (x : α) :
      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.
      Instances For
        @[simp]
        theorem Equiv.removeNone_symm {α : Type u_1} {β : Type u_2} (e : Option α Option β) :
        theorem Equiv.removeNone_some {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} (h : ∃ (x' : β), e (some x) = some x') :
        some ((Equiv.removeNone e) x) = e (some x)
        theorem Equiv.removeNone_none {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} (h : e (some x) = none) :
        some ((Equiv.removeNone e) x) = e none
        @[simp]
        theorem Equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : Option α Option β) :
        e.symm none = none e none = none
        theorem Equiv.some_removeNone_iff {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} :
        some ((Equiv.removeNone e) x) = e none e.symm none = some x
        @[simp]
        theorem Equiv.removeNone_optionCongr {α : Type u_1} {β : Type u_2} (e : α β) :
        theorem Equiv.optionCongr_injective {α : Type u_1} {β : Type u_2} :
        Function.Injective Equiv.optionCongr
        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
          @[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) :
          ((Equiv.optionSubtype x) e) a = { val := e (some a), property := h }
          @[simp]
          theorem Equiv.coe_optionSubtype_apply_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : { e : Option α β // e none = x }) (a : α) :
          (((Equiv.optionSubtype x) e) a) = e (some a)
          @[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 (((Equiv.optionSubtype x) e).symm b) = (e).symm b
          @[simp]
          theorem Equiv.optionSubtype_symm_apply_apply_coe {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α { y : β // y x }) (a : α) :
          ((Equiv.optionSubtype x).symm e) (some a) = (e a)
          @[simp]
          theorem Equiv.optionSubtype_symm_apply_apply_some {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α { y : β // y x }) (a : α) :
          ((Equiv.optionSubtype x).symm e) (some a) = (e a)
          @[simp]
          theorem Equiv.optionSubtype_symm_apply_apply_none {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α { y : β // y x }) :
          ((Equiv.optionSubtype x).symm e) none = x
          @[simp]
          theorem Equiv.optionSubtype_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [DecidableEq β] (x : β) (e : α { y : β // y x }) (b : { y : β // y x }) :
          (((Equiv.optionSubtype x).symm e)).symm b = some (e.symm b)