feat/refactor(library/algebra/interval): use i for infinite, add some theorems

library/algebra/interval.lean

@@ -5,17 +5,11 @@ Author: Jeremy Avigad
 
 Notation for intervals and some properties.
 
-The mnemonic: o = open, c = closed, u = unbounded. For example, Iou a b is '(a, ∞).
+The mnemonic: o = open, c = closed, i = infinity. For example, Ioi a b is '(a, ∞).
 -/
 import .order data.set
 open set
 
--- TODO: move
-section
-  open set
-
-end
-
 namespace interval
 
 section order_pair
@@ -25,26 +19,26 @@ definition Ioo (a b : A) : set A := {x | a < x ∧ x < b}
 definition Ioc (a b : A) : set A := {x | a < x ∧ x ≤ b}
 definition Ico (a b : A) : set A := {x | a ≤ x ∧ x < b}
 definition Icc (a b : A) : set A := {x | a ≤ x ∧ x ≤ b}
-definition Iou (a : A)   : set A := {x | a < x}
-definition Icu (a : A)   : set A := {x | a ≤ x}
-definition Iuo (b : A)   : set A := {x | x < b}
-definition Iuc (b : A)   : set A := {x | x ≤ b}
+definition Ioi (a : A)   : set A := {x | a < x}
+definition Ici (a : A)   : set A := {x | a ≤ x}
+definition Iio (b : A)   : set A := {x | x < b}
+definition Iic (b : A)   : set A := {x | x ≤ b}
 
 notation `'(` a `, ` b `)`     := Ioo a b
 notation `'(` a `, ` b `]`     := Ioc a b
 notation `'[` a `, ` b `)`     := Ico a b
 notation `'[` a `, ` b `]`     := Icc a b
-notation `'(` a `, ` `∞` `)`   := Iou a
-notation `'[` a `, ` `∞` `)`   := Icu a
-notation `'(` `-∞` `, ` b `)`  := Iuo b
-notation `'(` `-∞` `, ` b `]`  := Iuc b
+notation `'(` a `, ` `∞` `)`   := Ioi a
+notation `'[` a `, ` `∞` `)`   := Ici a
+notation `'(` `-∞` `, ` b `)`  := Iio b
+notation `'(` `-∞` `, ` b `]`  := Iic b
 
 variables a b : A
 
-proposition Iou_inter_Iuo : '(a, ∞) ∩ '(-∞, b) = '(a, b) := rfl
-proposition Icu_inter_Iuo : '[a, ∞) ∩ '(-∞, b) = '[a, b) := rfl
-proposition Iou_inter_Iuc : '(a, ∞) ∩ '(-∞, b] = '(a, b] := rfl
-proposition Ioc_inter_Iuc : '[a, ∞) ∩ '(-∞, b] = '[a, b] := rfl
+proposition Ioi_inter_Iio : '(a, ∞) ∩ '(-∞, b) = '(a, b) := rfl
+proposition Ici_inter_Iio : '[a, ∞) ∩ '(-∞, b) = '[a, b) := rfl
+proposition Ioi_inter_Iic : '(a, ∞) ∩ '(-∞, b] = '(a, b] := rfl
+proposition Ioc_inter_Iic : '[a, ∞) ∩ '(-∞, b] = '[a, b] := rfl
 
 proposition Icc_self : '[a, a] = '{a} :=
 set.ext (take x, iff.intro
@@ -55,21 +49,47 @@ set.ext (take x, iff.intro
     have x = a, from eq_of_mem_singleton this,
     show a ≤ x ∧ x ≤ a, from and.intro (eq.subst this !le.refl) (eq.subst this !le.refl)))
 
+proposition Icc_eq_empty {a b : A} (H : b < a) : '[a, b] = ∅ :=
+eq_empty_of_forall_not_mem
+  (take x, suppose x ∈ '[a, b],
+    have a ≤ b, from le.trans (and.left this) (and.right this),
+    not_le_of_gt H this)
+
 end order_pair
 
-section decidable_linear_order
+section strong_order_pair
 
-variables {A : Type} [decidable_linear_order A]
+variables {A : Type} [linear_strong_order_pair A]
+
+proposition compl_Ici (a : A) : -'[a, ∞) = '(-∞, a) :=
+ext (take x, iff.intro
+  (assume H, lt_of_not_ge H)
+  (assume H, not_le_of_gt H))
+
+proposition compl_Iic (a : A) : -'(-∞, a] = '(a, ∞) :=
+ext (take x, iff.intro
+  (assume H, lt_of_not_ge H)
+  (assume H, not_le_of_gt H))
+
+proposition compl_Ioi (a : A) : -'(a, ∞) = '(-∞, a] :=
+ext (take x, iff.intro
+  (assume H, le_of_not_gt H)
+  (assume H, not_lt_of_ge H))
+
+proposition compl_Iio (a : A) : -'(-∞, a) = '[a, ∞) :=
+ext (take x, iff.intro
+  (assume H, le_of_not_gt H)
+  (assume H, not_lt_of_ge H))
 
 proposition Icc_eq_Icc_union_Ioc {a b c : A} (H1 : a ≤ b) (H2 : b ≤ c) :
   '[a, c] = '[a, b] ∪ '(b, c] :=
 set.ext (take x, iff.intro
   (assume H3 :  x ∈ '[a, c],
-    decidable.by_cases
+    or.elim (le_or_gt x b)
       (suppose x ≤ b,
          or.inl (and.intro (and.left H3) this))
-      (suppose ¬ x ≤ b,
-         or.inr (and.intro (lt_of_not_ge this) (and.right H3))))
+      (suppose x > b,
+         or.inr (and.intro this (and.right H3))))
   (suppose x ∈ '[a, b] ∪ '(b, c],
     or.elim this
       (suppose x ∈ '[a, b],
@@ -77,7 +97,10 @@ set.ext (take x, iff.intro
       (suppose x ∈ '(b, c],
          and.intro (le_of_lt (lt_of_le_of_lt H1 (and.left this))) (and.right this))))
 
-end decidable_linear_order
+proposition singleton_union_Ioc {a b : A} (H : a ≤ b) : '{a} ∪ '(a, b] = '[a,b] :=
+by rewrite [-Icc_self, Icc_eq_Icc_union_Ioc !le.refl H]
+
+end strong_order_pair
 
 /- intervals of natural numbers -/
 
@@ -99,12 +122,12 @@ open nat eq.ops
     (assume H, and.intro (and.left H) (le_of_lt_succ (and.right H)))
     (assume H, and.intro (and.left H) (lt_succ_of_le (and.right H))))
 
-  proposition Icu_zero : '[(0 : nat), ∞) = univ :=
+  proposition Ici_zero : '[(0 : nat), ∞) = univ :=
   eq_univ_of_forall (take x, zero_le x)
 
   proposition Icc_zero (n : ℕ) : '[0, n] = '(-∞, n] :=
   have '[0, n] = '[0, ∞) ∩ '(-∞, n], from rfl,
-  by+ rewrite [this, Icu_zero, univ_inter]
+  by+ rewrite [this, Ici_zero, univ_inter]
 
   proposition bij_on_add_Icc_zero (m n : ℕ) : bij_on (add m) ('[0, n]) ('[m, m+n]) :=
   have mapsto : ∀₀ i ∈ '[0, n], m + i ∈ '[m, m+n], from
@@ -130,7 +153,7 @@ section nat -- put the instances in the intervals namespace
 open nat eq.ops
   variables m n : ℕ
 
-  proposition nat.Iuc_finite [instance] (n : ℕ) : finite '(-∞, n] :=
+  proposition nat.Iic_finite [instance] (n : ℕ) : finite '(-∞, n] :=
   nat.induction_on n
     (have '(-∞, 0] ⊆ '{0}, from λ x H, mem_singleton_of_eq (le.antisymm H !zero_le),
       finite_subset this)
@@ -139,7 +162,7 @@ open nat eq.ops
         by intro x H; rewrite [mem_union_iff, mem_singleton_iff]; apply le_or_eq_succ_of_le_succ H,
         finite_subset this)
 
-  proposition nat.Iuo_finite [instance] (n : ℕ) : finite '(-∞, n) :=
+  proposition nat.Iio_finite [instance] (n : ℕ) : finite '(-∞, n) :=
   have '(-∞, n) ⊆ '(-∞, n], from λ x, le_of_lt,
   finite_subset this