feat(library/init/algebra): add ordered_field
This commit is contained in:
Leonardo de Moura
parent
97fe22b20e
commit
303696e693
2 changed files with 457 additions and 1 deletions
362
library/init/algebra/ordered_field.lean
Normal file
362
library/init/algebra/ordered_field.lean
Normal file
|
|
@ -0,0 +1,362 @@
|
|||
/-
|
||||
Copyright (c) 2014 Robert Lewis. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Robert Lewis, Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.algebra.ordered_ring init.algebra.field
|
||||
|
||||
universe variables u
|
||||
|
||||
class linear_ordered_field (α : Type u) extends linear_ordered_ring α, field α
|
||||
|
||||
section linear_ordered_field
|
||||
variables {α : Type u} [linear_ordered_field α]
|
||||
|
||||
lemma mul_zero_lt_mul_inv_of_pos {a : α} (h : 0 < a) : a * 0 < a * (1 / a) :=
|
||||
calc a * 0 = 0 : by rw mul_zero
|
||||
... < 1 : zero_lt_one
|
||||
... = a * a⁻¹ : eq.symm (mul_inv_cancel (ne.symm (ne_of_lt h)))
|
||||
... = a * (1 / a) : by rw inv_eq_one_div
|
||||
|
||||
lemma mul_zero_lt_mul_inv_of_neg {a : α} (h : a < 0) : a * 0 < a * (1 / a) :=
|
||||
calc a * 0 = 0 : by rw mul_zero
|
||||
... < 1 : zero_lt_one
|
||||
... = a * a⁻¹ : eq.symm (mul_inv_cancel (ne_of_lt h))
|
||||
... = a * (1 / a) : by rw inv_eq_one_div
|
||||
|
||||
lemma one_div_pos_of_pos {a : α} (h : 0 < a) : 0 < 1 / a :=
|
||||
lt_of_mul_lt_mul_left (mul_zero_lt_mul_inv_of_pos h) (le_of_lt h)
|
||||
|
||||
lemma one_div_neg_of_neg {a : α} (h : a < 0) : 1 / a < 0 :=
|
||||
gt_of_mul_lt_mul_neg_left (mul_zero_lt_mul_inv_of_neg h) (le_of_lt h)
|
||||
|
||||
lemma le_mul_of_ge_one_right {a b : α} (hb : b ≥ 0) (h : a ≥ 1) : b ≤ b * a :=
|
||||
suffices b * 1 ≤ b * a, by rwa mul_one at this,
|
||||
mul_le_mul_of_nonneg_left h hb
|
||||
|
||||
lemma lt_mul_of_gt_one_right {a b : α} (hb : b > 0) (h : a > 1) : b < b * a :=
|
||||
suffices b * 1 < b * a, by rwa mul_one at this,
|
||||
mul_lt_mul_of_pos_left h hb
|
||||
|
||||
lemma one_le_div_of_le (a : α) {b : α} (hb : b > 0) (h : b ≤ a) : 1 ≤ a / b :=
|
||||
have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
|
||||
have hbinv : 1 / b > 0, from one_div_pos_of_pos hb,
|
||||
calc
|
||||
1 = b * (1 / b) : eq.symm (mul_one_div_cancel hb')
|
||||
... ≤ a * (1 / b) : mul_le_mul_of_nonneg_right h (le_of_lt hbinv)
|
||||
... = a / b : eq.symm $ div_eq_mul_one_div a b
|
||||
|
||||
lemma le_of_one_le_div (a : α) {b : α} (hb : b > 0) (h : 1 ≤ a / b) : b ≤ a :=
|
||||
have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
|
||||
calc
|
||||
b ≤ b * (a / b) : le_mul_of_ge_one_right (le_of_lt hb) h
|
||||
... = a : by rw [mul_div_cancel' _ hb']
|
||||
|
||||
lemma one_lt_div_of_lt (a : α) {b : α} (hb : b > 0) (h : b < a) : 1 < a / b :=
|
||||
have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
|
||||
have hbinv : 1 / b > 0, from one_div_pos_of_pos hb, calc
|
||||
1 = b * (1 / b) : eq.symm (mul_one_div_cancel hb')
|
||||
... < a * (1 / b) : mul_lt_mul_of_pos_right h hbinv
|
||||
... = a / b : eq.symm $ div_eq_mul_one_div a b
|
||||
|
||||
lemma lt_of_one_lt_div (a : α) {b : α} (hb : b > 0) (h : 1 < a / b) : b < a :=
|
||||
have hb' : b ≠ 0, from ne.symm (ne_of_lt hb),
|
||||
calc
|
||||
b < b * (a / b) : lt_mul_of_gt_one_right hb h
|
||||
... = a : by rw [mul_div_cancel' _ hb']
|
||||
|
||||
-- the following lemmas amount to four iffs, for <, ≤, ≥, >.
|
||||
|
||||
lemma mul_le_of_le_div {a b c : α} (hc : 0 < c) (h : a ≤ b / c) : a * c ≤ b :=
|
||||
div_mul_cancel b (ne.symm (ne_of_lt hc)) ▸ mul_le_mul_of_nonneg_right h (le_of_lt hc)
|
||||
|
||||
lemma le_div_of_mul_le {a b c : α} (hc : 0 < c) (h : a * c ≤ b) : a ≤ b / c :=
|
||||
calc
|
||||
a = a * c * (1 / c) : mul_mul_div a (ne.symm (ne_of_lt hc))
|
||||
... ≤ b * (1 / c) : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hc))
|
||||
... = b / c : eq.symm $ div_eq_mul_one_div b c
|
||||
|
||||
lemma mul_lt_of_lt_div {a b c : α} (hc : 0 < c) (h : a < b / c) : a * c < b :=
|
||||
div_mul_cancel b (ne.symm (ne_of_lt hc)) ▸ mul_lt_mul_of_pos_right h hc
|
||||
|
||||
lemma lt_div_of_mul_lt {a b c : α} (hc : 0 < c) (h : a * c < b) : a < b / c :=
|
||||
calc
|
||||
a = a * c * (1 / c) : mul_mul_div a (ne.symm (ne_of_lt hc))
|
||||
... < b * (1 / c) : mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
|
||||
... = b / c : eq.symm $ div_eq_mul_one_div b c
|
||||
|
||||
lemma mul_le_of_div_le_of_neg {a b c : α} (hc : c < 0) (h : b / c ≤ a) : a * c ≤ b :=
|
||||
div_mul_cancel b (ne_of_lt hc) ▸ mul_le_mul_of_nonpos_right h (le_of_lt hc)
|
||||
|
||||
lemma div_le_of_mul_le_of_neg {a b c : α} (hc : c < 0) (h : a * c ≤ b) : b / c ≤ a :=
|
||||
calc
|
||||
a = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc)
|
||||
... ≥ b * (1 / c) : mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc))
|
||||
... = b / c : eq.symm $ div_eq_mul_one_div b c
|
||||
|
||||
lemma mul_lt_of_gt_div_of_neg {a b c : α} (hc : c < 0) (h : a > b / c) : a * c < b :=
|
||||
div_mul_cancel b (ne_of_lt hc) ▸ mul_lt_mul_of_neg_right h hc
|
||||
|
||||
lemma div_lt_of_mul_lt_of_pos {a b c : α} (hc : c > 0) (h : b < a * c) : b / c < a :=
|
||||
calc
|
||||
a = a * c * (1 / c) : mul_mul_div a (ne_of_gt hc)
|
||||
... > b * (1 / c) : mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
|
||||
... = b / c : eq.symm $ div_eq_mul_one_div b c
|
||||
|
||||
lemma div_lt_of_mul_gt_of_neg {a b c : α} (hc : c < 0) (h : a * c < b) : b / c < a :=
|
||||
calc
|
||||
a = a * c * (1 / c) : mul_mul_div a (ne_of_lt hc)
|
||||
... > b * (1 / c) : mul_lt_mul_of_neg_right h (one_div_neg_of_neg hc)
|
||||
... = b / c : eq.symm $ div_eq_mul_one_div b c
|
||||
|
||||
lemma div_le_of_le_mul {a b c : α} (hb : b > 0) (h : a ≤ b * c) : a / b ≤ c :=
|
||||
calc
|
||||
a / b = a * (1 / b) : div_eq_mul_one_div a b
|
||||
... ≤ (b * c) * (1 / b) : mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hb))
|
||||
... = (b * c) / b : eq.symm $ div_eq_mul_one_div (b * c) b
|
||||
... = c : by rw [mul_div_cancel_left _ (ne.symm (ne_of_lt hb))]
|
||||
|
||||
lemma le_mul_of_div_le {a b c : α} (hc : c > 0) (h : a / c ≤ b) : a ≤ b * c :=
|
||||
calc
|
||||
a = a / c * c : by rw (div_mul_cancel _ (ne.symm (ne_of_lt hc)))
|
||||
... ≤ b * c : mul_le_mul_of_nonneg_right h (le_of_lt hc)
|
||||
|
||||
-- following these in the isabelle file, there are 8 biconditionals for the above with - signs
|
||||
-- skipping for now
|
||||
|
||||
lemma mul_sub_mul_div_mul_neg {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / c < b / d) :
|
||||
(a * d - b * c) / (c * d) < 0 :=
|
||||
have h1 : a / c - b / d < 0, from calc
|
||||
a / c - b / d < b / d - b / d : sub_lt_sub_right h _
|
||||
... = 0 : by rw sub_self,
|
||||
calc
|
||||
0 > a / c - b / d : h1
|
||||
... = (a * d - c * b) / (c * d) : div_sub_div _ _ hc hd
|
||||
... = (a * d - b * c) / (c * d) : by rw (mul_comm b c)
|
||||
|
||||
lemma mul_sub_mul_div_mul_nonpos {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0) (h : a / c ≤ b / d) :
|
||||
(a * d - b * c) / (c * d) ≤ 0 :=
|
||||
have h1 : a / c - b / d ≤ 0, from calc
|
||||
a / c - b / d ≤ b / d - b / d : sub_le_sub_right h _
|
||||
... = 0 : by rw sub_self,
|
||||
calc
|
||||
0 ≥ a / c - b / d : h1
|
||||
... = (a * d - c * b) / (c * d) : div_sub_div _ _ hc hd
|
||||
... = (a * d - b * c) / (c * d) : by rw (mul_comm b c)
|
||||
|
||||
lemma div_lt_div_of_mul_sub_mul_div_neg {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0)
|
||||
(h : (a * d - b * c) / (c * d) < 0) : a / c < b / d :=
|
||||
have (a * d - c * b) / (c * d) < 0, by rwa [mul_comm c b],
|
||||
have a / c - b / d < 0, by rwa [div_sub_div _ _ hc hd],
|
||||
have a / c - b / d + b / d < 0 + b / d, from add_lt_add_right this _,
|
||||
by rwa [zero_add, sub_eq_add_neg, neg_add_cancel_right] at this
|
||||
|
||||
|
||||
lemma div_le_div_of_mul_sub_mul_div_nonpos {a b c d : α} (hc : c ≠ 0) (hd : d ≠ 0)
|
||||
(h : (a * d - b * c) / (c * d) ≤ 0) : a / c ≤ b / d :=
|
||||
have (a * d - c * b) / (c * d) ≤ 0, by rwa [mul_comm c b],
|
||||
have a / c - b / d ≤ 0, by rwa [div_sub_div _ _ hc hd],
|
||||
have a / c - b / d + b / d ≤ 0 + b / d, from add_le_add_right this _,
|
||||
by rwa [zero_add, sub_eq_add_neg, neg_add_cancel_right] at this
|
||||
|
||||
|
||||
lemma div_pos_of_pos_of_pos {a b : α} : 0 < a → 0 < b → 0 < a / b :=
|
||||
begin
|
||||
intros,
|
||||
rw div_eq_mul_one_div,
|
||||
apply mul_pos,
|
||||
assumption,
|
||||
apply one_div_pos_of_pos,
|
||||
assumption
|
||||
end
|
||||
|
||||
lemma div_nonneg_of_nonneg_of_pos {a b : α} : 0 ≤ a → 0 < b → 0 ≤ a / b :=
|
||||
begin
|
||||
intros, rw div_eq_mul_one_div,
|
||||
apply mul_nonneg, assumption,
|
||||
apply le_of_lt,
|
||||
apply one_div_pos_of_pos,
|
||||
assumption
|
||||
end
|
||||
|
||||
lemma div_neg_of_neg_of_pos {a b : α} : a < 0 → 0 < b → a / b < 0 :=
|
||||
begin
|
||||
intros, rw div_eq_mul_one_div,
|
||||
apply mul_neg_of_neg_of_pos,
|
||||
assumption,
|
||||
apply one_div_pos_of_pos,
|
||||
assumption
|
||||
end
|
||||
|
||||
lemma div_nonpos_of_nonpos_of_pos {a b : α} : a ≤ 0 → 0 < b → a / b ≤ 0 :=
|
||||
begin
|
||||
intros, rw div_eq_mul_one_div,
|
||||
apply mul_nonpos_of_nonpos_of_nonneg,
|
||||
assumption,
|
||||
apply le_of_lt,
|
||||
apply one_div_pos_of_pos,
|
||||
assumption
|
||||
end
|
||||
|
||||
lemma div_neg_of_pos_of_neg {a b : α} : 0 < a → b < 0 → a / b < 0 :=
|
||||
begin
|
||||
intros, rw div_eq_mul_one_div,
|
||||
apply mul_neg_of_pos_of_neg,
|
||||
assumption,
|
||||
apply one_div_neg_of_neg,
|
||||
assumption
|
||||
end
|
||||
|
||||
lemma div_nonpos_of_nonneg_of_neg {a b : α} : 0 ≤ a → b < 0 → a / b ≤ 0 :=
|
||||
begin
|
||||
intros, rw div_eq_mul_one_div,
|
||||
apply mul_nonpos_of_nonneg_of_nonpos,
|
||||
assumption,
|
||||
apply le_of_lt,
|
||||
apply one_div_neg_of_neg,
|
||||
assumption
|
||||
end
|
||||
|
||||
lemma div_pos_of_neg_of_neg {a b : α} : a < 0 → b < 0 → 0 < a / b :=
|
||||
begin
|
||||
intros, rw div_eq_mul_one_div,
|
||||
apply mul_pos_of_neg_of_neg,
|
||||
assumption,
|
||||
apply one_div_neg_of_neg,
|
||||
assumption
|
||||
end
|
||||
|
||||
lemma div_nonneg_of_nonpos_of_neg {a b : α} : a ≤ 0 → b < 0 → 0 ≤ a / b :=
|
||||
begin
|
||||
intros, rw div_eq_mul_one_div,
|
||||
apply mul_nonneg_of_nonpos_of_nonpos,
|
||||
assumption,
|
||||
apply le_of_lt,
|
||||
apply one_div_neg_of_neg,
|
||||
assumption
|
||||
end
|
||||
|
||||
lemma div_lt_div_of_lt_of_pos {a b c : α} (h : a < b) (hc : 0 < c) : a / c < b / c :=
|
||||
begin
|
||||
intros,
|
||||
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
|
||||
exact mul_lt_mul_of_pos_right h (one_div_pos_of_pos hc)
|
||||
end
|
||||
|
||||
lemma div_le_div_of_le_of_pos {a b c : α} (h : a ≤ b) (hc : 0 < c) : a / c ≤ b / c :=
|
||||
begin
|
||||
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
|
||||
exact mul_le_mul_of_nonneg_right h (le_of_lt (one_div_pos_of_pos hc))
|
||||
end
|
||||
|
||||
lemma div_lt_div_of_lt_of_neg {a b c : α} (h : b < a) (hc : c < 0) : a / c < b / c :=
|
||||
begin
|
||||
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
|
||||
exact mul_lt_mul_of_neg_right h (one_div_neg_of_neg hc)
|
||||
end
|
||||
|
||||
lemma div_le_div_of_le_of_neg {a b c : α} (h : b ≤ a) (hc : c < 0) : a / c ≤ b / c :=
|
||||
begin
|
||||
rw [div_eq_mul_one_div a c, div_eq_mul_one_div b c],
|
||||
exact mul_le_mul_of_nonpos_right h (le_of_lt (one_div_neg_of_neg hc))
|
||||
end
|
||||
|
||||
lemma two_pos : (2:α) > 0 :=
|
||||
begin unfold bit0, exact add_pos zero_lt_one zero_lt_one end
|
||||
|
||||
lemma two_ne_zero : (2:α) ≠ 0 :=
|
||||
ne.symm (ne_of_lt two_pos)
|
||||
|
||||
lemma add_halves (a : α) : a / 2 + a / 2 = a :=
|
||||
calc
|
||||
a / 2 + a / 2 = (a + a) / 2 : by rw div_add_div_same
|
||||
... = (a * 1 + a * 1) / 2 : by rw mul_one
|
||||
... = (a * (1 + 1)) / 2 : by rw left_distrib
|
||||
... = (a * 2) / 2 : by rw one_add_one_eq_two
|
||||
... = a : by rw [@mul_div_cancel α _ _ _ two_ne_zero]
|
||||
|
||||
lemma sub_self_div_two (a : α) : a - a / 2 = a / 2 :=
|
||||
suffices a / 2 + a / 2 - a / 2 = a / 2, by rwa add_halves at this,
|
||||
by rw [add_sub_cancel]
|
||||
|
||||
lemma add_midpoint {a b : α} (h : a < b) : a + (b - a) / 2 < b :=
|
||||
begin
|
||||
rw [-div_sub_div_same, sub_eq_add_neg, add_comm (b/2), -add_assoc, -sub_eq_add_neg],
|
||||
apply add_lt_of_lt_sub_right,
|
||||
rw [sub_self_div_two, sub_self_div_two],
|
||||
apply div_lt_div_of_lt_of_pos h two_pos
|
||||
end
|
||||
|
||||
lemma div_two_sub_self (a : α) : a / 2 - a = - (a / 2) :=
|
||||
suffices a / 2 - (a / 2 + a / 2) = - (a / 2), by rwa add_halves at this,
|
||||
by rw [sub_add_eq_sub_sub, sub_self, zero_sub]
|
||||
|
||||
lemma add_self_div_two (a : α) : (a + a) / 2 = a :=
|
||||
eq.symm
|
||||
(iff.mpr (eq_div_iff_mul_eq _ _ (ne_of_gt (add_pos (@zero_lt_one α _) zero_lt_one)))
|
||||
(begin unfold bit0, rw [left_distrib, mul_one] end))
|
||||
|
||||
lemma two_gt_one : (2:α) > 1 :=
|
||||
calc (2:α) = 1+1 : one_add_one_eq_two
|
||||
... > 1+0 : add_lt_add_left zero_lt_one _
|
||||
... = 1 : add_zero 1
|
||||
|
||||
lemma two_ge_one : (2:α) ≥ 1 :=
|
||||
le_of_lt two_gt_one
|
||||
|
||||
lemma four_pos : (4:α) > 0 :=
|
||||
add_pos two_pos two_pos
|
||||
|
||||
lemma mul_le_mul_of_mul_div_le {a b c d : α} (h : a * (b / c) ≤ d) (hc : c > 0) : b * a ≤ d * c :=
|
||||
begin
|
||||
rw [-mul_div_assoc] at h, rw [mul_comm b],
|
||||
apply le_mul_of_div_le hc h
|
||||
end
|
||||
|
||||
lemma div_two_lt_of_pos {a b : α} (h : a > 0) : a / 2 < a :=
|
||||
suffices a / (1 + 1) < a, begin unfold bit0, assumption end,
|
||||
have ha : a / 2 > 0, from div_pos_of_pos_of_pos h (add_pos zero_lt_one zero_lt_one),
|
||||
calc
|
||||
a / 2 < a / 2 + a / 2 : lt_add_of_pos_left _ ha
|
||||
... = a : add_halves a
|
||||
|
||||
lemma div_mul_le_div_mul_of_div_le_div_pos {a b c d e : α} (hb : b ≠ 0) (hd : d ≠ 0) (h : a / b ≤ c / d)
|
||||
(he : e > 0) : a / (b * e) ≤ c / (d * e) :=
|
||||
begin
|
||||
note h₁ := field.div_mul_eq_div_mul_one_div a hb (ne_of_gt he),
|
||||
note h₂ := field.div_mul_eq_div_mul_one_div c hd (ne_of_gt he),
|
||||
rw [h₁, h₂],
|
||||
apply mul_le_mul_of_nonneg_right h,
|
||||
apply le_of_lt,
|
||||
apply one_div_pos_of_pos he
|
||||
end
|
||||
|
||||
lemma exists_add_lt_and_pos_of_lt {a b : α} (h : b < a) : ∃ c : α, b + c < a ∧ c > 0 :=
|
||||
begin
|
||||
apply exists.intro ((a - b) / (1 + 1)),
|
||||
split,
|
||||
{assert h2 : a + a > (b + b) + (a - b),
|
||||
calc
|
||||
a + a > b + a : add_lt_add_right h _
|
||||
... = b + a + b - b : by rw add_sub_cancel
|
||||
... = b + b + a - b : by simp
|
||||
... = (b + b) + (a - b) : by rw add_sub,
|
||||
assert h3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
|
||||
exact div_lt_div_of_lt_of_pos h2 two_pos,
|
||||
rw [one_add_one_eq_two, sub_eq_add_neg],
|
||||
rw [add_self_div_two, -div_add_div_same, add_self_div_two, sub_eq_add_neg] at h3,
|
||||
exact h3},
|
||||
exact div_pos_of_pos_of_pos (sub_pos_of_lt h) two_pos
|
||||
end
|
||||
|
||||
lemma ge_of_forall_ge_sub {a b : α} (h : ∀ ε : α, ε > 0 → a ≥ b - ε) : a ≥ b :=
|
||||
begin
|
||||
apply le_of_not_gt,
|
||||
intro hb,
|
||||
cases exists_add_lt_and_pos_of_lt hb with c hc,
|
||||
note hc' := h c (and.right hc),
|
||||
apply (not_le_of_gt (and.left hc)) (le_add_of_sub_right_le hc')
|
||||
end
|
||||
|
||||
end linear_ordered_field
|
||||
|
|
@ -104,6 +104,100 @@ le_of_add_le_add_left
|
|||
lemma lt_of_add_lt_add_right {a b c : α} (h : a + b < c + b) : a < c :=
|
||||
lt_of_add_lt_add_left
|
||||
(show b + a < b + c, begin rw [add_comm b a, add_comm b c], assumption end)
|
||||
|
||||
-- here we start using properties of zero.
|
||||
lemma add_nonneg {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b :=
|
||||
zero_add (0:α) ▸ (add_le_add ha hb)
|
||||
|
||||
lemma add_pos {a b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a + b :=
|
||||
zero_add (0:α) ▸ (add_lt_add ha hb)
|
||||
|
||||
lemma add_pos_of_pos_of_nonneg {a b : α} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b :=
|
||||
zero_add (0:α) ▸ (add_lt_add_of_lt_of_le ha hb)
|
||||
|
||||
lemma add_pos_of_nonneg_of_pos {a b : α} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b :=
|
||||
zero_add (0:α) ▸ (add_lt_add_of_le_of_lt ha hb)
|
||||
|
||||
lemma add_nonpos {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0 :=
|
||||
zero_add (0:α) ▸ (add_le_add ha hb)
|
||||
|
||||
lemma add_neg {a b : α} (ha : a < 0) (hb : b < 0) : a + b < 0 :=
|
||||
zero_add (0:α) ▸ (add_lt_add ha hb)
|
||||
|
||||
lemma add_neg_of_neg_of_nonpos {a b : α} (ha : a < 0) (hb : b ≤ 0) : a + b < 0 :=
|
||||
zero_add (0:α) ▸ (add_lt_add_of_lt_of_le ha hb)
|
||||
|
||||
lemma add_neg_of_nonpos_of_neg {a b : α} (ha : a ≤ 0) (hb : b < 0) : a + b < 0 :=
|
||||
zero_add (0:α) ▸ (add_lt_add_of_le_of_lt ha hb)
|
||||
|
||||
lemma add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg
|
||||
{a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : a + b = 0 ↔ a = 0 ∧ b = 0 :=
|
||||
iff.intro
|
||||
(assume hab : a + b = 0,
|
||||
have ha' : a ≤ 0, from
|
||||
calc
|
||||
a = a + 0 : by rw add_zero
|
||||
... ≤ a + b : add_le_add_left hb _
|
||||
... = 0 : hab,
|
||||
have haz : a = 0, from le_antisymm ha' ha,
|
||||
have hb' : b ≤ 0, from
|
||||
calc
|
||||
b = 0 + b : by rw zero_add
|
||||
... ≤ a + b : by exact add_le_add_right ha _
|
||||
... = 0 : hab,
|
||||
have hbz : b = 0, from le_antisymm hb' hb,
|
||||
and.intro haz hbz)
|
||||
(assume ⟨ha', hb'⟩,
|
||||
by rw [ha', hb', add_zero])
|
||||
|
||||
lemma le_add_of_nonneg_of_le {a b c : α} (ha : 0 ≤ a) (hbc : b ≤ c) : b ≤ a + c :=
|
||||
zero_add b ▸ add_le_add ha hbc
|
||||
|
||||
lemma le_add_of_le_of_nonneg {a b c : α} (hbc : b ≤ c) (ha : 0 ≤ a) : b ≤ c + a :=
|
||||
add_zero b ▸ add_le_add hbc ha
|
||||
|
||||
lemma lt_add_of_pos_of_le {a b c : α} (ha : 0 < a) (hbc : b ≤ c) : b < a + c :=
|
||||
zero_add b ▸ add_lt_add_of_lt_of_le ha hbc
|
||||
|
||||
lemma lt_add_of_le_of_pos {a b c : α} (hbc : b ≤ c) (ha : 0 < a) : b < c + a :=
|
||||
add_zero b ▸ add_lt_add_of_le_of_lt hbc ha
|
||||
|
||||
lemma add_le_of_nonpos_of_le {a b c : α} (ha : a ≤ 0) (hbc : b ≤ c) : a + b ≤ c :=
|
||||
zero_add c ▸ add_le_add ha hbc
|
||||
|
||||
lemma add_le_of_le_of_nonpos {a b c : α} (hbc : b ≤ c) (ha : a ≤ 0) : b + a ≤ c :=
|
||||
add_zero c ▸ add_le_add hbc ha
|
||||
|
||||
lemma add_lt_of_neg_of_le {a b c : α} (ha : a < 0) (hbc : b ≤ c) : a + b < c :=
|
||||
zero_add c ▸ add_lt_add_of_lt_of_le ha hbc
|
||||
|
||||
lemma add_lt_of_le_of_neg {a b c : α} (hbc : b ≤ c) (ha : a < 0) : b + a < c :=
|
||||
add_zero c ▸ add_lt_add_of_le_of_lt hbc ha
|
||||
|
||||
lemma lt_add_of_nonneg_of_lt {a b c : α} (ha : 0 ≤ a) (hbc : b < c) : b < a + c :=
|
||||
zero_add b ▸ add_lt_add_of_le_of_lt ha hbc
|
||||
|
||||
lemma lt_add_of_lt_of_nonneg {a b c : α} (hbc : b < c) (ha : 0 ≤ a) : b < c + a :=
|
||||
add_zero b ▸ add_lt_add_of_lt_of_le hbc ha
|
||||
|
||||
lemma lt_add_of_pos_of_lt {a b c : α} (ha : 0 < a) (hbc : b < c) : b < a + c :=
|
||||
zero_add b ▸ add_lt_add ha hbc
|
||||
|
||||
lemma lt_add_of_lt_of_pos {a b c : α} (hbc : b < c) (ha : 0 < a) : b < c + a :=
|
||||
add_zero b ▸ add_lt_add hbc ha
|
||||
|
||||
lemma add_lt_of_nonpos_of_lt {a b c : α} (ha : a ≤ 0) (hbc : b < c) : a + b < c :=
|
||||
zero_add c ▸ add_lt_add_of_le_of_lt ha hbc
|
||||
|
||||
lemma add_lt_of_lt_of_nonpos {a b c : α} (hbc : b < c) (ha : a ≤ 0) : b + a < c :=
|
||||
add_zero c ▸ add_lt_add_of_lt_of_le hbc ha
|
||||
|
||||
lemma add_lt_of_neg_of_lt {a b c : α} (ha : a < 0) (hbc : b < c) : a + b < c :=
|
||||
zero_add c ▸ add_lt_add ha hbc
|
||||
|
||||
lemma add_lt_of_lt_of_neg {a b c : α} (hbc : b < c) (ha : a < 0) : b + a < c :=
|
||||
add_zero c ▸ add_lt_add hbc ha
|
||||
|
||||
end ordered_cancel_comm_monoid
|
||||
|
||||
class ordered_mul_comm_group (α : Type u) extends comm_group α, order_pair α :=
|
||||
|
|
@ -142,7 +236,7 @@ instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u) [s : or
|
|||
section ordered_comm_group
|
||||
variables {α : Type u} [ordered_comm_group α]
|
||||
|
||||
theorem neg_le_neg {a b : α} (h : a ≤ b) : -b ≤ -a :=
|
||||
lemma neg_le_neg {a b : α} (h : a ≤ b) : -b ≤ -a :=
|
||||
have 0 ≤ -a + b, from add_left_neg a ▸ add_le_add_left h (-a),
|
||||
have 0 + -b ≤ -a + b + -b, from add_le_add_right this (-b),
|
||||
by rwa [add_neg_cancel_right, zero_add] at this
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue