Documentation

Mathlib.Logic.Equiv.Option

Equivalences for Option α #

We define

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

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

Equations
    Instances For
      @[simp]
      theorem Equiv.optionCongr_apply {α : Type u_1} {β : Type u_2} (e : α β) (a✝ : Option α) :
      e.optionCongr a✝ = Option.map (⇑e) a✝
      @[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₂ : β γ) :

      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
            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 (e.removeNone x) = e (some x)
              theorem Equiv.removeNone_none {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} (h : e (some x) = none) :
              @[simp]
              theorem Equiv.option_symm_apply_none_iff {α : Type u_1} {β : Type u_2} (e : Option α Option β) :
              theorem Equiv.some_removeNone_iff {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} :
              @[simp]
              theorem Equiv.removeNone_optionCongr {α : Type u_1} {β : Type u_2} (e : α β) :
              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
                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) :
                  ((optionSubtype x) e) a = e (some a), h
                  @[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)
                  @[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
                  @[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)
                  @[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)
                  @[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
                  @[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)
                  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
                    Instances For
                      @[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
                      @[simp]
                      theorem Equiv.optionSubtypeNe_apply {α : Type u_1} [DecidableEq α] (a : α) (a✝ : Option { y : α // y a }) :
                      theorem Equiv.optionSubtypeNe_symm_of_ne {α : Type u_1} [DecidableEq α] {a b : α} (hba : b a) :
                      @[simp]
                      theorem Equiv.optionSubtypeNe_none {α : Type u_1} [DecidableEq α] (a : α) :
                      @[simp]
                      theorem Equiv.optionSubtypeNe_some {α : Type u_1} [DecidableEq α] (a : α) (b : { b : α // b a }) :
                      (optionSubtypeNe a) (some b) = b

                      Option α is equivalent to α ⊕ PUnit

                      Equations
                        Instances For
                          @[simp]
                          theorem Equiv.optionEquivSumPUnit_some {α : Type u_4} (a : α) :
                          @[simp]
                          theorem Equiv.optionEquivSumPUnit_coe {α : Type u_4} (a : α) :
                          @[simp]
                          def Equiv.optionIsSomeEquiv (α : Type u_4) :
                          { x : Option α // x.isSome = true } α

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

                          Equations
                            Instances For
                              @[simp]
                              theorem Equiv.optionIsSomeEquiv_symm_apply_coe (α : Type u_4) (x : α) :
                              @[simp]
                              theorem Equiv.optionIsSomeEquiv_apply (α : Type u_4) (o : { x : Option α // x.isSome = true }) :
                              (optionIsSomeEquiv α) o = (↑o).get