Comparability and incomparability relations

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

In a linear order, CompRel (· ≤ ·) 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_compRel_iff and not_incompRel_iff.

Main declarations

• CompRel: The comparability relation. CompRel r a b means that a and b is related in either direction by r.
• 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

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.

Equations

• CompRel r a b = (r a b ∨ r b a)

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

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

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

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

@[simp]

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

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

instance instIsReflCompRel {α : Type u_1} {r : α → α → Prop} [IsRefl α r] : IsRefl α (CompRel r)

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

instance instIsSymmCompRel {α : Type u_1} {r : α → α → Prop} : IsSymm α (CompRel r)

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

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

Equations

• CompRel.decidableRel x✝¹ x✝ = inferInstanceAs (Decidable (r x✝¹ x✝ ∨ r x✝ x✝¹))

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

@[simp]

theorem IsTotal.compRel {α : Type u_1} {r : α → α → Prop} [IsTotal α r] (a b : α) : CompRel r a b

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

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.

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

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.

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.

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)

Equations

• instTransCompRelLeAntisymmRel = { trans := ⋯ }

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.

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)

Equations

• instTransAntisymmRelLeCompRel = { trans := ⋯ }

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

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

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 linearOrderOfComprel {α : Type u_1} [PartialOrder α] [dec : DecidableLE α] (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.

Equations

• linearOrderOfComprel h = LinearOrder.mk h dec decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

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.

Equations

• IncompRel r a b = (¬r a b ∧ ¬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) [IsIrrefl α r] (a : α) : IncompRel r a a

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

instance instIsReflIncompRelOfIsIrrefl {α : Type u_1} (r : α → α → Prop) [IsIrrefl α r] : IsRefl α (IncompRel r)

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

instance instIsSymmIncompRel {α : Type u_1} {r : α → α → Prop} : IsSymm α (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)

Equations

• IncompRel.decidableRel x✝¹ x✝ = inferInstanceAs (Decidable (¬r x✝¹ x✝ ∧ ¬r x✝ x✝¹))

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_compRel_iff {α : Type u_1} {a b : α} {r : α → α → Prop} : ¬CompRel r a b ↔ IncompRel r a b

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

@[simp]

theorem IsTotal.not_incompRel {α : Type u_1} {r : α → α → Prop} [IsTotal α r] (a b : α) : ¬IncompRel r 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)

Equations

• instTransIncompRelLeAntisymmRel = { trans := ⋯ }

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)

Equations

• instTransAntisymmRelLeIncompRel = { trans := ⋯ }

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.