feat(data/set/intervals): add lemmas about unions of intervals (#14636)

leanprover-community · Jun 9, 2022 · abee649 · abee649
1 parent e0f3ea3
commit abee649
Show file tree

Hide file tree

Showing 2 changed files with 37 additions and 0 deletions.
diff --git a/src/data/set/intervals/disjoint.lean b/src/data/set/intervals/disjoint.lean
@@ -42,6 +42,39 @@ by rw [set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]
 @[simp] lemma Iic_disjoint_Ici : disjoint (Iic a) (Ici b) ↔ ¬(b ≤ a) :=
 disjoint.comm.trans Ici_disjoint_Iic
 
+@[simp] lemma Union_Iic : (⋃ a : α, Iic a) = univ := Union_eq_univ_iff.2 $ λ x, ⟨x, right_mem_Iic⟩
+@[simp] lemma Union_Ici : (⋃ a : α, Ici a) = univ := Union_eq_univ_iff.2 $ λ x, ⟨x, left_mem_Ici⟩
+
+@[simp] lemma Union_Icc_right (a : α) : (⋃ b, Icc a b) = Ici a :=
+by simp only [← Ici_inter_Iic, ← inter_Union, Union_Iic, inter_univ]
+
+@[simp] lemma Union_Ioc_right (a : α) : (⋃ b, Ioc a b) = Ioi a :=
+by simp only [← Ioi_inter_Iic, ← inter_Union, Union_Iic, inter_univ]
+
+@[simp] lemma Union_Icc_left (b : α) : (⋃ a, Icc a b) = Iic b :=
+by simp only [← Ici_inter_Iic, ← Union_inter, Union_Ici, univ_inter]
+
+@[simp] lemma Union_Ico_left (b : α) : (⋃ a, Ico a b) = Iio b :=
+by simp only [← Ici_inter_Iio, ← Union_inter, Union_Ici, univ_inter]
+
+@[simp] lemma Union_Iio [no_max_order α] : (⋃ a : α, Iio a) = univ :=
+Union_eq_univ_iff.2 exists_gt
+
+@[simp] lemma Union_Ioi [no_min_order α] : (⋃ a : α, Ioi a) = univ :=
+Union_eq_univ_iff.2 exists_lt
+
+@[simp] lemma Union_Ico_right [no_max_order α] (a : α) : (⋃ b, Ico a b) = Ici a :=
+by simp only [← Ici_inter_Iio, ← inter_Union, Union_Iio, inter_univ]
+
+@[simp] lemma Union_Ioo_right [no_max_order α] (a : α) : (⋃ b, Ioo a b) = Ioi a :=
+by simp only [← Ioi_inter_Iio, ← inter_Union, Union_Iio, inter_univ]
+
+@[simp] lemma Union_Ioc_left [no_min_order α] (b : α) : (⋃ a, Ioc a b) = Iic b :=
+by simp only [← Ioi_inter_Iic, ← Union_inter, Union_Ioi, univ_inter]
+
+@[simp] lemma Union_Ioo_left [no_min_order α] (b : α) : (⋃ a, Ioo a b) = Iio b :=
+by simp only [← Ioi_inter_Iio, ← Union_inter, Union_Ioi, univ_inter]
+
 end preorder
 
 section linear_order

diff --git a/src/data/set/lattice.lean b/src/data/set/lattice.lean
@@ -384,6 +384,10 @@ theorem union_Inter (s : set β) (t : ι → set β) :
   s ∪ (⋂ i, t i) = ⋂ i, s ∪ t i :=
 sup_infi_eq _ _
 
+theorem Inter_union (s : ι → set β) (t : set β) :
+  (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t :=
+infi_sup_eq _ _
+
 theorem Union_diff (s : set β) (t : ι → set β) :
   (⋃ i, t i) \ s = ⋃ i, t i \ s :=
 Union_inter _ _