From 1affeec3c6d80cf2f85b3a73ed0ac9747926f9c2 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 12 Sep 2015 20:44:34 -0400 Subject: [PATCH] fix(library/algebra/ordered_filed): rename theorems --- library/algebra/ordered_field.lean | 18 +++++++++--------- library/data/pnat.lean | 14 +++++++------- library/data/real/complete.lean | 4 ++-- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index 6eca78bf5d..42266592e1 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -434,37 +434,37 @@ section discrete_linear_ordered_field absurd Hl' (ne_of_lt Hl)), lt_of_le_of_ne H1 Hn - theorem div_lt_div_of_lt (Ha : 0 < a) (H : a < b) : 1 / b < 1 / a := + theorem one_div_lt_one_div_of_lt (Ha : 0 < a) (H : a < b) : 1 / b < 1 / a := lt_of_not_ge (assume H', absurd H (not_lt_of_ge (le_of_one_div_le_one_div Ha H'))) - theorem div_le_div_of_le (Ha : 0 < a) (H : a ≤ b) : 1 / b ≤ 1 / a := + theorem one_div_le_one_div_of_le (Ha : 0 < a) (H : a ≤ b) : 1 / b ≤ 1 / a := le_of_not_gt (assume H', absurd H (not_le_of_gt (lt_of_one_div_lt_one_div Ha H'))) - theorem div_lt_div_of_lt_neg (Hb : b < 0) (H : a < b) : 1 / b < 1 / a := + theorem one_div_lt_one_div_of_lt_of_neg (Hb : b < 0) (H : a < b) : 1 / b < 1 / a := lt_of_not_ge (assume H', absurd H (not_lt_of_ge (le_of_one_div_le_one_div_of_neg Hb H'))) - theorem div_le_div_of_le_neg (Hb : b < 0) (H : a ≤ b) : 1 / b ≤ 1 / a := + theorem one_div_le_one_div_of_le_of_neg (Hb : b < 0) (H : a ≤ b) : 1 / b ≤ 1 / a := le_of_not_gt (assume H', absurd H (not_le_of_gt (lt_of_one_div_lt_one_div_of_neg Hb H'))) theorem one_lt_one_div (H1 : 0 < a) (H2 : a < 1) : 1 < 1 / a := - one_div_one ▸ div_lt_div_of_lt H1 H2 + one_div_one ▸ one_div_lt_one_div_of_lt H1 H2 theorem one_le_one_div (H1 : 0 < a) (H2 : a ≤ 1) : 1 ≤ 1 / a := - one_div_one ▸ div_le_div_of_le H1 H2 + one_div_one ▸ one_div_le_one_div_of_le H1 H2 theorem one_div_lt_neg_one (H1 : a < 0) (H2 : -1 < a) : 1 / a < -1 := - one_div_neg_one_eq_neg_one ▸ div_lt_div_of_lt_neg H1 H2 + one_div_neg_one_eq_neg_one ▸ one_div_lt_one_div_of_lt_of_neg H1 H2 theorem one_div_le_neg_one (H1 : a < 0) (H2 : -1 ≤ a) : 1 / a ≤ -1 := - one_div_neg_one_eq_neg_one ▸ div_le_div_of_le_neg H1 H2 + one_div_neg_one_eq_neg_one ▸ one_div_le_one_div_of_le_of_neg H1 H2 theorem div_lt_div_of_pos_of_lt_of_pos (Hb : 0 < b) (H : b < a) (Hc : 0 < c) : c / a < c / b := begin @@ -473,7 +473,7 @@ section discrete_linear_ordered_field apply mul_neg_of_pos_of_neg, exact Hc, apply iff.mpr !sub_neg_iff_lt, - apply div_lt_div_of_lt, + apply one_div_lt_one_div_of_lt, repeat assumption end diff --git a/library/data/pnat.lean b/library/data/pnat.lean index c1a277f8bf..7cff0416dd 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -116,7 +116,7 @@ theorem inv_pos (n : ℕ+) : n⁻¹ > 0 := one_div_pos_of_pos !rat_of_pnat_is_po theorem inv_le_one (n : ℕ+) : n⁻¹ ≤ (1 : ℚ) := begin rewrite [↑inv, -one_div_one], - apply div_le_div_of_le, + apply one_div_le_one_div_of_le, apply rat.zero_lt_one, apply rat_of_pnat_ge_one end @@ -124,7 +124,7 @@ theorem inv_le_one (n : ℕ+) : n⁻¹ ≤ (1 : ℚ) := theorem inv_lt_one_of_gt {n : ℕ+} (H : n~ > 1) : n⁻¹ < (1 : ℚ) := begin rewrite [↑inv, -one_div_one], - apply div_lt_div_of_lt, + apply one_div_lt_one_div_of_lt, apply rat.zero_lt_one, rewrite pnat.to_rat_of_nat, apply (of_nat_lt_of_nat_of_lt H) @@ -158,7 +158,7 @@ theorem one_lt_two : pone < 2 := !nat.le.refl theorem inv_two_mul_lt_inv (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ := begin rewrite ↑inv, - apply div_lt_div_of_lt, + apply one_div_lt_one_div_of_lt, apply rat_of_pnat_is_pos, have H : n~ < (2 * n)~, begin rewrite -one_mul at {1}, @@ -172,10 +172,10 @@ theorem inv_two_mul_lt_inv (n : ℕ+) : (2 * n)⁻¹ < n⁻¹ := theorem inv_two_mul_le_inv (n : ℕ+) : (2 * n)⁻¹ ≤ n⁻¹ := rat.le_of_lt !inv_two_mul_lt_inv theorem inv_ge_of_le {p q : ℕ+} (H : p ≤ q) : q⁻¹ ≤ p⁻¹ := - div_le_div_of_le !rat_of_pnat_is_pos (rat_of_pnat_le_of_pnat_le H) + one_div_le_one_div_of_le !rat_of_pnat_is_pos (rat_of_pnat_le_of_pnat_le H) theorem inv_gt_of_lt {p q : ℕ+} (H : p < q) : q⁻¹ < p⁻¹ := - div_lt_div_of_lt !rat_of_pnat_is_pos (rat_of_pnat_lt_of_pnat_lt H) + one_div_lt_one_div_of_lt !rat_of_pnat_is_pos (rat_of_pnat_lt_of_pnat_lt H) theorem ge_of_inv_le {p q : ℕ+} (H : p⁻¹ ≤ q⁻¹) : q ≤ p := pnat_le_of_rat_of_pnat_le (le_of_one_div_le_one_div !rat_of_pnat_is_pos H) @@ -274,10 +274,10 @@ theorem pnat_cancel' (n m : ℕ+) : (n * n * m)⁻¹ * (rat_of_pnat n * rat_of_p definition pceil (a : ℚ) : ℕ+ := tag (ubound a) !ubound_pos theorem pceil_helper {a : ℚ} {n : ℕ+} (H : pceil a ≤ n) (Ha : a > 0) : n⁻¹ ≤ 1 / a := - rat.le.trans (inv_ge_of_le H) (div_le_div_of_le Ha (ubound_ge a)) + rat.le.trans (inv_ge_of_le H) (one_div_le_one_div_of_le Ha (ubound_ge a)) theorem inv_pceil_div (a b : ℚ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻¹ ≤ b / a := - !one_div_one_div ▸ div_le_div_of_le + !one_div_one_div ▸ one_div_le_one_div_of_le (one_div_pos_of_pos (div_pos_of_pos_of_pos Hb Ha)) (!div_div_eq_mul_div⁻¹ ▸ !rat.one_mul⁻¹ ▸ !ubound_ge) diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index cbf66a9ad9..58ddc5be8a 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -509,7 +509,7 @@ have H₁ : succ n ≥ ceil (2 / ε), from of_int_le_of_int_of_le this, have H₂ : succ n ≥ 2 / ε, from !le.trans !le_ceil H₁, have H₃ : 2 / ε > 0, from div_pos_of_pos_of_pos two_pos H, have 1 / succ n < ε, from calc - 1 / succ n ≤ 1 / (2 / ε) : div_le_div_of_le H₃ H₂ + 1 / succ n ≤ 1 / (2 / ε) : one_div_le_one_div_of_le H₃ H₂ ... = ε / 2 : one_div_div ... < ε : div_two_lt_of_pos H, exists.intro n this @@ -832,7 +832,7 @@ theorem over_seq_mono (i j : ℕ) (H : i ≤ j) : over_seq j ≤ over_seq i := end theorem rat_power_two_inv_ge (k : ℕ+) : 1 / rat.pow 2 k~ ≤ k⁻¹ := - rat.div_le_div_of_le !rat_of_pnat_is_pos !rat_power_two_le + rat.one_div_le_one_div_of_le !rat_of_pnat_is_pos !rat_power_two_le open rat_seq theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n)