src/HOL/Real_Vector_Spaces.thy
changeset 53374 a14d2a854c02
parent 52381 63eec9cea2c7
child 53381 355a4cac5440
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -758,10 +758,10 @@
     1.4    show "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
     1.5    proof (safe intro!: exI[of _ "\<lambda>n. {y. dist x y < inverse (Suc n)}"])
     1.6      fix S assume "open S" "x \<in> S"
     1.7 -    then obtain e where "0 < e" "{y. dist x y < e} \<subseteq> S"
     1.8 +    then obtain e where e: "0 < e" and "{y. dist x y < e} \<subseteq> S"
     1.9        by (auto simp: open_dist subset_eq dist_commute)
    1.10      moreover
    1.11 -    then obtain i where "inverse (Suc i) < e"
    1.12 +    from e obtain i where "inverse (Suc i) < e"
    1.13        by (auto dest!: reals_Archimedean)
    1.14      then have "{y. dist x y < inverse (Suc i)} \<subseteq> {y. dist x y < e}"
    1.15        by auto