Documentation

Mathlib.Order.RelClasses

Unbundled relation classes #

In this file we prove some properties of Is* classes defined in Order.Defs. 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 of_eq {α : Type u} {r : ααProp} [IsRefl α r] {a : α} {b : α} :
a = br a b
theorem comm {α : Type u} {r : ααProp} [IsSymm α r] {a : α} {b : α} :
r a b r b a
theorem antisymm' {α : Type u} {r : ααProp} [IsAntisymm α r] {a : α} {b : α} :
r a br b ab = a
theorem antisymm_iff {α : Type u} {r : ααProp} [IsRefl α r] [IsAntisymm α r] {a : α} {b : α} :
r a b r b a a = b
@[elab_without_expected_type]
theorem antisymm_of {α : Type u} (r : ααProp) [IsAntisymm α r] {a : α} {b : α} :
r a br b aa = b

A version of antisymm with r explicit.

This lemma matches the lemmas from lean core in Init.Algebra.Classes, but is missing there.

@[elab_without_expected_type]
theorem antisymm_of' {α : Type u} (r : ααProp) [IsAntisymm α r] {a : α} {b : α} :
r a br b ab = a

A version of antisymm' with r explicit.

This lemma matches the lemmas from lean core in Init.Algebra.Classes, but is missing there.

theorem comm_of {α : Type u} (r : ααProp) [IsSymm α r] {a : α} {b : α} :
r a b r b a

A version of comm with r explicit.

This lemma matches the lemmas from lean core in Init.Algebra.Classes, but is missing there.

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] :
@[deprecated]
theorem IsLinearOrder.swap {α : Type u} (r : ααProp) [IsLinearOrder α r] :
theorem IsAsymm.isAntisymm {α : Type u} (r : ααProp) [IsAsymm α r] :
theorem IsAsymm.isIrrefl {α : Type u} {r : ααProp} [IsAsymm α r] :
theorem IsTotal.isTrichotomous {α : Type u} (r : ααProp) [IsTotal α r] :
@[instance 100]
instance IsTotal.to_isRefl {α : Type u} (r : ααProp) [IsTotal α r] :
IsRefl α r
Equations
  • =
theorem ne_of_irrefl {α : Type u} {r : ααProp} [IsIrrefl α r] {x : α} {y : α} :
r x yx y
theorem ne_of_irrefl' {α : Type u} {r : ααProp} [IsIrrefl α r] {x : α} {y : α} :
r x yy x
theorem not_rel_of_subsingleton {α : Type u} (r : ααProp) [IsIrrefl α r] [Subsingleton α] (x : α) (y : α) :
¬r x y
theorem rel_of_subsingleton {α : Type u} (r : ααProp) [IsRefl α r] [Subsingleton α] (x : α) (y : α) :
r x y
@[simp]
theorem empty_relation_apply {α : Type u} (a : α) (b : α) :
theorem eq_empty_relation {α : Type u} (r : ααProp) [IsIrrefl α r] [Subsingleton α] :
r = EmptyRelation
instance instIsIrreflEmptyRelation {α : Type u} :
IsIrrefl α EmptyRelation
Equations
  • =
theorem trans_trichotomous_left {α : Type u} {r : ααProp} [IsTrans α r] [IsTrichotomous α r] {a : α} {b : α} {c : α} :
¬r b ar b cr a c
theorem trans_trichotomous_right {α : Type u} {r : ααProp} [IsTrans α r] [IsTrichotomous α r] {a : α} {b : α} {c : α} :
r a b¬r c br a c
theorem transitive_of_trans {α : Type u} (r : ααProp) [IsTrans α r] :
theorem extensional_of_trichotomous_of_irrefl {α : Type u} (r : ααProp) [IsTrichotomous α r] [IsIrrefl α r] {a : α} {b : α} (H : ∀ (x : α), r x a r x b) :
a = b

In a trichotomous irreflexive order, every element is determined by the set of predecessors.

@[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] [(x y : α) → Decidable ¬r x y] :

    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.conn {α : Type u} {lt : ααProp} [self : IsOrderConnected α lt] (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.

        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]
        Equations
        • =
        @[deprecated, instance 100]
        Equations
        • =

        Well-order #

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

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

        Instances
          theorem IsWellFounded.wf {α : Type u} {r : ααProp} [self : IsWellFounded α r] :

          The relation is WellFounded, as a proposition.

          instance WellFoundedRelation.isWellFounded {α : Type u} [h : WellFoundedRelation α] :
          IsWellFounded α WellFoundedRelation.rel
          Equations
          • =
          @[irreducible]
          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) :
          @[deprecated WellFounded.psigma_lex]
          theorem PSigma.lex_wf {α : Sort u_1} {β : αSort u_2} {r : ααProp} {s : (a : α) → β aβ aProp} (ha : WellFounded r) (hb : ∀ (x : α), WellFounded (s x)) :

          Alias of WellFounded.psigma_lex.


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

          @[deprecated WellFounded.psigma_revLex]
          theorem PSigma.revLex_wf {α : Sort u_1} {β : Sort u_2} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :

          Alias of WellFounded.psigma_revLex.

          @[deprecated WellFounded.psigma_skipLeft]
          theorem PSigma.skipLeft_wf (α : Type u) {β : Type v} {s : ββProp} (hb : WellFounded s) :

          Alias of WellFounded.psigma_skipLeft.

          theorem IsWellFounded.induction {α : Type u} (r : ααProp) [IsWellFounded α r] {C : αProp} (a : α) :
          (∀ (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 : α) :
            IsWellFounded.fix r F x = F x fun (y : α) (x : r y x) => IsWellFounded.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
              @[instance 100]
              instance instIsAsymmOfIsWellFounded {α : Type u} (r : ααProp) [IsWellFounded α r] :
              IsAsymm α r
              Equations
              • =
              @[instance 100]
              instance instIsIrreflOfIsWellFounded {α : Type u} (r : ααProp) [IsWellFounded α r] :
              Equations
              • =
              instance instIsWellFoundedTransGen {α : Type u} (r : ααProp) [i : IsWellFounded α r] :
              Equations
              • =
              @[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]
                  Equations
                  • = h
                  @[instance 100]
                  Equations
                  • = h
                  class IsWellOrder (α : Type u) (r : ααProp) extends IsTrichotomous , IsTrans , IsWellFounded :

                  A well order is a well-founded linear order.

                    Instances
                      @[instance 100]
                      instance instIsStrictTotalOrderOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                      Equations
                      • =
                      @[instance 100]
                      instance instIsTrichotomousOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                      Equations
                      • =
                      @[instance 100]
                      instance instIsTransOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                      IsTrans α r
                      Equations
                      • =
                      @[instance 100]
                      instance instIsIrreflOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                      Equations
                      • =
                      @[instance 100]
                      instance instIsAsymmOfIsWellOrder {α : Type u_1} (r : ααProp) [IsWellOrder α r] :
                      IsAsymm α r
                      Equations
                      • =
                      theorem WellFoundedLT.induction {α : Type u} [LT α] [WellFoundedLT α] {C : αProp} (a : α) :
                      (∀ (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 : α) :
                        WellFoundedLT.fix F x = F x fun (y : α) (x : y < x) => WellFoundedLT.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 : α) :
                          (∀ (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 : α) :
                            WellFoundedGT.fix F x = F x fun (y : α) (x : x < y) => WellFoundedGT.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
                                • IsWellOrder.toHasWellFounded = { rel := fun (x1 x2 : α) => x1 < x2, wf := }
                                Instances For
                                  theorem Subsingleton.isWellOrder {α : Type u} [Subsingleton α] (r : ααProp) [hr : IsIrrefl α r] :
                                  Equations
                                  • =
                                  @[instance 100]
                                  instance instIsWellOrderOfIsEmpty {α : Type u} [IsEmpty α] (r : ααProp) :
                                  Equations
                                  • =
                                  instance instIsWellFoundedProdLex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsWellFounded α r] [IsWellFounded β s] :
                                  IsWellFounded (α × β) (Prod.Lex r s)
                                  Equations
                                  • =
                                  instance instIsWellOrderProdLex {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} [IsWellOrder α r] [IsWellOrder β s] :
                                  IsWellOrder (α × β) (Prod.Lex r s)
                                  Equations
                                  • =
                                  instance instIsWellFoundedInvImage {α : Type u} {β : Type v} (r : ααProp) [IsWellFounded α r] (f : βα) :
                                  Equations
                                  • =
                                  instance instIsWellFoundedInvImageNatLt {α : Type u} (f : α) :
                                  IsWellFounded α (InvImage (fun (x1 x2 : ) => x1 < x2) f)
                                  Equations
                                  • =
                                  theorem Subrelation.isWellFounded {α : Type u} (r : ααProp) [IsWellFounded α r] {s : ααProp} (h : Subrelation s r) :
                                  instance Prod.wellFoundedLT {α : Type u} {β : Type v} [PartialOrder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] :
                                  Equations
                                  • =
                                  instance Prod.wellFoundedGT {α : Type u} {β : Type v} [PartialOrder α] [WellFoundedGT α] [Preorder β] [WellFoundedGT β] :
                                  Equations
                                  • =
                                  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)
                                      Equations
                                      • =
                                      instance Order.Preimage.instIsTrans {α : Type u} {β : Type v} {r : ααProp} [IsTrans α r] {f : βα} :
                                      IsTrans β (f ⁻¹'o r)
                                      Equations
                                      • =

                                      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 IsNonstrictStrictOrder.right_iff_left_not_left {α : Type u_1} {r : semiOutParam (ααProp)} {s : ααProp} [self : IsNonstrictStrictOrder α r s] (a : α) (b : α) :
                                        s a b r a b ¬r b a

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

                                        theorem right_iff_left_not_left {α : Type u} {r : ααProp} {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 : ααProp) (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 : ααProp} {s : ααProp} [IsNonstrictStrictOrder α r s] :
                                        Equations
                                        • =

                                        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
                                        Equations
                                        • =
                                        instance instIsReflGe {α : Type u} [Preorder α] :
                                        IsRefl α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsTransLe {α : Type u} [Preorder α] :
                                        IsTrans α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsTransGe {α : Type u} [Preorder α] :
                                        IsTrans α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsPreorderLe {α : Type u} [Preorder α] :
                                        IsPreorder α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsPreorderGe {α : Type u} [Preorder α] :
                                        IsPreorder α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsIrreflLt {α : Type u} [Preorder α] :
                                        IsIrrefl α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        instance instIsIrreflGt {α : Type u} [Preorder α] :
                                        IsIrrefl α fun (x1 x2 : α) => x1 > x2
                                        Equations
                                        • =
                                        instance instIsTransLt {α : Type u} [Preorder α] :
                                        IsTrans α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        instance instIsTransGt {α : Type u} [Preorder α] :
                                        IsTrans α fun (x1 x2 : α) => x1 > x2
                                        Equations
                                        • =
                                        instance instIsAsymmLt {α : Type u} [Preorder α] :
                                        IsAsymm α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        instance instIsAsymmGt {α : Type u} [Preorder α] :
                                        IsAsymm α fun (x1 x2 : α) => x1 > x2
                                        Equations
                                        • =
                                        instance instIsAntisymmLt {α : Type u} [Preorder α] :
                                        IsAntisymm α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        instance instIsAntisymmGt {α : Type u} [Preorder α] :
                                        IsAntisymm α fun (x1 x2 : α) => x1 > x2
                                        Equations
                                        • =
                                        instance instIsStrictOrderLt {α : Type u} [Preorder α] :
                                        IsStrictOrder α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        instance instIsStrictOrderGt {α : Type u} [Preorder α] :
                                        IsStrictOrder α fun (x1 x2 : α) => x1 > x2
                                        Equations
                                        • =
                                        instance instIsNonstrictStrictOrderLeLt {α : Type u} [Preorder α] :
                                        IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 x2) fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        instance instIsAntisymmLe {α : Type u} [PartialOrder α] :
                                        IsAntisymm α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsAntisymmGe {α : Type u} [PartialOrder α] :
                                        IsAntisymm α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsPartialOrderLe {α : Type u} [PartialOrder α] :
                                        IsPartialOrder α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsPartialOrderGe {α : Type u} [PartialOrder α] :
                                        IsPartialOrder α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance LE.isTotal {α : Type u} [LinearOrder α] :
                                        IsTotal α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsTotalGe {α : Type u} [LinearOrder α] :
                                        IsTotal α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsLinearOrderLe {α : Type u} [LinearOrder α] :
                                        IsLinearOrder α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsLinearOrderGe {α : Type u} [LinearOrder α] :
                                        IsLinearOrder α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsTrichotomousLt {α : Type u} [LinearOrder α] :
                                        IsTrichotomous α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        instance instIsTrichotomousGt {α : Type u} [LinearOrder α] :
                                        IsTrichotomous α fun (x1 x2 : α) => x1 > x2
                                        Equations
                                        • =
                                        instance instIsTrichotomousLe {α : Type u} [LinearOrder α] :
                                        IsTrichotomous α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsTrichotomousGe {α : Type u} [LinearOrder α] :
                                        IsTrichotomous α fun (x1 x2 : α) => x1 x2
                                        Equations
                                        • =
                                        instance instIsStrictTotalOrderLt {α : Type u} [LinearOrder α] :
                                        IsStrictTotalOrder α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        instance instIsOrderConnectedLt {α : Type u} [LinearOrder α] :
                                        IsOrderConnected α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        @[deprecated]
                                        instance instIsStrictWeakOrderLt {α : Type u} [LinearOrder α] :
                                        IsStrictWeakOrder α fun (x1 x2 : α) => x1 < x2
                                        Equations
                                        • =
                                        theorem transitive_le {α : Type u} [Preorder α] :
                                        theorem transitive_lt {α : Type u} [Preorder α] :
                                        theorem transitive_ge {α : Type u} [Preorder α] :
                                        theorem transitive_gt {α : Type u} [Preorder α] :
                                        instance OrderDual.isTotal_le {α : Type u} [LE α] [h : IsTotal α fun (x1 x2 : α) => x1 x2] :
                                        IsTotal αᵒᵈ fun (x1 x2 : αᵒᵈ) => x1 x2
                                        Equations
                                        • =
                                        instance Nat.lt.isWellOrder :
                                        IsWellOrder fun (x1 x2 : ) => x1 < x2
                                        Equations
                                        instance instIsWellOrderOrderDualGtOfLt {α : Type u} [LinearOrder α] [h : IsWellOrder α fun (x1 x2 : α) => x1 < x2] :
                                        IsWellOrder αᵒᵈ fun (x1 x2 : αᵒᵈ) => x1 > x2
                                        Equations
                                        • = h
                                        instance instIsWellOrderOrderDualLtOfGt {α : Type u} [LinearOrder α] [h : IsWellOrder α fun (x1 x2 : α) => x1 > x2] :
                                        IsWellOrder αᵒᵈ fun (x1 x2 : αᵒᵈ) => x1 < x2
                                        Equations
                                        • = h