Documentation

Mathlib.Data.Sum.Order

Orders on a sum type #

This file defines the disjoint sum and the linear (aka lexicographic) sum of two orders and provides relation instances for Sum.LiftRel and Sum.Lex.

We declare the disjoint sum of orders as the default set of instances. The linear order goes on a type synonym.

Main declarations #

Notation #

Unbundled relation classes #

theorem Sum.LiftRel.refl {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsRefl α r] [IsRefl β s] (x : α β) :
Sum.LiftRel r s x x
instance Sum.instIsReflLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsRefl α r] [IsRefl β s] :
IsRefl (α β) (Sum.LiftRel r s)
Equations
  • =
instance Sum.instIsIrreflLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsIrrefl α r] [IsIrrefl β s] :
IsIrrefl (α β) (Sum.LiftRel r s)
Equations
  • =
theorem Sum.LiftRel.trans {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrans α r] [IsTrans β s] {a : α β} {b : α β} {c : α β} :
Sum.LiftRel r s a bSum.LiftRel r s b cSum.LiftRel r s a c
instance Sum.instIsTransLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrans α r] [IsTrans β s] :
IsTrans (α β) (Sum.LiftRel r s)
Equations
  • =
instance Sum.instIsAntisymmLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsAntisymm α r] [IsAntisymm β s] :
IsAntisymm (α β) (Sum.LiftRel r s)
Equations
  • =
instance Sum.instIsReflLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsRefl α r] [IsRefl β s] :
IsRefl (α β) (Sum.Lex r s)
Equations
  • =
instance Sum.instIsIrreflLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsIrrefl α r] [IsIrrefl β s] :
IsIrrefl (α β) (Sum.Lex r s)
Equations
  • =
instance Sum.instIsTransLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrans α r] [IsTrans β s] :
IsTrans (α β) (Sum.Lex r s)
Equations
  • =
instance Sum.instIsAntisymmLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsAntisymm α r] [IsAntisymm β s] :
IsAntisymm (α β) (Sum.Lex r s)
Equations
  • =
instance Sum.instIsTotalLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTotal α r] [IsTotal β s] :
IsTotal (α β) (Sum.Lex r s)
Equations
  • =
instance Sum.instIsTrichotomousLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrichotomous α r] [IsTrichotomous β s] :
IsTrichotomous (α β) (Sum.Lex r s)
Equations
  • =
instance Sum.instIsWellOrderLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsWellOrder α r] [IsWellOrder β s] :
IsWellOrder (α β) (Sum.Lex r s)
Equations
  • =

Disjoint sum of two orders #

instance Sum.instLESum {α : Type u_1} {β : Type u_2} [LE α] [LE β] :
LE (α β)
Equations
  • Sum.instLESum = { le := Sum.LiftRel (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : β) => x1 x2 }
instance Sum.instLTSum {α : Type u_1} {β : Type u_2} [LT α] [LT β] :
LT (α β)
Equations
  • Sum.instLTSum = { lt := Sum.LiftRel (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2 }
theorem Sum.le_def {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α β} {b : α β} :
a b Sum.LiftRel (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) a b
theorem Sum.lt_def {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α β} {b : α β} :
a < b Sum.LiftRel (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : β) => x1 < x2) a b
@[simp]
theorem Sum.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : α} :
@[simp]
theorem Sum.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : β} {b : β} :
@[simp]
theorem Sum.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : α} :
@[simp]
theorem Sum.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : β} {b : β} :
@[simp]
theorem Sum.not_inl_le_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : β} :
@[simp]
theorem Sum.not_inl_lt_inr {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : β} :
@[simp]
theorem Sum.not_inr_le_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : β} :
@[simp]
theorem Sum.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : β} :
instance Sum.instPreorderSum {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
Preorder (α β)
Equations
theorem Sum.inl_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
Monotone Sum.inl
theorem Sum.inr_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
Monotone Sum.inr
theorem Sum.inl_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
StrictMono Sum.inl
theorem Sum.inr_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
StrictMono Sum.inr
instance Sum.instPartialOrder {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] :
Equations
instance Sum.noMinOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMinOrder α] [NoMinOrder β] :
NoMinOrder (α β)
Equations
  • =
instance Sum.noMaxOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder α] [NoMaxOrder β] :
NoMaxOrder (α β)
Equations
  • =
@[simp]
theorem Sum.noMinOrder_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] :
@[simp]
theorem Sum.noMaxOrder_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] :
instance Sum.denselyOrdered {α : Type u_1} {β : Type u_2} [LT α] [LT β] [DenselyOrdered α] [DenselyOrdered β] :
Equations
  • =
@[simp]
theorem Sum.denselyOrdered_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] :
@[simp]
theorem Sum.swap_le_swap_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α β} {b : α β} :
a.swap b.swap a b
@[simp]
theorem Sum.swap_lt_swap_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α β} {b : α β} :
a.swap < b.swap a < b

Linear sum of two orders #

The linear sum of two orders

Equations
Instances For
    @[reducible, match_pattern, inline]
    abbrev Sum.inlₗ {α : Type u_1} {β : Type u_2} (x : α) :
    Lex (α β)

    Lexicographical Sum.inl. Only used for pattern matching.

    Equations
    Instances For
      @[reducible, match_pattern, inline]
      abbrev Sum.inrₗ {α : Type u_1} {β : Type u_2} (x : β) :
      Lex (α β)

      Lexicographical Sum.inr. Only used for pattern matching.

      Equations
      Instances For
        instance Sum.Lex.LE {α : Type u_1} {β : Type u_2} [LE α] [LE β] :
        LE (Lex (α β))

        The linear/lexicographical on a sum.

        Equations
        • Sum.Lex.LE = { le := Sum.Lex (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : β) => x1 x2 }
        instance Sum.Lex.LT {α : Type u_1} {β : Type u_2} [LT α] [LT β] :
        LT (Lex (α β))

        The linear/lexicographical < on a sum.

        Equations
        • Sum.Lex.LT = { lt := Sum.Lex (fun (x1 x2 : α) => x1 < x2) fun (x1 x2 : β) => x1 < x2 }
        @[simp]
        theorem Sum.Lex.toLex_le_toLex {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α β} {b : α β} :
        toLex a toLex b Sum.Lex (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) a b
        @[simp]
        theorem Sum.Lex.toLex_lt_toLex {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α β} {b : α β} :
        toLex a < toLex b Sum.Lex (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : β) => x1 < x2) a b
        theorem Sum.Lex.le_def {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : Lex (α β)} {b : Lex (α β)} :
        a b Sum.Lex (fun (x1 x2 : α) => x1 x2) (fun (x1 x2 : β) => x1 x2) (ofLex a) (ofLex b)
        theorem Sum.Lex.lt_def {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : Lex (α β)} {b : Lex (α β)} :
        a < b Sum.Lex (fun (x1 x2 : α) => x1 < x2) (fun (x1 x2 : β) => x1 < x2) (ofLex a) (ofLex b)
        theorem Sum.Lex.inl_le_inl_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : α} :
        toLex (Sum.inl a) toLex (Sum.inl b) a b
        theorem Sum.Lex.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : β} {b : β} :
        toLex (Sum.inr a) toLex (Sum.inr b) a b
        theorem Sum.Lex.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : α} :
        toLex (Sum.inl a) < toLex (Sum.inl b) a < b
        theorem Sum.Lex.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : β} {b : β} :
        toLex (Sum.inr a) < toLex (Sum.inr b) a < b
        theorem Sum.Lex.inl_le_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) (b : β) :
        toLex (Sum.inl a) toLex (Sum.inr b)
        theorem Sum.Lex.inl_lt_inr {α : Type u_1} {β : Type u_2} [LT α] [LT β] (a : α) (b : β) :
        toLex (Sum.inl a) < toLex (Sum.inr b)
        theorem Sum.Lex.not_inr_le_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : β} :
        ¬toLex (Sum.inr b) toLex (Sum.inl a)
        theorem Sum.Lex.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : β} :
        ¬toLex (Sum.inr b) < toLex (Sum.inl a)
        instance Sum.Lex.preorder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        Preorder (Lex (α β))
        Equations
        theorem Sum.Lex.toLex_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        Monotone toLex
        theorem Sum.Lex.toLex_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        StrictMono toLex
        theorem Sum.Lex.inl_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        Monotone (toLex Sum.inl)
        theorem Sum.Lex.inr_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        Monotone (toLex Sum.inr)
        theorem Sum.Lex.inl_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        StrictMono (toLex Sum.inl)
        theorem Sum.Lex.inr_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        StrictMono (toLex Sum.inr)
        instance Sum.Lex.partialOrder {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] :
        PartialOrder (Lex (α β))
        Equations
        instance Sum.Lex.linearOrder {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] :
        LinearOrder (Lex (α β))
        Equations
        • Sum.Lex.linearOrder = LinearOrder.mk Sum.instDecidableRelSumLex instDecidableEqSum decidableLTOfDecidableLE
        instance Sum.Lex.orderBot {α : Type u_1} {β : Type u_2} [LE α] [OrderBot α] [LE β] :
        OrderBot (Lex (α β))

        The lexicographical bottom of a sum is the bottom of the left component.

        Equations
        @[simp]
        theorem Sum.Lex.inl_bot {α : Type u_1} {β : Type u_2} [LE α] [OrderBot α] [LE β] :
        toLex (Sum.inl ) =
        instance Sum.Lex.orderTop {α : Type u_1} {β : Type u_2} [LE α] [LE β] [OrderTop β] :
        OrderTop (Lex (α β))

        The lexicographical top of a sum is the top of the right component.

        Equations
        @[simp]
        theorem Sum.Lex.inr_top {α : Type u_1} {β : Type u_2} [LE α] [LE β] [OrderTop β] :
        toLex (Sum.inr ) =
        instance Sum.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [LE α] [LE β] [OrderBot α] [OrderTop β] :
        BoundedOrder (Lex (α β))
        Equations
        • Sum.Lex.boundedOrder = BoundedOrder.mk
        instance Sum.Lex.noMinOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMinOrder α] [NoMinOrder β] :
        NoMinOrder (Lex (α β))
        Equations
        • =
        instance Sum.Lex.noMaxOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder α] [NoMaxOrder β] :
        NoMaxOrder (Lex (α β))
        Equations
        • =
        instance Sum.Lex.noMinOrder_of_nonempty {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMinOrder α] [Nonempty α] :
        NoMinOrder (Lex (α β))
        Equations
        • =
        instance Sum.Lex.noMaxOrder_of_nonempty {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder β] [Nonempty β] :
        NoMaxOrder (Lex (α β))
        Equations
        • =
        instance Sum.Lex.denselyOrdered_of_noMaxOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [DenselyOrdered α] [DenselyOrdered β] [NoMaxOrder α] :
        Equations
        • =
        instance Sum.Lex.denselyOrdered_of_noMinOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [DenselyOrdered α] [DenselyOrdered β] [NoMinOrder β] :
        Equations
        • =

        Order isomorphisms #

        @[simp]
        theorem OrderIso.sumComm_apply (α : Type u_4) (β : Type u_5) [LE α] [LE β] :
        ∀ (a : α β), (OrderIso.sumComm α β) a = a.swap
        def OrderIso.sumComm (α : Type u_4) (β : Type u_5) [LE α] [LE β] :
        α β ≃o β α

        Equiv.sumComm promoted to an order isomorphism.

        Equations
        Instances For
          @[simp]
          theorem OrderIso.sumComm_symm (α : Type u_4) (β : Type u_5) [LE α] [LE β] :
          def OrderIso.sumAssoc (α : Type u_4) (β : Type u_5) (γ : Type u_6) [LE α] [LE β] [LE γ] :
          (α β) γ ≃o α β γ

          Equiv.sumAssoc promoted to an order isomorphism.

          Equations
          Instances For
            @[simp]
            theorem OrderIso.sumAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) :
            @[simp]
            theorem OrderIso.sumAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) :
            @[simp]
            theorem OrderIso.sumAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) :
            @[simp]
            theorem OrderIso.sumAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) :
            (OrderIso.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
            @[simp]
            theorem OrderIso.sumAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) :
            (OrderIso.sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
            @[simp]
            theorem OrderIso.sumAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) :
            (OrderIso.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
            def OrderIso.sumDualDistrib (α : Type u_4) (β : Type u_5) [LE α] [LE β] :

            orderDual is distributive over up to an order isomorphism.

            Equations
            Instances For
              @[simp]
              theorem OrderIso.sumDualDistrib_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) :
              (OrderIso.sumDualDistrib α β) (OrderDual.toDual (Sum.inl a)) = Sum.inl (OrderDual.toDual a)
              @[simp]
              theorem OrderIso.sumDualDistrib_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) :
              (OrderIso.sumDualDistrib α β) (OrderDual.toDual (Sum.inr b)) = Sum.inr (OrderDual.toDual b)
              @[simp]
              theorem OrderIso.sumDualDistrib_symm_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) :
              (OrderIso.sumDualDistrib α β).symm (Sum.inl (OrderDual.toDual a)) = OrderDual.toDual (Sum.inl a)
              @[simp]
              theorem OrderIso.sumDualDistrib_symm_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) :
              (OrderIso.sumDualDistrib α β).symm (Sum.inr (OrderDual.toDual b)) = OrderDual.toDual (Sum.inr b)
              def OrderIso.sumLexAssoc (α : Type u_4) (β : Type u_5) (γ : Type u_6) [LE α] [LE β] [LE γ] :
              Lex (Lex (α β) γ) ≃o Lex (α Lex (β γ))

              Equiv.SumAssoc promoted to an order isomorphism.

              Equations
              Instances For
                @[simp]
                theorem OrderIso.sumLexAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) :
                (OrderIso.sumLexAssoc α β γ) (toLex (Sum.inl (toLex (Sum.inl a)))) = toLex (Sum.inl a)
                @[simp]
                theorem OrderIso.sumLexAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) :
                (OrderIso.sumLexAssoc α β γ) (toLex (Sum.inl (toLex (Sum.inr b)))) = toLex (Sum.inr (toLex (Sum.inl b)))
                @[simp]
                theorem OrderIso.sumLexAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) :
                (OrderIso.sumLexAssoc α β γ) (toLex (Sum.inr c)) = toLex (Sum.inr (toLex (Sum.inr c)))
                @[simp]
                theorem OrderIso.sumLexAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) :
                (OrderIso.sumLexAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
                @[simp]
                theorem OrderIso.sumLexAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) :
                @[simp]
                theorem OrderIso.sumLexAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) :
                (OrderIso.sumLexAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
                def OrderIso.sumLexDualAntidistrib (α : Type u_4) (β : Type u_5) [LE α] [LE β] :

                OrderDual is antidistributive over ⊕ₗ up to an order isomorphism.

                Equations
                Instances For
                  @[simp]
                  theorem OrderIso.sumLexDualAntidistrib_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) :
                  (OrderIso.sumLexDualAntidistrib α β) (OrderDual.toDual (Sum.inl a)) = Sum.inr (OrderDual.toDual a)
                  @[simp]
                  theorem OrderIso.sumLexDualAntidistrib_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) :
                  (OrderIso.sumLexDualAntidistrib α β) (OrderDual.toDual (Sum.inr b)) = Sum.inl (OrderDual.toDual b)
                  @[simp]
                  theorem OrderIso.sumLexDualAntidistrib_symm_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) :
                  (OrderIso.sumLexDualAntidistrib α β).symm (Sum.inl (OrderDual.toDual b)) = OrderDual.toDual (Sum.inr b)
                  @[simp]
                  theorem OrderIso.sumLexDualAntidistrib_symm_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) :
                  (OrderIso.sumLexDualAntidistrib α β).symm (Sum.inr (OrderDual.toDual a)) = OrderDual.toDual (Sum.inl a)

                  WithBot α is order-isomorphic to PUnit ⊕ₗ α, by sending to Unit and ↑a to a.

                  Equations
                  Instances For
                    @[simp]
                    theorem WithBot.orderIsoPUnitSumLex_bot {α : Type u_1} [LE α] :
                    WithBot.orderIsoPUnitSumLex = toLex (Sum.inl PUnit.unit)
                    @[simp]
                    theorem WithBot.orderIsoPUnitSumLex_toLex {α : Type u_1} [LE α] (a : α) :
                    WithBot.orderIsoPUnitSumLex a = toLex (Sum.inr a)
                    @[simp]
                    theorem WithBot.orderIsoPUnitSumLex_symm_inl {α : Type u_1} [LE α] (x : PUnit.{u_4 + 1} ) :
                    WithBot.orderIsoPUnitSumLex.symm (toLex (Sum.inl x)) =
                    @[simp]
                    theorem WithBot.orderIsoPUnitSumLex_symm_inr {α : Type u_1} [LE α] (a : α) :
                    WithBot.orderIsoPUnitSumLex.symm (toLex (Sum.inr a)) = a

                    WithTop α is order-isomorphic to α ⊕ₗ PUnit, by sending to Unit and ↑a to a.

                    Equations
                    Instances For
                      @[simp]
                      theorem WithTop.orderIsoSumLexPUnit_top {α : Type u_1} [LE α] :
                      WithTop.orderIsoSumLexPUnit = toLex (Sum.inr PUnit.unit)
                      @[simp]
                      theorem WithTop.orderIsoSumLexPUnit_toLex {α : Type u_1} [LE α] (a : α) :
                      WithTop.orderIsoSumLexPUnit a = toLex (Sum.inl a)
                      @[simp]
                      theorem WithTop.orderIsoSumLexPUnit_symm_inr {α : Type u_1} [LE α] (x : PUnit.{u_4 + 1} ) :
                      WithTop.orderIsoSumLexPUnit.symm (toLex (Sum.inr x)) =
                      @[simp]
                      theorem WithTop.orderIsoSumLexPUnit_symm_inl {α : Type u_1} [LE α] (a : α) :
                      WithTop.orderIsoSumLexPUnit.symm (toLex (Sum.inl a)) = a