Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit ca79513

Browse files
vihdzpvihdzp
committed
feat(order/bounded): Proved many lemmas about bounded and unbounded sets (#11179)
These include more convenient characterizations of unboundedness in preorders and linear orders, and many results about bounded intervals and initial segments.
1 parent 884d813 commit ca79513

File tree

3 files changed

+344
-2
lines changed

3 files changed

+344
-2
lines changed

‎src/order/bounded.lean‎

Lines changed: 330 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,330 @@
1+
/-
2+
Copyright (c) 2022 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 order.min_max
7+
import order.rel_classes
8+
import data.set.intervals.basic
9+
10+
/-!
11+
# Bounded and unbounded sets
12+
13+
We prove miscellaneous lemmas about bounded and unbounded sets. Many of these are just variations on
14+
the same ideas, or similar results with a few minor differences. The file is divided into these
15+
different general ideas.
16+
-/
17+
18+
variables {α : Type*} {r : α → α → Prop} {s t : set α}
19+
20+
/-! ### Subsets of bounded and unbounded sets -/
21+
22+
theorem bounded.mono (hst : s ⊆ t) (hs : bounded r t) : bounded r s :=
23+
hs.imp $ λ a ha b hb, ha b (hst hb)
24+
25+
theorem unbounded.mono (hst : s ⊆ t) (hs : unbounded r s) : unbounded r t :=
26+
λ a, let ⟨b, hb, hb'⟩ := hs a in ⟨b, hst hb, hb'⟩
27+
28+
/-! ### Alternate characterizations of unboundedness on orders -/
29+
30+
lemma unbounded_le_of_forall_exists_lt [preorder α] (h : ∀ a, ∃ b ∈ s, a < b) : unbounded (≤) s :=
31+
λ a, let ⟨b, hb, hb'⟩ := h a in ⟨b, hb, λ hba, hba.not_lt hb'⟩
32+
33+
lemma unbounded_le_iff [linear_order α] : unbounded (≤) s ↔ ∀ a, ∃ b ∈ s, a < b :=
34+
by simp only [unbounded, not_le]
35+
36+
lemma unbounded_lt_of_forall_exists_le [preorder α] (h : ∀ a, ∃ b ∈ s, a ≤ b) : unbounded (<) s :=
37+
λ a, let ⟨b, hb, hb'⟩ := h a in ⟨b, hb, λ hba, hba.not_le hb'⟩
38+
39+
lemma unbounded_lt_iff [linear_order α] : unbounded (<) s ↔ ∀ a, ∃ b ∈ s, a ≤ b :=
40+
by simp only [unbounded, not_lt]
41+
42+
lemma unbounded_ge_of_forall_exists_gt [preorder α] (h : ∀ a, ∃ b ∈ s, b < a) : unbounded (≥) s :=
43+
@unbounded_le_of_forall_exists_lt (order_dual α) _ _ h
44+
45+
lemma unbounded_ge_iff [linear_order α] : unbounded (≥) s ↔ ∀ a, ∃ b ∈ s, b < a :=
46+
⟨λ h a, let ⟨b, hb, hba⟩ := h a in ⟨b, hb, lt_of_not_ge hba⟩, unbounded_ge_of_forall_exists_gt⟩
47+
48+
lemma unbounded_gt_of_forall_exists_ge [preorder α] (h : ∀ a, ∃ b ∈ s, b ≤ a) : unbounded (>) s :=
49+
λ a, let ⟨b, hb, hb'⟩ := h a in ⟨b, hb, λ hba, not_le_of_gt hba hb'⟩
50+
51+
lemma unbounded_gt_iff [linear_order α] : unbounded (>) s ↔ ∀ a, ∃ b ∈ s, b ≤ a :=
52+
⟨λ h a, let ⟨b, hb, hba⟩ := h a in ⟨b, hb, le_of_not_gt hba⟩, unbounded_gt_of_forall_exists_ge⟩
53+
54+
/-! ### Relation between boundedness by strict and nonstrict orders. -/
55+
56+
/-! #### Less and less or equal -/
57+
58+
lemma bounded.rel_mono {r' : α → α → Prop} (h : bounded r s) (hrr' : r ≤ r') : bounded r' s :=
59+
let ⟨a, ha⟩ := h in ⟨a, λ b hb, hrr' b a (ha b hb)⟩
60+
61+
lemma bounded_le_of_bounded_lt [preorder α] (h : bounded (<) s) : bounded (≤) s :=
62+
h.rel_mono $ λ _ _, le_of_lt
63+
64+
lemma unbounded.rel_mono {r' : α → α → Prop} (hr : r' ≤ r) (h : unbounded r s) : unbounded r' s :=
65+
λ a, let ⟨b, hb, hba⟩ := h a in ⟨b, hb, λ hba', hba (hr b a hba')⟩
66+
67+
lemma unbounded_lt_of_unbounded_le [preorder α] (h : unbounded (≤) s) :
68+
unbounded (<) s :=
69+
h.rel_mono $ λ _ _, le_of_lt
70+
71+
lemma bounded_le_iff_bounded_lt [preorder α] [no_max_order α] : bounded (≤) s ↔ bounded (<) s :=
72+
begin
73+
refine ⟨λ h, _, bounded_le_of_bounded_lt⟩,
74+
cases h with a ha,
75+
cases exists_gt a with b hb,
76+
exact ⟨b, λ c hc, lt_of_le_of_lt (ha c hc) hb⟩
77+
end
78+
79+
lemma unbounded_lt_iff_unbounded_le [preorder α] [no_max_order α] :
80+
unbounded (<) s ↔ unbounded (≤) s :=
81+
by simp_rw [← not_bounded_iff, bounded_le_iff_bounded_lt]
82+
83+
/-! #### Greater and greater or equal -/
84+
85+
lemma bounded_ge_of_bounded_gt [preorder α] (h : bounded (>) s) : bounded (≥) s :=
86+
let ⟨a, ha⟩ := h in ⟨a, λ b hb, le_of_lt (ha b hb)⟩
87+
88+
lemma unbounded_gt_of_unbounded_ge [preorder α] (h : unbounded (≥) s) : unbounded (>) s :=
89+
λ a, let ⟨b, hb, hba⟩ := h a in ⟨b, hb, λ hba', hba (le_of_lt hba')⟩
90+
91+
lemma bounded_ge_iff_bounded_gt [preorder α] [no_min_order α] : bounded (≥) s ↔ bounded (>) s :=
92+
@bounded_le_iff_bounded_lt (order_dual α) _ _ _
93+
94+
lemma unbounded_ge_iff_unbounded_gt [preorder α] [no_min_order α] :
95+
unbounded (≥) s ↔ unbounded (>) s :=
96+
(@unbounded_lt_iff_unbounded_le (order_dual α) _ _ _).symm
97+
98+
/-! ### Bounded and unbounded intervals -/
99+
100+
theorem bounded_self (a : α) : bounded r {b | r b a} :=
101+
⟨a, λ x, id⟩
102+
103+
/-! #### Half-open bounded intervals -/
104+
105+
theorem bounded_lt_Iio [preorder α] (a : α) : bounded (<) (set.Iio a) :=
106+
bounded_self a
107+
108+
theorem bounded_le_Iio [preorder α] (a : α) : bounded (≤) (set.Iio a) :=
109+
bounded_le_of_bounded_lt (bounded_lt_Iio a)
110+
111+
theorem bounded_le_Iic [preorder α] (a : α) : bounded (≤) (set.Iic a) :=
112+
bounded_self a
113+
114+
theorem bounded_lt_Iic [preorder α] [no_max_order α] (a : α) : bounded (<) (set.Iic a) :=
115+
by simp only [← bounded_le_iff_bounded_lt, bounded_le_Iic]
116+
117+
theorem bounded_gt_Ioi [preorder α] (a : α) : bounded (>) (set.Ioi a) :=
118+
bounded_self a
119+
120+
theorem bounded_ge_Ioi [preorder α] (a : α) : bounded (≥) (set.Ioi a) :=
121+
bounded_ge_of_bounded_gt (bounded_gt_Ioi a)
122+
123+
theorem bounded_ge_Ici [preorder α] (a : α) : bounded (≥) (set.Ici a) :=
124+
bounded_self a
125+
126+
theorem bounded_gt_Ici [preorder α] [no_min_order α] (a : α) : bounded (>) (set.Ici a) :=
127+
by simp only [← bounded_ge_iff_bounded_gt, bounded_ge_Ici]
128+
129+
/-! #### Other bounded intervals -/
130+
131+
theorem bounded_lt_Ioo [preorder α] (a b : α) : bounded (<) (set.Ioo a b) :=
132+
(bounded_lt_Iio b).mono set.Ioo_subset_Iio_self
133+
134+
theorem bounded_lt_Ico [preorder α] (a b : α) : bounded (<) (set.Ico a b) :=
135+
(bounded_lt_Iio b).mono set.Ico_subset_Iio_self
136+
137+
theorem bounded_lt_Ioc [preorder α] [no_max_order α] (a b : α) : bounded (<) (set.Ioc a b) :=
138+
(bounded_lt_Iic b).mono set.Ioc_subset_Iic_self
139+
140+
theorem bounded_lt_Icc [preorder α] [no_max_order α] (a b : α) : bounded (<) (set.Icc a b) :=
141+
(bounded_lt_Iic b).mono set.Icc_subset_Iic_self
142+
143+
theorem bounded_le_Ioo [preorder α] (a b : α) : bounded (≤) (set.Ioo a b) :=
144+
(bounded_le_Iio b).mono set.Ioo_subset_Iio_self
145+
146+
theorem bounded_le_Ico [preorder α] (a b : α) : bounded (≤) (set.Ico a b) :=
147+
(bounded_le_Iio b).mono set.Ico_subset_Iio_self
148+
149+
theorem bounded_le_Ioc [preorder α] (a b : α) : bounded (≤) (set.Ioc a b) :=
150+
(bounded_le_Iic b).mono set.Ioc_subset_Iic_self
151+
152+
theorem bounded_le_Icc [preorder α] (a b : α) : bounded (≤) (set.Icc a b) :=
153+
(bounded_le_Iic b).mono set.Icc_subset_Iic_self
154+
155+
theorem bounded_gt_Ioo [preorder α] (a b : α) : bounded (>) (set.Ioo a b) :=
156+
(bounded_gt_Ioi a).mono set.Ioo_subset_Ioi_self
157+
158+
theorem bounded_gt_Ioc [preorder α] (a b : α) : bounded (>) (set.Ioc a b) :=
159+
(bounded_gt_Ioi a).mono set.Ioc_subset_Ioi_self
160+
161+
theorem bounded_gt_Ico [preorder α] [no_min_order α] (a b : α) : bounded (>) (set.Ico a b) :=
162+
(bounded_gt_Ici a).mono set.Ico_subset_Ici_self
163+
164+
theorem bounded_gt_Icc [preorder α] [no_min_order α] (a b : α) : bounded (>) (set.Icc a b) :=
165+
(bounded_gt_Ici a).mono set.Icc_subset_Ici_self
166+
167+
theorem bounded_ge_Ioo [preorder α] (a b : α) : bounded (≥) (set.Ioo a b) :=
168+
(bounded_ge_Ioi a).mono set.Ioo_subset_Ioi_self
169+
170+
theorem bounded_ge_Ioc [preorder α] (a b : α) : bounded (≥) (set.Ioc a b) :=
171+
(bounded_ge_Ioi a).mono set.Ioc_subset_Ioi_self
172+
173+
theorem bounded_ge_Ico [preorder α] (a b : α) : bounded (≥) (set.Ico a b) :=
174+
(bounded_ge_Ici a).mono set.Ico_subset_Ici_self
175+
176+
theorem bounded_ge_Icc [preorder α] (a b : α) : bounded (≥) (set.Icc a b) :=
177+
(bounded_ge_Ici a).mono set.Icc_subset_Ici_self
178+
179+
/-! #### Unbounded intervals -/
180+
181+
theorem unbounded_le_Ioi [semilattice_sup α] [no_max_order α] (a : α) : unbounded (≤) (set.Ioi a) :=
182+
λ b, let ⟨c, hc⟩ := exists_gt (a ⊔ b) in
183+
⟨c, le_sup_left.trans_lt hc, (le_sup_right.trans_lt hc).not_le⟩
184+
185+
theorem unbounded_le_Ici [semilattice_sup α] [no_max_order α] (a : α) : unbounded (≤) (set.Ici a) :=
186+
(unbounded_le_Ioi a).mono set.Ioi_subset_Ici_self
187+
188+
theorem unbounded_lt_Ioi [semilattice_sup α] [no_max_order α] (a : α) : unbounded (<) (set.Ioi a) :=
189+
unbounded_lt_of_unbounded_le (unbounded_le_Ioi a)
190+
191+
theorem unbounded_lt_Ici [semilattice_sup α] (a : α) : unbounded (<) (set.Ici a) :=
192+
λ b, ⟨a ⊔ b, le_sup_left, le_sup_right.not_lt⟩
193+
194+
/-! ### Bounded initial segments -/
195+
196+
theorem bounded_inter_not (H : ∀ a b, ∃ m, ∀ c, r c a ∨ r c b → r c m) (a : α) :
197+
bounded r (s ∩ {b | ¬ r b a}) ↔ bounded r s :=
198+
begin
199+
refine ⟨_, bounded.mono (set.inter_subset_left s _)⟩,
200+
rintro ⟨b, hb⟩,
201+
cases H a b with m hm,
202+
exact ⟨m, λ c hc, hm c (or_iff_not_imp_left.2 (λ hca, (hb c ⟨hc, hca⟩)))⟩
203+
end
204+
205+
theorem unbounded_inter_not (H : ∀ a b, ∃ m, ∀ c, r c a ∨ r c b → r c m) (a : α) :
206+
unbounded r (s ∩ {b | ¬ r b a}) ↔ unbounded r s :=
207+
by simp_rw [← not_bounded_iff, bounded_inter_not H]
208+
209+
/-! #### Less or equal -/
210+
211+
theorem bounded_le_inter_not_le [semilattice_sup α] (a : α) :
212+
bounded (≤) (s ∩ {b | ¬ b ≤ a}) ↔ bounded (≤) s :=
213+
bounded_inter_not (λ x y, ⟨x ⊔ y, λ z h, h.elim le_sup_of_le_left le_sup_of_le_right⟩) a
214+
215+
theorem unbounded_le_inter_not_le [semilattice_sup α] (a : α) :
216+
unbounded (≤) (s ∩ {b | ¬ b ≤ a}) ↔ unbounded (≤) s :=
217+
begin
218+
rw [←not_bounded_iff, ←not_bounded_iff, not_iff_not],
219+
exact bounded_le_inter_not_le a
220+
end
221+
222+
theorem bounded_le_inter_lt [linear_order α] (a : α) :
223+
bounded (≤) (s ∩ {b | a < b}) ↔ bounded (≤) s :=
224+
by simp_rw [← not_le, bounded_le_inter_not_le]
225+
226+
theorem unbounded_le_inter_lt [linear_order α] (a : α) :
227+
unbounded (≤) (s ∩ {b | a < b}) ↔ unbounded (≤) s :=
228+
by { convert unbounded_le_inter_not_le a, ext, exact lt_iff_not_ge' }
229+
230+
theorem bounded_le_inter_le [linear_order α] (a : α) :
231+
bounded (≤) (s ∩ {b | a ≤ b}) ↔ bounded (≤) s :=
232+
begin
233+
refine ⟨_, bounded.mono (set.inter_subset_left s _)⟩,
234+
rw ←@bounded_le_inter_lt _ s _ a,
235+
exact bounded.mono (λ x ⟨hx, hx'⟩, ⟨hx, le_of_lt hx'⟩)
236+
end
237+
238+
theorem unbounded_le_inter_le [linear_order α] (a : α) :
239+
unbounded (≤) (s ∩ {b | a ≤ b}) ↔ unbounded (≤) s :=
240+
begin
241+
rw [←not_bounded_iff, ←not_bounded_iff, not_iff_not],
242+
exact bounded_le_inter_le a
243+
end
244+
245+
/-! #### Less than -/
246+
247+
theorem bounded_lt_inter_not_lt [semilattice_sup α] (a : α) :
248+
bounded (<) (s ∩ {b | ¬ b < a}) ↔ bounded (<) s :=
249+
bounded_inter_not (λ x y, ⟨x ⊔ y, λ z h, h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩) a
250+
251+
theorem unbounded_lt_inter_not_lt [semilattice_sup α] (a : α) :
252+
unbounded (<) (s ∩ {b | ¬ b < a}) ↔ unbounded (<) s :=
253+
begin
254+
rw [←not_bounded_iff, ←not_bounded_iff, not_iff_not],
255+
exact bounded_lt_inter_not_lt a
256+
end
257+
258+
theorem bounded_lt_inter_le [linear_order α] (a : α) :
259+
bounded (<) (s ∩ {b | a ≤ b}) ↔ bounded (<) s :=
260+
by { convert bounded_lt_inter_not_lt a, ext, exact not_lt.symm }
261+
262+
theorem unbounded_lt_inter_le [linear_order α] (a : α) :
263+
unbounded (<) (s ∩ {b | a ≤ b}) ↔ unbounded (<) s :=
264+
by { convert unbounded_lt_inter_not_lt a, ext, exact not_lt.symm }
265+
266+
theorem bounded_lt_inter_lt [linear_order α] [no_max_order α] (a : α) :
267+
bounded (<) (s ∩ {b | a < b}) ↔ bounded (<) s :=
268+
begin
269+
rw [←bounded_le_iff_bounded_lt, ←bounded_le_iff_bounded_lt],
270+
exact bounded_le_inter_lt a
271+
end
272+
273+
theorem unbounded_lt_inter_lt [linear_order α] [no_max_order α] (a : α) :
274+
unbounded (<) (s ∩ {b | a < b}) ↔ unbounded (<) s :=
275+
begin
276+
rw [←not_bounded_iff, ←not_bounded_iff, not_iff_not],
277+
exact bounded_lt_inter_lt a
278+
end
279+
280+
/-! #### Greater or equal -/
281+
282+
theorem bounded_ge_inter_not_ge [semilattice_inf α] (a : α) :
283+
bounded (≥) (s ∩ {b | ¬ a ≤ b}) ↔ bounded (≥) s :=
284+
@bounded_le_inter_not_le (order_dual α) s _ a
285+
286+
theorem unbounded_ge_inter_not_ge [semilattice_inf α] (a : α) :
287+
unbounded (≥) (s ∩ {b | ¬ a ≤ b}) ↔ unbounded (≥) s :=
288+
@unbounded_le_inter_not_le (order_dual α) s _ a
289+
290+
theorem bounded_ge_inter_gt [linear_order α] (a : α) :
291+
bounded (≥) (s ∩ {b | b < a}) ↔ bounded (≥) s :=
292+
@bounded_le_inter_lt (order_dual α) s _ a
293+
294+
theorem unbounded_ge_inter_gt [linear_order α] (a : α) :
295+
unbounded (≥) (s ∩ {b | b < a}) ↔ unbounded (≥) s :=
296+
@unbounded_le_inter_lt (order_dual α) s _ a
297+
298+
theorem bounded_ge_inter_ge [linear_order α] (a : α) :
299+
bounded (≥) (s ∩ {b | b ≤ a}) ↔ bounded (≥) s :=
300+
@bounded_le_inter_le (order_dual α) s _ a
301+
302+
theorem unbounded_ge_iff_unbounded_inter_ge [linear_order α] (a : α) :
303+
unbounded (≥) (s ∩ {b | b ≤ a}) ↔ unbounded (≥) s :=
304+
@unbounded_le_inter_le (order_dual α) s _ a
305+
306+
/-! #### Greater than -/
307+
308+
theorem bounded_gt_inter_not_gt [semilattice_inf α] (a : α) :
309+
bounded (>) (s ∩ {b | ¬ a < b}) ↔ bounded (>) s :=
310+
@bounded_lt_inter_not_lt (order_dual α) s _ a
311+
312+
theorem unbounded_gt_inter_not_gt [semilattice_inf α] (a : α) :
313+
unbounded (>) (s ∩ {b | ¬ a < b}) ↔ unbounded (>) s :=
314+
@unbounded_lt_inter_not_lt (order_dual α) s _ a
315+
316+
theorem bounded_gt_inter_ge [linear_order α] (a : α) :
317+
bounded (>) (s ∩ {b | b ≤ a}) ↔ bounded (>) s :=
318+
@bounded_lt_inter_le (order_dual α) s _ a
319+
320+
theorem unbounded_inter_ge [linear_order α] (a : α) :
321+
unbounded (>) (s ∩ {b | b ≤ a}) ↔ unbounded (>) s :=
322+
@unbounded_lt_inter_le (order_dual α) s _ a
323+
324+
theorem bounded_gt_inter_gt [linear_order α] [no_min_order α] (a : α) :
325+
bounded (>) (s ∩ {b | b < a}) ↔ bounded (>) s :=
326+
@bounded_lt_inter_lt (order_dual α) s _ _ a
327+
328+
theorem unbounded_gt_inter_gt [linear_order α] [no_min_order α] (a : α) :
329+
unbounded (>) (s ∩ {b | b < a}) ↔ unbounded (>) s :=
330+
@unbounded_lt_inter_lt (order_dual α) s _ _ a

‎src/order/lattice.lean‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,12 @@ le_trans h le_sup_left
143143
theorem le_sup_of_le_right (h : c ≤ b) : c ≤ a ⊔ b :=
144144
le_trans h le_sup_right
145145

146+
theorem lt_sup_of_lt_left (h : c < a) : c < a ⊔ b :=
147+
h.trans_le le_sup_left
148+
149+
theorem lt_sup_of_lt_right (h : c < b) : c < a ⊔ b :=
150+
h.trans_le le_sup_right
151+
146152
theorem sup_le : a ≤ c → b ≤ c → a ⊔ b ≤ c :=
147153
semilattice_sup.sup_le a b c
148154

@@ -196,7 +202,7 @@ lemma sup_ind [is_total α (≤)] (a b : α) {p : α → Prop} (ha : p a) (hb :
196202
⟨λ h, (total_of (≤) c b).imp
197203
(λ bc, by rwa sup_eq_left.2 bc at h)
198204
(λ bc, by rwa sup_eq_right.2 bc at h),
199-
λ h, h.elim (λ h, h.trans_le le_sup_left) (λ h, h.trans_le le_sup_right)⟩
205+
λ h, h.elim lt_sup_of_lt_left lt_sup_of_lt_right⟩
200206

201207
@[simp] theorem sup_idem : a ⊔ a = a :=
202208
by apply le_antisymm; simp
@@ -330,6 +336,12 @@ le_trans inf_le_left h
330336
theorem inf_le_of_right_le (h : b ≤ c) : a ⊓ b ≤ c :=
331337
le_trans inf_le_right h
332338

339+
theorem inf_lt_of_left_lt (h : a < c) : a ⊓ b < c :=
340+
lt_of_le_of_lt inf_le_left h
341+
342+
theorem inf_lt_of_right_lt (h : b < c) : a ⊓ b < c :=
343+
lt_of_le_of_lt inf_le_right h
344+
333345
@[simp] theorem le_inf_iff : a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c :=
334346
@sup_le_iff (order_dual α) _ _ _ _
335347

‎src/order/rel_classes.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -284,7 +284,7 @@ instance prod.lex.is_well_order [is_well_order α r] [is_well_order β s] :
284284
/-- An unbounded or cofinal set -/
285285
def unbounded (r : α → α → Prop) (s : set α) : Prop := ∀ a, ∃ b ∈ s, ¬ r b a
286286
/-- A bounded or final set -/
287-
def bounded (r : α → α → Prop) (s : set α) : Prop := ∃a, ∀ b ∈ s, r b a
287+
def bounded (r : α → α → Prop) (s : set α) : Prop := ∃ a, ∀ b ∈ s, r b a
288288

289289
@[simp] lemma not_bounded_iff {r : α → α → Prop} (s : set α) : ¬bounded r s ↔ unbounded r s :=
290290
by simp only [bounded, unbounded, not_forall, not_exists, exists_prop, not_and, not_not]

0 commit comments

Comments
 (0)