| author | haftmann |
| Tue Feb 09 16:07:09 2010 +0100 (2010-02-09) | |
| changeset 35066 | 894e82be8d05 |
| parent 35028 | 108662d50512 |
| child 35090 | 88cc65ae046e |
| permissions | -rw-r--r-- |
1 theory Real
2 imports RComplete RealVector
3 begin
5 lemma field_le_epsilon:
6 fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}"
7 assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
8 shows "x \<le> y"
9 proof (rule ccontr)
10 assume xy: "\<not> x \<le> y"
11 hence "(x-y)/2 > 0"
12 by simp
13 hence "x \<le> y + (x - y) / 2"
14 by (rule e [of "(x-y)/2"])
15 also have "... = (x - y + 2*y)/2"
16 by (simp add: diff_divide_distrib)
17 also have "... = (x + y) / 2"
18 by simp
19 also have "... < x" using xy
20 by simp
21 finally have "x<x" .
22 thus False
23 by simp
24 qed
26 end