feat(data/set/intervals/unordered_interval): Intervals are injective …

…in both endpoints (#16168)

`set.interval a` and `set.interval_oc a` are injective.

src/data/set/intervals/unordered_interval.lean

@@ -26,6 +26,8 @@ make the notation available.
 -/
 
 universe u
+
+open function
 open_locale pointwise
 open order_dual (to_dual of_dual)
 
@@ -63,17 +65,18 @@ interval_of_gt (lt_of_not_ge h)
 lemma interval_of_not_ge (h : ¬ b ≤ a) : [a, b] = Icc a b :=
 interval_of_lt (lt_of_not_ge h)
 
+lemma interval_eq_union : [a, b] = Icc a b ∪ Icc b a := by rw [Icc_union_Icc', max_comm]; refl
+
+lemma mem_interval : a ∈ [b, c] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b := by simp [interval_eq_union]
+
 @[simp] lemma interval_self : [a, a] = {a} :=
 set.ext $ by simp [le_antisymm_iff, and_comm]
 
 @[simp] lemma nonempty_interval : set.nonempty [a, b] :=
 by { simp only [interval, min_le_iff, le_max_iff, nonempty_Icc], left, left, refl }
 
-@[simp] lemma left_mem_interval : a ∈ [a, b] :=
-by { rw [interval, mem_Icc], exact ⟨min_le_left _ _, le_max_left _ _⟩ }
-
-@[simp] lemma right_mem_interval : b ∈ [a, b] :=
-by { rw interval_swap, exact left_mem_interval }
+@[simp] lemma left_mem_interval : a ∈ [a, b] := by simp [mem_interval, le_total]
+@[simp] lemma right_mem_interval : b ∈ [a, b] := by simp [mem_interval, le_total]
 
 lemma Icc_subset_interval : Icc a b ⊆ [a, b] :=
 Icc_subset_Icc (min_le_left _ _) (le_max_right _ _)
@@ -87,10 +90,10 @@ Icc_subset_interval ⟨ha, hb⟩
 lemma mem_interval_of_ge (hb : b ≤ x) (ha : x ≤ a) : x ∈ [a, b] :=
 Icc_subset_interval' ⟨hb, ha⟩
 
-lemma not_mem_interval_of_lt (ha : c < a) (hb : c < b) : c ∉ interval a b :=
+lemma not_mem_interval_of_lt (ha : c < a) (hb : c < b) : c ∉ [a, b] :=
 not_mem_Icc_of_lt $ lt_min_iff.mpr ⟨ha, hb⟩
 
-lemma not_mem_interval_of_gt (ha : a < c) (hb : b < c) : c ∉ interval a b :=
+lemma not_mem_interval_of_gt (ha : a < c) (hb : b < c) : c ∉ [a, b] :=
 not_mem_Icc_of_gt $ max_lt_iff.mpr ⟨ha, hb⟩
 
 lemma interval_subset_interval (h₁ : a₁ ∈ [a₂, b₂]) (h₂ : b₁ ∈ [a₂, b₂]) : [a₁, b₁] ⊆ [a₂, b₂] :=
@@ -114,18 +117,21 @@ interval_subset_interval left_mem_interval h
 
 /-- A sort of triangle inequality. -/
 lemma interval_subset_interval_union_interval : [a, c] ⊆ [a, b] ∪ [b, c] :=
-begin
-  rintro x hx,
-  obtain hac | hac := le_total a c,
-  { rw interval_of_le hac at hx,
-    obtain hb | hb := le_total x b,
-    { exact or.inl (mem_interval_of_le hx.1 hb) },
-    { exact or.inr (mem_interval_of_le hb hx.2) } },
-  { rw interval_of_ge hac at hx,
-    obtain hb | hb := le_total x b,
-    { exact or.inr (mem_interval_of_ge hx.1 hb) },
-    { exact or.inl (mem_interval_of_ge hb hx.2) } }
-end
+λ x, by simp only [mem_interval, mem_union]; cases le_total a c; cases le_total x b; tauto
+
+lemma eq_of_mem_interval_of_mem_interval : a ∈ [b, c] → b ∈ [a, c] → a = b :=
+by simp_rw mem_interval; rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩); apply le_antisymm;
+  assumption <|> { exact le_trans ‹_› ‹_› }
+
+lemma eq_of_mem_interval_of_mem_interval' : b ∈ [a, c] → c ∈ [a, b] → b = c :=
+by simpa only [interval_swap a] using eq_of_mem_interval_of_mem_interval
+
+lemma interval_injective_right (a : α) : injective (λ b, interval b a) :=
+λ b c h, by { rw ext_iff at h,
+  exact eq_of_mem_interval_of_mem_interval ((h _).1 left_mem_interval) ((h _).2 left_mem_interval) }
+
+lemma interval_injective_left (a : α) : injective (interval a) :=
+by simpa only [interval_swap] using interval_injective_right a
 
 lemma bdd_below_bdd_above_iff_subset_interval (s : set α) :
   bdd_below s ∧ bdd_above s ↔ ∃ a b, s ⊆ [a, b] :=
@@ -142,15 +148,24 @@ def interval_oc : α → α → set α := λ a b, Ioc (min a b) (max a b)
 -- Below is a capital iota
 localized "notation `Ι` := set.interval_oc" in interval
 
-lemma interval_oc_of_le (h : a ≤ b) : Ι a b = Ioc a b :=
+@[simp] lemma interval_oc_of_le (h : a ≤ b) : Ι a b = Ioc a b :=
 by simp [interval_oc, h]
 
-lemma interval_oc_of_lt (h : b < a) : Ι a b = Ioc b a :=
+@[simp] lemma interval_oc_of_lt (h : b < a) : Ι a b = Ioc b a :=
 by simp [interval_oc, le_of_lt h]
 
 lemma interval_oc_eq_union : Ι a b = Ioc a b ∪ Ioc b a :=
 by cases le_total a b; simp [interval_oc, *]
 
+lemma mem_interval_oc : a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b :=
+by simp only [interval_oc_eq_union, mem_union, mem_Ioc]
+
+lemma not_mem_interval_oc : a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a :=
+by { simp only [interval_oc_eq_union, mem_union, mem_Ioc, not_lt, ←not_le], tauto }
+
+@[simp] lemma left_mem_interval_oc : a ∈ Ι a b ↔ b < a := by simp [mem_interval_oc]
+@[simp] lemma right_mem_interval_oc : b ∈ Ι a b ↔ a < b := by simp [mem_interval_oc]
+
 lemma forall_interval_oc_iff  {P : α → Prop} :
   (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ (∀ x ∈ Ioc b a, P x) :=
 by simp only [interval_oc_eq_union, mem_union, or_imp_distrib, forall_and_distrib]
@@ -168,6 +183,36 @@ Ioc_subset_Ioc (min_le_left _ _) (le_max_right _ _)
 lemma Ioc_subset_interval_oc' : Ioc a b ⊆ Ι b a :=
 Ioc_subset_Ioc (min_le_right _ _) (le_max_left _ _)
 
+lemma eq_of_mem_interval_oc_of_mem_interval_oc : a ∈ Ι b c → b ∈ Ι a c → a = b :=
+by simp_rw mem_interval_oc; rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩); apply le_antisymm;
+  assumption <|> exact le_of_lt ‹_› <|> exact le_trans ‹_› (le_of_lt ‹_›)
+
+lemma eq_of_mem_interval_oc_of_mem_interval_oc' : b ∈ Ι a c → c ∈ Ι a b → b = c :=
+by simpa only [interval_oc_swap a] using eq_of_mem_interval_oc_of_mem_interval_oc
+
+lemma eq_of_not_mem_interval_oc_of_not_mem_interval_oc (ha : a ≤ c) (hb : b ≤ c) :
+  a ∉ Ι b c → b ∉ Ι a c → a = b :=
+by simp_rw not_mem_interval_oc; rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩); apply le_antisymm;
+    assumption <|> exact le_of_lt ‹_› <|> cases not_le_of_lt ‹_› ‹_›
+
+lemma interval_oc_injective_right (a : α) : injective (λ b, Ι b a) :=
+begin
+  rintro b c h,
+  rw ext_iff at h,
+  obtain ha | ha := le_or_lt b a,
+  { have hb := (h b).not,
+    simp only [ha, left_mem_interval_oc, not_lt, true_iff, not_mem_interval_oc, ←not_le, and_true,
+      not_true, false_and, not_false_iff, true_iff, or_false] at hb,
+    refine hb.eq_of_not_lt (λ hc, _),
+    simpa [ha, and_iff_right hc, ←@not_le _ _ _ a, -not_le] using h c },
+  { refine eq_of_mem_interval_oc_of_mem_interval_oc ((h _).1 $ left_mem_interval_oc.2 ha)
+      ((h _).2 $ left_mem_interval_oc.2 $ ha.trans_le _),
+    simpa [ha, ha.not_le, mem_interval_oc] using h b }
+end
+
+lemma interval_oc_injective_left (a : α) : injective (Ι a) :=
+by simpa only [interval_oc_swap] using interval_oc_injective_right a
+
 end linear_order
 
 open_locale interval