Orders

Defines classes for preorders, partial orders, and linear orders and proves some basic lemmas about them.

Unbundled classes

class IsTrans (α : Sort u_1) (r : α → α → Prop) : Prop

IsTrans X r means the binary relation r on X is transitive.

• trans (a b c : α) : r a b → r b c → r a c

@[instance_reducible]

instance instTransOfIsTrans {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] : Trans r r r

Equations

• instTransOfIsTrans = { trans := ⋯ }

@[instance 100]

instance instIsTransOfTrans {α : Sort u_1} {r : α → α → Prop} [Trans r r r] : IsTrans α r

class IsPreorder (α : Sort u_1) (r : α → α → Prop) extends Std.Refl r, IsTrans α r : Prop

IsPreorder X r means that the binary relation r on X is a pre-order, that is, reflexive and transitive.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c

class IsPartialOrder (α : Sort u_1) (r : α → α → Prop) extends IsPreorder α r, Std.Antisymm r : Prop

IsPartialOrder X r means that the binary relation r on X is a partial order, that is, IsPreorder X r and Std.Antisymm r.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c
• antisymm (a b : α) : r a b → r b a → a = b

class IsLinearOrder (α : Sort u_1) (r : α → α → Prop) extends IsPartialOrder α r, Std.Total r : Prop

IsLinearOrder X r means that the binary relation r on X is a linear order, that is, IsPartialOrder X r and Std.Total r.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c
• antisymm (a b : α) : r a b → r b a → a = b
• total (a b : α) : r a b ∨ r b a

class IsEquiv (α : Sort u_1) (r : α → α → Prop) extends IsPreorder α r, Std.Symm r : Prop

IsEquiv X r means that the binary relation r on X is an equivalence relation, that is, IsPreorder X r and Std.Symm r.

• refl (a : α) : r a a
• trans (a b c : α) : r a b → r b c → r a c
• symm (a b : α) : r a b → r b a

class IsStrictOrder (α : Sort u_1) (r : α → α → Prop) extends Std.Irrefl r, IsTrans α r : Prop

IsStrictOrder X r means that the binary relation r on X is a strict order, that is, Std.Irrefl r and IsTrans X r.

• irrefl (a : α) : ¬r a a
• trans (a b c : α) : r a b → r b c → r a c

class IsStrictWeakOrder (α : Sort u_1) (lt : α → α → Prop) extends IsStrictOrder α lt : Prop

IsStrictWeakOrder X lt means that the binary relation lt on X is a strict weak order, that is, IsStrictOrder X lt and ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a.

• irrefl (a : α) : ¬lt a a
• trans (a b c : α) : lt a b → lt b c → lt a c
• incomp_trans (a b c : α) : ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a

class IsStrictTotalOrder (α : Sort u_1) (lt : α → α → Prop) extends Std.Trichotomous lt, IsStrictOrder α lt : Prop

IsStrictTotalOrder X lt means that the binary relation lt on X is a strict total order, that is, Std.Trichotomous lt and IsStrictOrder X lt.

• trichotomous (a b : α) : ¬lt a b → ¬lt b a → a = b
• irrefl (a : α) : ¬lt a a
• trans (a b c : α) : lt a b → lt b c → lt a c

theorem Equivalence.of_isEquiv {α : Sort u_1} (lt : α → α → Prop) [IsEquiv α lt] : Equivalence lt

theorem IsEquiv.of_equivalence {α : Sort u_1} {lt : α → α → Prop} (h : Equivalence lt) : IsEquiv α lt

theorem equivalence_iff_isEquiv {α : Sort u_1} (lt : α → α → Prop) : Equivalence lt ↔ IsEquiv α lt

instance eq_isEquiv (α : Sort u_1) : IsEquiv α fun (x1 x2 : α) => x1 = x2

Equality is an equivalence relation.

instance instSymmNe_mathlib (α : Sort u_1) : Std.Symm Ne

instance instIrreflNe_mathlib (α : Sort u_1) : Std.Irrefl Ne

instance iff_isEquiv : IsEquiv Prop Iff

Iff is an equivalence relation.

instance instIsTransPropAnd : IsTrans Prop And

theorem irrefl {α : Sort u_1} {r : α → α → Prop} [Std.Irrefl r] (a : α) : ¬r a a

theorem refl {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] (a : α) : r a a

theorem trans {α : Sort u_1} {r : α → α → Prop} {a b c : α} [IsTrans α r] : r a b → r b c → r a c

theorem symm {α : Sort u_1} {r : α → α → Prop} {a b : α} [Std.Symm r] : r a b → r b a

theorem antisymm {α : Sort u_1} {r : α → α → Prop} {a b : α} [Std.Antisymm r] : r a b → r b a → a = b

theorem asymm {α : Sort u_1} {r : α → α → Prop} {a b : α} [Std.Asymm r] : r a b → ¬r b a

theorem trichotomous {α : Sort u_1} {r : α → α → Prop} [Std.Trichotomous r] (a b : α) : r a b ∨ a = b ∨ r b a

theorem irrefl_def {α : Sort u_1} {r : α → α → Prop} : Std.Irrefl r ↔ ∀ ⦃a : α⦄, ¬r a a

theorem refl_def {α : Sort u_1} {r : α → α → Prop} : Std.Refl r ↔ ∀ ⦃a : α⦄, r a a

theorem isTrans_def {α : Sort u_2} {r : α → α → Prop} : IsTrans α r ↔ ∀ ⦃a b c : α⦄, r a b → r b c → r a c

theorem symm_def {α : Sort u_1} {r : α → α → Prop} : Std.Symm r ↔ ∀ ⦃a b : α⦄, r a b → r b a

theorem antisymm_def {α : Sort u_1} {r : α → α → Prop} : Std.Antisymm r ↔ ∀ ⦃a b : α⦄, r a b → r b a → a = b

theorem asymm_def {α : Sort u_1} {r : α → α → Prop} : Std.Asymm r ↔ ∀ ⦃a b : α⦄, r a b → ¬r b a

theorem total_def {α : Sort u_1} {r : α → α → Prop} : Std.Total r ↔ ∀ ⦃a b : α⦄, r a b ∨ r b a

theorem trichotomous_def {α : Sort u_1} {r : α → α → Prop} : Std.Trichotomous r ↔ ∀ ⦃a b : α⦄, ¬r a b → ¬r b a → a = b

@[instance 90]

instance asymm_of_isTrans_of_irrefl {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] [Std.Irrefl r] : Std.Asymm r

instance Std.Irrefl.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [Irrefl r] : Irrefl fun (a b : α) => Decidable.decide (r a b) = true

instance Std.Refl.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [Refl r] : Refl fun (a b : α) => Decidable.decide (r a b) = true

instance IsTrans.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [IsTrans α r] : IsTrans α fun (a b : α) => Decidable.decide (r a b) = true

instance Std.Symm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [Symm r] : Symm fun (a b : α) => Decidable.decide (r a b) = true

instance Std.Antisymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [Antisymm r] : Antisymm fun (a b : α) => Decidable.decide (r a b) = true

instance Std.Asymm.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [Asymm r] : Asymm fun (a b : α) => Decidable.decide (r a b) = true

instance Std.Total.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [Total r] : Total fun (a b : α) => Decidable.decide (r a b) = true

instance Std.Trichotomous.decide {α : Sort u_1} {r : α → α → Prop} [DecidableRel r] [Trichotomous r] : Trichotomous fun (a b : α) => Decidable.decide (r a b) = true

@[elab_without_expected_type]

theorem irrefl_of {α : Sort u_1} (r : α → α → Prop) [Std.Irrefl r] (a : α) : ¬r a a

@[elab_without_expected_type]

theorem refl_of {α : Sort u_1} (r : α → α → Prop) [Std.Refl r] (a : α) : r a a

@[elab_without_expected_type]

theorem trans_of {α : Sort u_1} (r : α → α → Prop) {a b c : α} [IsTrans α r] : r a b → r b c → r a c

@[elab_without_expected_type]

theorem symm_of {α : Sort u_1} (r : α → α → Prop) {a b : α} [Std.Symm r] : r a b → r b a

@[elab_without_expected_type]

theorem asymm_of {α : Sort u_1} (r : α → α → Prop) {a b : α} [Std.Asymm r] : r a b → ¬r b a

@[elab_without_expected_type]

theorem total_of {α : Sort u_1} (r : α → α → Prop) [Std.Total r] (a b : α) : r a b ∨ r b a

@[elab_without_expected_type]

theorem trichotomous_of {α : Sort u_1} (r : α → α → Prop) [Std.Trichotomous r] (a b : α) : r a b ∨ a = b ∨ r b a

theorem stdIsPreorder_iff {α : Type u_2} [LE α] : Std.IsPreorder α ↔ IsPreorder α fun (x1 x2 : α) => x1 ≤ x2

theorem stdIsPartialOrder_iff {α : Type u_2} [LE α] : Std.IsPartialOrder α ↔ IsPartialOrder α fun (x1 x2 : α) => x1 ≤ x2

theorem stdIsLinearOrder_iff {α : Type u_2} [LE α] : Std.IsLinearOrder α ↔ IsLinearOrder α fun (x1 x2 : α) => x1 ≤ x2

@[deprecated Std.Symm (since := "2026-06-10")]

def Symmetric {α : Sort u_1} (r : α → α → Prop) : Prop

Std.Symm as a definition, suitable for use in proofs.

Equations

• Symmetric r = ∀ ⦃x y : α⦄, r x y → r y x

theorem Equivalence.stdRefl {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Std.Refl r

theorem Equivalence.stdSymm {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Std.Symm r

@[deprecated Equivalence.stdSymm (since := "2026-06-10")]

theorem Equivalence.symmetric {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : Std.Symm r

Alias of Equivalence.stdSymm.

theorem Equivalence.isTrans {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : IsTrans α r

theorem Equivalence.isEquiv {α : Sort u_1} (r : α → α → Prop) (h : Equivalence r) : IsEquiv α r

instance InvImage.isTrans {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [IsTrans β r] : IsTrans α (InvImage r f)

instance InvImage.irrefl {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [Std.Irrefl r] : Std.Irrefl (InvImage r f)

Minimal and maximal

def Minimal {α : Type u_1} [LE α] (P : α → Prop) (x : α) : Prop

Minimal P x means that x is a minimal element satisfying P.

Equations

• Minimal P x = (P x ∧ ∀ ⦃y : α⦄, P y → y ≤ x → x ≤ y)

def Maximal {α : Type u_1} [LE α] (P : α → Prop) (x : α) : Prop

Maximal P x means that x is a maximal element satisfying P.

Equations

• Maximal P x = (P x ∧ ∀ ⦃y : α⦄, P y → x ≤ y → y ≤ x)

theorem Minimal.prop {α : Type u_1} [LE α] {P : α → Prop} {x : α} (h : Minimal P x) : P x

theorem Maximal.prop {α : Type u_1} [LE α] {P : α → Prop} {x : α} (h : Maximal P x) : P x

theorem Minimal.le_of_le {α : Type u_1} [LE α] {P : α → Prop} {x y : α} (h : Minimal P x) (hy : P y) (hle : y ≤ x) : x ≤ y

theorem Maximal.le_of_ge {α : Type u_1} [LE α] {P : α → Prop} {x y : α} (h : Maximal P x) (hy : P y) (hle : x ≤ y) : y ≤ x

def MinimalFor {ι : Sort u_1} {α : Type u_2} [LE α] (P : ι → Prop) (f : ι → α) (i : ι) : Prop

MinimalFor P f i means that f i is minimal over all i satisfying P.

Equations

• MinimalFor P f i = (P i ∧ ∀ ⦃j : ι⦄, P j → f j ≤ f i → f i ≤ f j)

def MaximalFor {ι : Sort u_1} {α : Type u_2} [LE α] (P : ι → Prop) (f : ι → α) (i : ι) : Prop

MaximalFor P f i means that f i is maximal over all i satisfying P.

Equations

• MaximalFor P f i = (P i ∧ ∀ ⦃j : ι⦄, P j → f i ≤ f j → f j ≤ f i)

theorem MinimalFor.prop {ι : Sort u_1} {α : Type u_2} [LE α] {P : ι → Prop} {f : ι → α} {i : ι} (h : MinimalFor P f i) : P i

theorem MaximalFor.prop {ι : Sort u_1} {α : Type u_2} [LE α] {P : ι → Prop} {f : ι → α} {i : ι} (h : MaximalFor P f i) : P i

theorem MinimalFor.le_of_le {ι : Sort u_1} {α : Type u_2} [LE α] {P : ι → Prop} {f : ι → α} {i j : ι} (h : MinimalFor P f i) (hj : P j) (hji : f j ≤ f i) : f i ≤ f j

theorem MaximalFor.le_of_le {ι : Sort u_1} {α : Type u_2} [LE α] {P : ι → Prop} {f : ι → α} {i j : ι} (h : MaximalFor P f i) (hj : P j) (hji : f i ≤ f j) : f j ≤ f i

Upper and lower sets

def IsUpperSet {α : Type u_1} [LE α] (s : Set α) : Prop

An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

Equations

• IsUpperSet s = ∀ ⦃a b : α⦄, a ≤ b → a ∈ s → b ∈ s

def IsLowerSet {α : Type u_1} [LE α] (s : Set α) : Prop

A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

Equations

• IsLowerSet s = ∀ ⦃a b : α⦄, b ≤ a → a ∈ s → b ∈ s

structure UpperSet (α : Type u_1) [LE α] : Type u_1

An upper set in an order α is a set such that any element greater than one of its members is also a member. Also called up-set, upward-closed set.

• carrier : Set α

  The carrier of an UpperSet.

• upper' : IsUpperSet self.carrier

  The carrier of an UpperSet is an upper set.

structure LowerSet (α : Type u_1) [LE α] : Type u_1

A lower set in an order α is a set such that any element less than one of its members is also a member. Also called down-set, downward-closed set.

• carrier : Set α

  The carrier of a LowerSet.

• lower' : IsLowerSet self.carrier

  The carrier of a LowerSet is a lower set.

def IsRelUpperSet {α : Type u_1} [LE α] (s : Set α) (P : α → Prop) : Prop

An upper set relative to a predicate P is a set such that all elements satisfy P and any element greater than one of its members and satisfying P is also a member.

Equations

• IsRelUpperSet s P = ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s

def IsRelLowerSet {α : Type u_1} [LE α] (s : Set α) (P : α → Prop) : Prop

A lower set relative to a predicate P is a set such that all elements satisfy P and any element less than one of its members and satisfying P is also a member.

Equations

• IsRelLowerSet s P = ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ s

structure RelUpperSet {α : Type u_1} [LE α] (P : α → Prop) : Type u_1

An upper set relative to a predicate P is a set such that all elements satisfy P and any element greater than one of its members and satisfying P is also a member.

• carrier : Set α

  The carrier of a RelUpperSet.

• isRelUpperSet' : IsRelUpperSet self.carrier P

  The carrier of a RelUpperSet is an upper set relative to P.

  Do NOT use directly. Please use RelUpperSet.isRelUpperSet instead.

structure RelLowerSet {α : Type u_1} [LE α] (P : α → Prop) : Type u_1

A lower set relative to a predicate P is a set such that all elements satisfy P and any element less than one of its members and satisfying P is also a member.

• carrier : Set α

  The carrier of a RelLowerSet.

• isRelLowerSet' : IsRelLowerSet self.carrier P

  The carrier of a RelLowerSet is a lower set relative to P.

  Do NOT use directly. Please use RelLowerSet.isRelLowerSet instead.

theorem of_eq {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] {a b : α} : a = b → r a b

theorem comm {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] {a b : α} : r a b ↔ r b a

theorem antisymm' {α : Sort u_1} {r : α → α → Prop} [Std.Antisymm r] {a b : α} : r a b → r b a → b = a

theorem antisymm_iff {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] [Std.Antisymm r] {a b : α} : r a b ∧ r b a ↔ a = b

@[elab_without_expected_type]

theorem antisymm_of {α : Sort u_1} (r : α → α → Prop) [Std.Antisymm r] {a b : α} : r a b → r b a → a = 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' {α : Sort u_1} (r : α → α → Prop) [Std.Antisymm r] {a b : α} : r a b → r b a → b = 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 {α : Sort u_1} (r : α → α → Prop) [Std.Symm 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 Std.Asymm.antisymm {α : Sort u_1} (r : α → α → Prop) [Asymm r] : Antisymm r

theorem Std.Asymm.irrefl {α : Sort u_1} {r : α → α → Prop} [Asymm r] : Irrefl r

theorem Std.Total.trichotomous {α : Sort u_1} (r : α → α → Prop) [Total r] : Trichotomous r

@[instance 100]

instance Std.Total.to_refl {α : Sort u_1} (r : α → α → Prop) [Total r] : Refl r

theorem ne_of_irrefl {α : Sort u_1} {r : α → α → Prop} [Std.Irrefl r] {x y : α} : r x y → x ≠ y

theorem ne_of_irrefl' {α : Sort u_1} {r : α → α → Prop} [Std.Irrefl r] {x y : α} : r x y → y ≠ x

theorem not_rel_of_subsingleton {α : Sort u_1} (r : α → α → Prop) [Std.Irrefl r] [Subsingleton α] (x y : α) : ¬r x y

theorem rel_of_subsingleton {α : Sort u_1} (r : α → α → Prop) [Std.Refl r] [Subsingleton α] (x y : α) : r x y

@[simp]

theorem empty_relation_apply {α : Sort u_1} (a b : α) : emptyRelation a b ↔ False

instance instIrreflEmptyRelation_mathlib {α : Sort u_1} : Std.Irrefl emptyRelation

theorem rel_congr_left {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] {a b c : α} (h : r a b) : r a c ↔ r b c

theorem rel_congr_right {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] {a b c : α} (h : r b c) : r a b ↔ r a c

theorem rel_congr {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] {a b c d : α} (h₁ : r a b) (h₂ : r c d) : r a c ↔ r b d

theorem trans_trichotomous_left {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] [Std.Trichotomous r] {a b c : α} (h₁ : ¬r b a) (h₂ : r b c) : r a c

theorem trans_trichotomous_right {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] [Std.Trichotomous r] {a b c : α} (h₁ : r a b) (h₂ : ¬r c b) : r a c

theorem extensional_of_trichotomous_of_irrefl {α : Sort u_1} (r : α → α → Prop) [Std.Trichotomous r] [Std.Irrefl 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.