michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/algebra): add min/max to ordered algebraic structures

Browse source
This commit is contained in:
Rob Lewis 2015-05-26 11:45:09 +10:00
parent 4152ebfa23
commit eb537daa1c
2 changed files with 50 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
library/algebra/order.lean
View file

@ -340,6 +340,47 @@ section
theorem lt.cases_of_gt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a > b) : theorem lt.cases_of_gt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a > b) :
lt.cases a b t_lt t_eq t_gt = t_gt := lt.cases a b t_lt t_eq t_gt = t_gt :=
if_neg (ne.symm (ne_of_lt H)) ⬝ if_neg (lt.asymm H) if_neg (ne.symm (ne_of_lt H)) ⬝ if_neg (lt.asymm H)
definition max (a b : A) : A :=
if a < b then b else a
definition min (a b : A) : A :=
if a < b then a else b
theorem max_a_a (a : A) : a = max a a :=
eq.rec_on !if_t_t rfl
theorem max.eq_right {a b : A} (H : a < b) : max a b = b :=
if_pos H
theorem max.eq_left {a b : A} (H : ¬ a < b) : max a b = a :=
if_neg H
theorem max.right_eq {a b : A} (H : a < b) : b = max a b :=
eq.rec_on (max.eq_right H) rfl
theorem max.left_eq {a b : A} (H : ¬ a < b) : a = max a b :=
eq.rec_on (max.eq_left H) rfl
theorem max.left (a b : A) : a ≤ max a b :=
decidable.by_cases
(λ h : a < b, le_of_lt (eq.rec_on (max.right_eq h) h))
(λ h : ¬ a < b, eq.rec_on (max.eq_left h) !le.refl)
theorem eq_or_lt_of_not_lt (H : ¬ a < b) : a = b ∨ b < a :=
have H' : b = a ∨ b < a, from or.swap (lt_or_eq_of_le (le_of_not_gt H)),
or.elim H'
(take H'' : b = a, or.inl (symm H''))
(take H'' : b < a, or.inr H'')
theorem max.right (a b : A) : b ≤ max a b :=
decidable.by_cases
(λ h : a < b, eq.rec_on (max.eq_right h) !le.refl)
(λ h : ¬ a < b, or.rec_on (eq_or_lt_of_not_lt h)
(λ heq, eq.rec_on heq (eq.rec_on (max_a_a a) !le.refl))
(λ h : b < a,
have aux : a = max a b, from max.left_eq (lt.asymm h),
eq.rec_on aux (le_of_lt h)))
end end
end algebra end algebra

9
library/algebra/ordered_field.lean
View file

@ -253,6 +253,15 @@ section linear_ordered_field
theorem div_lt_div_of_lt_of_neg (H : b < a) (Hc : c < 0) : a / c < b / c := theorem div_lt_div_of_lt_of_neg (H : b < a) (Hc : c < 0) : a / c < b / c :=
div_eq_mul_one_div⁻¹ ▸ div_eq_mul_one_div⁻¹ ▸ mul_lt_mul_of_neg_right H (div_neg_of_neg Hc) div_eq_mul_one_div⁻¹ ▸ div_eq_mul_one_div⁻¹ ▸ mul_lt_mul_of_neg_right H (div_neg_of_neg Hc)
theorem two_ne_zero : (1 : A) + 1 ≠ 0 :=
ne.symm (ne_of_lt (add_pos zero_lt_one zero_lt_one))
theorem add_halves : a / (1 + 1) + a / (1 + 1) = a :=
calc
a / (1 + 1) + a / (1 + 1) = (a + a) / (1 + 1) : div_add_div_same
... = (a * 1 + a * 1) / (1 + 1) : by rewrite mul_one
... = (a * (1 + 1)) / (1 + 1) : left_distrib
... = a : mul_div_cancel two_ne_zero
end linear_ordered_field end linear_ordered_field