From 80f210d8ce9b3511ef50ecc97239cc8d3be97b47 Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Wed, 9 Oct 2019 07:24:44 +0200 Subject: [PATCH] feat(algebra/ordered...): Two tiny lemmas (#1522) * feat(algebra/ordered...): Two tiny lemmas * style(src/algebra/ordered_field) Co-Authored-By: Reid Barton --- src/algebra/floor.lean | 7 +++++-- src/algebra/ordered_field.lean | 5 ++++- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/algebra/floor.lean b/src/algebra/floor.lean index 6014d7953df23..eade208b4e78c 100644 --- a/src/algebra/floor.lean +++ b/src/algebra/floor.lean @@ -254,8 +254,11 @@ begin refl end -theorem nat_ceil_lt_add_one {a : α} (a_nonneg : 0 ≤ a) [decidable (↑(nat_ceil a) < a + 1)] : - ↑(nat_ceil a) < a + 1 := +theorem nat_ceil_lt_add_one {a : α} (a_nonneg : 0 ≤ a) [decidable ((nat_ceil a : α) < a + 1)] : + (nat_ceil a : α) < a + 1 := lt_nat_ceil.1 $ by rw ( show nat_ceil (a + 1) = nat_ceil a + 1, by exact_mod_cast (nat_ceil_add_nat a_nonneg 1)); apply nat.lt_succ_self + +lemma lt_of_nat_ceil_lt {x : α} {n : ℕ} (h : nat_ceil x < n) : x < n := +lt_of_le_of_lt (le_nat_ceil x) (by exact_mod_cast h) diff --git a/src/algebra/ordered_field.lean b/src/algebra/ordered_field.lean index 39f3c63149213..1af895815bdb1 100644 --- a/src/algebra/ordered_field.lean +++ b/src/algebra/ordered_field.lean @@ -50,7 +50,7 @@ lemma div_le_iff_of_neg (hc : c < 0) : b / c ≤ a ↔ a * c ≤ b := ⟨mul_le_of_div_le_of_neg hc, div_le_of_mul_le_of_neg hc⟩ lemma le_div_iff_of_neg (hc : c < 0) : a ≤ b / c ↔ b ≤ a * c := -by rw [← neg_neg c, mul_neg_eq_neg_mul_symm, div_neg _ (ne_of_gt (neg_pos.2 hc)), le_neg, +by rw [← neg_neg c, mul_neg_eq_neg_mul_symm, div_neg _ (ne_of_gt (neg_pos.2 hc)), le_neg, div_le_iff (neg_pos.2 hc), neg_mul_eq_neg_mul_symm] lemma div_lt_iff (hc : 0 < c) : b / c < a ↔ b < a * c := @@ -81,6 +81,9 @@ lt_iff_lt_of_le_iff_le (inv_le_inv hb ha) lemma inv_lt (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a := lt_iff_lt_of_le_iff_le (le_inv hb ha) +lemma one_div_lt (ha : 0 < a) (hb : 0 < b) : 1 / a < b ↔ 1 / b < a := +(one_div_eq_inv a).symm ▸ (one_div_eq_inv b).symm ▸ inv_lt ha hb + lemma lt_inv (ha : 0 < a) (hb : 0 < b) : a < b⁻¹ ↔ b < a⁻¹ := lt_iff_lt_of_le_iff_le (inv_le hb ha)