chore(data/set/intervals): more lemmas (#4662)

Author: urkud

src/data/set/intervals/basic.lean

@@ -221,6 +221,8 @@ lemma Icc_subset_Ici_self : Icc a b ⊆ Ici a := λ x, and.left
 
 lemma Icc_subset_Iic_self : Icc a b ⊆ Iic b := λ x, and.right
 
+lemma Ioc_subset_Iic_self : Ioc a b ⊆ Iic b := λ x, and.right
+
 lemma Ioc_subset_Ioc (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) :
   Ioc a₁ b₁ ⊆ Ioc a₂ b₂ :=
 λ x ⟨hx₁, hx₂⟩, ⟨lt_of_le_of_lt h₁ hx₁, le_trans hx₂ h₂⟩
@@ -263,6 +265,8 @@ lemma Ioi_subset_Ici_self : Ioi a ⊆ Ici a := λx hx, le_of_lt hx
 
 lemma Iio_subset_Iic_self : Iio a ⊆ Iic a := λx hx, le_of_lt hx
 
+lemma Ico_subset_Ici_self : Ico a b ⊆ Ici a := λ x, and.left
+
 lemma Icc_subset_Icc_iff (h₁ : a₁ ≤ b₁) :
   Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
 ⟨λ h, ⟨(h ⟨le_refl _, h₁⟩).1, (h ⟨h₁, le_refl _⟩).2⟩,
@@ -378,6 +382,20 @@ by rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 right_m
 
 @[simp] lemma Iio_union_right : Iio a ∪ {a} = Iic a := ext $ λ x, le_iff_lt_or_eq.symm
 
+lemma Ioo_union_left (hab : a < b) : Ioo a b ∪ {a} = Ico a b :=
+by rw [← Ico_diff_left, diff_union_self,
+  union_eq_self_of_subset_right (singleton_subset_iff.2 $ left_mem_Ico.2 hab)]
+
+lemma Ioo_union_right (hab : a < b) : Ioo a b ∪ {b} = Ioc a b :=
+by simpa only [dual_Ioo, dual_Ico] using @Ioo_union_left (order_dual α) _ b a hab
+
+lemma Ioc_union_left (hab : a ≤ b) : Ioc a b ∪ {a} = Icc a b :=
+by rw [← Icc_diff_left, diff_union_self,
+  union_eq_self_of_subset_right (singleton_subset_iff.2 $ left_mem_Icc.2 hab)]
+
+lemma Ico_union_right (hab : a ≤ b) : Ico a b ∪ {b} = Icc a b :=
+by simpa only [dual_Ioc, dual_Icc] using @Ioc_union_left (order_dual α) _ b a hab
+
 lemma mem_Ici_Ioi_of_subset_of_subset {s : set α} (ho : Ioi a ⊆ s) (hc : s ⊆ Ici a) :
   s ∈ ({Ici a, Ioi a} : set (set α)) :=
 classical.by_cases
@@ -447,13 +465,27 @@ lemma Iic_singleton_of_bot {a : α} (h_bot : ∀ x, a ≤ x) : Iic a = {a} :=
 
 end partial_order
 
-section order_top_or_bot
-variables {α : Type u}
+section order_top
+
+variables {α : Type u} [order_top α] {a : α}
+
+@[simp] lemma Ici_top : Ici (⊤ : α) = {⊤} := Ici_singleton_of_top (λ _, le_top)
+@[simp] lemma Iic_top : Iic (⊤ : α) = univ := eq_univ_of_forall $ λ x, le_top
+@[simp] lemma Icc_top : Icc a ⊤ = Ici a := by simp [← Ici_inter_Iic]
+@[simp] lemma Ioc_top : Ioc a ⊤ = Ioi a := by simp [← Ioi_inter_Iic]
+
+end order_top
+
+section order_bot
+
+variables {α : Type u} [order_bot α] {a : α}
 
-@[simp] lemma Ici_top [order_top α] : Ici (⊤ : α) = {⊤} := Ici_singleton_of_top (λ _, le_top)
-@[simp] lemma Ici_bot [order_bot α] : Iic (⊥ : α) = {⊥} := Iic_singleton_of_bot (λ _, bot_le)
+@[simp] lemma Iic_bot : Iic (⊥ : α) = {⊥} := Iic_singleton_of_bot (λ _, bot_le)
+@[simp] lemma Ici_bot : Ici (⊥ : α) = univ := @Iic_top (order_dual α) _
+@[simp] lemma Icc_bot : Icc ⊥ a = Iic a := by simp [← Ici_inter_Iic]
+@[simp] lemma Ico_bot : Ico ⊥ a = Iio a := by simp [← Ici_inter_Iio]
 
-end order_top_or_bot
+end order_bot
 
 section linear_order
 variables {α : Type u} [linear_order α] {a a₁ a₂ b b₁ b₂ : α}