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
```