Documentation

Mathlib.Order.RelClasses

Unbundled relation classes #

In this file we prove some properties of Is* classes defined in Mathlib/Order/Defs.lean. The main difference between these classes and the usual order classes (Preorder etc) is that usual classes extend LE and/or LT while these classes take a relation as an explicit argument.

theorem IsRefl.swap {α : Type u} (r : ααProp) [IsRefl α r] :
theorem IsIrrefl.swap {α : Type u} (r : ααProp) [IsIrrefl α r] :
theorem IsTrans.swap {α : Type u} (r : ααProp) [IsTrans α r] :
theorem IsAntisymm.swap {α : Type u} (r : ααProp) [IsAntisymm α r] :
theorem IsAsymm.swap {α : Type u} (r : ααProp) [IsAsymm α r] :
theorem IsTotal.swap {α : Type u} (r : ααProp) [IsTotal α r] :
theorem IsTrichotomous.swap {α : Type u} (r : ααProp) [IsTrichotomous α r] :
theorem IsPreorder.swap {α : Type u} (r : ααProp) [IsPreorder α r] :
theorem IsStrictOrder.swap {α : Type u} (r : ααProp) [IsStrictOrder α r] :
theorem IsPartialOrder.swap {α : Type u} (r : ααProp) [IsPartialOrder α r] :
theorem eq_empty_relation {α : Type u} (r : ααProp) [IsIrrefl α r] [Subsingleton α] :
@[reducible, inline]
abbrev partialOrderOfSO {α : Type u} (r : ααProp) [IsStrictOrder α r] :

Construct a partial order from an isStrictOrder relation.

See note [reducible non-instances].

Equations
    Instances For
      @[reducible, inline]
      abbrev linearOrderOfSTO {α : Type u} (r : ααProp) [IsStrictTotalOrder α r] [DecidableRel r] :

      Construct a linear order from an IsStrictTotalOrder relation.

      See note [reducible non-instances].

      Equations
        Instances For

          Order connection #

          class IsOrderConnected (α : Type u) (lt : ααProp) :

          A connected order is one satisfying the condition a < c → a < b ∨ b < c. This is recognizable as an intuitionistic substitute for a ≤ b ∨ b ≤ a on the constructive reals, and is also known as negative transitivity, since the contrapositive asserts transitivity of the relation ¬ a < b.

          • conn (a b c : α) : lt a clt a b lt b c

            A connected order is one satisfying the condition a < c → a < b ∨ b < c.

          Instances
            theorem IsOrderConnected.neg_trans {α : Type u} {r : ααProp} [IsOrderConnected α r] {a b c : α} (h₁ : ¬r a b) (h₂ : ¬r b c) :
            ¬r a c
            theorem isStrictWeakOrder_of_isOrderConnected {α : Type u} {r : ααProp} [IsAsymm α r] [IsOrderConnected α r] :
            @[instance 100]

            Inverse Image #

            theorem InvImage.isTrichotomous {α : Type u} {β : Type v} {r : ααProp} [IsTrichotomous α r] {f : βα} (h : Function.Injective f) :
            instance InvImage.isAsymm {α : Type u} {β : Type v} {r : ααProp} [IsAsymm α r] (f : βα) :
            IsAsymm β (InvImage r f)

            Well-order #

            class IsWellFounded (α : Type u) (r : ααProp) :

            A well-founded relation. Not to be confused with IsWellOrder.

            Instances
              theorem isWellFounded_iff (α : Type u) (r : ααProp) :
              @[irreducible]
              theorem WellFoundedRelation.asymmetric {α : Sort u_1} [WellFoundedRelation α] {a b : α} :
              rel a b¬rel b a
              @[irreducible]
              theorem WellFoundedRelation.asymmetric₃ {α : Sort u_1} [WellFoundedRelation α] {a b c : α} :
              rel a brel b c¬rel c a
              theorem WellFounded.prod_lex {α : Type u} {β : Type v} {ra : ααProp} {rb : ββProp} (ha : WellFounded ra) (hb : WellFounded rb) :
              theorem WellFounded.psigma_lex {α : Sort u_1} {β : αSort u_2} {r : ααProp} {s : (a : α) → β aβ aProp} (ha : WellFounded r) (hb : ∀ (x : α), WellFounded (s x)) :

              The lexicographical order of well-founded relations is well-founded.

              theorem WellFounded.psigma_revLex {α : Sort u_1} {β : Sort u_2} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
              theorem WellFounded.psigma_skipLeft (α : Type u) {β : Type v} {s : ββProp} (hb : WellFounded s) :
              theorem IsWellFounded.induction {α : Type u} (r : ααProp) [IsWellFounded α r] {C : αProp} (a : α) (ind : ∀ (x : α), (∀ (y : α), r y xC y)C x) :
              C a

              Induction on a well-founded relation.

              theorem IsWellFounded.apply {α : Type u} (r : ααProp) [IsWellFounded α r] (a : α) :
              Acc r a

              All values are accessible under the well-founded relation.

              def IsWellFounded.fix {α : Type u} (r : ααProp) [IsWellFounded α r] {C : αSort u_1} :
              ((x : α) → ((y : α) → r y xC y)C x)(x : α) → C x

              Creates data, given a way to generate a value from all that compare as less under a well-founded relation. See also IsWellFounded.fix_eq.

              Equations
                Instances For
                  theorem IsWellFounded.fix_eq {α : Type u} (r : ααProp) [IsWellFounded α r] {C : αSort u_1} (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) :
                  fix r F x = F x fun (y : α) (x : r y x) => fix r F y

                  The value from IsWellFounded.fix is built from the previous ones as specified.

                  Derive a WellFoundedRelation instance from an isWellFounded instance.

                  Equations
                    Instances For
                      theorem WellFounded.asymmetric {α : Sort u_1} {r : ααProp} (h : WellFounded r) (a b : α) :
                      r a b¬r b a
                      theorem WellFounded.asymmetric₃ {α : Sort u_1} {r : ααProp} (h : WellFounded r) (a b c : α) :
                      r a br b c¬r c a
                      @[instance 100]
                      instance instIsAsymmOfIsWellFounded {α : Type u} (r : ααProp) [IsWellFounded α r] :
                      IsAsymm α r
                      @[instance 100]
                      instance instIsIrreflOfIsWellFounded {α : Type u} (r : ααProp) [IsWellFounded α r] :
                      instance instIsWellFoundedTransGen {α : Type u} (r : ααProp) [i : IsWellFounded α r] :
                      @[reducible, inline]
                      abbrev WellFoundedLT (α : Type u_1) [LT α] :

                      A class for a well founded relation <.

                      Equations
                        Instances For
                          @[reducible, inline]
                          abbrev WellFoundedGT (α : Type u_1) [LT α] :

                          A class for a well founded relation >.

                          Equations
                            Instances For
                              theorem wellFounded_lt {α : Type u} [LT α] [WellFoundedLT α] :
                              WellFounded fun (x1 x2 : α) => x1 < x2
                              theorem wellFounded_gt {α : Type u} [LT α] [WellFoundedGT α] :
                              WellFounded fun (x1 x2 : α) => x1 > x2
                              @[instance 100]
                              @[instance 100]
                              class IsWellOrder (α : Type u) (r : ααProp) extends IsTrichotomous α r, IsTrans α r, IsWellFounded α r :

                              A well order is a well-founded linear order.

                              Instances
                                @[instance 100]
                                instance instIsStrictTotalOrderOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                                @[instance 100]
                                instance instIsTrichotomousOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                                @[instance 100]
                                instance instIsTransOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                                IsTrans α r
                                @[instance 100]
                                instance instIsIrreflOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                                @[instance 100]
                                instance instIsAsymmOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                                IsAsymm α r
                                theorem WellFoundedLT.induction {α : Type u} [LT α] [WellFoundedLT α] {C : αProp} (a : α) (ind : ∀ (x : α), (∀ (y : α), y < xC y)C x) :
                                C a

                                Inducts on a well-founded < relation.

                                theorem WellFoundedLT.apply {α : Type u} [LT α] [WellFoundedLT α] (a : α) :
                                Acc (fun (x1 x2 : α) => x1 < x2) a

                                All values are accessible under the well-founded <.

                                def WellFoundedLT.fix {α : Type u} [LT α] [WellFoundedLT α] {C : αSort u_1} :
                                ((x : α) → ((y : α) → y < xC y)C x)(x : α) → C x

                                Creates data, given a way to generate a value from all that compare as lesser. See also WellFoundedLT.fix_eq.

                                Equations
                                  Instances For
                                    theorem WellFoundedLT.fix_eq {α : Type u} [LT α] [WellFoundedLT α] {C : αSort u_1} (F : (x : α) → ((y : α) → y < xC y)C x) (x : α) :
                                    fix F x = F x fun (y : α) (x : y < x) => fix F y

                                    The value from WellFoundedLT.fix is built from the previous ones as specified.

                                    Derive a WellFoundedRelation instance from a WellFoundedLT instance.

                                    Equations
                                      Instances For
                                        theorem WellFoundedGT.induction {α : Type u} [LT α] [WellFoundedGT α] {C : αProp} (a : α) (ind : ∀ (x : α), (∀ (y : α), x < yC y)C x) :
                                        C a

                                        Inducts on a well-founded > relation.

                                        theorem WellFoundedGT.apply {α : Type u} [LT α] [WellFoundedGT α] (a : α) :
                                        Acc (fun (x1 x2 : α) => x1 > x2) a

                                        All values are accessible under the well-founded >.

                                        def WellFoundedGT.fix {α : Type u} [LT α] [WellFoundedGT α] {C : αSort u_1} :
                                        ((x : α) → ((y : α) → x < yC y)C x)(x : α) → C x

                                        Creates data, given a way to generate a value from all that compare as greater. See also WellFoundedGT.fix_eq.

                                        Equations
                                          Instances For
                                            theorem WellFoundedGT.fix_eq {α : Type u} [LT α] [WellFoundedGT α] {C : αSort u_1} (F : (x : α) → ((y : α) → x < yC y)C x) (x : α) :
                                            fix F x = F x fun (y : α) (x : x < y) => fix F y

                                            The value from WellFoundedGT.fix is built from the successive ones as specified.

                                            Derive a WellFoundedRelation instance from a WellFoundedGT instance.

                                            Equations
                                              Instances For
                                                noncomputable def IsWellOrder.linearOrder {α : Type u} (r : ααProp) [IsWellOrder α r] :

                                                Construct a decidable linear order from a well-founded linear order.

                                                Equations
                                                  Instances For
                                                    def IsWellOrder.toHasWellFounded {α : Type u} [LT α] [hwo : IsWellOrder α fun (x1 x2 : α) => x1 < x2] :

                                                    Derive a WellFoundedRelation instance from an IsWellOrder instance.

                                                    Equations
                                                      Instances For
                                                        theorem Subsingleton.isWellOrder {α : Type u} [Subsingleton α] (r : ααProp) [hr : IsIrrefl α r] :
                                                        @[instance 100]
                                                        instance instIsWellOrderOfIsEmpty {α : Type u} [IsEmpty α] (r : ααProp) :
                                                        instance Prod.Lex.instIsWellFounded {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsWellFounded α r] [IsWellFounded β s] :
                                                        IsWellFounded (α × β) (Prod.Lex r s)
                                                        instance instIsWellOrderProdLex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
                                                        IsWellOrder (α × β) (Prod.Lex r s)
                                                        instance instIsWellFoundedInvImage {α : Type u} {β : Type v} (r : ααProp) [IsWellFounded α r] (f : βα) :
                                                        instance instIsWellFoundedInvImageNatLt {α : Type u} (f : α) :
                                                        IsWellFounded α (InvImage (fun (x1 x2 : ) => x1 < x2) f)
                                                        theorem Subrelation.isWellFounded {α : Type u} (r : ααProp) [IsWellFounded α r] {s : ααProp} (h : Subrelation s r) :
                                                        theorem Prod.wellFoundedLT' {α : Type u} {β : Type v} [PartialOrder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] :

                                                        See Prod.wellFoundedLT for a version that only requires Preorder α.

                                                        theorem Prod.wellFoundedGT' {α : Type u} {β : Type v} [PartialOrder α] [WellFoundedGT α] [Preorder β] [WellFoundedGT β] :

                                                        See Prod.wellFoundedGT for a version that only requires Preorder α.

                                                        def Set.Unbounded {α : Type u} (r : ααProp) (s : Set α) :

                                                        An unbounded or cofinal set.

                                                        Equations
                                                          Instances For
                                                            def Set.Bounded {α : Type u} (r : ααProp) (s : Set α) :

                                                            A bounded or final set. Not to be confused with Bornology.IsBounded.

                                                            Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem Set.not_bounded_iff {α : Type u} {r : ααProp} (s : Set α) :
                                                                @[simp]
                                                                theorem Set.not_unbounded_iff {α : Type u} {r : ααProp} (s : Set α) :
                                                                theorem Set.unbounded_of_isEmpty {α : Type u} [IsEmpty α] {r : ααProp} (s : Set α) :
                                                                instance Order.Preimage.instIsRefl {α : Type u} {β : Type v} {r : ααProp} [IsRefl α r] {f : βα} :
                                                                IsRefl β (f ⁻¹'o r)
                                                                instance Order.Preimage.instIsIrrefl {α : Type u} {β : Type v} {r : ααProp} [IsIrrefl α r] {f : βα} :
                                                                IsIrrefl β (f ⁻¹'o r)
                                                                instance Order.Preimage.instIsSymm {α : Type u} {β : Type v} {r : ααProp} [IsSymm α r] {f : βα} :
                                                                IsSymm β (f ⁻¹'o r)
                                                                instance Order.Preimage.instIsAsymm {α : Type u} {β : Type v} {r : ααProp} [IsAsymm α r] {f : βα} :
                                                                IsAsymm β (f ⁻¹'o r)
                                                                instance Order.Preimage.instIsTrans {α : Type u} {β : Type v} {r : ααProp} [IsTrans α r] {f : βα} :
                                                                IsTrans β (f ⁻¹'o r)
                                                                instance Order.Preimage.instIsPreorder {α : Type u} {β : Type v} {r : ααProp} [IsPreorder α r] {f : βα} :
                                                                instance Order.Preimage.instIsStrictOrder {α : Type u} {β : Type v} {r : ααProp} [IsStrictOrder α r] {f : βα} :
                                                                instance Order.Preimage.instIsStrictWeakOrder {α : Type u} {β : Type v} {r : ααProp} [IsStrictWeakOrder α r] {f : βα} :
                                                                instance Order.Preimage.instIsEquiv {α : Type u} {β : Type v} {r : ααProp} [IsEquiv α r] {f : βα} :
                                                                IsEquiv β (f ⁻¹'o r)
                                                                instance Order.Preimage.instIsTotal {α : Type u} {β : Type v} {r : ααProp} [IsTotal α r] {f : βα} :
                                                                IsTotal β (f ⁻¹'o r)
                                                                theorem Order.Preimage.isAntisymm {α : Type u} {β : Type v} {r : ααProp} [IsAntisymm α r] {f : βα} (hf : Function.Injective f) :

                                                                Strict-non strict relations #

                                                                class IsNonstrictStrictOrder (α : Type u_1) (r : semiOutParam (ααProp)) (s : ααProp) :

                                                                An unbundled relation class stating that r is the nonstrict relation corresponding to the strict relation s. Compare Preorder.lt_iff_le_not_le. This is mostly meant to provide dot notation on (⊆) and (⊂).

                                                                • right_iff_left_not_left (a b : α) : s a b r a b ¬r b a

                                                                  The relation r is the nonstrict relation corresponding to the strict relation s.

                                                                Instances
                                                                  theorem right_iff_left_not_left {α : Type u} {r s : ααProp} [IsNonstrictStrictOrder α r s] {a b : α} :
                                                                  s a b r a b ¬r b a
                                                                  theorem right_iff_left_not_left_of {α : Type u} (r s : ααProp) [IsNonstrictStrictOrder α r s] {a b : α} :
                                                                  s a b r a b ¬r b a

                                                                  A version of right_iff_left_not_left with explicit r and s.

                                                                  instance instIsIrreflOfIsNonstrictStrictOrder {α : Type u} {r s : ααProp} [IsNonstrictStrictOrder α r s] :

                                                                  and #

                                                                  theorem subset_of_eq_of_subset {α : Type u} [HasSubset α] {a b c : α} (hab : a = b) (hbc : b c) :
                                                                  a c
                                                                  theorem subset_of_subset_of_eq {α : Type u} [HasSubset α] {a b c : α} (hab : a b) (hbc : b = c) :
                                                                  a c
                                                                  @[simp]
                                                                  theorem subset_refl {α : Type u} [HasSubset α] [IsRefl α fun (x1 x2 : α) => x1 x2] (a : α) :
                                                                  a a
                                                                  theorem subset_rfl {α : Type u} [HasSubset α] {a : α} [IsRefl α fun (x1 x2 : α) => x1 x2] :
                                                                  a a
                                                                  theorem subset_of_eq {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] :
                                                                  a = ba b
                                                                  theorem superset_of_eq {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] :
                                                                  a = bb a
                                                                  theorem ne_of_not_subset {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] :
                                                                  ¬a ba b
                                                                  theorem ne_of_not_superset {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] :
                                                                  ¬a bb a
                                                                  theorem subset_trans {α : Type u} [HasSubset α] [IsTrans α fun (x1 x2 : α) => x1 x2] {a b c : α} :
                                                                  a bb ca c
                                                                  theorem subset_antisymm {α : Type u} [HasSubset α] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] :
                                                                  a bb aa = b
                                                                  theorem superset_antisymm {α : Type u} [HasSubset α] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] :
                                                                  a bb ab = a
                                                                  theorem Eq.trans_subset {α : Type u} [HasSubset α] {a b c : α} (hab : a = b) (hbc : b c) :
                                                                  a c

                                                                  Alias of subset_of_eq_of_subset.

                                                                  theorem HasSubset.subset.trans_eq {α : Type u} [HasSubset α] {a b c : α} (hab : a b) (hbc : b = c) :
                                                                  a c

                                                                  Alias of subset_of_subset_of_eq.

                                                                  theorem Eq.subset' {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] :
                                                                  a = ba b

                                                                  Alias of subset_of_eq.

                                                                  theorem Eq.superset {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] :
                                                                  a = bb a

                                                                  Alias of superset_of_eq.

                                                                  theorem HasSubset.Subset.trans {α : Type u} [HasSubset α] [IsTrans α fun (x1 x2 : α) => x1 x2] {a b c : α} :
                                                                  a bb ca c

                                                                  Alias of subset_trans.

                                                                  theorem HasSubset.Subset.antisymm {α : Type u} [HasSubset α] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] :
                                                                  a bb aa = b

                                                                  Alias of subset_antisymm.

                                                                  theorem HasSubset.Subset.antisymm' {α : Type u} [HasSubset α] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] :
                                                                  a bb ab = a

                                                                  Alias of superset_antisymm.

                                                                  theorem subset_antisymm_iff {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] [IsAntisymm α fun (x1 x2 : α) => x1 x2] :
                                                                  a = b a b b a
                                                                  theorem superset_antisymm_iff {α : Type u} [HasSubset α] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] [IsAntisymm α fun (x1 x2 : α) => x1 x2] :
                                                                  a = b b a a b
                                                                  theorem ssubset_of_eq_of_ssubset {α : Type u} [HasSSubset α] {a b c : α} (hab : a = b) (hbc : b c) :
                                                                  a c
                                                                  theorem ssubset_of_ssubset_of_eq {α : Type u} [HasSSubset α] {a b c : α} (hab : a b) (hbc : b = c) :
                                                                  a c
                                                                  theorem ssubset_irrefl {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 x2] (a : α) :
                                                                  ¬a a
                                                                  theorem ssubset_irrfl {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 x2] {a : α} :
                                                                  ¬a a
                                                                  theorem ne_of_ssubset {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 x2] {a b : α} :
                                                                  a ba b
                                                                  theorem ne_of_ssuperset {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 x2] {a b : α} :
                                                                  a bb a
                                                                  theorem ssubset_trans {α : Type u} [HasSSubset α] [IsTrans α fun (x1 x2 : α) => x1 x2] {a b c : α} :
                                                                  a bb ca c
                                                                  theorem ssubset_asymm {α : Type u} [HasSSubset α] [IsAsymm α fun (x1 x2 : α) => x1 x2] {a b : α} :
                                                                  a b¬b a
                                                                  theorem Eq.trans_ssubset {α : Type u} [HasSSubset α] {a b c : α} (hab : a = b) (hbc : b c) :
                                                                  a c

                                                                  Alias of ssubset_of_eq_of_ssubset.

                                                                  theorem HasSSubset.SSubset.trans_eq {α : Type u} [HasSSubset α] {a b c : α} (hab : a b) (hbc : b = c) :
                                                                  a c

                                                                  Alias of ssubset_of_ssubset_of_eq.

                                                                  theorem HasSSubset.SSubset.false {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 x2] {a : α} :
                                                                  ¬a a

                                                                  Alias of ssubset_irrfl.

                                                                  theorem HasSSubset.SSubset.ne {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 x2] {a b : α} :
                                                                  a ba b

                                                                  Alias of ne_of_ssubset.

                                                                  theorem HasSSubset.SSubset.ne' {α : Type u} [HasSSubset α] [IsIrrefl α fun (x1 x2 : α) => x1 x2] {a b : α} :
                                                                  a bb a

                                                                  Alias of ne_of_ssuperset.

                                                                  theorem HasSSubset.SSubset.trans {α : Type u} [HasSSubset α] [IsTrans α fun (x1 x2 : α) => x1 x2] {a b c : α} :
                                                                  a bb ca c

                                                                  Alias of ssubset_trans.

                                                                  theorem HasSSubset.SSubset.asymm {α : Type u} [HasSSubset α] [IsAsymm α fun (x1 x2 : α) => x1 x2] {a b : α} :
                                                                  a b¬b a

                                                                  Alias of ssubset_asymm.

                                                                  theorem ssubset_iff_subset_not_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} :
                                                                  a b a b ¬b a
                                                                  theorem subset_of_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} (h : a b) :
                                                                  a b
                                                                  theorem not_subset_of_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} (h : a b) :
                                                                  ¬b a
                                                                  theorem not_ssubset_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} (h : a b) :
                                                                  ¬b a
                                                                  theorem ssubset_of_subset_not_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} (h₁ : a b) (h₂ : ¬b a) :
                                                                  a b
                                                                  theorem HasSSubset.SSubset.subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} (h : a b) :
                                                                  a b

                                                                  Alias of subset_of_ssubset.

                                                                  theorem HasSSubset.SSubset.not_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} (h : a b) :
                                                                  ¬b a

                                                                  Alias of not_subset_of_ssubset.

                                                                  theorem HasSubset.Subset.not_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} (h : a b) :
                                                                  ¬b a

                                                                  Alias of not_ssubset_of_subset.

                                                                  theorem HasSubset.Subset.ssubset_of_not_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} (h₁ : a b) (h₂ : ¬b a) :
                                                                  a b

                                                                  Alias of ssubset_of_subset_not_subset.

                                                                  theorem ssubset_of_subset_of_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b c : α} [IsTrans α fun (x1 x2 : α) => x1 x2] (h₁ : a b) (h₂ : b c) :
                                                                  a c
                                                                  theorem ssubset_of_ssubset_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b c : α} [IsTrans α fun (x1 x2 : α) => x1 x2] (h₁ : a b) (h₂ : b c) :
                                                                  a c
                                                                  theorem ssubset_of_subset_of_ne {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (h₁ : a b) (h₂ : a b) :
                                                                  a b
                                                                  theorem ssubset_of_ne_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (h₁ : a b) (h₂ : a b) :
                                                                  a b
                                                                  theorem eq_or_ssubset_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (h : a b) :
                                                                  a = b a b
                                                                  theorem ssubset_or_eq_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (h : a b) :
                                                                  a b a = b
                                                                  theorem eq_of_subset_of_not_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (hab : a b) (hba : ¬a b) :
                                                                  a = b
                                                                  theorem eq_of_superset_of_not_ssuperset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (hab : a b) (hba : ¬a b) :
                                                                  b = a
                                                                  theorem HasSubset.Subset.trans_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b c : α} [IsTrans α fun (x1 x2 : α) => x1 x2] (h₁ : a b) (h₂ : b c) :
                                                                  a c

                                                                  Alias of ssubset_of_subset_of_ssubset.

                                                                  theorem HasSSubset.SSubset.trans_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b c : α} [IsTrans α fun (x1 x2 : α) => x1 x2] (h₁ : a b) (h₂ : b c) :
                                                                  a c

                                                                  Alias of ssubset_of_ssubset_of_subset.

                                                                  theorem HasSubset.Subset.ssubset_of_ne {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (h₁ : a b) (h₂ : a b) :
                                                                  a b

                                                                  Alias of ssubset_of_subset_of_ne.

                                                                  theorem Ne.ssubset_of_subset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (h₁ : a b) (h₂ : a b) :
                                                                  a b

                                                                  Alias of ssubset_of_ne_of_subset.

                                                                  theorem HasSubset.Subset.eq_or_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (h : a b) :
                                                                  a = b a b

                                                                  Alias of eq_or_ssubset_of_subset.

                                                                  theorem HasSubset.Subset.ssubset_or_eq {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (h : a b) :
                                                                  a b a = b

                                                                  Alias of ssubset_or_eq_of_subset.

                                                                  theorem HasSubset.Subset.eq_of_not_ssubset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (hab : a b) (hba : ¬a b) :
                                                                  a = b

                                                                  Alias of eq_of_subset_of_not_ssubset.

                                                                  theorem HasSubset.Subset.eq_of_not_ssuperset {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] (hab : a b) (hba : ¬a b) :
                                                                  b = a

                                                                  Alias of eq_of_superset_of_not_ssuperset.

                                                                  theorem ssubset_iff_subset_ne {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsAntisymm α fun (x1 x2 : α) => x1 x2] :
                                                                  a b a b a b
                                                                  theorem subset_iff_ssubset_or_eq {α : Type u} [HasSubset α] [HasSSubset α] [IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 x2] {a b : α} [IsRefl α fun (x1 x2 : α) => x1 x2] [IsAntisymm α fun (x1 x2 : α) => x1 x2] :
                                                                  a b a b a = b

                                                                  Conversion of bundled order typeclasses to unbundled relation typeclasses #

                                                                  instance instIsReflLe {α : Type u} [Preorder α] :
                                                                  IsRefl α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsReflGe {α : Type u} [Preorder α] :
                                                                  IsRefl α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsTransLe {α : Type u} [Preorder α] :
                                                                  IsTrans α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsTransGe {α : Type u} [Preorder α] :
                                                                  IsTrans α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsPreorderLe {α : Type u} [Preorder α] :
                                                                  IsPreorder α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsPreorderGe {α : Type u} [Preorder α] :
                                                                  IsPreorder α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsIrreflLt {α : Type u} [Preorder α] :
                                                                  IsIrrefl α fun (x1 x2 : α) => x1 < x2
                                                                  instance instIsIrreflGt {α : Type u} [Preorder α] :
                                                                  IsIrrefl α fun (x1 x2 : α) => x1 > x2
                                                                  instance instIsTransLt {α : Type u} [Preorder α] :
                                                                  IsTrans α fun (x1 x2 : α) => x1 < x2
                                                                  instance instIsTransGt {α : Type u} [Preorder α] :
                                                                  IsTrans α fun (x1 x2 : α) => x1 > x2
                                                                  instance instIsAsymmLt {α : Type u} [Preorder α] :
                                                                  IsAsymm α fun (x1 x2 : α) => x1 < x2
                                                                  instance instIsAsymmGt {α : Type u} [Preorder α] :
                                                                  IsAsymm α fun (x1 x2 : α) => x1 > x2
                                                                  instance instIsAntisymmLt {α : Type u} [Preorder α] :
                                                                  IsAntisymm α fun (x1 x2 : α) => x1 < x2
                                                                  instance instIsAntisymmGt {α : Type u} [Preorder α] :
                                                                  IsAntisymm α fun (x1 x2 : α) => x1 > x2
                                                                  instance instIsStrictOrderLt {α : Type u} [Preorder α] :
                                                                  IsStrictOrder α fun (x1 x2 : α) => x1 < x2
                                                                  instance instIsStrictOrderGt {α : Type u} [Preorder α] :
                                                                  IsStrictOrder α fun (x1 x2 : α) => x1 > x2
                                                                  instance instIsNonstrictStrictOrderLeLt {α : Type u} [Preorder α] :
                                                                  IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 < x2
                                                                  instance instIsAntisymmLe {α : Type u} [PartialOrder α] :
                                                                  IsAntisymm α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsAntisymmGe {α : Type u} [PartialOrder α] :
                                                                  IsAntisymm α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsPartialOrderLe {α : Type u} [PartialOrder α] :
                                                                  IsPartialOrder α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsPartialOrderGe {α : Type u} [PartialOrder α] :
                                                                  IsPartialOrder α fun (x1 x2 : α) => x1 x2
                                                                  instance LE.isTotal {α : Type u} [LinearOrder α] :
                                                                  IsTotal α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsTotalGe {α : Type u} [LinearOrder α] :
                                                                  IsTotal α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsLinearOrderLe {α : Type u} [LinearOrder α] :
                                                                  IsLinearOrder α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsLinearOrderGe {α : Type u} [LinearOrder α] :
                                                                  IsLinearOrder α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsTrichotomousLt {α : Type u} [LinearOrder α] :
                                                                  IsTrichotomous α fun (x1 x2 : α) => x1 < x2
                                                                  instance instIsTrichotomousGt {α : Type u} [LinearOrder α] :
                                                                  IsTrichotomous α fun (x1 x2 : α) => x1 > x2
                                                                  instance instIsTrichotomousLe {α : Type u} [LinearOrder α] :
                                                                  IsTrichotomous α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsTrichotomousGe {α : Type u} [LinearOrder α] :
                                                                  IsTrichotomous α fun (x1 x2 : α) => x1 x2
                                                                  instance instIsStrictTotalOrderLt {α : Type u} [LinearOrder α] :
                                                                  IsStrictTotalOrder α fun (x1 x2 : α) => x1 < x2
                                                                  instance instIsOrderConnectedLt {α : Type u} [LinearOrder α] :
                                                                  IsOrderConnected α fun (x1 x2 : α) => x1 < x2
                                                                  instance OrderDual.isTotal_le {α : Type u} [LE α] [h : IsTotal α fun (x1 x2 : α) => x1 x2] :
                                                                  IsTotal αᵒᵈ fun (x1 x2 : αᵒᵈ) => x1 x2
                                                                  @[instance 100]
                                                                  instance isWellOrder_lt {α : Type u} [LinearOrder α] [WellFoundedLT α] :
                                                                  IsWellOrder α fun (x1 x2 : α) => x1 < x2
                                                                  @[instance 100]
                                                                  instance isWellOrder_gt {α : Type u} [LinearOrder α] [WellFoundedGT α] :
                                                                  IsWellOrder α fun (x1 x2 : α) => x1 > x2