From 780c950414c89ce75fadc36a493f92bc8e3f64a6 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 12 Sep 2015 20:51:34 -0400 Subject: [PATCH] refactor(library/data/int/order): use 'exists' instead of 'ex', 'least' instead of 'smallest', etc. --- library/data/int/order.lean | 6 ++++-- library/data/real/complete.lean | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/library/data/int/order.lean b/library/data/int/order.lean index 2b4f35201..68c535820 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -389,7 +389,8 @@ dvd.elim H' suppose 1 = a * b, eq_one_of_mul_eq_one_right H this⁻¹) -theorem ex_smallest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≤ b → ¬ P z) +theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] + (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≤ b → ¬ P z) (Hinh : ∃ z : ℤ, P z) : ∃ lb : ℤ, P lb ∧ (∀ z : ℤ, z < lb → ¬ P z) := begin cases Hbdd with [b, Hb], @@ -426,7 +427,8 @@ theorem ex_smallest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] (Hbdd : apply least_lt _ !lt_succ_self H' end -theorem ex_largest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≥ b → ¬ P z) +theorem exists_greatest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P] + (Hbdd : ∃ b : ℤ, ∀ z : ℤ, z ≥ b → ¬ P z) (Hinh : ∃ z : ℤ, P z) : ∃ ub : ℤ, P ub ∧ (∀ z : ℤ, z > ub → ¬ P z) := begin cases Hbdd with [b, Hb], diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 58ddc5be8..a62dfac9f 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -423,7 +423,7 @@ theorem archimedean_lower_strict (x : ℝ) : ∃ z : ℤ, x > of_int z := end private definition ex_floor (x : ℝ) := - (@ex_largest_of_bdd (λ z, x ≥ of_int z) _ + (@exists_greatest_of_bdd (λ z, x ≥ of_int z) _ (begin existsi some (archimedean_upper_strict x), let Har := some_spec (archimedean_upper_strict x),