src/HOL/Topological_Spaces.thy
changeset 62343 24106dc44def
parent 62217 527488dc8b90
child 62367 d2bc8a7e5fec
     1.1 --- a/src/HOL/Topological_Spaces.thy	Wed Feb 17 21:51:55 2016 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -1133,10 +1133,11 @@
     1.4        using A by auto
     1.5      show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
     1.6        using A unfolding nhds_def
     1.7 -      apply (intro INF_eq)
     1.8 +      apply -
     1.9 +      apply (rule INF_eq)
    1.10        apply simp_all
    1.11 -      apply force
    1.12 -      apply (intro exI[of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
    1.13 +      apply fastforce
    1.14 +      apply (intro exI [of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
    1.15        apply auto
    1.16        done
    1.17    qed
    1.18 @@ -1464,7 +1465,7 @@
    1.19  
    1.20  lemma continuous_on_open_UN:
    1.21    "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
    1.22 -  unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
    1.23 +  by (rule continuous_on_open_Union) auto
    1.24  
    1.25  lemma continuous_on_open_Un:
    1.26    "open s \<Longrightarrow> open t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
    1.27 @@ -1689,7 +1690,7 @@
    1.28  lemma compactE_image:
    1.29    assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
    1.30    obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
    1.31 -  using assms unfolding ball_simps[symmetric] SUP_def
    1.32 +  using assms unfolding ball_simps [symmetric]
    1.33    by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
    1.34  
    1.35  lemma compact_inter_closed [intro]: