Skip to content

Commit c99eb62

Browse files
vihdzpvihdzp
committed
feat(Order/Comparable): comparability/incomparability relations (#19580)
We define two new relations for comparability and incomparability in a preorder, and introduce basic API for them. See [this comment](#19580 (comment)) for an explanation of why we want both. This will be used in the new [CGT repo](https://github.com/vihdzp/combinatorial-games) to define the fuzzy relation `x ‖ y = IncompRel (· ≤ ·) x y`.
1 parent b523ce8 commit c99eb62

File tree

3 files changed

+311
-3
lines changed

3 files changed

+311
-3
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4371,6 +4371,7 @@ import Mathlib.Order.Closure
43714371
import Mathlib.Order.Cofinal
43724372
import Mathlib.Order.CompactlyGenerated.Basic
43734373
import Mathlib.Order.CompactlyGenerated.Intervals
4374+
import Mathlib.Order.Comparable
43744375
import Mathlib.Order.Compare
43754376
import Mathlib.Order.CompleteBooleanAlgebra
43764377
import Mathlib.Order.CompleteLattice

‎Mathlib/Order/Antisymmetrization.lean‎

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,9 @@ def AntisymmRel (a b : α) : Prop :=
4242
theorem antisymmRel_swap : AntisymmRel (swap r) = AntisymmRel r :=
4343
funext₂ fun _ _ ↦ propext and_comm
4444

45+
theorem antisymmRel_swap_apply : AntisymmRel (swap r) a b ↔ AntisymmRel r a b :=
46+
and_comm
47+
4548
@[refl]
4649
theorem AntisymmRel.refl [IsRefl α r] (a : α) : AntisymmRel r a a :=
4750
⟨_root_.refl _, _root_.refl _⟩
@@ -87,11 +90,17 @@ theorem antisymmRel_iff_eq [IsRefl α r] [IsAntisymm α r] : AntisymmRel r a b
8790

8891
alias ⟨AntisymmRel.eq, _⟩ := antisymmRel_iff_eq
8992

90-
theorem AntisymmRel.le [LE α] (h : AntisymmRel (· ≤ ·) a b) : a ≤ b := h.1
91-
theorem AntisymmRel.ge [LE α] (h : AntisymmRel (· ≤ ·) a b) : b ≤ a := h.2
92-
9393
end Relation
9494

95+
section LE
96+
97+
variable [LE α]
98+
99+
theorem AntisymmRel.le (h : AntisymmRel (· ≤ ·) a b) : a ≤ b := h.1
100+
theorem AntisymmRel.ge (h : AntisymmRel (· ≤ ·) a b) : b ≤ a := h.2
101+
102+
end LE
103+
95104
section IsPreorder
96105

97106
variable (α) (r : α → α → Prop) [IsPreorder α r]

‎Mathlib/Order/Comparable.lean‎

Lines changed: 298 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,298 @@
1+
/-
2+
Copyright (c) 2025 Violeta Hernández Palacios. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Violeta Hernández Palacios
5+
-/
6+
import Mathlib.Order.Antisymmetrization
7+
8+
/-!
9+
# Comparability and incomparability relations
10+
11+
Two values in a preorder are said to be comparable whenever `a ≤ b` or `b ≤ a`. We define both the
12+
comparability and incomparability relations.
13+
14+
In a linear order, `CompRel (· ≤ ·) a b` is always true, and `IncompRel (· ≤ ·) a b` is always
15+
false.
16+
17+
## Implementation notes
18+
19+
Although comparability and incomparability are negations of each other, both relations are
20+
convenient in different contexts, and as such, it's useful to keep them distinct. To move from one
21+
to the other, use `not_compRel_iff` and `not_incompRel_iff`.
22+
23+
## Main declarations
24+
25+
* `CompRel`: The comparability relation. `CompRel r a b` means that `a` and `b` is related in
26+
either direction by `r`.
27+
* `IncompRel`: The incomparability relation. `IncompRel r a b` means that `a` and `b` are related in
28+
neither direction by `r`.
29+
30+
## Todo
31+
32+
These definitions should be linked to `IsChain` and `IsAntichain`.
33+
-/
34+
35+
open Function
36+
37+
variable {α : Type*} {a b c d : α}
38+
39+
/-! ### Comparability -/
40+
41+
section Relation
42+
43+
variable {r : α → α → Prop}
44+
45+
/-- The comparability relation `CompRel r a b` means that either `r a b` or `r b a`. -/
46+
def CompRel (r : α → α → Prop) (a b : α) : Prop :=
47+
r a b ∨ r b a
48+
49+
theorem CompRel.of_rel (h : r a b) : CompRel r a b :=
50+
Or.inl h
51+
52+
theorem CompRel.of_rel_symm (h : r b a) : CompRel r a b :=
53+
Or.inr h
54+
55+
theorem compRel_swap (r : α → α → Prop) : CompRel (swap r) = CompRel r :=
56+
funext₂ fun _ _ ↦ propext or_comm
57+
58+
theorem compRel_swap_apply (r : α → α → Prop) : CompRel (swap r) a b ↔ CompRel r a b :=
59+
or_comm
60+
61+
@[refl]
62+
theorem CompRel.refl (r : α → α → Prop) [IsRefl α r] (a : α) : CompRel r a a :=
63+
.of_rel (_root_.refl _)
64+
65+
theorem CompRel.rfl [IsRefl α r] : CompRel r a a := .refl ..
66+
67+
instance [IsRefl α r] : IsRefl α (CompRel r) where
68+
refl := .refl r
69+
70+
@[symm]
71+
theorem CompRel.symm : CompRel r a b → CompRel r b a :=
72+
Or.symm
73+
74+
instance : IsSymm α (CompRel r) where
75+
symm _ _ := CompRel.symm
76+
77+
theorem compRel_comm {a b : α} : CompRel r a b ↔ CompRel r b a :=
78+
comm
79+
80+
instance CompRel.decidableRel [DecidableRel r] : DecidableRel (CompRel r) :=
81+
fun _ _ ↦ inferInstanceAs (Decidable (_ ∨ _))
82+
83+
theorem AntisymmRel.compRel (h : AntisymmRel r a b) : CompRel r a b :=
84+
Or.inl h.1
85+
86+
@[simp]
87+
theorem IsTotal.compRel [IsTotal α r] (a b : α) : CompRel r a b :=
88+
IsTotal.total a b
89+
90+
end Relation
91+
92+
section LE
93+
94+
variable [LE α]
95+
96+
theorem CompRel.of_le (h : a ≤ b) : CompRel (· ≤ ·) a b := .of_rel h
97+
theorem CompRel.of_ge (h : b ≤ a) : CompRel (· ≤ ·) a b := .of_rel_symm h
98+
99+
alias LE.le.compRel := CompRel.of_le
100+
alias LE.le.compRel_symm := CompRel.of_ge
101+
102+
end LE
103+
104+
section Preorder
105+
106+
variable [Preorder α]
107+
108+
theorem CompRel.of_lt (h : a < b) : CompRel (· ≤ ·) a b := h.le.compRel
109+
theorem CompRel.of_gt (h : b < a) : CompRel (· ≤ ·) a b := h.le.compRel_symm
110+
111+
alias LT.lt.compRel := CompRel.of_lt
112+
alias LT.lt.compRel_symm := CompRel.of_gt
113+
114+
@[trans]
115+
theorem CompRel.of_compRel_of_antisymmRel
116+
(h₁ : CompRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) b c) : CompRel (· ≤ ·) a c := by
117+
obtain (h | h) := h₁
118+
· exact (h.trans h₂.le).compRel
119+
· exact (h₂.ge.trans h).compRel_symm
120+
121+
alias CompRel.trans_antisymmRel := CompRel.of_compRel_of_antisymmRel
122+
123+
instance : @Trans α α α (CompRel (· ≤ ·)) (AntisymmRel (· ≤ ·)) (CompRel (· ≤ ·)) where
124+
trans := CompRel.of_compRel_of_antisymmRel
125+
126+
@[trans]
127+
theorem CompRel.of_antisymmRel_of_compRel
128+
(h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : CompRel (· ≤ ·) b c) : CompRel (· ≤ ·) a c :=
129+
(h₂.symm.trans_antisymmRel h₁.symm).symm
130+
131+
alias AntisymmRel.trans_compRel := CompRel.of_antisymmRel_of_compRel
132+
133+
instance : @Trans α α α (AntisymmRel (· ≤ ·)) (CompRel (· ≤ ·)) (CompRel (· ≤ ·)) where
134+
trans := CompRel.of_antisymmRel_of_compRel
135+
136+
theorem AntisymmRel.compRel_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) :
137+
CompRel (· ≤ ·) a c ↔ CompRel (· ≤ ·) b d where
138+
mp h := (h₁.symm.trans_compRel h).trans_antisymmRel h₂
139+
mpr h := (h₁.trans_compRel h).trans_antisymmRel h₂.symm
140+
141+
theorem AntisymmRel.compRel_congr_left (h : AntisymmRel (· ≤ ·) a b) :
142+
CompRel (· ≤ ·) a c ↔ CompRel (· ≤ ·) b c :=
143+
h.compRel_congr .rfl
144+
145+
theorem AntisymmRel.compRel_congr_right (h : AntisymmRel (· ≤ ·) b c) :
146+
CompRel (· ≤ ·) a b ↔ CompRel (· ≤ ·) a c :=
147+
AntisymmRel.rfl.compRel_congr h
148+
149+
end Preorder
150+
151+
/-- A partial order where any two elements are comparable is a linear order. -/
152+
def linearOrderOfComprel [PartialOrder α] [dec : DecidableLE α]
153+
(h : ∀ a b : α, CompRel (· ≤ ·) a b) : LinearOrder α where
154+
le_total := h
155+
decidableLE := dec
156+
157+
/-! ### Incomparability relation -/
158+
159+
section Relation
160+
161+
variable (r : α → α → Prop)
162+
163+
/-- The incomparability relation `IncompRel r a b` means `¬ r a b` and `¬ r b a`. -/
164+
def IncompRel (a b : α) : Prop :=
165+
¬ r a b ∧ ¬ r b a
166+
167+
@[simp]
168+
theorem antisymmRel_compl : AntisymmRel rᶜ = IncompRel r :=
169+
rfl
170+
171+
theorem antisymmRel_compl_apply : AntisymmRel rᶜ a b ↔ IncompRel r a b :=
172+
.rfl
173+
174+
@[simp]
175+
theorem incompRel_compl : IncompRel rᶜ = AntisymmRel r := by
176+
simp [← antisymmRel_compl, AntisymmRel, compl]
177+
178+
@[simp]
179+
theorem incompRel_compl_apply : IncompRel rᶜ a b ↔ AntisymmRel r a b := by
180+
simp
181+
182+
theorem incompRel_swap : IncompRel (swap r) = IncompRel r :=
183+
antisymmRel_swap rᶜ
184+
185+
theorem incompRel_swap_apply : IncompRel (swap r) a b ↔ IncompRel r a b :=
186+
antisymmRel_swap_apply rᶜ
187+
188+
@[refl]
189+
theorem IncompRel.refl [IsIrrefl α r] (a : α) : IncompRel r a a :=
190+
AntisymmRel.refl rᶜ a
191+
192+
variable {r} in
193+
theorem IncompRel.rfl [IsIrrefl α r] {a : α} : IncompRel r a a := .refl ..
194+
195+
instance [IsIrrefl α r] : IsRefl α (IncompRel r) where
196+
refl := .refl r
197+
198+
variable {r}
199+
200+
@[symm]
201+
theorem IncompRel.symm : IncompRel r a b → IncompRel r b a :=
202+
And.symm
203+
204+
instance : IsSymm α (IncompRel r) where
205+
symm _ _ := IncompRel.symm
206+
207+
theorem incompRel_comm {a b : α} : IncompRel r a b ↔ IncompRel r b a :=
208+
comm
209+
210+
instance IncompRel.decidableRel [DecidableRel r] : DecidableRel (IncompRel r) :=
211+
fun _ _ ↦ inferInstanceAs (Decidable (¬ _ ∧ ¬ _))
212+
213+
theorem IncompRel.not_antisymmRel (h : IncompRel r a b) : ¬ AntisymmRel r a b :=
214+
fun h' ↦ h.1 h'.1
215+
216+
theorem AntisymmRel.not_incompRel (h : AntisymmRel r a b) : ¬ IncompRel r a b :=
217+
fun h' ↦ h'.1 h.1
218+
219+
theorem not_compRel_iff : ¬ CompRel r a b ↔ IncompRel r a b := by
220+
simp [CompRel, IncompRel]
221+
222+
theorem not_incompRel_iff : ¬ IncompRel r a b ↔ CompRel r a b := by
223+
rw [← not_compRel_iff, not_not]
224+
225+
@[simp]
226+
theorem IsTotal.not_incompRel [IsTotal α r] (a b : α) : ¬ IncompRel r a b := by
227+
rw [not_incompRel_iff]
228+
exact IsTotal.compRel a b
229+
230+
end Relation
231+
232+
section LE
233+
234+
variable [LE α]
235+
236+
theorem IncompRel.not_le (h : IncompRel (· ≤ ·) a b) : ¬ a ≤ b := h.1
237+
theorem IncompRel.not_ge (h : IncompRel (· ≤ ·) a b) : ¬ b ≤ a := h.2
238+
theorem LE.le.not_incompRel (h : a ≤ b) : ¬ IncompRel (· ≤ ·) a b := fun h' ↦ h'.not_le h
239+
240+
end LE
241+
242+
section Preorder
243+
244+
variable [Preorder α]
245+
246+
theorem IncompRel.not_lt (h : IncompRel (· ≤ ·) a b) : ¬ a < b := mt le_of_lt h.not_le
247+
theorem IncompRel.not_gt (h : IncompRel (· ≤ ·) a b) : ¬ b < a := mt le_of_lt h.not_ge
248+
theorem LT.lt.not_incompRel (h : a < b) : ¬ IncompRel (· ≤ ·) a b := fun h' ↦ h'.not_lt h
249+
250+
theorem not_le_iff_lt_or_incompRel : ¬ b ≤ a ↔ a < b ∨ IncompRel (· ≤ ·) a b := by
251+
rw [lt_iff_le_not_le, IncompRel]
252+
tauto
253+
254+
/-- Exactly one of the following is true. -/
255+
theorem lt_or_antisymmRel_or_gt_or_incompRel (a b : α) :
256+
a < b ∨ AntisymmRel (· ≤ ·) a b ∨ b < a ∨ IncompRel (· ≤ ·) a b := by
257+
simp_rw [lt_iff_le_not_le]
258+
tauto
259+
260+
@[trans]
261+
theorem incompRel_of_incompRel_of_antisymmRel
262+
(h₁ : IncompRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) b c) : IncompRel (· ≤ ·) a c :=
263+
⟨fun h ↦ h₁.not_le (h.trans h₂.ge), fun h ↦ h₁.not_ge (h₂.le.trans h)⟩
264+
265+
alias IncompRel.trans_antisymmRel := incompRel_of_incompRel_of_antisymmRel
266+
267+
instance : @Trans α α α (IncompRel (· ≤ ·)) (AntisymmRel (· ≤ ·)) (IncompRel (· ≤ ·)) where
268+
trans := incompRel_of_incompRel_of_antisymmRel
269+
270+
@[trans]
271+
theorem incompRel_of_antisymmRel_of_incompRel
272+
(h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : IncompRel (· ≤ ·) b c) : IncompRel (· ≤ ·) a c :=
273+
(h₂.symm.trans_antisymmRel h₁.symm).symm
274+
275+
alias AntisymmRel.trans_incompRel := incompRel_of_antisymmRel_of_incompRel
276+
277+
instance : @Trans α α α (AntisymmRel (· ≤ ·)) (IncompRel (· ≤ ·)) (IncompRel (· ≤ ·)) where
278+
trans := incompRel_of_antisymmRel_of_incompRel
279+
280+
theorem AntisymmRel.incompRel_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) :
281+
IncompRel (· ≤ ·) a c ↔ IncompRel (· ≤ ·) b d where
282+
mp h := (h₁.symm.trans_incompRel h).trans_antisymmRel h₂
283+
mpr h := (h₁.trans_incompRel h).trans_antisymmRel h₂.symm
284+
285+
theorem AntisymmRel.incompRel_congr_left (h : AntisymmRel (· ≤ ·) a b) :
286+
IncompRel (· ≤ ·) a c ↔ IncompRel (· ≤ ·) b c :=
287+
h.incompRel_congr AntisymmRel.rfl
288+
289+
theorem AntisymmRel.incompRel_congr_right (h : AntisymmRel (· ≤ ·) b c) :
290+
IncompRel (· ≤ ·) a b ↔ IncompRel (· ≤ ·) a c :=
291+
AntisymmRel.rfl.incompRel_congr h
292+
293+
end Preorder
294+
295+
/-- Exactly one of the following is true. -/
296+
theorem lt_or_eq_or_gt_or_incompRel [PartialOrder α] (a b : α) :
297+
a < b ∨ a = b ∨ b < a ∨ IncompRel (· ≤ ·) a b := by
298+
simpa using lt_or_antisymmRel_or_gt_or_incompRel a b

0 commit comments

Comments
 (0)