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

Commit b9db169

Browse files
b-mehtaYaelDillies
b-mehta
and
YaelDillies
committed
chore(order/locally_finite): fill in finset interval API (#11338)
A bunch of statements about finset intervals, mimicking the set interval API and mostly proved using it. `simp` attributes are chosen as they were for sets. Also some golf. Co-authored-by: YaelDillies <yael.dillies@gmail.com>
1 parent 924aab1 commit b9db169

File tree

2 files changed

+225
-105
lines changed

2 files changed

+225
-105
lines changed

‎src/data/finset/locally_finite.lean‎

Lines changed: 204 additions & 79 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ variables {α : Type*}
2222

2323
namespace finset
2424
section preorder
25-
variables [preorder α] [locally_finite_order α] {a b : α}
25+
variables [preorder α] [locally_finite_order α] {a a₁ a₂ b b₁ b₂ c x : α}
2626

2727
@[simp] lemma nonempty_Icc : (Icc a b).nonempty ↔ a ≤ b :=
2828
by rw [←coe_nonempty, coe_Icc, set.nonempty_Icc]
@@ -60,95 +60,187 @@ eq_empty_iff_forall_not_mem.2 $ λ x hx, h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx
6060
@[simp] lemma Ioc_eq_empty_of_le (h : b ≤ a) : Ioc a b = ∅ := Ioc_eq_empty h.not_lt
6161
@[simp] lemma Ioo_eq_empty_of_le (h : b ≤ a) : Ioo a b = ∅ := Ioo_eq_empty h.not_lt
6262

63-
variables (a)
64-
65-
@[simp] lemma Ico_self : Ico a a = ∅ := by rw [←coe_eq_empty, coe_Ico, set.Ico_self]
66-
@[simp] lemma Ioc_self : Ioc a a = ∅ := by rw [←coe_eq_empty, coe_Ioc, set.Ioc_self]
67-
@[simp] lemma Ioo_self : Ioo a a = ∅ := by rw [←coe_eq_empty, coe_Ioo, set.Ioo_self]
68-
69-
variables {a b}
70-
71-
lemma left_mem_Icc : a ∈ Icc a b ↔ a ≤ b := by simp only [mem_Icc, true_and, le_refl]
72-
lemma left_mem_Ico : a ∈ Ico a b ↔ a < b := by simp only [mem_Ico, true_and, le_refl]
73-
lemma right_mem_Icc : b ∈ Icc a b ↔ a ≤ b := by simp only [mem_Icc, and_true, le_refl]
74-
lemma right_mem_Ioc : b ∈ Ioc a b ↔ a < b := by simp only [mem_Ioc, and_true, le_refl]
63+
@[simp] lemma left_mem_Icc : a ∈ Icc a b ↔ a ≤ b := by simp only [mem_Icc, true_and, le_rfl]
64+
@[simp] lemma left_mem_Ico : a ∈ Ico a b ↔ a < b := by simp only [mem_Ico, true_and, le_refl]
65+
@[simp] lemma right_mem_Icc : b ∈ Icc a b ↔ a ≤ b := by simp only [mem_Icc, and_true, le_rfl]
66+
@[simp] lemma right_mem_Ioc : b ∈ Ioc a b ↔ a < b := by simp only [mem_Ioc, and_true, le_rfl]
7567

7668
@[simp] lemma left_not_mem_Ioc : a ∉ Ioc a b := λ h, lt_irrefl _ (mem_Ioc.1 h).1
7769
@[simp] lemma left_not_mem_Ioo : a ∉ Ioo a b := λ h, lt_irrefl _ (mem_Ioo.1 h).1
7870
@[simp] lemma right_not_mem_Ico : b ∉ Ico a b := λ h, lt_irrefl _ (mem_Ico.1 h).2
7971
@[simp] lemma right_not_mem_Ioo : b ∉ Ioo a b := λ h, lt_irrefl _ (mem_Ioo.1 h).2
8072

81-
lemma Ico_filter_lt_of_le_left {a b c : α} [decidable_pred (< c)] (hca : c ≤ a) :
82-
(Ico a b).filter (λ x, x < c) = ∅ :=
83-
finset.filter_false_of_mem (λ x hx, (hca.trans (mem_Ico.1 hx).1).not_lt)
73+
lemma Icc_subset_Icc (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊆ Icc a₂ b₂ :=
74+
by simpa [←coe_subset] using set.Icc_subset_Icc ha hb
75+
76+
lemma Ico_subset_Ico (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ico a₁ b₁ ⊆ Ico a₂ b₂ :=
77+
by simpa [←coe_subset] using set.Ico_subset_Ico ha hb
78+
79+
lemma Ioc_subset_Ioc (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ioc a₁ b₁ ⊆ Ioc a₂ b₂ :=
80+
by simpa [←coe_subset] using set.Ioc_subset_Ioc ha hb
81+
82+
lemma Ioo_subset_Ioo (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Ioo a₁ b₁ ⊆ Ioo a₂ b₂ :=
83+
by simpa [←coe_subset] using set.Ioo_subset_Ioo ha hb
84+
85+
lemma Icc_subset_Icc_left (h : a₁ ≤ a₂) : Icc a₂ b ⊆ Icc a₁ b := Icc_subset_Icc h le_rfl
86+
lemma Ico_subset_Ico_left (h : a₁ ≤ a₂) : Ico a₂ b ⊆ Ico a₁ b := Ico_subset_Ico h le_rfl
87+
lemma Ioc_subset_Ioc_left (h : a₁ ≤ a₂) : Ioc a₂ b ⊆ Ioc a₁ b := Ioc_subset_Ioc h le_rfl
88+
lemma Ioo_subset_Ioo_left (h : a₁ ≤ a₂) : Ioo a₂ b ⊆ Ioo a₁ b := Ioo_subset_Ioo h le_rfl
89+
lemma Icc_subset_Icc_right (h : b₁ ≤ b₂) : Icc a b₁ ⊆ Icc a b₂ := Icc_subset_Icc le_rfl h
90+
lemma Ico_subset_Ico_right (h : b₁ ≤ b₂) : Ico a b₁ ⊆ Ico a b₂ := Ico_subset_Ico le_rfl h
91+
lemma Ioc_subset_Ioc_right (h : b₁ ≤ b₂) : Ioc a b₁ ⊆ Ioc a b₂ := Ioc_subset_Ioc le_rfl h
92+
lemma Ioo_subset_Ioo_right (h : b₁ ≤ b₂) : Ioo a b₁ ⊆ Ioo a b₂ := Ioo_subset_Ioo le_rfl h
93+
94+
lemma Ico_subset_Ioo_left (h : a₁ < a₂) : Ico a₂ b ⊆ Ioo a₁ b :=
95+
by { rw [←coe_subset, coe_Ico, coe_Ioo], exact set.Ico_subset_Ioo_left h }
96+
97+
lemma Ioc_subset_Ioo_right (h : b₁ < b₂) : Ioc a b₁ ⊆ Ioo a b₂ :=
98+
by { rw [←coe_subset, coe_Ioc, coe_Ioo], exact set.Ioc_subset_Ioo_right h }
99+
100+
lemma Icc_subset_Ico_right (h : b₁ < b₂) : Icc a b₁ ⊆ Ico a b₂ :=
101+
by { rw [←coe_subset, coe_Icc, coe_Ico], exact set.Icc_subset_Ico_right h }
102+
103+
lemma Ioo_subset_Ico_self : Ioo a b ⊆ Ico a b :=
104+
by { rw [←coe_subset, coe_Ioo, coe_Ico], exact set.Ioo_subset_Ico_self }
105+
106+
lemma Ioo_subset_Ioc_self : Ioo a b ⊆ Ioc a b :=
107+
by { rw [←coe_subset, coe_Ioo, coe_Ioc], exact set.Ioo_subset_Ioc_self }
108+
109+
lemma Ico_subset_Icc_self : Ico a b ⊆ Icc a b :=
110+
by { rw [←coe_subset, coe_Ico, coe_Icc], exact set.Ico_subset_Icc_self }
111+
112+
lemma Ioc_subset_Icc_self : Ioc a b ⊆ Icc a b :=
113+
by { rw [←coe_subset, coe_Ioc, coe_Icc], exact set.Ioc_subset_Icc_self }
114+
115+
lemma Ioo_subset_Icc_self : Ioo a b ⊆ Icc a b := Ioo_subset_Ico_self.trans Ico_subset_Icc_self
116+
117+
lemma Icc_subset_Icc_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
118+
by rw [←coe_subset, coe_Icc, coe_Icc, set.Icc_subset_Icc_iff h₁]
119+
120+
lemma Icc_subset_Ioo_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂ :=
121+
by rw [←coe_subset, coe_Icc, coe_Ioo, set.Icc_subset_Ioo_iff h₁]
122+
123+
lemma Icc_subset_Ico_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂ :=
124+
by rw [←coe_subset, coe_Icc, coe_Ico, set.Icc_subset_Ico_iff h₁]
125+
126+
lemma Icc_subset_Ioc_iff (h₁ : a₁ ≤ b₁) : Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂ :=
127+
(Icc_subset_Ico_iff h₁.dual).trans and.comm
128+
129+
--TODO: `Ico_subset_Ioo_iff`, `Ioc_subset_Ioo_iff`
130+
131+
lemma Icc_ssubset_Icc_left (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : Icc a₁ b₁ ⊂ Icc a₂ b₂ :=
132+
by { rw [←coe_ssubset, coe_Icc, coe_Icc], exact set.Icc_ssubset_Icc_left hI ha hb }
133+
134+
lemma Icc_ssubset_Icc_right (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) : Icc a₁ b₁ ⊂ Icc a₂ b₂ :=
135+
by { rw [←coe_ssubset, coe_Icc, coe_Icc], exact set.Icc_ssubset_Icc_right hI ha hb }
84136

85-
lemma Ico_filter_lt_of_right_le {a b c : α} [decidable_pred (< c)] (hbc : b ≤ c) :
86-
(Ico a b).filter (λ x, x < c) = Ico a b :=
87-
finset.filter_true_of_mem (λ x hx, (mem_Ico.1 hx).2.trans_le hbc)
137+
variables (a)
138+
139+
@[simp] lemma Ico_self : Ico a a = ∅ := Ico_eq_empty $ lt_irrefl _
140+
@[simp] lemma Ioc_self : Ioc a a = ∅ := Ioc_eq_empty $ lt_irrefl _
141+
@[simp] lemma Ioo_self : Ioo a a = ∅ := Ioo_eq_empty $ lt_irrefl _
142+
143+
variables {a}
144+
145+
/-- A set with upper and lower bounds in a locally finite order is a fintype -/
146+
def _root_.set.fintype_of_mem_bounds {s : set α} [decidable_pred (∈ s)]
147+
(ha : a ∈ lower_bounds s) (hb : b ∈ upper_bounds s) : fintype s :=
148+
set.fintype_subset (set.Icc a b) $ λ x hx, ⟨ha hx, hb hx⟩
149+
150+
lemma _root_.bdd_below.finite_of_bdd_above {s : set α} (h₀ : bdd_below s) (h₁ : bdd_above s) :
151+
s.finite :=
152+
let ⟨a, ha⟩ := h₀, ⟨b, hb⟩ := h₁ in by { classical, exact ⟨set.fintype_of_mem_bounds ha hb⟩ }
88153

89-
lemma Ico_filter_lt_of_le_right {a b c : α} [decidable_pred (< c)] (hcb : c ≤ b) :
90-
(Ico a b).filter (λ x, x < c) = Ico a c :=
154+
section filter
155+
156+
lemma Ico_filter_lt_of_le_left [decidable_pred (< c)] (hca : c ≤ a) : (Ico a b).filter (< c) = ∅ :=
157+
filter_false_of_mem (λ x hx, (hca.trans (mem_Ico.1 hx).1).not_lt)
158+
159+
lemma Ico_filter_lt_of_right_le [decidable_pred (< c)] (hbc : b ≤ c) :
160+
(Ico a b).filter (< c) = Ico a b :=
161+
filter_true_of_mem (λ x hx, (mem_Ico.1 hx).2.trans_le hbc)
162+
163+
lemma Ico_filter_lt_of_le_right [decidable_pred (< c)] (hcb : c ≤ b) :
164+
(Ico a b).filter (< c) = Ico a c :=
91165
begin
92166
ext x,
93167
rw [mem_filter, mem_Ico, mem_Ico, and.right_comm],
94168
exact and_iff_left_of_imp (λ h, h.2.trans_le hcb),
95169
end
96170

97171
lemma Ico_filter_le_of_le_left {a b c : α} [decidable_pred ((≤) c)] (hca : c ≤ a) :
98-
(Ico a b).filter (λ x, c ≤ x) = Ico a b :=
99-
finset.filter_true_of_mem (λ x hx, hca.trans (mem_Ico.1 hx).1)
172+
(Ico a b).filter ((≤) c) = Ico a b :=
173+
filter_true_of_mem (λ x hx, hca.trans (mem_Ico.1 hx).1)
100174

101-
lemma Ico_filter_le_of_right_le {a b : α} [decidable_pred ((≤) b)] :
102-
(Ico a b).filter (λ x, b ≤ x) = ∅ :=
103-
finset.filter_false_of_mem (λ x hx, (mem_Ico.1 hx).2.not_le)
175+
lemma Ico_filter_le_of_right_le {a b : α} [decidable_pred ((≤) b)] : (Ico a b).filter ((≤) b) = ∅ :=
176+
filter_false_of_mem (λ x hx, (mem_Ico.1 hx).2.not_le)
104177

105178
lemma Ico_filter_le_of_left_le {a b c : α} [decidable_pred ((≤) c)] (hac : a ≤ c) :
106-
(Ico a b).filter (λ x, c ≤ x) = Ico c b :=
179+
(Ico a b).filter ((≤) c) = Ico c b :=
107180
begin
108181
ext x,
109182
rw [mem_filter, mem_Ico, mem_Ico, and_comm, and.left_comm],
110183
exact and_iff_right_of_imp (λ h, hac.trans h.1),
111184
end
112185

113-
/-- A set with upper and lower bounds in a locally finite order is a fintype -/
114-
def _root_.set.fintype_of_mem_bounds {a b} {s : set α} [decidable_pred (∈ s)]
115-
(ha : a ∈ lower_bounds s) (hb : b ∈ upper_bounds s) : fintype s :=
116-
set.fintype_subset (set.Icc a b) $ λ x hx, ⟨ha hx, hb hx⟩
186+
variables (a b) [fintype α]
117187

118-
lemma _root_.bdd_below.finite_of_bdd_above {s : set α} (h₀ : bdd_below s) (h₁ : bdd_above s) :
119-
s.finite :=
120-
let ⟨a, ha⟩ := h₀, ⟨b, hb⟩ := h₁ in by { classical, exact ⟨set.fintype_of_mem_bounds ha hb⟩ }
188+
lemma filter_lt_lt_eq_Ioo [decidable_pred (λ j, a < j ∧ j < b)] :
189+
univ.filter (λ j, a < j ∧ j < b) = Ioo a b := by { ext, simp }
121190

122-
section filter
191+
lemma filter_lt_le_eq_Ioc [decidable_pred (λ j, a < j ∧ j ≤ b)] :
192+
univ.filter (λ j, a < j ∧ j ≤ b) = Ioc a b := by { ext, simp }
123193

124-
variables (a b) [fintype α]
194+
lemma filter_le_lt_eq_Ico [decidable_pred (λ j, a ≤ j ∧ j < b)] :
195+
univ.filter (λ j, a ≤ j ∧ j < b) = Ico a b := by { ext, simp }
125196

126-
lemma filter_lt_lt_eq_Ioo [decidable_pred (λ (j : α), a < j ∧ j < b)] :
127-
finset.univ.filter (λ j, a < j ∧ j < b) = Ioo a b := by { ext, simp }
197+
lemma filter_le_le_eq_Icc [decidable_pred (λ j, a ≤ j ∧ j ≤ b)] :
198+
univ.filter (λ j, a ≤ j ∧ j ≤ b) = Icc a b := by { ext, simp }
128199

129-
lemma filter_lt_le_eq_Ioc [decidable_pred (λ (j : α), a < j ∧ j ≤ b)] :
130-
finset.univ.filter (λ j, a < j ∧ j ≤ b) = Ioc a b := by { ext, simp }
200+
lemma filter_lt_eq_Ioi [order_top α] [decidable_pred ((<) a)] : univ.filter ((<) a) = Ioi a :=
201+
by { ext, simp }
131202

132-
lemma filter_le_lt_eq_Ico [decidable_pred (λ (j : α), a ≤ j ∧ j < b)] :
133-
finset.univ.filter (λ j, a ≤ j ∧ j < b) = Ico a b := by { ext, simp }
203+
lemma filter_le_eq_Ici [order_top α] [decidable_pred ((≤) a)] : univ.filter ((≤) a) = Ici a :=
204+
by { ext, simp }
134205

135-
lemma filter_le_le_eq_Icc [decidable_pred (λ (j : α), a ≤ j ∧ j ≤ b)] :
136-
finset.univ.filter (λ j, a ≤ j ∧ j ≤ b) = Icc a b := by { ext, simp }
206+
lemma filter_gt_eq_Iio [order_bot α] [decidable_pred (< a)] : univ.filter (< a) = Iio a :=
207+
by { ext, simp }
137208

138-
lemma filter_lt_eq_Ioi [order_top α] [decidable_pred ((<) a)] :
139-
finset.univ.filter (λ j, a < j) = Ioi a := by { ext, simp }
209+
lemma filter_ge_eq_Iic [order_bot α] [decidable_pred (≤ a)] : univ.filter (≤ a) = Iic a :=
210+
by { ext, simp }
140211

141-
lemma filter_le_eq_Ici [order_top α] [decidable_pred ((≤) a)] :
142-
finset.univ.filter (λ j, a ≤ j) = Ici a := by { ext, simp }
212+
end filter
143213

144-
lemma filter_gt_eq_Iio [order_bot α] [decidable_pred (< a)] :
145-
finset.univ.filter (λ j, j < a) = Iio a := by { ext, simp }
214+
section order_top
215+
variables [order_top α]
146216

147-
lemma filter_ge_eq_Iic [order_bot α] [decidable_pred (≤ a)] :
148-
finset.univ.filter (λ j, j ≤ a) = Iic a := by { ext, simp }
217+
lemma Icc_subset_Ici_self : Icc a b ⊆ Ici a := Icc_subset_Icc_right le_top
218+
lemma Ico_subset_Ici_self : Ico a b ⊆ Ici a := Ico_subset_Icc_self.trans Icc_subset_Ici_self
219+
lemma Ioc_subset_Ici_self : Ioc a b ⊆ Ici a := Ioc_subset_Icc_self.trans Icc_subset_Ici_self
220+
lemma Ioo_subset_Ici_self : Ioo a b ⊆ Ici a := Ioo_subset_Icc_self.trans Icc_subset_Ici_self
221+
lemma Ioi_subset_Ici_self : Ioi a ⊆ Ici a := Ioc_subset_Icc_self
222+
lemma Ioc_subset_Ioi_self : Ioc a b ⊆ Ioi a := Ioc_subset_Ioc_right le_top
223+
lemma Ioo_subset_Ioi_self : Ioo a b ⊆ Ioi a := Ioo_subset_Ioc_self.trans Ioc_subset_Ioi_self
149224

150-
end filter
225+
lemma _root_.bdd_below.finite {s : set α} (hs : bdd_below s) : s.finite :=
226+
hs.finite_of_bdd_above $ order_top.bdd_above s
151227

228+
end order_top
229+
230+
section order_bot
231+
variables [order_bot α]
232+
233+
lemma Icc_subset_Iic_self : Icc a b ⊆ Iic b := Icc_subset_Icc_left bot_le
234+
lemma Ico_subset_Iic_self : Ico a b ⊆ Iic b := Ico_subset_Icc_self.trans Icc_subset_Iic_self
235+
lemma Ioc_subset_Iic_self : Ioc a b ⊆ Iic b := Ioc_subset_Icc_self.trans Icc_subset_Iic_self
236+
lemma Ioo_subset_Iic_self : Ioo a b ⊆ Iic b := Ioo_subset_Icc_self.trans Icc_subset_Iic_self
237+
lemma Iio_subset_Iic_self : Iio b ⊆ Iic b := Ico_subset_Icc_self
238+
lemma Ico_subset_Iio_self : Ico a b ⊆ Iio b := Ico_subset_Ico_left bot_le
239+
lemma Ioo_subset_Iio_self : Ioo a b ⊆ Iio b := Ioo_subset_Ico_self.trans Ico_subset_Iio_self
240+
241+
lemma _root_.bdd_above.finite {s : set α} (hs : bdd_above s) : s.finite := hs.dual.finite
242+
243+
end order_bot
152244
end preorder
153245

154246
section partial_order
@@ -162,18 +254,30 @@ by rw [←coe_eq_singleton, coe_Icc, set.Icc_eq_singleton_iff]
162254
section decidable_eq
163255
variables [decidable_eq α]
164256

165-
lemma Icc_erase_left : (Icc a b).erase a = Ioc a b :=
166-
by rw [←coe_inj, coe_erase, coe_Icc, coe_Ioc, set.Icc_diff_left]
167-
168-
lemma Icc_erase_right : (Icc a b).erase b = Ico a b :=
169-
by rw [←coe_inj, coe_erase, coe_Icc, coe_Ico, set.Icc_diff_right]
257+
@[simp] lemma Icc_erase_left (a b : α) : (Icc a b).erase a = Ioc a b := by simp [←coe_inj]
258+
@[simp] lemma Icc_erase_right (a b : α) : (Icc a b).erase b = Ico a b := by simp [←coe_inj]
259+
@[simp] lemma Ico_erase_left (a b : α) : (Ico a b).erase a = Ioo a b := by simp [←coe_inj]
260+
@[simp] lemma Ioc_erase_right (a b : α) : (Ioc a b).erase b = Ioo a b := by simp [←coe_inj]
261+
@[simp] lemma Icc_diff_both (a b : α) : Icc a b \ {a, b} = Ioo a b := by simp [←coe_inj]
170262

171-
lemma Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b :=
263+
@[simp] lemma Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b :=
172264
by rw [←coe_inj, coe_insert, coe_Icc, coe_Ico, set.insert_eq, set.union_comm, set.Ico_union_right h]
173265

174-
lemma Ioo_insert_left (h : a < b) : insert a (Ioo a b) = Ico a b :=
266+
@[simp] lemma Ioc_insert_left (h : a ≤ b) : insert a (Ioc a b) = Icc a b :=
267+
by rw [←coe_inj, coe_insert, coe_Ioc, coe_Icc, set.insert_eq, set.union_comm, set.Ioc_union_left h]
268+
269+
@[simp] lemma Ioo_insert_left (h : a < b) : insert a (Ioo a b) = Ico a b :=
175270
by rw [←coe_inj, coe_insert, coe_Ioo, coe_Ico, set.insert_eq, set.union_comm, set.Ioo_union_left h]
176271

272+
@[simp] lemma Ioo_insert_right (h : a < b) : insert b (Ioo a b) = Ioc a b :=
273+
by rw [←coe_inj, coe_insert, coe_Ioo, coe_Ioc, set.insert_eq, set.union_comm, set.Ioo_union_right h]
274+
275+
@[simp] lemma Icc_diff_Ico_self (h : a ≤ b) : Icc a b \ Ico a b = {b} := by simp [←coe_inj, h]
276+
@[simp] lemma Icc_diff_Ioc_self (h : a ≤ b) : Icc a b \ Ioc a b = {a} := by simp [←coe_inj, h]
277+
@[simp] lemma Icc_diff_Ioo_self (h : a ≤ b) : Icc a b \ Ioo a b = {a, b} := by simp [←coe_inj, h]
278+
@[simp] lemma Ico_diff_Ioo_self (h : a < b) : Ico a b \ Ioo a b = {a} := by simp [←coe_inj, h]
279+
@[simp] lemma Ioc_diff_Ioo_self (h : a < b) : Ioc a b \ Ioo a b = {b} := by simp [←coe_inj, h]
280+
177281
@[simp] lemma Ico_inter_Ico_consecutive (a b c : α) : Ico a b ∩ Ico b c = ∅ :=
178282
begin
179283
refine eq_empty_of_forall_not_mem (λ x hx, _),
@@ -186,6 +290,14 @@ le_of_eq $ Ico_inter_Ico_consecutive a b c
186290

187291
end decidable_eq
188292

293+
-- Those lemmas are purposefully the other way around
294+
295+
lemma Icc_eq_cons_Ico (h : a ≤ b) : Icc a b = (Ico a b).cons b right_not_mem_Ico :=
296+
by { classical, rw [cons_eq_insert, Ico_insert_right h] }
297+
298+
lemma Icc_eq_cons_Ioc (h : a ≤ b) : Icc a b = (Ioc a b).cons a left_not_mem_Ioc :=
299+
by { classical, rw [cons_eq_insert, Ioc_insert_left h] }
300+
189301
lemma Ico_filter_le_left {a b : α} [decidable_pred (≤ a)] (hab : a < b) :
190302
(Ico a b).filter (λ x, x ≤ a) = {a} :=
191303
begin
@@ -217,9 +329,37 @@ begin
217329
{ rw [Ioo_eq_empty (λ h', h h'.le), Ico_eq_empty (λ h', h h'.le), card_empty, zero_tsub] }
218330
end
219331

332+
lemma card_Ioo_eq_card_Ioc_sub_one (a b : α) : (Ioo a b).card = (Ioc a b).card - 1 :=
333+
@card_Ioo_eq_card_Ico_sub_one (order_dual α) _ _ _ _
334+
220335
lemma card_Ioo_eq_card_Icc_sub_two (a b : α) : (Ioo a b).card = (Icc a b).card - 2 :=
221336
by { rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one], refl }
222337

338+
section order_top
339+
variables [order_top α]
340+
341+
@[simp] lemma Ici_erase [decidable_eq α] (a : α) : (Ici a).erase a = Ioi a := Icc_erase_left _ _
342+
@[simp] lemma Ioi_insert [decidable_eq α] (a : α) : insert a (Ioi a) = Ici a :=
343+
Ioc_insert_left le_top
344+
345+
-- Purposefully written the other way around
346+
lemma Ici_eq_cons_Ioi (a : α) : Ici a = (Ioi a).cons a left_not_mem_Ioc :=
347+
by { classical, rw [cons_eq_insert, Ioi_insert] }
348+
349+
end order_top
350+
351+
section order_bot
352+
variables [order_bot α]
353+
354+
@[simp] lemma Iic_erase [decidable_eq α] (b : α) : (Iic b).erase b = Iio b := Icc_erase_right _ _
355+
@[simp] lemma Iio_insert [decidable_eq α] (b : α) : insert b (Iio b) = Iic b :=
356+
Ico_insert_right bot_le
357+
358+
-- Purposefully written the other way around
359+
lemma Iic_eq_cons_Iio (b : α) : Iic b = (Iio b).cons b right_not_mem_Ico :=
360+
by { classical, rw [cons_eq_insert, Iio_insert] }
361+
362+
end order_bot
223363
end partial_order
224364

225365
section linear_order
@@ -278,21 +418,6 @@ end
278418

279419
end linear_order
280420

281-
section order_top
282-
variables [preorder α] [order_top α] [locally_finite_order α]
283-
284-
lemma _root_.bdd_below.finite {s : set α} (hs : bdd_below s) : s.finite :=
285-
hs.finite_of_bdd_above $ order_top.bdd_above s
286-
287-
end order_top
288-
289-
section order_bot
290-
variables [preorder α] [order_bot α] [locally_finite_order α]
291-
292-
lemma _root_.bdd_above.finite {s : set α} (hs : bdd_above s) : s.finite := hs.dual.finite
293-
294-
end order_bot
295-
296421
section ordered_cancel_add_comm_monoid
297422
variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] [decidable_eq α]
298423
[locally_finite_order α]
@@ -355,16 +480,16 @@ begin
355480
exact ⟨a + y, mem_Ioo.2 ⟨lt_of_add_lt_add_left hx.1, lt_of_add_lt_add_left hx.2⟩, hy.symm⟩ }
356481
end
357482

358-
lemma image_add_right_Icc (a b c : α) : (Icc a b).image (λ x, x + c) = Icc (a + c) (b + c) :=
483+
lemma image_add_right_Icc (a b c : α) : (Icc a b).image (+ c) = Icc (a + c) (b + c) :=
359484
by { simp_rw add_comm _ c, exact image_add_left_Icc a b c }
360485

361-
lemma image_add_right_Ico (a b c : α) : (Ico a b).image (λ x, x + c) = Ico (a + c) (b + c) :=
486+
lemma image_add_right_Ico (a b c : α) : (Ico a b).image (+ c) = Ico (a + c) (b + c) :=
362487
by { simp_rw add_comm _ c, exact image_add_left_Ico a b c }
363488

364-
lemma image_add_right_Ioc (a b c : α) : (Ioc a b).image (λ x, x + c) = Ioc (a + c) (b + c) :=
489+
lemma image_add_right_Ioc (a b c : α) : (Ioc a b).image (+ c) = Ioc (a + c) (b + c) :=
365490
by { simp_rw add_comm _ c, exact image_add_left_Ioc a b c }
366491

367-
lemma image_add_right_Ioo (a b c : α) : (Ioo a b).image (λ x, x + c) = Ioo (a + c) (b + c) :=
492+
lemma image_add_right_Ioo (a b c : α) : (Ioo a b).image (+ c) = Ioo (a + c) (b + c) :=
368493
by { simp_rw add_comm _ c, exact image_add_left_Ioo a b c }
369494

370495
end ordered_cancel_add_comm_monoid

0 commit comments

Comments
 (0)