src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 59587 8ea7b22525cb
parent 58877 262572d90bc6
child 59765 26d1c71784f1
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Mar 04 23:31:04 2015 +0100
     1.3 @@ -1156,15 +1156,15 @@
     1.4    {
     1.5      fix x b :: 'a
     1.6      assume [simp]: "b \<in> Basis"
     1.7 -    have "\<bar>x \<bullet> b\<bar> \<le> real (natceiling \<bar>x \<bullet> b\<bar>)"
     1.8 -      by (rule real_natceiling_ge)
     1.9 -    also have "\<dots> \<le> real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
    1.10 -      by (auto intro!: natceiling_mono)
    1.11 -    also have "\<dots> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
    1.12 +    have "\<bar>x \<bullet> b\<bar> \<le> real (ceiling \<bar>x \<bullet> b\<bar>)"
    1.13 +      by (rule real_of_int_ceiling_ge)
    1.14 +    also have "\<dots> \<le> real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)))"
    1.15 +      by (auto intro!: ceiling_mono)
    1.16 +    also have "\<dots> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)"
    1.17        by simp
    1.18 -    finally have "\<bar>x \<bullet> b\<bar> < real (natceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
    1.19 +    finally have "\<bar>x \<bullet> b\<bar> < real (ceiling (Max ((\<lambda>b. \<bar>x \<bullet> b\<bar>)`Basis)) + 1)" . }
    1.20    then have "\<And>x::'a. \<exists>n::nat. \<forall>b\<in>Basis. \<bar>x \<bullet> b\<bar> < real n"
    1.21 -    by auto
    1.22 +    by (metis order.strict_trans reals_Archimedean2)
    1.23    moreover have "\<And>x b::'a. \<And>n::nat.  \<bar>x \<bullet> b\<bar> < real n \<longleftrightarrow> - real n < x \<bullet> b \<and> x \<bullet> b < real n"
    1.24      by auto
    1.25    ultimately show ?thesis