feat(algebra/order,...): material on orders (#554)

Author: sgouezel

algebra/order.lean

@@ -104,18 +104,26 @@ lemma le_of_forall_le [preorder α] {a b : α}
   (H : ∀ c, c ≤ a → c ≤ b) : a ≤ b :=
 H _ (le_refl _)
 
+lemma le_of_forall_le' [preorder α] {a b : α}
+  (H : ∀ c, a ≤ c → b ≤ c) : b ≤ a :=
+H _ (le_refl _)
+
 lemma le_of_forall_lt [linear_order α] {a b : α}
   (H : ∀ c, c < a → c < b) : a ≤ b :=
 le_of_not_lt $ λ h, lt_irrefl _ (H _ h)
 
+lemma le_of_forall_lt' [linear_order α] {a b : α}
+  (H : ∀ c, a < c → b < c) : b ≤ a :=
+le_of_not_lt $ λ h, lt_irrefl _ (H _ h)
+
 lemma eq_of_forall_ge_iff [partial_order α] {a b : α}
   (H : ∀ c, a ≤ c ↔ b ≤ c) : a = b :=
 le_antisymm ((H _).2 (le_refl _)) ((H _).1 (le_refl _))
 
 /-- monotonicity of `≤` with respect to `→` -/
 lemma le_implies_le_of_le_of_le {a b c d : α} [preorder α]
    (h₀ : c ≤ a) (h₁ : b ≤ d) :
-  a ≤ b -> c ≤ d :=
+  a ≤ b → c ≤ d :=
 assume h₂ : a ≤ b,
 calc  c
     ≤ a : h₀

algebra/order_functions.lean

@@ -16,8 +16,8 @@ section
 variables [decidable_linear_order α] [decidable_linear_order β] {f : α → β} {a b c d : α}
 
 -- translate from lattices to linear orders (sup → max, inf → min)
-lemma le_min_iff : c ≤ min a b ↔ c ≤ a ∧ c ≤ b := le_inf_iff
-lemma max_le_iff : max a b ≤ c ↔ a ≤ c ∧ b ≤ c := sup_le_iff
+@[simp] lemma le_min_iff : c ≤ min a b ↔ c ≤ a ∧ c ≤ b := le_inf_iff
+@[simp] lemma max_le_iff : max a b ≤ c ↔ a ≤ c ∧ b ≤ c := sup_le_iff
 lemma max_le_max : a ≤ c → b ≤ d → max a b ≤ max c d := sup_le_sup
 lemma min_le_min : a ≤ c → b ≤ d → min a b ≤ min c d := inf_le_inf
 lemma le_max_left_of_le : a ≤ b → a ≤ max b c := le_sup_left_of_le
@@ -32,30 +32,30 @@ lemma min_max_distrib_right : min (max a b) c = max (min a c) (min b c) := inf_s
 instance max_idem : is_idempotent α max := by apply_instance
 instance min_idem : is_idempotent α min := by apply_instance
 
-lemma min_le_iff : min a b ≤ c ↔ a ≤ c ∨ b ≤ c :=
+@[simp] lemma min_le_iff : min a b ≤ c ↔ a ≤ c ∨ b ≤ c :=
 have a ≤ b → (a ≤ c ∨ b ≤ c ↔ a ≤ c),
   from assume h, or_iff_left_of_imp $ le_trans h,
 have b ≤ a → (a ≤ c ∨ b ≤ c ↔ b ≤ c),
   from assume h, or_iff_right_of_imp $ le_trans h,
 by cases le_total a b; simp *
 
-lemma le_max_iff : a ≤ max b c ↔ a ≤ b ∨ a ≤ c :=
+@[simp] lemma le_max_iff : a ≤ max b c ↔ a ≤ b ∨ a ≤ c :=
 have b ≤ c → (a ≤ b ∨ a ≤ c ↔ a ≤ c),
   from assume h, or_iff_right_of_imp $ assume h', le_trans h' h,
 have c ≤ b → (a ≤ b ∨ a ≤ c ↔ a ≤ b),
   from assume h, or_iff_left_of_imp $ assume h', le_trans h' h,
 by cases le_total b c; simp *
 
-lemma max_lt_iff : max a b < c ↔ (a < c ∧ b < c) :=
+@[simp] lemma max_lt_iff : max a b < c ↔ (a < c ∧ b < c) :=
 by rw [lt_iff_not_ge]; simp [(≥), le_max_iff, not_or_distrib]
 
-lemma lt_min_iff : a < min b c ↔ (a < b ∧ a < c) :=
+@[simp] lemma lt_min_iff : a < min b c ↔ (a < b ∧ a < c) :=
 by rw [lt_iff_not_ge]; simp [(≥), min_le_iff, not_or_distrib]
 
-lemma lt_max_iff : a < max b c ↔ a < b ∨ a < c :=
+@[simp] lemma lt_max_iff : a < max b c ↔ a < b ∨ a < c :=
 by rw [lt_iff_not_ge]; simp [(≥), max_le_iff, not_and_distrib]
 
-lemma min_lt_iff : min a b < c ↔ a < c ∨ b < c :=
+@[simp] lemma min_lt_iff : min a b < c ↔ a < c ∨ b < c :=
 by rw [lt_iff_not_ge]; simp [(≥), le_min_iff, not_and_distrib]
 
 theorem min_right_comm (a b c : α) : min (min a b) c = min (min a c) b :=

algebra/ordered_group.lean

@@ -277,6 +277,15 @@ coe_lt_coe
 lemma add_eq_top [ordered_comm_monoid α] (a b : with_top α) : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
 by cases a; cases b; simp [none_eq_top, some_eq_coe, coe_add.symm]
 
+lemma add_lt_top [ordered_comm_monoid α] (a b : with_top α) : a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤ :=
+begin
+  apply not_iff_not.1,
+  simp [lt_top_iff_ne_top, add_eq_top],
+  finish,
+  apply classical.dec _,
+  apply classical.dec _,
+end
+
 instance [canonically_ordered_monoid α] : canonically_ordered_monoid (with_top α) :=
 { le_iff_exists_add := assume a b,
   match a, b with
@@ -440,6 +449,10 @@ lemma with_top.add_lt_add_iff_left :
       exact add_lt_add_iff_left _ }
   end
 
+lemma with_top.add_lt_add_iff_right
+  {a b c : with_top α} : a < ⊤ → (c + a < b + a ↔ c < b) :=
+by simpa [add_comm] using @with_top.add_lt_add_iff_left _ _ a b c
+
 end ordered_cancel_comm_monoid
 
 section ordered_comm_group

algebra/ordered_ring.lean

@@ -367,6 +367,15 @@ begin
   simp [ha, hb, mul_def, option.bind_comm a b, mul_comm]
 end
 
+@[simp] lemma mul_eq_top_iff {a b : with_top α} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
+begin
+  have H : ∀x:α, (¬x = 0) ↔ (⊤ : with_top α) * ↑x = ⊤ :=
+    λx, ⟨λhx, by simp [top_mul, hx], λhx f, by simpa [f] using hx⟩,
+  cases a; cases b; simp [none_eq_top, top_mul, coe_ne_top, some_eq_coe, coe_mul.symm],
+  { rw [H b] },
+  { rw [H a, comm] }
+end
+
 private lemma distrib' (a b c : with_top α) : (a + b) * c = a * c + b * c :=
 begin
   cases c,

data/finset.lean

@@ -1299,15 +1299,8 @@ lemma sup_mono (h : s₁ ⊆ s₂) : s₁.sup f ≤ s₂.sup f :=
 sup_le $ assume b hb, le_sup (h hb)
 
 lemma sup_lt [is_total α (≤)] {a : α} : (⊥ < a) → (∀b ∈ s, f b < a) → s.sup f < a :=
-have A : ∀ x y, x < a → y < a → x ⊔ y < a :=
-begin
-  assume x y hx hy,
-  cases (is_total.total (≤) x y) with h,
-  { simpa [sup_of_le_right h] using hy },
-  { simpa [sup_of_le_left h] using hx }
-end,
 by letI := classical.dec_eq β; from
-finset.induction_on s (by simp) (by simp [A] {contextual := tt})
+finset.induction_on s (by simp) (by simp {contextual := tt})
 
 lemma comp_sup_eq_sup_comp [is_total α (≤)] {γ : Type} [semilattice_sup_bot γ]
   (g : α → γ) (mono_g : monotone g) (bot : g ⊥ = ⊥) : g (s.sup f) = s.sup (g ∘ f) :=
@@ -1377,15 +1370,8 @@ lemma inf_mono (h : s₁ ⊆ s₂) : s₂.inf f ≤ s₁.inf f :=
 le_inf $ assume b hb, inf_le (h hb)
 
 lemma lt_inf [is_total α (≤)] {a : α} : (a < ⊤) → (∀b ∈ s, a < f b) → a < s.inf f :=
-have A : ∀ x y, a < x → a < y → a < x ⊓ y :=
-begin
-  assume x y hx hy,
-  cases (is_total.total (≤) x y) with h,
-  { simpa [inf_of_le_left h] using hy },
-  { simpa [inf_of_le_right h] using hx }
-end,
 by letI := classical.dec_eq β; from
-finset.induction_on s (by simp) (by simp [A] {contextual := tt})
+finset.induction_on s (by simp) (by simp {contextual := tt})
 
 lemma comp_inf_eq_inf_comp [is_total α (≤)] {γ : Type} [semilattice_inf_top γ]
   (g : α → γ) (mono_g : monotone g) (top : g ⊤ = ⊤) : g (s.inf f) = s.inf (g ∘ f) :=

order/bounded_lattice.lean

@@ -61,6 +61,9 @@ begin
   by simp [-top_le_iff, lt_iff_le_not_le, not_iff_not.2 (@top_le_iff _ _ a)]
 end
 
+lemma ne_top_of_lt (h : a < b) : a ≠ ⊤ :=
+lt_top_iff_ne_top.1 $ lt_of_lt_of_le h le_top
+
 end order_top
 
 theorem order_top.ext_top {α} {A B : order_top α}
@@ -113,6 +116,9 @@ begin
   simp [-le_bot_iff, lt_iff_le_not_le, not_iff_not.2 (@le_bot_iff _ _ a)]
 end
 
+lemma ne_bot_of_gt (h : a < b) : b ≠ ⊥ :=
+bot_lt_iff_ne_bot.1 $ lt_of_le_of_lt bot_le h
+
 end order_bot
 
 theorem order_bot.ext_bot {α} {A B : order_bot α}

order/lattice.lean

@@ -93,6 +93,13 @@ by finish
 theorem le_of_sup_eq (h : a ⊔ b = b) : a ≤ b :=
 by finish
 
+@[simp] lemma sup_lt_iff [is_total α (≤)] {a b c : α} : b ⊔ c < a ↔ b < a ∧ c < a :=
+begin
+  cases (is_total.total (≤) b c) with h,
+  { simp [sup_of_le_right h], exact ⟨λI, ⟨lt_of_le_of_lt h I, I⟩, λH, H.2⟩ },
+  { simp [sup_of_le_left h], exact ⟨λI, ⟨I, lt_of_le_of_lt h I⟩, λH, H.1⟩ }
+end
+
 @[simp] theorem sup_idem : a ⊔ a = a :=
 by apply le_antisymm; finish
 
@@ -179,6 +186,13 @@ by finish
 theorem le_of_inf_eq (h : a ⊓ b = a) : a ≤ b :=
 by finish
 
+@[simp] lemma lt_inf_iff [is_total α (≤)] {a b c : α} : a < b ⊓ c ↔ a < b ∧ a < c :=
+begin
+  cases (is_total.total (≤) b c) with h,
+  { simp [inf_of_le_left h], exact ⟨λI, ⟨I, lt_of_lt_of_le I h⟩, λH, H.1⟩ },
+  { simp [inf_of_le_right h], exact ⟨λI, ⟨lt_of_lt_of_le I h, I⟩, λH, H.2⟩ }
+end
+
 @[simp] theorem inf_idem : a ⊓ a = a :=
 by apply le_antisymm; finish