Comparability and incomparability relations

Two values in a preorder are said to be comparable (SymmRel) whenever a ≤ b or b ≤ a. We define both the comparability and incomparability relations.

In a linear order, SymmGen (· ≤ ·) a b is always true, and IncompRel (· ≤ ·) a b is always false.

Implementation notes

Although comparability and incomparability are negations of each other, both relations are convenient in different contexts, and as such, it's useful to keep them distinct. To move from one to the other, use not_symmGen_iff and not_incompRel_iff_symmGen.

Main declarations

• CompRel: The comparability relation. CompRel r a b means that a and b is related in either direction by r. This is deprecated in favor of Relation.SymmGen, with naming chosen for consistency with Relation.TransGen in core and other definitions in Mathlib.Logic.Relation.
• IncompRel: The incomparability relation. IncompRel r a b means that a and b are related in neither direction by r.

Todo

These definitions should be linked to IsChain and IsAntichain.

Comparability

@[deprecated Relation.SymmGen (since := "2026-01-25")]

def CompRel {α : Type u_1} (r : α → α → Prop) (a b : α) : Prop

The comparability relation CompRel r a b means that either r a b or r b a.

@[deprecated Relation.SymmGen.of_rel (since := "2026-01-25")]

theorem CompRel.of_rel {α : Type u_1} {a b : α} {r : α → α → Prop} (h : r a b) : CompRel r a b

@[deprecated Relation.SymmGen.of_rel_symm (since := "2026-01-25")]

theorem CompRel.of_rel_symm {α : Type u_1} {a b : α} {r : α → α → Prop} (h : r b a) : CompRel r a b

@[deprecated Relation.symmGen_swap (since := "2026-01-25")]

theorem compRel_swap {α : Type u_1} (r : α → α → Prop) : CompRel (Function.swap r) = CompRel r

@[deprecated Relation.symmGen_swap_apply (since := "2026-01-25")]

theorem compRel_swap_apply {α : Type u_1} {a b : α} (r : α → α → Prop) : CompRel (Function.swap r) a b ↔ CompRel r a b

@[simp, deprecated Relation.SymmGen.refl (since := "2026-01-25")]

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

@[deprecated Relation.SymmGen.rfl (since := "2026-01-25")]

theorem CompRel.rfl {α : Type u_1} {a : α} {r : α → α → Prop} [Std.Refl r] : CompRel r a a

@[deprecated Relation.SymmGen.instRefl (since := "2026-01-25")]

instance instReflCompRel {α : Type u_1} {r : α → α → Prop} [Std.Refl r] : Std.Refl (CompRel r)

@[deprecated Relation.SymmGen.symm (since := "2026-01-25")]

theorem CompRel.symm {α : Type u_1} {a b : α} {r : α → α → Prop} : CompRel r a b → CompRel r b a

@[deprecated Relation.SymmGen.instSymm (since := "2026-01-25")]

instance instSymmCompRel {α : Type u_1} {r : α → α → Prop} : Std.Symm (CompRel r)

@[deprecated Relation.symmGen_comm (since := "2026-01-25")]

theorem compRel_comm {α : Type u_1} {r : α → α → Prop} {a b : α} : CompRel r a b ↔ CompRel r b a

@[deprecated Relation.SymmGen.decidableRel (since := "2026-01-25")]

instance CompRel.decidableRel {α : Type u_1} {r : α → α → Prop} [DecidableRel r] : DecidableRel (CompRel r)

@[deprecated AntisymmRel.symmGen (since := "2026-01-25")]

theorem AntisymmRel.compRel {α : Type u_1} {a b : α} {r : α → α → Prop} (h : AntisymmRel r a b) : CompRel r a b

@[simp, deprecated Relation.symmGen_of_total (since := "2026-01-25")]

theorem compRel_of_total {α : Type u_1} {r : α → α → Prop} [Std.Total r] (a b : α) : CompRel r a b

@[deprecated Relation.symmGen_of_total (since := "2026-01-13")]

theorem IsTotal.compRel {α : Sort u_1} {r : α → α → Prop} [Std.Total r] (a b : α) : Relation.SymmGen r a b

Alias of Relation.symmGen_of_total.

@[deprecated Relation.SymmGen.of_le (since := "2026-01-25")]

theorem CompRel.of_le {α : Type u_1} {a b : α} [LE α] (h : a ≤ b) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

@[deprecated Relation.SymmGen.of_ge (since := "2026-01-25")]

theorem CompRel.of_ge {α : Type u_1} {a b : α} [LE α] (h : b ≤ a) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

theorem LE.le.compRel {α : Type u_1} {a b : α} [LE α] (h : a ≤ b) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

Alias of CompRel.of_le.

theorem LE.le.compRel_symm {α : Type u_1} {a b : α} [LE α] (h : b ≤ a) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

Alias of CompRel.of_ge.

@[deprecated Relation.SymmGen.of_lt (since := "2026-01-25")]

theorem CompRel.of_lt {α : Type u_1} {a b : α} [Preorder α] (h : a < b) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

@[deprecated Relation.SymmGen.of_gt (since := "2026-01-25")]

theorem CompRel.of_gt {α : Type u_1} {a b : α} [Preorder α] (h : b < a) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

theorem LT.lt.compRel {α : Type u_1} {a b : α} [Preorder α] (h : a < b) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

Alias of CompRel.of_lt.

theorem LT.lt.compRel_symm {α : Type u_1} {a b : α} [Preorder α] (h : b < a) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

Alias of CompRel.of_gt.

@[deprecated Relation.SymmGen.of_symmGen_of_antisymmRel (since := "2026-01-25")]

theorem CompRel.of_compRel_of_antisymmRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

theorem CompRel.trans_antisymmRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

Alias of CompRel.of_compRel_of_antisymmRel.

@[deprecated instTransSymmGenLeAntisymmRel (since := "2026-01-25")]

instance instTransCompRelLeAntisymmRel {α : Type u_1} [Preorder α] : Trans (CompRel fun (x1 x2 : α) => x1 ≤ x2) (AntisymmRel fun (x1 x2 : α) => x1 ≤ x2) (CompRel fun (x1 x2 : α) => x1 ≤ x2)

@[deprecated Relation.SymmGen.of_antisymmRel_of_symmGen (since := "2026-01-25")]

theorem CompRel.of_antisymmRel_of_compRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : CompRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

theorem AntisymmRel.trans_compRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : CompRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

Alias of CompRel.of_antisymmRel_of_compRel.

@[deprecated instTransAntisymmRelLeSymmGen (since := "2026-01-25")]

instance instTransAntisymmRelLeCompRel {α : Type u_1} [Preorder α] : Trans (AntisymmRel fun (x1 x2 : α) => x1 ≤ x2) (CompRel fun (x1 x2 : α) => x1 ≤ x2) (CompRel fun (x1 x2 : α) => x1 ≤ x2)

@[deprecated AntisymmRel.symmGen_congr (since := "2026-01-25")]

theorem AntisymmRel.compRel_congr {α : Type u_1} {a b c d : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) c d) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a c ↔ CompRel (fun (x1 x2 : α) => x1 ≤ x2) b d

@[deprecated AntisymmRel.symmGen_congr_left (since := "2026-01-25")]

theorem AntisymmRel.compRel_congr_left {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a c ↔ CompRel (fun (x1 x2 : α) => x1 ≤ x2) b c

@[deprecated AntisymmRel.symmGen_congr_right (since := "2026-01-25")]

theorem AntisymmRel.compRel_congr_right {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b ↔ CompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

def Relation.linearOrderOfSymmGen {α : Type u_1} [PartialOrder α] [decLE : DecidableLE α] [decLT : DecidableLT α] [decEq : DecidableEq α] (h : ∀ (a b : α), SymmGen (fun (x1 x2 : α) => x1 ≤ x2) a b) : LinearOrder α

A partial order where any two elements are comparable is a linear order.

@[deprecated Relation.linearOrderOfSymmGen (since := "2026-01-25")]

def linearOrderOfComprel {α : Type u_1} [PartialOrder α] [decLE : DecidableLE α] [decLT : DecidableLT α] [decEq : DecidableEq α] (h : ∀ (a b : α), CompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : LinearOrder α

A partial order where any two elements are comparable is a linear order.

Incomparability relation

def IncompRel {α : Type u_1} (r : α → α → Prop) (a b : α) : Prop

The incomparability relation IncompRel r a b means ¬ r a b and ¬ r b a.

@[simp]

theorem antisymmRel_compl {α : Type u_1} (r : α → α → Prop) : AntisymmRel rᶜ = IncompRel r

theorem antisymmRel_compl_apply {α : Type u_1} {a b : α} (r : α → α → Prop) : AntisymmRel rᶜ a b ↔ IncompRel r a b

@[simp]

theorem incompRel_compl {α : Type u_1} (r : α → α → Prop) : IncompRel rᶜ = AntisymmRel r

@[simp]

theorem incompRel_compl_apply {α : Type u_1} {a b : α} (r : α → α → Prop) : IncompRel rᶜ a b ↔ AntisymmRel r a b

theorem incompRel_swap {α : Type u_1} (r : α → α → Prop) : IncompRel (Function.swap r) = IncompRel r

theorem incompRel_swap_apply {α : Type u_1} {a b : α} (r : α → α → Prop) : IncompRel (Function.swap r) a b ↔ IncompRel r a b

@[simp]

theorem IncompRel.refl {α : Type u_1} (r : α → α → Prop) [Std.Irrefl r] (a : α) : IncompRel r a a

theorem IncompRel.rfl {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] {a : α} : IncompRel r a a

instance instReflIncompRelOfIrrefl {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] : Std.Refl (IncompRel r)

theorem IncompRel.symm {α : Type u_1} {a b : α} {r : α → α → Prop} : IncompRel r a b → IncompRel r b a

instance instSymmIncompRel {α : Type u_1} {r : α → α → Prop} : Std.Symm (IncompRel r)

theorem incompRel_comm {α : Type u_1} {r : α → α → Prop} {a b : α} : IncompRel r a b ↔ IncompRel r b a

instance IncompRel.decidableRel {α : Type u_1} {r : α → α → Prop} [DecidableRel r] : DecidableRel (IncompRel r)

theorem IncompRel.not_antisymmRel {α : Type u_1} {a b : α} {r : α → α → Prop} (h : IncompRel r a b) : ¬AntisymmRel r a b

theorem AntisymmRel.not_incompRel {α : Type u_1} {a b : α} {r : α → α → Prop} (h : AntisymmRel r a b) : ¬IncompRel r a b

theorem not_symmGen_iff {α : Type u_1} {a b : α} {r : α → α → Prop} : ¬Relation.SymmGen r a b ↔ IncompRel r a b

@[deprecated not_symmGen_iff (since := "2026-01-25")]

theorem not_compRel_iff {α : Type u_1} {a b : α} {r : α → α → Prop} : ¬CompRel r a b ↔ IncompRel r a b

theorem not_incompRel_iff_symmGen {α : Type u_1} {a b : α} {r : α → α → Prop} : ¬IncompRel r a b ↔ Relation.SymmGen r a b

@[deprecated not_incompRel_iff_symmGen (since := "2026-01-25")]

theorem not_incompRel_iff {α : Type u_1} {a b : α} {r : α → α → Prop} : ¬IncompRel r a b ↔ CompRel r a b

@[simp]

theorem not_incompRel_of_total {α : Type u_1} {r : α → α → Prop} [Std.Total r] (a b : α) : ¬IncompRel r a b

@[deprecated not_incompRel_of_total (since := "2026-01-13")]

theorem IsTotal.not_incompRel {α : Type u_1} {r : α → α → Prop} [Std.Total r] (a b : α) : ¬IncompRel r a b

Alias of not_incompRel_of_total.

theorem IncompRel.ne {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {a b : α} (h : IncompRel r a b) : a ≠ b

theorem IncompRel.not_le {α : Type u_1} {a b : α} [LE α] (h : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : ¬a ≤ b

theorem IncompRel.not_ge {α : Type u_1} {a b : α} [LE α] (h : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : ¬b ≤ a

theorem LE.le.not_incompRel {α : Type u_1} {a b : α} [LE α] (h : a ≤ b) : ¬IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

theorem IncompRel.not_lt {α : Type u_1} {a b : α} [Preorder α] (h : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : ¬a < b

theorem IncompRel.not_gt {α : Type u_1} {a b : α} [Preorder α] (h : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : ¬b < a

theorem LT.lt.not_incompRel {α : Type u_1} {a b : α} [Preorder α] (h : a < b) : ¬IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

theorem not_le_iff_lt_or_incompRel {α : Type u_1} {a b : α} [Preorder α] : ¬b ≤ a ↔ a < b ∨ IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

theorem lt_or_antisymmRel_or_gt_or_incompRel {α : Type u_1} [Preorder α] (a b : α) : a < b ∨ AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b ∨ b < a ∨ IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

Exactly one of the following is true.

theorem incompRel_of_incompRel_of_antisymmRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

theorem IncompRel.trans_antisymmRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

Alias of incompRel_of_incompRel_of_antisymmRel.

instance instTransIncompRelLeAntisymmRel {α : Type u_1} [Preorder α] : Trans (IncompRel fun (x1 x2 : α) => x1 ≤ x2) (AntisymmRel fun (x1 x2 : α) => x1 ≤ x2) (IncompRel fun (x1 x2 : α) => x1 ≤ x2)

theorem incompRel_of_antisymmRel_of_incompRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

theorem AntisymmRel.trans_incompRel {α : Type u_1} {a b c : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

Alias of incompRel_of_antisymmRel_of_incompRel.

instance instTransAntisymmRelLeIncompRel {α : Type u_1} [Preorder α] : Trans (AntisymmRel fun (x1 x2 : α) => x1 ≤ x2) (IncompRel fun (x1 x2 : α) => x1 ≤ x2) (IncompRel fun (x1 x2 : α) => x1 ≤ x2)

theorem AntisymmRel.incompRel_congr {α : Type u_1} {a b c d : α} [Preorder α] (h₁ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) (h₂ : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) c d) : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a c ↔ IncompRel (fun (x1 x2 : α) => x1 ≤ x2) b d

theorem AntisymmRel.incompRel_congr_left {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) a b) : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a c ↔ IncompRel (fun (x1 x2 : α) => x1 ≤ x2) b c

theorem AntisymmRel.incompRel_congr_right {α : Type u_1} {a b c : α} [Preorder α] (h : AntisymmRel (fun (x1 x2 : α) => x1 ≤ x2) b c) : IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b ↔ IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a c

theorem lt_or_eq_or_gt_or_incompRel {α : Type u_1} [PartialOrder α] (a b : α) : a < b ∨ a = b ∨ b < a ∨ IncompRel (fun (x1 x2 : α) => x1 ≤ x2) a b

Exactly one of the following is true.