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

chore(library/data/{rat, pnat}): move theorems from reals to more appropriate places

Browse source
This commit is contained in:
Rob Lewis 2015-09-14 13:39:01 -04:00 committed by Leonardo de Moura
parent b7271c39af
commit f4fa38e365
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/pnat.lean
View file

@ -325,5 +325,7 @@ theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)
assert T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial,
by rewrite[*inv_mul_eq_mul_inv,-*rat.right_distrib,T,rat.one_mul]
theorem rat_power_two_le (k : ℕ+) : rat_of_pnat k ≤ rat.pow 2 k~ :=
!binary_nat_bound
end pnat

15
library/data/rat/order.lean
View file

@ -449,4 +449,19 @@ calc
theorem ubound_pos (a : ℚ) : nat.gt (ubound a) nat.zero := !nat.succ_pos
theorem binary_nat_bound (a : ℕ) : of_nat a ≤ pow 2 a :=
nat.induction_on a (zero_le_one)
(take n, assume Hn,
calc
of_nat (nat.succ n) = (of_nat n) + 1 : of_nat_add
... ≤ pow 2 n + 1 : add_le_add_right Hn
... ≤ pow 2 n + rat.pow 2 n :
add_le_add_left (pow_ge_one_of_ge_one two_ge_one _)
... = pow 2 (nat.succ n) : pow_two_add)
theorem binary_bound (a : ℚ) : ∃ n : ℕ, a ≤ pow 2 n :=
exists.intro (ubound a) (calc
a ≤ of_nat (ubound a) : ubound_ge
... ≤ pow 2 (ubound a) : binary_nat_bound)
end rat