Documentation

Mathlib.Logic.Equiv.Option

Equivalences for Option α #

We define

@[simp]
theorem Equiv.optionCongr_apply {α : Type u_1} {β : Type u_2} (e : α β) :
∀ (a : Option α), e.optionCongr 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
  • e.optionCongr = { toFun := Option.map e, invFun := Option.map e.symm, left_inv := , right_inv := }
Instances For
    @[simp]
    theorem Equiv.optionCongr_refl {α : Type u_1} :
    (Equiv.refl α).optionCongr = Equiv.refl (Option α)
    @[simp]
    theorem Equiv.optionCongr_symm {α : Type u_1} {β : Type u_2} (e : α β) :
    e.optionCongr.symm = e.symm.optionCongr
    @[simp]
    theorem Equiv.optionCongr_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e₁ : α β) (e₂ : β γ) :
    e₁.optionCongr.trans e₂.optionCongr = (e₁.trans e₂).optionCongr
    theorem Equiv.optionCongr_eq_equivFunctor_mapEquiv {α : Type u} {β : Type u} (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
    • e.removeNone_aux x = if h : (e (some x)).isSome = true then (e (some x)).get h else (e none).get
    Instances For
      theorem Equiv.removeNone_aux_some {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} (h : ∃ (x' : β), e (some x) = some x') :
      some (e.removeNone_aux x) = e (some x)
      theorem Equiv.removeNone_aux_none {α : Type u_1} {β : Type u_2} (e : Option α Option β) {x : α} (h : e (some x) = none) :
      some (e.removeNone_aux x) = e none
      theorem Equiv.removeNone_aux_inv {α : Type u_1} {β : Type u_2} (e : Option α Option β) (x : α) :
      e.symm.removeNone_aux (e.removeNone_aux x) = 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
      • e.removeNone = { toFun := e.removeNone_aux, invFun := e.symm.removeNone_aux, left_inv := , right_inv := }
      Instances For
        @[simp]
        theorem Equiv.removeNone_symm {α : Type u_1} {β : Type u_2} (e : Option α Option β) :
        e.removeNone.symm = e.symm.removeNone
        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) :
        some (e.removeNone 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 (e.removeNone x) = e none e.symm none = some x
        @[simp]
        theorem Equiv.removeNone_optionCongr {α : Type u_1} {β : Type u_2} (e : α β) :
        e.optionCongr.removeNone = 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 = 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 : α) :
          (((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)
          @[simp]
          theorem Equiv.optionSubtypeNe_symm_apply {α : Type u_1} [DecidableEq α] (a : α) (b : α) :
          (Equiv.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✝ }) :
          (Equiv.optionSubtypeNe a✝) a = a.casesOn' a✝ Subtype.val
          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
            theorem Equiv.optionSubtypeNe_symm_self {α : Type u_1} [DecidableEq α] (a : α) :
            (Equiv.optionSubtypeNe a).symm a = none
            theorem Equiv.optionSubtypeNe_symm_of_ne {α : Type u_1} [DecidableEq α] {a : α} {b : α} (hba : b a) :
            (Equiv.optionSubtypeNe a).symm b = some b, hba
            @[simp]
            theorem Equiv.optionSubtypeNe_none {α : Type u_1} [DecidableEq α] (a : α) :
            @[simp]
            theorem Equiv.optionSubtypeNe_some {α : Type u_1} [DecidableEq α] (a : α) (b : { b : α // b a }) :