src/HOL/Analysis/Connected.thy
changeset 66835 ecc99a5a1ab8
parent 66827 c94531b5007d
child 66884 c2128ab11f61
     1.1 --- a/src/HOL/Analysis/Connected.thy	Tue Oct 10 20:33:29 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Connected.thy	Tue Oct 10 22:18:58 2017 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4 -(*  Author:     L C Paulson, University of Cambridge*)
     1.5 +(*  Author:     L C Paulson, University of Cambridge
     1.6 +    Material split off from Topology_Euclidean_Space
     1.7 +*)
     1.8  
     1.9  section \<open>Connected Components, Homeomorphisms, Baire property, etc.\<close>
    1.10  
    1.11 -text\<open>Material split off from Topology_Euclidean_Space\<close>
    1.12 -
    1.13  theory Connected
    1.14  imports Topology_Euclidean_Space
    1.15  begin
    1.16 @@ -1266,18 +1266,9 @@
    1.17        then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"
    1.18          using l[unfolded lim_sequentially] by auto
    1.19        have "t (max n N) \<in> s n"
    1.20 -        using assms(3)
    1.21 -        unfolding subset_eq
    1.22 -        apply (erule_tac x=n in allE)
    1.23 -        apply (erule_tac x="max n N" in allE)
    1.24 -        using t
    1.25 -        apply auto
    1.26 -        done
    1.27 +        by (meson assms(3) contra_subsetD max.cobounded1 t)
    1.28        then have "\<exists>y\<in>s n. dist y l < e"
    1.29 -        apply (rule_tac x="t (max n N)" in bexI)
    1.30 -        using N
    1.31 -        apply auto
    1.32 -        done
    1.33 +        using N max.cobounded2 by blast
    1.34      }
    1.35      then have "l \<in> s n"
    1.36        using closed_approachable[of "s n" l] assms(1) by auto
    1.37 @@ -1495,11 +1486,7 @@
    1.38    have *: "f ` s \<subseteq> cball 0 b"
    1.39      using assms(2)[unfolded mem_cball_0[symmetric]] by auto
    1.40    show ?thesis
    1.41 -    using image_closure_subset[OF assms(1) closed_cball[of 0 b] *] assms(3)
    1.42 -    unfolding subset_eq
    1.43 -    apply (erule_tac x="f x" in ballE)
    1.44 -    apply (auto simp: dist_norm)
    1.45 -    done
    1.46 +    by (meson "*" assms(1) assms(3) closed_cball image_closure_subset image_subset_iff mem_cball_0)
    1.47  qed
    1.48  
    1.49  lemma isCont_indicator: