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

refactor(library/data/int/order): use 'exists' instead of 'ex', 'least' instead of 'smallest', etc.

Browse source
This commit is contained in:
Jeremy Avigad 2015-09-12 20:51:34 -04:00
parent 1affeec3c6
commit 780c950414
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/int/order.lean
View file

@ -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],

2
library/data/real/complete.lean
View file

@ -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),