Unbundled relation classes

In this file we prove some properties of Is* classes defined in Mathlib/Order/Defs/Unbundled.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.

@[deprecated inferInstance (since := "2026-04-28")]

theorem Std.Refl.swap {α : Type u} (r : α → α → Prop) [Refl r] : Refl (Function.swap r)

@[deprecated Std.Refl.swap (since := "2026-01-09")]

theorem IsRefl.swap {α : Type u} (r : α → α → Prop) [Std.Refl r] : Std.Refl (Function.swap r)

Alias of Std.Refl.swap.

@[deprecated inferInstance (since := "2026-04-28")]

theorem Std.Irrefl.swap {α : Type u} (r : α → α → Prop) [Irrefl r] : Irrefl (Function.swap r)

@[deprecated inferInstance (since := "2026-04-28")]

theorem IsTrans.swap {α : Type u} (r : α → α → Prop) [IsTrans α r] : IsTrans α (Function.swap r)

@[deprecated inferInstance (since := "2026-04-28")]

theorem Std.Antisymm.swap {α : Type u} (r : α → α → Prop) [Antisymm r] : Antisymm (Function.swap r)

@[deprecated inferInstance (since := "2026-04-28")]

theorem Std.Asymm.swap {α : Type u} (r : α → α → Prop) [Asymm r] : Asymm (Function.swap r)

@[deprecated Std.Asymm.swap (since := "2026-01-05")]

theorem IsAsymm.swap {α : Type u} (r : α → α → Prop) [Std.Asymm r] : Std.Asymm (Function.swap r)

Alias of Std.Asymm.swap.

@[deprecated inferInstance (since := "2026-04-28")]

theorem Std.Total.swap {α : Type u} (r : α → α → Prop) [Total r] : Total (Function.swap r)

@[deprecated inferInstance (since := "2026-04-28")]

theorem Std.Trichotomous.swap {α : Type u} (r : α → α → Prop) [Trichotomous r] : Trichotomous (Function.swap r)

@[deprecated Std.Trichotomous.swap (since := "2026-01-24")]

theorem IsTrichotomous.swap {α : Type u} (r : α → α → Prop) [Std.Trichotomous r] : Std.Trichotomous (Function.swap r)

Alias of Std.Trichotomous.swap.

@[deprecated inferInstance (since := "2026-04-28")]

theorem IsPreorder.swap {α : Type u} (r : α → α → Prop) [IsPreorder α r] : IsPreorder α (Function.swap r)

@[deprecated inferInstance (since := "2026-04-28")]

theorem IsStrictOrder.swap {α : Type u} (r : α → α → Prop) [IsStrictOrder α r] : IsStrictOrder α (Function.swap r)

@[deprecated inferInstance (since := "2026-04-28")]

theorem IsPartialOrder.swap {α : Type u} (r : α → α → Prop) [IsPartialOrder α r] : IsPartialOrder α (Function.swap r)

theorem eq_empty_relation {α : Type u} (r : α → α → Prop) [Std.Irrefl r] [Subsingleton α] : r = emptyRelation

@[reducible, inline]

abbrev partialOrderOfSO {α : Type u} (r : α → α → Prop) [IsStrictOrder α r] : PartialOrder α

Construct a partial order from an isStrictOrder relation.

See note [reducible non-instances].

Equations

• partialOrderOfSO r = { le := fun (x y : α) => x = y ∨ r x y, lt := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[reducible, inline]

abbrev linearOrderOfSTO {α : Type u} (r : α → α → Prop) [IsStrictTotalOrder α r] [DecidableRel r] : LinearOrder α

Construct a linear order from an IsStrictTotalOrder relation.

See note [reducible non-instances].

Equations

• One or more equations did not get rendered due to their size.

@[deprecated inferInstance (since := "2026-04-28")]

theorem IsStrictTotalOrder.swap {α : Type u} (r : α → α → Prop) [IsStrictTotalOrder α r] : IsStrictTotalOrder α (Function.swap r)

Order connection

class IsOrderConnected (α : Type u) (lt : α → α → Prop) : 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 c → lt 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} [Std.Asymm r] [IsOrderConnected α r] : IsStrictWeakOrder α r

@[instance 100]

instance isStrictOrderConnected_of_isStrictTotalOrder {α : Type u} {r : α → α → Prop} [IsStrictTotalOrder α r] : IsOrderConnected α r

Inverse Image

theorem InvImage.trichotomous {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Trichotomous r] {f : β → α} (h : Function.Injective f) : Std.Trichotomous (InvImage r f)

@[deprecated InvImage.trichotomous (since := "2026-01-24")]

theorem InvImage.isTrichotomous {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Trichotomous r] {f : β → α} (h : Function.Injective f) : Std.Trichotomous (InvImage r f)

Alias of InvImage.trichotomous.

instance InvImage.asymm {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Asymm r] (f : β → α) : Std.Asymm (InvImage r f)

Well-order

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

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

• wf : WellFounded r

  The relation is WellFounded, as a proposition.

theorem isWellFounded_iff (α : Type u) (r : α → α → Prop) : IsWellFounded α r ↔ WellFounded r

instance WellFoundedRelation.isWellFounded {α : Type u} [h : WellFoundedRelation α] : IsWellFounded α rel

theorem WellFoundedRelation.asymmetric {α : Sort u_1} [WellFoundedRelation α] {a b : α} : rel a b → ¬rel b a

theorem WellFoundedRelation.asymmetric₃ {α : Sort u_1} [WellFoundedRelation α] {a b c : α} : rel a b → rel b c → ¬rel c a

theorem WellFounded.prod_lex {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Prod.Lex ra rb)

theorem WellFounded.psigma_lex {α : Sort u_1} {β : α → Sort u_2} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} (ha : WellFounded r) (hb : ∀ (x : α), WellFounded (s x)) : WellFounded (PSigma.Lex r s)

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) : WellFounded (PSigma.RevLex r s)

theorem WellFounded.psigma_skipLeft (α : Type u) {β : Type v} {s : β → β → Prop} (hb : WellFounded s) : WellFounded (PSigma.SkipLeft α s)

theorem IsWellFounded.induction {α : Type u} (r : α → α → Prop) [IsWellFounded α r] {motive : α → Prop} (a : α) (ind : ∀ (x : α), (∀ (y : α), r y x → motive y) → motive x) : motive 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] {motive : α → Sort u_1} (ind : (x : α) → ((y : α) → r y x → motive y) → motive x) (x : α) : motive 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

• IsWellFounded.fix r = ⋯.fix

theorem IsWellFounded.fix_eq {α : Type u} (r : α → α → Prop) [IsWellFounded α r] {motive : α → Sort u_1} (ind : (x : α) → ((y : α) → r y x → motive y) → motive x) (x : α) : fix r ind x = ind x fun (y : α) (x : r y x) => fix r ind y

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

@[implicit_reducible]

def IsWellFounded.toWellFoundedRelation {α : Type u} (r : α → α → Prop) [IsWellFounded α r] : WellFoundedRelation α

Derive a WellFoundedRelation instance from an isWellFounded instance.

Equations

• IsWellFounded.toWellFoundedRelation r = { rel := r, wf := ⋯ }

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 b → r b c → ¬r c a

@[instance 100]

instance instAsymmOfIsWellFounded {α : Type u} (r : α → α → Prop) [IsWellFounded α r] : Std.Asymm r

instance instIsWellFoundedTransGen {α : Type u} (r : α → α → Prop) [i : IsWellFounded α r] : IsWellFounded α (Relation.TransGen r)

@[reducible, inline]

abbrev WellFoundedLT (α : Type u_1) [LT α] : Prop

A class for a well-founded relation <.

Equations

• WellFoundedLT α = IsWellFounded α fun (x1 x2 : α) => x1 < x2

@[reducible, inline]

abbrev WellFoundedGT (α : Type u_1) [LT α] : Prop

A class for a well-founded relation >.

Equations

• WellFoundedGT α = IsWellFounded α fun (x1 x2 : α) => x2 < x1

theorem wellFounded_lt {α : Type u} [LT α] [WellFoundedLT α] : WellFounded fun (x1 x2 : α) => x1 < x2

theorem wellFounded_gt {α : Type u} [LT α] [WellFoundedGT α] : WellFounded fun (x1 x2 : α) => x2 < x1

@[instance 100]

instance instWellFoundedGTOrderDualOfWellFoundedLT (α : Type u_1) [LT α] [h : WellFoundedLT α] : WellFoundedGT αᵒᵈ

@[instance 100]

instance instWellFoundedLTOrderDualOfWellFoundedGT (α : Type u_1) [LT α] [h : WellFoundedGT α] : WellFoundedLT αᵒᵈ

theorem wellFoundedGT_dual_iff (α : Type u_1) [LT α] : WellFoundedGT αᵒᵈ ↔ WellFoundedLT α

theorem wellFoundedLT_dual_iff (α : Type u_1) [LT α] : WellFoundedLT αᵒᵈ ↔ WellFoundedGT α

class IsWellOrder (α : Type u) (r : α → α → Prop) extends IsWellFounded α r, Std.Trichotomous r : Prop

A well order is a well-founded linear order.

• wf : WellFounded r
• trichotomous (a b : α) : ¬r a b → ¬r b a → a = b

instance instIsTransOfIsWellOrder {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : IsTrans α r

@[instance 100]

instance instIsStrictTotalOrderOfIsWellOrder {α : Type u_1} (r : α → α → Prop) [IsWellOrder α r] : IsStrictTotalOrder α r

theorem WellFoundedLT.induction {α : Type u} [LT α] [WellFoundedLT α] {motive : α → Prop} (a : α) (ind : ∀ (x : α), (∀ (y : α), y < x → motive y) → motive x) : motive a

Inducts on a well-founded < relation.

theorem WellFoundedGT.induction {α : Type u} [LT α] [WellFoundedGT α] {motive : α → Prop} (a : α) (ind : ∀ (x : α), (∀ (y : α), x < y → motive y) → motive x) : motive 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 <.

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

All values are accessible under the well-founded >.

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

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

Equations

• WellFoundedLT.fix = IsWellFounded.fix fun (x1 x2 : α) => x1 < x2

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

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

Equations

• WellFoundedGT.fix = IsWellFounded.fix fun (x1 x2 : α) => x2 < x1

theorem WellFoundedLT.fix_eq {α : Type u} [LT α] [WellFoundedLT α] {motive : α → Sort u_1} (ind : (x : α) → ((y : α) → y < x → motive y) → motive x) (x : α) : fix ind x = ind x fun (y : α) (x : y < x) => fix ind y

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

theorem WellFoundedGT.fix_eq {α : Type u} [LT α] [WellFoundedGT α] {motive : α → Sort u_1} (ind : (x : α) → ((y : α) → x < y → motive y) → motive x) (x : α) : fix ind x = ind x fun (y : α) (x : x < y) => fix ind y

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

@[implicit_reducible]

def WellFoundedLT.toWellFoundedRelation {α : Type u} [LT α] [WellFoundedLT α] : WellFoundedRelation α

Derive a WellFoundedRelation instance from a WellFoundedLT instance.

Equations

• WellFoundedLT.toWellFoundedRelation = IsWellFounded.toWellFoundedRelation fun (x1 x2 : α) => x1 < x2

@[implicit_reducible]

def WellFoundedGT.toWellFoundedRelation {α : Type u} [LT α] [WellFoundedGT α] : WellFoundedRelation α

Derive a WellFoundedRelation instance from a WellFoundedGT instance.

Equations

• WellFoundedGT.toWellFoundedRelation = IsWellFounded.toWellFoundedRelation fun (x1 x2 : α) => x2 < x1

@[implicit_reducible]

noncomputable def IsWellOrder.linearOrder {α : Type u} (r : α → α → Prop) [IsWellOrder α r] : LinearOrder α

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

Equations

• IsWellOrder.linearOrder r = linearOrderOfSTO r

@[implicit_reducible]

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

Derive a WellFoundedRelation instance from an IsWellOrder instance.

Equations

• IsWellOrder.toHasWellFounded = { rel := fun (x1 x2 : α) => x1 < x2, wf := ⋯ }

theorem Subsingleton.isWellOrder {α : Type u} [Subsingleton α] (r : α → α → Prop) [Std.Irrefl r] : IsWellOrder α r

instance instIsWellOrderEmptyRelationOfSubsingleton {α : Type u} [Subsingleton α] : IsWellOrder α emptyRelation

@[instance 100]

instance instIsWellOrderOfIsEmpty {α : Type u} [IsEmpty α] (r : α → α → Prop) : IsWellOrder α r

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 : β → α) : IsWellFounded β (InvImage 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) : IsWellFounded α s

instance Prod.wellFoundedLT {α : Type u} {β : Type v} [Preorder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] : WellFoundedLT (α × β)

instance Prod.wellFoundedGT {α : Type u} {β : Type v} [Preorder α] [WellFoundedGT α] [Preorder β] [WellFoundedGT β] : WellFoundedGT (α × β)

@[deprecated Prod.wellFoundedLT (since := "2026-01-12")]

theorem Prod.wellFoundedLT' {α : Type u} {β : Type v} [Preorder α] [WellFoundedLT α] [Preorder β] [WellFoundedLT β] : WellFoundedLT (α × β)

Alias of Prod.wellFoundedLT.

@[deprecated Prod.wellFoundedGT (since := "2026-01-12")]

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

Alias of Prod.wellFoundedGT.

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

An unbounded or cofinal set.

Equations

• Set.Unbounded r s = ∀ (a : α), ∃ (b : α), b ∈ s ∧ ¬r b a

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

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

Equations

• Set.Bounded r s = ∃ (a : α), ∀ (b : α), b ∈ s → r b a

@[simp]

theorem Set.not_bounded_iff {α : Type u} {r : α → α → Prop} (s : Set α) : ¬Bounded r s ↔ Unbounded r s

@[simp]

theorem Set.not_unbounded_iff {α : Type u} {r : α → α → Prop} (s : Set α) : ¬Unbounded r s ↔ Bounded r s

theorem Set.unbounded_of_isEmpty {α : Type u} [IsEmpty α] {r : α → α → Prop} (s : Set α) : Unbounded r s

instance Order.Preimage.instRefl {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Refl r] {f : β → α} : Std.Refl (f ⁻¹'o r)

instance Order.Preimage.instIrrefl {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Irrefl r] {f : β → α} : Std.Irrefl (f ⁻¹'o r)

instance Order.Preimage.instIsSymm {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Symm r] {f : β → α} : Std.Symm (f ⁻¹'o r)

instance Order.Preimage.instAsymm {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Asymm r] {f : β → α} : Std.Asymm (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 : β → α} : IsPreorder β (f ⁻¹'o r)

instance Order.Preimage.instIsStrictOrder {α : Type u} {β : Type v} {r : α → α → Prop} [IsStrictOrder α r] {f : β → α} : IsStrictOrder β (f ⁻¹'o r)

instance Order.Preimage.instIsStrictWeakOrder {α : Type u} {β : Type v} {r : α → α → Prop} [IsStrictWeakOrder α r] {f : β → α} : IsStrictWeakOrder β (f ⁻¹'o r)

instance Order.Preimage.instIsEquiv {α : Type u} {β : Type v} {r : α → α → Prop} [IsEquiv α r] {f : β → α} : IsEquiv β (f ⁻¹'o r)

instance Order.Preimage.instTotal {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Total r] {f : β → α} : Std.Total (f ⁻¹'o r)

theorem Order.Preimage.antisymm {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Antisymm r] {f : β → α} (hf : Function.Injective f) : Std.Antisymm (f ⁻¹'o r)

@[deprecated Order.Preimage.antisymm (since := "2026-01-06")]

theorem Order.Preimage.isAntisymm {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Antisymm r] {f : β → α} (hf : Function.Injective f) : Std.Antisymm (f ⁻¹'o r)

Alias of Order.Preimage.antisymm.

Strict-non strict relations

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

An unbundled relation class stating that r is the nonstrict relation corresponding to the strict relation s. Compare lt_iff_le_not_ge. 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.

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 instIrreflOfIsNonstrictStrictOrder {α : Type u} {r s : α → α → Prop} [IsNonstrictStrictOrder α r s] : Std.Irrefl s

⊆ and ⊂

theorem subset_of_eq_of_subset {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [LE α] (h₁ : a = b) (h₂ : b ⊆ c) : a ⊆ c

Set notation form of le_of_eq_of_le

theorem ne_of_not_superset {α : Type u_2} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (h : ¬b ⊆ a) : a ≠ b

Set notation form of ne_of_not_ge

theorem subset_refl {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] (a : α) : a ⊆ a

Set notation form of le_refl

theorem subset_antisymm {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b → b ⊆ a → a = b

Set notation form of le_antisymm

theorem superset_antisymm {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : b ⊆ a → a ⊆ b → a = b

Set notation form of ge_antisymm

theorem Eq.subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a = b) : a ⊆ b

Set notation form of Eq.le

theorem ne_of_not_subset {α : Type u_2} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (h : ¬a ⊆ b) : a ≠ b

Set notation form of ne_of_not_le

theorem subset_antisymm_iff {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a = b ↔ a ⊆ b ∧ b ⊆ a

Set notation form of le_antisymm_iff

theorem subset_rfl {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a : α} : a ⊆ a

Set notation form of le_rfl

theorem superset_antisymm_iff {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a = b ↔ b ⊆ a ∧ a ⊆ b

Set notation form of ge_antisymm_iff

theorem Eq.superset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a = b) : b ⊆ a

Set notation form of Eq.ge

theorem subset_of_subset_of_eq {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [LE α] (h₁ : a ⊆ b) (h₂ : b = c) : a ⊆ c

Set notation form of le_of_le_of_eq

theorem superset_of_eq {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a = b) : b ⊆ a

Set notation form of ge_of_eq

theorem subset_of_eq {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a = b) : a ⊆ b

Set notation form of le_of_eq

theorem subset_trans {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} : a ⊆ b → b ⊆ c → a ⊆ c

Set notation form of le_trans

theorem Eq.trans_subset {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [LE α] (h₁ : a = b) (h₂ : b ⊆ c) : a ⊆ c

Set notation form of Eq.trans_le

@[deprecated LE.le.trans_eq (since := "2026-05-24")]

theorem HasSubset.subset.trans_eq {α : Type u_1} {a b c : α} [LE α] (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c

Alias of LE.le.trans_eq.

@[deprecated Eq.subset (since := "2026-01-24")]

theorem Eq.subset' {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a = b) : a ⊆ b

Alias of Eq.subset.

---

Set notation form of Eq.le

@[deprecated LE.le.trans (since := "2026-05-24")]

theorem HasSubset.Subset.trans {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} : a ⊆ b → b ⊆ c → a ⊆ c

Alias of subset_trans.

---

Set notation form of le_trans

@[deprecated LE.le.antisymm (since := "2026-05-24")]

theorem HasSubset.Subset.antisymm {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b → b ⊆ a → a = b

Alias of subset_antisymm.

---

Set notation form of le_antisymm

@[deprecated LE.le.antisymm' (since := "2026-05-24")]

theorem HasSubset.Subset.antisymm' {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : b ⊆ a → a ⊆ b → a = b

Alias of superset_antisymm.

---

Set notation form of ge_antisymm

theorem ne_of_ssubset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (h : a ⊂ b) : a ≠ b

Set notation form of ne_of_lt

theorem ssubset_irrefl {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] (a : α) : ¬a ⊂ a

Set notation form of lt_irrefl

theorem ssubset_of_ssubset_of_eq {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [LT α] (h₁ : a ⊂ b) (h₂ : b = c) : a ⊂ c

Set notation form of lt_of_lt_of_eq

theorem ne_of_ssuperset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (h : b ⊂ a) : a ≠ b

Set notation form of ne_of_gt

theorem ssubset_of_eq_of_ssubset {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [LT α] (h₁ : a = b) (h₂ : b ⊂ c) : a ⊂ c

Set notation form of lt_of_eq_of_lt

theorem ssubset_trans {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} : a ⊂ b → b ⊂ c → a ⊂ c

Set notation form of lt_trans

theorem Eq.trans_ssubset {α : Type u_1} [UsesSetNotationForOrder α] {a b c : α} [LT α] (h₁ : a = b) (h₂ : b ⊂ c) : a ⊂ c

Set notation form of Eq.trans_lt

theorem ssubset_asymm {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (h : a ⊂ b) : ¬b ⊂ a

Set notation form of lt_asymm

@[deprecated ssubset_irrefl (since := "2026-06-11")]

theorem ssubset_irrfl {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] (a : α) : ¬a ⊂ a

Alias of ssubset_irrefl.

---

Set notation form of lt_irrefl

@[deprecated LT.lt.trans_eq (since := "2026-05-24")]

theorem HasSSubset.SSubset.trans_eq {α : Type u_1} {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) : a < c

Alias of LT.lt.trans_eq.

@[deprecated LT.lt.false (since := "2026-05-24")]

theorem HasSSubset.SSubset.false {α : Type u_2} [Preorder α] {a : α} : a < a → False

Alias of LT.lt.false.

@[deprecated LT.lt.ne (since := "2026-05-24")]

theorem HasSSubset.SSubset.ne {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : a ≠ b

Alias of LT.lt.ne.

@[deprecated LT.lt.ne' (since := "2026-05-24")]

theorem HasSSubset.SSubset.ne' {α : Type u_1} [Preorder α] {a b : α} (h : b < a) : a ≠ b

Alias of LT.lt.ne'.

@[deprecated LT.lt.trans (since := "2026-05-24")]

theorem HasSSubset.SSubset.trans {α : Type u_1} [Preorder α] {a b c : α} : a < b → b < c → a < c

Alias of LT.lt.trans.

@[deprecated LT.lt.asymm (since := "2026-05-24")]

theorem HasSSubset.SSubset.asymm {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : ¬b < a

Alias of LT.lt.asymm.

theorem LE.le.not_ssuperset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) : ¬b ⊂ a

Set notation form of LE.le.not_gt

theorem LE.le.ssubset_of_not_superset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) (hba : ¬b ⊆ a) : a ⊂ b

Set notation form of LE.le.lt_of_not_ge

theorem LE.le.ssubset_of_ne {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b → a ≠ b → a ⊂ b

Set notation form of LE.le.lt_of_ne

theorem LE.le.eq_or_ssubset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h : a ⊆ b) : a = b ∨ a ⊂ b

Set notation form of LE.le.eq_or_lt

theorem not_subset_of_ssuperset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊂ b) : ¬b ⊆ a

Set notation form of not_le_of_gt

theorem LT.lt.not_superset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊂ b) : ¬b ⊆ a

Set notation form of LT.lt.not_ge

theorem Ne.ssubset_of_subset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ≠ b → a ⊆ b → a ⊂ b

Set notation form of Ne.lt_of_le

theorem LE.le.eq_of_not_ssubset' {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h₁ : b ⊆ a) (h₂ : ¬b ⊂ a) : a = b

Set notation form of LE.le.eq_of_not_lt'

theorem ssubset_or_eq_of_subset {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b → a ⊂ b ∨ a = b

Set notation form of lt_or_eq_of_le

theorem subset_of_ssubset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊂ b) : a ⊆ b

Set notation form of le_of_lt

theorem ssubset_of_subset_of_ne {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b → a ≠ b → a ⊂ b

Set notation form of lt_of_le_of_ne

theorem ssubset_of_ssubset_of_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} (hab : a ⊂ b) (hbc : b ⊆ c) : a ⊂ c

Set notation form of lt_of_lt_of_le

theorem eq_of_subset_of_not_ssubset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h₁ : a ⊆ b) (h₂ : ¬a ⊂ b) : a = b

Set notation form of eq_of_le_of_not_lt

theorem ssubset_iff_subset_and_ne {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊂ b ↔ a ⊆ b ∧ a ≠ b

Set notation form of lt_iff_le_and_ne

theorem subset_iff_ssubset_or_eq {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b ↔ a ⊂ b ∨ a = b

Set notation form of le_iff_lt_or_eq

theorem LT.lt.trans_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} (hab : a ⊂ b) (hbc : b ⊆ c) : a ⊂ c

Set notation form of LT.lt.trans_le

theorem LE.le.trans_ssubset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} (hab : a ⊆ b) (hbc : b ⊂ c) : a ⊂ c

Set notation form of LE.le.trans_lt

theorem LE.le.eq_of_not_ssubset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h₁ : a ⊆ b) (h₂ : ¬a ⊂ b) : a = b

Set notation form of LE.le.eq_of_not_lt

theorem eq_or_ssubset_of_subset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h : a ⊆ b) : a = b ∨ a ⊂ b

Set notation form of eq_or_lt_of_le

theorem not_ssubset_of_superset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) : ¬b ⊂ a

Set notation form of not_lt_of_ge

theorem ssubset_of_subset_not_superset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) (hba : ¬b ⊆ a) : a ⊂ b

Set notation form of lt_of_le_not_ge

theorem LE.le.ssubset_or_eq {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b → a ⊂ b ∨ a = b

Set notation form of LE.le.lt_or_eq

theorem ssubset_of_ne_of_subset {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ≠ b → a ⊆ b → a ⊂ b

Set notation form of lt_of_ne_of_le

theorem eq_of_subset_of_not_ssubset' {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h₁ : b ⊆ a) (h₂ : ¬b ⊂ a) : a = b

Set notation form of eq_of_le_of_not_lt'

theorem ssubset_iff_subset_not_superset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} : a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a

Set notation form of lt_iff_le_not_ge

theorem ssubset_of_subset_of_ssubset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} (hab : a ⊆ b) (hbc : b ⊂ c) : a ⊂ c

Set notation form of lt_of_le_of_lt

theorem LT.lt.subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊂ b) : a ⊆ b

Set notation form of LT.lt.le

theorem ssubset_iff_subset_not_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} : a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a

Alias of ssubset_iff_subset_not_superset.

---

Set notation form of lt_iff_le_not_ge

theorem not_subset_of_ssubset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊂ b) : ¬b ⊆ a

Alias of not_subset_of_ssuperset.

---

Set notation form of not_le_of_gt

theorem not_ssubset_of_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) : ¬b ⊂ a

Alias of not_ssubset_of_superset.

---

Set notation form of not_lt_of_ge

theorem ssubset_of_subset_not_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) (hba : ¬b ⊆ a) : a ⊂ b

Alias of ssubset_of_subset_not_superset.

---

Set notation form of lt_of_le_not_ge

theorem LT.lt.not_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊂ b) : ¬b ⊆ a

Alias of LT.lt.not_superset.

---

Set notation form of LT.lt.not_ge

theorem LE.le.not_ssubset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) : ¬b ⊂ a

Alias of LE.le.not_ssuperset.

---

Set notation form of LE.le.not_gt

theorem LE.le.ssubset_of_not_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) (hba : ¬b ⊆ a) : a ⊂ b

Alias of LE.le.ssubset_of_not_superset.

---

Set notation form of LE.le.lt_of_not_ge

@[deprecated LT.lt.subset (since := "2026-05-24")]

theorem HasSSubset.SSubset.subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊂ b) : a ⊆ b

Alias of LT.lt.subset.

---

Set notation form of LT.lt.le

@[deprecated LT.lt.not_superset (since := "2026-05-24")]

theorem HasSSubset.SSubset.not_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊂ b) : ¬b ⊆ a

Alias of LT.lt.not_superset.

---

Set notation form of LT.lt.not_ge

@[deprecated LE.le.not_ssuperset (since := "2026-05-24")]

theorem HasSubset.Subset.not_ssubset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) : ¬b ⊂ a

Alias of LE.le.not_ssuperset.

---

Set notation form of LE.le.not_gt

@[deprecated LE.le.ssubset_of_not_superset (since := "2026-05-24")]

theorem HasSubset.Subset.ssubset_of_not_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b : α} (hab : a ⊆ b) (hba : ¬b ⊆ a) : a ⊂ b

Alias of LE.le.ssubset_of_not_superset.

---

Set notation form of LE.le.lt_of_not_ge

theorem eq_of_superset_of_not_ssuperset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h₁ : b ⊆ a) (h₂ : ¬b ⊂ a) : a = b

Alias of eq_of_subset_of_not_ssubset'.

---

Set notation form of eq_of_le_of_not_lt'

theorem LE.le.eq_of_not_ssuperset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h₁ : b ⊆ a) (h₂ : ¬b ⊂ a) : a = b

Alias of LE.le.eq_of_not_ssubset'.

---

Set notation form of LE.le.eq_of_not_lt'

@[deprecated LE.le.trans_ssubset (since := "2026-05-24")]

theorem HasSubset.Subset.trans_ssubset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} (hab : a ⊆ b) (hbc : b ⊂ c) : a ⊂ c

Alias of LE.le.trans_ssubset.

---

Set notation form of LE.le.trans_lt

@[deprecated LT.lt.trans_subset (since := "2026-05-24")]

theorem HasSSubset.SSubset.trans_subset {α : Type u_1} [UsesSetNotationForOrder α] [Preorder α] {a b c : α} (hab : a ⊂ b) (hbc : b ⊆ c) : a ⊂ c

Alias of LT.lt.trans_subset.

---

Set notation form of LT.lt.trans_le

@[deprecated LE.le.ssubset_of_ne (since := "2026-05-24")]

theorem HasSubset.Subset.ssubset_of_ne {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b → a ≠ b → a ⊂ b

Alias of LE.le.ssubset_of_ne.

---

Set notation form of LE.le.lt_of_ne

@[deprecated LE.le.eq_or_ssubset (since := "2026-05-24")]

theorem HasSubset.Subset.eq_or_ssubset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h : a ⊆ b) : a = b ∨ a ⊂ b

Alias of LE.le.eq_or_ssubset.

---

Set notation form of LE.le.eq_or_lt

@[deprecated LE.le.ssubset_or_eq (since := "2026-05-24")]

theorem HasSubset.Subset.ssubset_or_eq {α : Type u_1} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊆ b → a ⊂ b ∨ a = b

Alias of LE.le.ssubset_or_eq.

---

Set notation form of LE.le.lt_or_eq

@[deprecated LE.le.eq_of_not_ssubset (since := "2026-05-24")]

theorem HasSubset.Subset.eq_of_not_ssubset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h₁ : a ⊆ b) (h₂ : ¬a ⊂ b) : a = b

Alias of LE.le.eq_of_not_ssubset.

---

Set notation form of LE.le.eq_of_not_lt

@[deprecated LE.le.eq_of_not_ssuperset (since := "2026-05-24")]

theorem HasSubset.Subset.eq_of_not_ssuperset {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} (h₁ : b ⊆ a) (h₂ : ¬b ⊂ a) : a = b

Alias of LE.le.eq_of_not_ssuperset.

---

Alias of LE.le.eq_of_not_ssubset'.

---

Set notation form of LE.le.eq_of_not_lt'

theorem ssubset_iff_subset_ne {α : Type u_2} [UsesSetNotationForOrder α] [PartialOrder α] {a b : α} : a ⊂ b ↔ a ⊆ b ∧ a ≠ b

Alias of ssubset_iff_subset_and_ne.

---

Set notation form of lt_iff_le_and_ne

Conversion of bundled order typeclasses to unbundled relation typeclasses

instance instReflLe {α : Type u} [Preorder α] : Std.Refl fun (x1 x2 : α) => x1 ≤ x2

instance instReflGe {α : Type u} [Preorder α] : Std.Refl fun (x1 x2 : α) => x2 ≤ x1

theorem Std.ge_refl {α : Type u_1} [LE α] [inst : Refl fun (x1 x2 : α) => x1 ≥ x2] (a : α) : a ≤ a

A version of Std.le_refl that works with Std.Refl (· ≥ ·). This is needed for to_dual translations because Std.le_refl requires Std.Refl (· ≤ ·), but after translation instReflLe becomes instReflGe : Std.Refl (· ≥ ·).

instance instIsTransLe {α : Type u} [Preorder α] : IsTrans α fun (x1 x2 : α) => x1 ≤ x2

instance instIsTransGe {α : Type u} [Preorder α] : IsTrans α fun (x1 x2 : α) => x2 ≤ x1

instance instIsPreorderLe {α : Type u} [Preorder α] : IsPreorder α fun (x1 x2 : α) => x1 ≤ x2

instance instIsPreorderGe {α : Type u} [Preorder α] : IsPreorder α fun (x1 x2 : α) => x2 ≤ x1

instance instIrreflLt {α : Type u} [Preorder α] : Std.Irrefl fun (x1 x2 : α) => x1 < x2

instance instIrreflGt {α : Type u} [Preorder α] : Std.Irrefl fun (x1 x2 : α) => x2 < x1

instance instIsTransLt {α : Type u} [Preorder α] : IsTrans α fun (x1 x2 : α) => x1 < x2

instance instIsTransGt {α : Type u} [Preorder α] : IsTrans α fun (x1 x2 : α) => x2 < x1

instance instAsymmLt {α : Type u} [Preorder α] : Std.Asymm fun (x1 x2 : α) => x1 < x2

instance instAsymmGt {α : Type u} [Preorder α] : Std.Asymm fun (x1 x2 : α) => x2 < x1

instance instAntisymmLt {α : Type u} [Preorder α] : Std.Antisymm fun (x1 x2 : α) => x1 < x2

instance instAntisymmGt {α : Type u} [Preorder α] : Std.Antisymm fun (x1 x2 : α) => x2 < x1

instance instIsStrictOrderLt {α : Type u} [Preorder α] : IsStrictOrder α fun (x1 x2 : α) => x1 < x2

instance instIsStrictOrderGt {α : Type u} [Preorder α] : IsStrictOrder α fun (x1 x2 : α) => x2 < x1

instance instIsNonstrictStrictOrderLeLt {α : Type u} [Preorder α] : IsNonstrictStrictOrder α (fun (x1 x2 : α) => x1 ≤ x2) fun (x1 x2 : α) => x1 < x2

instance instIsNonstrictStrictOrderGeGt {α : Type u} [Preorder α] : IsNonstrictStrictOrder α (fun (x1 x2 : α) => x2 ≤ x1) fun (x1 x2 : α) => x2 < x1

instance instAntisymmLe {α : Type u} [PartialOrder α] : Std.Antisymm fun (x1 x2 : α) => x1 ≤ x2

instance instAntisymmGe {α : Type u} [PartialOrder α] : Std.Antisymm fun (x1 x2 : α) => x2 ≤ x1

instance instIsPartialOrderLe {α : Type u} [PartialOrder α] : IsPartialOrder α fun (x1 x2 : α) => x1 ≤ x2

instance instIsPartialOrderGe {α : Type u} [PartialOrder α] : IsPartialOrder α fun (x1 x2 : α) => x2 ≤ x1

instance LE.total {α : Type u} [LinearOrder α] : Std.Total fun (x1 x2 : α) => x1 ≤ x2

instance LE.total' {α : Type u} [LinearOrder α] : Std.Total fun (x1 x2 : α) => x2 ≤ x1

instance instIsLinearOrderLe {α : Type u} [LinearOrder α] : IsLinearOrder α fun (x1 x2 : α) => x1 ≤ x2

instance instIsLinearOrderGe {α : Type u} [LinearOrder α] : IsLinearOrder α fun (x1 x2 : α) => x2 ≤ x1

instance instTrichotomousLt {α : Type u} [LinearOrder α] : Std.Trichotomous fun (x1 x2 : α) => x1 < x2

instance instTrichotomousGt {α : Type u} [LinearOrder α] : Std.Trichotomous fun (x1 x2 : α) => x2 < x1

instance instTrichotomousLe {α : Type u} [LinearOrder α] : Std.Trichotomous fun (x1 x2 : α) => x1 ≤ x2

instance instTrichotomousGe {α : Type u} [LinearOrder α] : Std.Trichotomous fun (x1 x2 : α) => x2 ≤ x1

instance instIsStrictTotalOrderLt {α : Type u} [LinearOrder α] : IsStrictTotalOrder α fun (x1 x2 : α) => x1 < x2

instance instIsStrictTotalOrderGt {α : Type u} [LinearOrder α] : IsStrictTotalOrder α fun (x1 x2 : α) => x2 < x1

theorem isTrans_le {α : Type u} [Preorder α] : IsTrans α LE.le

theorem isTrans_ge {α : Type u} [Preorder α] : IsTrans α fun (a a_1 : α) => a_1 ≤ a

@[deprecated isTrans_ge (since := "2026-02-21")]

theorem transitive_ge {α : Type u} [Preorder α] : IsTrans α fun (a a_1 : α) => a_1 ≤ a

Alias of isTrans_ge.

@[deprecated isTrans_le (since := "2026-02-21")]

theorem transitive_le {α : Type u} [Preorder α] : IsTrans α LE.le

Alias of isTrans_le.

theorem isTrans_lt {α : Type u} [Preorder α] : IsTrans α LT.lt

theorem isTrans_gt {α : Type u} [Preorder α] : IsTrans α fun (a a_1 : α) => a_1 < a

@[deprecated isTrans_gt (since := "2026-02-21")]

theorem transitive_gt {α : Type u} [Preorder α] : IsTrans α fun (a a_1 : α) => a_1 < a

Alias of isTrans_gt.

@[deprecated isTrans_lt (since := "2026-02-21")]

theorem transitive_lt {α : Type u} [Preorder α] : IsTrans α LT.lt

Alias of isTrans_lt.

instance OrderDual.total_le {α : Type u} [LE α] [h : Std.Total fun (x1 x2 : α) => x1 ≤ x2] : Std.Total fun (x1 x2 : αᵒᵈ) => x1 ≤ x2

instance OrderDual.total_ge {α : Type u} [LE α] [h : Std.Total fun (x1 x2 : α) => x2 ≤ x1] : Std.Total fun (x1 x2 : αᵒᵈ) => x2 ≤ x1

instance instWellFoundedLTNat : WellFoundedLT ℕ

@[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 : α) => x2 < x1