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 : α β) :
LiftRel r s x x
instance Sum.instIsReflLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsRefl α r] [IsRefl β s] :
IsRefl (α β) (LiftRel r s)
instance Sum.instIsIrreflLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsIrrefl α r] [IsIrrefl β s] :
IsIrrefl (α β) (LiftRel r s)
theorem Sum.LiftRel.trans {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrans α r] [IsTrans β s] {a b c : α β} :
LiftRel r s a bLiftRel r s b cLiftRel r s a c
instance Sum.instIsTransLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrans α r] [IsTrans β s] :
IsTrans (α β) (LiftRel r s)
instance Sum.instIsAntisymmLiftRel {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsAntisymm α r] [IsAntisymm β s] :
IsAntisymm (α β) (LiftRel r s)
instance Sum.instIsReflLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsRefl α r] [IsRefl β s] :
IsRefl (α β) (Lex r s)
instance Sum.instIsIrreflLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsIrrefl α r] [IsIrrefl β s] :
IsIrrefl (α β) (Lex r s)
instance Sum.instIsTransLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrans α r] [IsTrans β s] :
IsTrans (α β) (Lex r s)
instance Sum.instIsAntisymmLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsAntisymm α r] [IsAntisymm β s] :
IsAntisymm (α β) (Lex r s)
instance Sum.instIsTotalLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTotal α r] [IsTotal β s] :
IsTotal (α β) (Lex r s)
instance Sum.instIsTrichotomousLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsTrichotomous α r] [IsTrichotomous β s] :
IsTrichotomous (α β) (Lex r s)
instance Sum.instIsWellOrderLex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) [IsWellOrder α r] [IsWellOrder β s] :
IsWellOrder (α β) (Lex r s)

Disjoint sum of two orders #

instance Sum.instLESum {α : Type u_1} {β : Type u_2} [LE α] [LE β] :
LE (α β)
Equations
    instance Sum.instLTSum {α : Type u_1} {β : Type u_2} [LT α] [LT β] :
    LT (α β)
    Equations
      theorem Sum.le_def {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : α β} :
      a b 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 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 : α} :
      inl a inl b a b
      @[simp]
      theorem Sum.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : β} :
      inr a inr b a b
      @[simp]
      theorem Sum.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : α} :
      inl a < inl b a < b
      @[simp]
      theorem Sum.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : β} :
      inr a < inr b 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 : β} :
      ¬inl b < inr a
      @[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 : β} :
      ¬inr b < inl a
      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 β] :
        theorem Sum.inr_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        theorem Sum.inl_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        theorem Sum.inr_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
        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 (α β)
          instance Sum.noMaxOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder α] [NoMaxOrder β] :
          NoMaxOrder (α β)
          @[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 β] :
          @[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 : α) :
              _root_.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 : β) :
                  _root_.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 (_root_.Lex (α β))

                      The linear/lexicographical on a sum.

                      Equations
                        instance Sum.Lex.LT {α : Type u_1} {β : Type u_2} [LT α] [LT β] :
                        LT (_root_.Lex (α β))

                        The linear/lexicographical < on a sum.

                        Equations
                          @[simp]
                          theorem Sum.Lex.toLex_le_toLex {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : α β} :
                          toLex a toLex b 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 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 b : _root_.Lex (α β)} :
                          a b 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 b : _root_.Lex (α β)} :
                          a < b 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 (inl a) toLex (inl b) a b
                          theorem Sum.Lex.inr_le_inr_iff {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a b : β} :
                          toLex (inr a) toLex (inr b) a b
                          theorem Sum.Lex.inl_lt_inl_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : α} :
                          toLex (inl a) < toLex (inl b) a < b
                          theorem Sum.Lex.inr_lt_inr_iff {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a b : β} :
                          toLex (inr a) < toLex (inr b) a < b
                          theorem Sum.Lex.inl_le_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) (b : β) :
                          theorem Sum.Lex.inl_lt_inr {α : Type u_1} {β : Type u_2} [LT α] [LT β] (a : α) (b : β) :
                          toLex (inl a) < toLex (inr b)
                          theorem Sum.Lex.not_inr_le_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] {a : α} {b : β} :
                          theorem Sum.Lex.not_inr_lt_inl {α : Type u_1} {β : Type u_2} [LT α] [LT β] {a : α} {b : β} :
                          instance Sum.Lex.preorder {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                          Equations
                            theorem Sum.Lex.toLex_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                            theorem Sum.Lex.toLex_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                            theorem Sum.Lex.inl_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                            theorem Sum.Lex.inr_mono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                            theorem Sum.Lex.inl_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                            theorem Sum.Lex.inr_strictMono {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] :
                            instance Sum.Lex.partialOrder {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] :
                            Equations
                              instance Sum.Lex.linearOrder {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] :
                              Equations
                                instance Sum.Lex.orderBot {α : Type u_1} {β : Type u_2} [LE α] [OrderBot α] [LE β] :

                                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 β] :
                                  instance Sum.Lex.orderTop {α : Type u_1} {β : Type u_2} [LE α] [LE β] [OrderTop β] :

                                  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 β] :
                                    instance Sum.Lex.boundedOrder {α : Type u_1} {β : Type u_2} [LE α] [LE β] [OrderBot α] [OrderTop β] :
                                    Equations
                                      instance Sum.Lex.noMinOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMinOrder α] [NoMinOrder β] :
                                      instance Sum.Lex.noMaxOrder {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder α] [NoMaxOrder β] :
                                      instance Sum.Lex.noMinOrder_of_nonempty {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMinOrder α] [Nonempty α] :
                                      instance Sum.Lex.noMaxOrder_of_nonempty {α : Type u_1} {β : Type u_2} [LT α] [LT β] [NoMaxOrder β] [Nonempty β] :

                                      Order isomorphisms #

                                      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_apply (α : Type u_4) (β : Type u_5) [LE α] [LE β] (a✝ : α β) :
                                          (sumComm α β) a✝ = a✝.swap
                                          @[simp]
                                          theorem OrderIso.sumComm_symm (α : Type u_4) (β : Type u_5) [LE α] [LE β] :
                                          (sumComm α β).symm = sumComm β α
                                          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 : α) :
                                              (sumAssoc α β γ) (Sum.inl (Sum.inl a)) = Sum.inl a
                                              @[simp]
                                              theorem OrderIso.sumAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (b : β) :
                                              (sumAssoc α β γ) (Sum.inl (Sum.inr b)) = Sum.inr (Sum.inl b)
                                              @[simp]
                                              theorem OrderIso.sumAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) :
                                              (sumAssoc α β γ) (Sum.inr c) = Sum.inr (Sum.inr c)
                                              @[simp]
                                              theorem OrderIso.sumAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (a : α) :
                                              (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 : β) :
                                              @[simp]
                                              theorem OrderIso.sumAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) :
                                              (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 : α) :
                                                  @[simp]
                                                  theorem OrderIso.sumDualDistrib_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) :
                                                  @[simp]
                                                  theorem OrderIso.sumDualDistrib_symm_inl {α : Type u_1} {β : Type u_2} [LE α] [LE β] (a : α) :
                                                  @[simp]
                                                  theorem OrderIso.sumDualDistrib_symm_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (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 : α) :
                                                      (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 : β) :
                                                      @[simp]
                                                      theorem OrderIso.sumLexAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LE α] [LE β] [LE γ] (c : γ) :
                                                      (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 : α) :
                                                      @[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 : γ) :
                                                      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 : α) :
                                                          @[simp]
                                                          theorem OrderIso.sumLexDualAntidistrib_inr {α : Type u_1} {β : Type u_2} [LE α] [LE β] (b : β) :
                                                          @[simp]
                                                          @[simp]

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

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem WithBot.orderIsoPUnitSumLex_toLex {α : Type u_1} [LE α] (a : α) :
                                                              @[simp]
                                                              theorem WithBot.orderIsoPUnitSumLex_symm_inr {α : Type u_1} [LE α] (a : α) :

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

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem WithTop.orderIsoSumLexPUnit_toLex {α : Type u_1} [LE α] (a : α) :
                                                                  @[simp]
                                                                  theorem WithTop.orderIsoSumLexPUnit_symm_inl {α : Type u_1} [LE α] (a : α) :