src/HOL/Real_Vector_Spaces.thy
changeset 53381 355a4cac5440
parent 53374 a14d2a854c02
child 53600 8fda7ad57466
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 19:58:00 2013 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 22:04:23 2013 +0200
     1.3 @@ -833,7 +833,8 @@
     1.4    show "(open :: real set \<Rightarrow> bool) = generate_topology (range lessThan \<union> range greaterThan)"
     1.5    proof (rule ext, safe)
     1.6      fix S :: "real set" assume "open S"
     1.7 -    then guess f unfolding open_real_def bchoice_iff ..
     1.8 +    then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
     1.9 +      unfolding open_real_def bchoice_iff ..
    1.10      then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
    1.11        by (fastforce simp: dist_real_def)
    1.12      show "generate_topology (range lessThan \<union> range greaterThan) S"
    1.13 @@ -1525,7 +1526,8 @@
    1.14    with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
    1.15      by (auto simp: LIMSEQ_def dist_real_def)
    1.16    { fix x :: real
    1.17 -    from ex_le_of_nat[of x] guess n ..
    1.18 +    obtain n where "x \<le> real_of_nat n"
    1.19 +      using ex_le_of_nat[of x] ..
    1.20      note monoD[OF mono this]
    1.21      also have "f (real_of_nat n) \<le> y"
    1.22        by (rule LIMSEQ_le_const[OF limseq])