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

@[instance_reducible]

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.

Equations

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

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) [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_reducible]

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

Equations

• IncompRel.decidableRel x✝¹ x✝ = IncompRel.decidableRel._aux_1 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_symmGen_iff {α : Type u_1} {a b : α} {r : α → α → Prop} : ¬Relation.SymmGen 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

@[simp]

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

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_reducible]

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_reducible]

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.