feat(data/set/intervals): add missing intervals + some lemmas

The lemmas about Icc ⊆ I** are important for convexity

src/data/set/intervals.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johannes Hölzl, Mario Carneiro
+Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 
 Intervals
 
@@ -12,9 +12,10 @@ Naming conventions:
 
 Each interval has the name `I` + letter for left side + letter for right side
 
-TODO: This is just the beginning; a lot of intervals and rules are missing
+TODO: This is just the beginning; a lot of rules are missing
 -/
 import data.set.lattice algebra.order algebra.order_functions
+import tactic.linarith
 
 namespace set
 
@@ -29,16 +30,32 @@ def Ioo (a b : α) := {x | a < x ∧ x < b}
 /-- Left-closed right-open interval -/
 def Ico (a b : α) := {x | a ≤ x ∧ x < b}
 
+/-- Left-infinite right-open interval -/
+def Iio (a : α) := {x | x < a}
+
 /-- Left-closed right-closed interval -/
 def Icc (a b : α) := {x | a ≤ x ∧ x ≤ b}
 
-/-- Left-infinite right-open interval -/
-def Iio (a : α) := {x | x < a}
+/-- Left-infinite right-closed interval -/
+def Iic (b : α) := {x | x ≤ b}
+
+/-- Left-open right-closed interval -/
+def Ioc (a b : α) := {x | a < x ∧ x ≤ b}
+
+/-- Left-closed right-infinite interval -/
+def Ici (a : α) := {x | a ≤ x}
+
+/-- Left-open right-infinite interval -/
+def Ioi (a : α) := {x | a < x}
 
 @[simp] lemma mem_Ioo : x ∈ Ioo a b ↔ a < x ∧ x < b := iff.rfl
 @[simp] lemma mem_Ico : x ∈ Ico a b ↔ a ≤ x ∧ x < b := iff.rfl
-@[simp] lemma mem_Icc : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b := iff.rfl
 @[simp] lemma mem_Iio : x ∈ Iio b ↔ x < b := iff.rfl
+@[simp] lemma mem_Icc : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b := iff.rfl
+@[simp] lemma mem_Iic : x ∈ Iic b ↔ x ≤ b := iff.rfl
+@[simp] lemma mem_Ioc : x ∈ Ioc a b ↔ a < x ∧ x ≤ b := iff.rfl
+@[simp] lemma mem_Ici : x ∈ Ici a ↔ a ≤ x := iff.rfl
+@[simp] lemma mem_Ioi : x ∈ Ioi a ↔ a < x := iff.rfl
 
 @[simp] lemma Ioo_eq_empty (h : b ≤ a) : Ioo a b = ∅ :=
 eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, not_le_of_lt (lt_trans h₁ h₂) h
@@ -49,12 +66,24 @@ eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, not_le_of_lt (lt_of_le_of
 @[simp] lemma Icc_eq_empty (h : b < a) : Icc a b = ∅ :=
 eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, not_lt_of_le (le_trans h₁ h₂) h
 
+@[simp] lemma Ioc_eq_empty (h : b ≤ a) : Ioc a b = ∅ :=
+eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, not_lt_of_le (le_trans h₂ h) h₁
+
 @[simp] lemma Ioo_self (a : α) : Ioo a a = ∅ := Ioo_eq_empty $ le_refl _
 @[simp] lemma Ico_self (a : α) : Ico a a = ∅ := Ico_eq_empty $ le_refl _
 
 lemma Iio_ne_empty [no_bot_order α] (a : α) : Iio a ≠ ∅ :=
 ne_empty_iff_exists_mem.2 (no_bot a)
 
+lemma Ioi_ne_empty [no_top_order α] (a : α) : Ioi a ≠ ∅ :=
+ne_empty_iff_exists_mem.2 (no_top a)
+
+lemma Iic_ne_empty (b : α) : Iic b ≠ ∅ :=
+ne_empty_iff_exists_mem.2 ⟨b, le_refl b⟩
+
+lemma Ici_ne_empty (a : α) : Ici a ≠ ∅ :=
+ne_empty_iff_exists_mem.2 ⟨a, le_refl a⟩
+
 lemma Ioo_subset_Ioo (h₁ : a₂ ≤ a₁) (h₂ : b₁ ≤ b₂) :
   Ioo a₁ b₁ ⊆ Ioo a₂ b₂ :=
 λ x ⟨hx₁, hx₂⟩, ⟨lt_of_le_of_lt h₁ hx₁, lt_of_lt_of_le hx₂ h₂⟩
@@ -100,6 +129,41 @@ subset.trans Ioo_subset_Ico_self Ico_subset_Icc_self
 
 lemma Ico_subset_Iio_self : Ioo a b ⊆ Iio b := λ x, and.right
 
+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⟩,
+ λ ⟨h, h'⟩ x ⟨hx, hx'⟩, ⟨le_trans h hx, le_trans hx' h'⟩⟩
+
+lemma Icc_subset_Ioo_iff (h₁ : a₁ ≤ b₁) :
+  Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂ :=
+⟨λ h, ⟨(h ⟨le_refl _, h₁⟩).1, (h ⟨h₁, le_refl _⟩).2⟩,
+ λ ⟨h, h'⟩ x ⟨hx, hx'⟩, ⟨lt_of_lt_of_le h hx, lt_of_le_of_lt hx' h'⟩⟩
+
+lemma Icc_subset_Ico_iff (h₁ : a₁ ≤ b₁) :
+  Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂ :=
+⟨λ h, ⟨(h ⟨le_refl _, h₁⟩).1, (h ⟨h₁, le_refl _⟩).2⟩,
+ λ ⟨h, h'⟩ x ⟨hx, hx'⟩, ⟨le_trans h hx, lt_of_le_of_lt hx' h'⟩⟩
+
+lemma Icc_subset_Ioc_iff (h₁ : a₁ ≤ b₁) :
+  Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂ :=
+⟨λ h, ⟨(h ⟨le_refl _, h₁⟩).1, (h ⟨h₁, le_refl _⟩).2⟩,
+ λ ⟨h, h'⟩ x ⟨hx, hx'⟩, ⟨lt_of_lt_of_le h hx, le_trans hx' h'⟩⟩
+
+lemma Icc_subset_Iio_iff (h₁ : a₁ ≤ b₁) :
+  Icc a₁ b₁ ⊆ Iio b₂ ↔ b₁ < b₂ :=
+⟨λ h, h ⟨h₁, le_refl _⟩, λ h x ⟨hx, hx'⟩, lt_of_le_of_lt hx' h⟩
+
+lemma Icc_subset_Ioi_iff (h₁ : a₁ ≤ b₁) :
+  Icc a₁ b₁ ⊆ Ioi a₂ ↔ a₂ < a₁ :=
+⟨λ h, h ⟨le_refl _, h₁⟩, λ h x ⟨hx, hx'⟩, lt_of_lt_of_le h hx⟩
+
+lemma Icc_subset_Iic_iff (h₁ : a₁ ≤ b₁) :
+  Icc a₁ b₁ ⊆ Iic b₂ ↔ b₁ ≤ b₂ :=
+⟨λ h, h ⟨h₁, le_refl _⟩, λ h x ⟨hx, hx'⟩, le_trans hx' h⟩
+
+lemma Icc_subset_Ici_iff (h₁ : a₁ ≤ b₁) :
+  Icc a₁ b₁ ⊆ Ici a₂ ↔ a₂ ≤ a₁ :=
+⟨λ h, h ⟨le_refl _, h₁⟩, λ h x ⟨hx, hx'⟩, le_trans h hx⟩
 end intervals
 
 section partial_order
@@ -147,8 +211,7 @@ lemma Icc_eq_empty_iff : Icc a b = ∅ ↔ b < a :=
 
 lemma Ico_subset_Ico_iff (h₁ : a₁ < b₁) :
   Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
-⟨λ h, 
-  have a₂ ≤ a₁ ∧ a₁ < b₂ := h ⟨le_refl _, h₁⟩,
+⟨λ h, have a₂ ≤ a₁ ∧ a₁ < b₂ := h ⟨le_refl _, h₁⟩,
   ⟨this.1, le_of_not_lt $ λ h', lt_irrefl b₂ (h ⟨le_of_lt this.2, h'⟩).2⟩,
  λ ⟨h₁, h₂⟩, Ico_subset_Ico h₁ h₂⟩
 
@@ -188,4 +251,4 @@ set.ext $ by simp [iff_def, Ioo, lt_min_iff, max_lt_iff] {contextual := tt}
 
 end decidable_linear_order
 
-end set
+end set