New abstract topological material
authorpaulson <lp15@cam.ac.uk>
Fri Mar 22 12:34:49 2019 +0000 (4 weeks ago)
changeset 6994535ba13ac6e5c
parent 69944 ab8aad4aa76e
child 69946 494934c30f38
New abstract topological material
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Locally.thy
src/HOL/Analysis/Product_Topology.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Thu Mar 21 19:46:26 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Fri Mar 22 12:34:49 2019 +0000
     1.3 @@ -2761,6 +2761,11 @@
     1.4  definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
     1.5    "connectedin X S \<equiv> S \<subseteq> topspace X \<and> connected_space (subtopology X S)"
     1.6  
     1.7 +lemma connected_spaceD:
     1.8 +  "\<lbrakk>connected_space X;
     1.9 +    openin X U; openin X V; topspace X \<subseteq> U \<union> V; U \<inter> V = {}; U \<noteq> {}; V \<noteq> {}\<rbrakk> \<Longrightarrow> False"
    1.10 +  by (auto simp: connected_space_def)
    1.11 +
    1.12  lemma connectedin_subset_topspace: "connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
    1.13    by (simp add: connectedin_def)
    1.14  
     2.1 --- a/src/HOL/Analysis/Analysis.thy	Thu Mar 21 19:46:26 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Analysis.thy	Fri Mar 22 12:34:49 2019 +0000
     2.3 @@ -6,6 +6,7 @@
     2.4    (* Topology *)
     2.5    Connected
     2.6    Abstract_Limits
     2.7 +  Locally
     2.8    (* Functional Analysis *)
     2.9    Elementary_Normed_Spaces
    2.10    Norm_Arith
     3.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Mar 21 19:46:26 2019 +0100
     3.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Mar 22 12:34:49 2019 +0000
     3.3 @@ -84,7 +84,7 @@
     3.4      done
     3.5  qed
     3.6  
     3.7 -lemma retraction_imp_quotient_map:
     3.8 +lemma retraction_openin_vimage_iff:
     3.9    "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
    3.10    if retraction: "retraction S T r" and "U \<subseteq> T"
    3.11    using retraction apply (rule retractionE)
    3.12 @@ -110,13 +110,13 @@
    3.13    assumes "locally connected T" "S retract_of T"
    3.14    shows "locally connected S"
    3.15    using assms
    3.16 -  by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image retract_ofE)
    3.17 +  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE)
    3.18  
    3.19  lemma retract_of_locally_path_connected:
    3.20    assumes "locally path_connected T" "S retract_of T"
    3.21    shows "locally path_connected S"
    3.22    using assms
    3.23 -  by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image retract_ofE)
    3.24 +  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE)
    3.25  
    3.26  text \<open>A few simple lemmas about deformation retracts\<close>
    3.27  
     4.1 --- a/src/HOL/Analysis/Function_Topology.thy	Thu Mar 21 19:46:26 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Fri Mar 22 12:34:49 2019 +0000
     4.3 @@ -3,7 +3,7 @@
     4.4  *)
     4.5  
     4.6  theory Function_Topology
     4.7 -imports Topology_Euclidean_Space
     4.8 +imports Topology_Euclidean_Space Abstract_Limits
     4.9  begin
    4.10  
    4.11  
    4.12 @@ -1480,6 +1480,8 @@
    4.13     "k \<in> I \<Longrightarrow> continuous_map (product_topology X I) (X k) (\<lambda>x. x k)"
    4.14    using continuous_map_componentwise [of "product_topology X I" X I id] by simp
    4.15  
    4.16 +declare continuous_map_from_subtopology [OF continuous_map_product_projection, continuous_intros]
    4.17 +
    4.18  proposition open_map_product_projection:
    4.19    assumes "i \<in> I"
    4.20    shows "open_map (product_topology Y I) (Y i) (\<lambda>f. f i)"
    4.21 @@ -1752,4 +1754,245 @@
    4.22     apply (auto simp: image_iff inj_on_def)
    4.23    done
    4.24  
    4.25 +subsection\<open>Relationship with connected spaces, paths, etc.\<close>
    4.26 +
    4.27 +proposition connected_space_product_topology:
    4.28 +   "connected_space(product_topology X I) \<longleftrightarrow>
    4.29 +    (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = {} \<or> (\<forall>i \<in> I. connected_space(X i))"
    4.30 +  (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
    4.31 +proof (cases ?eq)
    4.32 +  case False
    4.33 +  moreover have "?lhs = ?rhs"
    4.34 +  proof
    4.35 +    assume ?lhs
    4.36 +    moreover
    4.37 +    have "connectedin(X i) (topspace(X i))"
    4.38 +      if "i \<in> I" and ci: "connectedin(product_topology X I) (topspace(product_topology X I))" for i
    4.39 +    proof -
    4.40 +      have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
    4.41 +        by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
    4.42 +      show ?thesis
    4.43 +        using connectedin_continuous_map_image [OF cm ci] \<open>i \<in> I\<close>
    4.44 +        by (simp add: False image_projection_PiE)
    4.45 +    qed
    4.46 +    ultimately show ?rhs
    4.47 +      by (meson connectedin_topspace)
    4.48 +  next
    4.49 +    assume cs [rule_format]: ?rhs
    4.50 +    have False
    4.51 +      if disj: "U \<inter> V = {}" and subUV: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U \<union> V"
    4.52 +        and U: "openin (product_topology X I) U"
    4.53 +        and V: "openin (product_topology X I) V"
    4.54 +        and "U \<noteq> {}" "V \<noteq> {}"
    4.55 +      for U V
    4.56 +    proof -
    4.57 +      obtain f where "f \<in> U"
    4.58 +        using \<open>U \<noteq> {}\<close> by blast
    4.59 +      then have f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
    4.60 +        using U openin_subset by fastforce
    4.61 +      have "U \<subseteq> topspace(product_topology X I)" "V \<subseteq> topspace(product_topology X I)"
    4.62 +        using U V openin_subset by blast+
    4.63 +      moreover have "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U"
    4.64 +      proof -
    4.65 +        obtain C where "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
    4.66 +            (\<Pi>\<^sub>E i\<in>I. topspace (X i))) C" "C \<subseteq> U" "f \<in> C"
    4.67 +          using U \<open>f \<in> U\<close> unfolding openin_product_topology union_of_def by auto
    4.68 +        then obtain \<T> where "finite \<T>"
    4.69 +          and t: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i u. (i \<in> I \<and> openin (X i) u) \<and> C = {x. x i \<in> u}"
    4.70 +          and subU: "topspace (product_topology X I) \<inter> \<Inter>\<T> \<subseteq> U"
    4.71 +          and ftop: "f \<in> topspace (product_topology X I)"
    4.72 +          and fint: "f \<in> \<Inter> \<T>"
    4.73 +          by (fastforce simp: relative_to_def intersection_of_def subset_iff)
    4.74 +        let ?L = "\<Union>C\<in>\<T>. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
    4.75 +        obtain L where "finite L"
    4.76 +          and L: "\<And>i U. \<lbrakk>i \<in> I; openin (X i) U; U \<subset> topspace(X i); {x. x i \<in> U} \<in> \<T>\<rbrakk> \<Longrightarrow> i \<in> L"
    4.77 +        proof
    4.78 +          show "finite ?L"
    4.79 +          proof (rule finite_Union)
    4.80 +            fix M
    4.81 +            assume "M \<in> (\<lambda>C. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}) ` \<T>"
    4.82 +            then obtain C where "C \<in> \<T>" and C: "M = {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
    4.83 +              by blast
    4.84 +            then obtain j V where "j \<in> I" and ope: "openin (X j) V" and Ceq: "C = {x. x j \<in> V}"
    4.85 +              using t by meson
    4.86 +            then have "f j \<in> V"
    4.87 +              using \<open>C \<in> \<T>\<close> fint by force
    4.88 +            then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
    4.89 +              using that
    4.90 +              apply (clarsimp simp add: set_eq_iff)
    4.91 +              apply (rule_tac x="\<lambda>m. if m = k then x else f m" in image_eqI, auto)
    4.92 +              done
    4.93 +            then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
    4.94 +              using Ceq by auto
    4.95 +            then show "finite M"
    4.96 +              using C finite_subset by fastforce
    4.97 +          qed (use \<open>finite \<T>\<close> in blast)
    4.98 +        next
    4.99 +          fix i U
   4.100 +          assume  "i \<in> I" and ope: "openin (X i) U" and psub: "U \<subset> topspace (X i)" and int: "{x. x i \<in> U} \<in> \<T>"
   4.101 +          then show "i \<in> ?L"
   4.102 +            by (rule_tac a="{x. x i \<in> U}" in UN_I) (force+)
   4.103 +        qed
   4.104 +        show ?thesis
   4.105 +        proof
   4.106 +          fix h
   4.107 +          assume h: "h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
   4.108 +          define g where "g \<equiv> \<lambda>i. if i \<in> L then f i else h i"
   4.109 +          have gin: "g \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
   4.110 +            unfolding g_def using f h by auto
   4.111 +          moreover have "g \<in> X" if "X \<in> \<T>" for X
   4.112 +            using fint openin_subset t [OF that] L g_def h that by fastforce
   4.113 +          ultimately have "g \<in> U"
   4.114 +            using subU by auto
   4.115 +          have "h \<in> U" if "finite M" "h \<in> PiE I (topspace \<circ> X)" "{i \<in> I. h i \<noteq> g i} \<subseteq> M" for M h
   4.116 +            using that
   4.117 +          proof (induction arbitrary: h)
   4.118 +            case empty
   4.119 +            then show ?case
   4.120 +              using PiE_ext \<open>g \<in> U\<close> gin by force
   4.121 +          next
   4.122 +            case (insert i M)
   4.123 +            define f where "f \<equiv> \<lambda>j. if j = i then g i else h j"
   4.124 +            have fin: "f \<in> PiE I (topspace \<circ> X)"
   4.125 +              unfolding f_def using gin insert.prems(1) by auto
   4.126 +            have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
   4.127 +              unfolding f_def using insert.prems(2) by auto
   4.128 +            have "f \<in> U"
   4.129 +              using insert.IH [OF fin subM] .
   4.130 +            show ?case
   4.131 +            proof (cases "h \<in> V")
   4.132 +              case True
   4.133 +              show ?thesis
   4.134 +              proof (cases "i \<in> I")
   4.135 +                case True
   4.136 +                let ?U = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> U}"
   4.137 +                let ?V = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> V}"
   4.138 +                have False
   4.139 +                proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
   4.140 +                  have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
   4.141 +                    using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
   4.142 +                  then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x j. if j = i then x else h j)"
   4.143 +                    using \<open>i \<in> I\<close> insert.prems(1)
   4.144 +                    by (auto simp: continuous_map_componentwise extensional_def)
   4.145 +                  show "openin (X i) ?U"
   4.146 +                    by (rule openin_continuous_map_preimage [OF cm U])
   4.147 +                  show "openin (X i) ?V"
   4.148 +                    by (rule openin_continuous_map_preimage [OF cm V])
   4.149 +                  show "topspace (X i) \<subseteq> ?U \<union> ?V"
   4.150 +                  proof clarsimp
   4.151 +                    fix x
   4.152 +                    assume "x \<in> topspace (X i)" and "(\<lambda>j. if j = i then x else h j) \<notin> V"
   4.153 +                    with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
   4.154 +                    show "(\<lambda>j. if j = i then x else h j) \<in> U"
   4.155 +                      by (drule_tac c="(\<lambda>j. if j = i then x else h j)" in subsetD) auto
   4.156 +                  qed
   4.157 +                  show "?U \<inter> ?V = {}"
   4.158 +                    using disj by blast
   4.159 +                  show "?U \<noteq> {}"
   4.160 +                    using \<open>U \<noteq> {}\<close> f_def
   4.161 +                  proof -
   4.162 +                    have "(\<lambda>j. if j = i then g i else h j) \<in> U"
   4.163 +                      using \<open>f \<in> U\<close> f_def by blast
   4.164 +                    moreover have "f i \<in> topspace (X i)"
   4.165 +                      by (metis PiE_iff True comp_apply fin)
   4.166 +                    ultimately have "\<exists>b. b \<in> topspace (X i) \<and> (\<lambda>a. if a = i then b else h a) \<in> U"
   4.167 +                      using f_def by auto
   4.168 +                    then show ?thesis
   4.169 +                      by blast
   4.170 +                  qed
   4.171 +                  have "(\<lambda>j. if j = i then h i else h j) = h"
   4.172 +                    by force
   4.173 +                  moreover have "h i \<in> topspace (X i)"
   4.174 +                    using True insert.prems(1) by auto
   4.175 +                  ultimately show "?V \<noteq> {}"
   4.176 +                    using \<open>h \<in> V\<close>  by force
   4.177 +                qed
   4.178 +                then show ?thesis ..
   4.179 +              next
   4.180 +                case False
   4.181 +                show ?thesis
   4.182 +                proof (cases "h = f")
   4.183 +                  case True
   4.184 +                  show ?thesis
   4.185 +                    by (rule insert.IH [OF insert.prems(1)]) (simp add: True subM)
   4.186 +                next
   4.187 +                  case False
   4.188 +                  then show ?thesis
   4.189 +                    using gin insert.prems(1) \<open>i \<notin> I\<close> unfolding f_def by fastforce
   4.190 +                qed
   4.191 +              qed
   4.192 +            next
   4.193 +              case False
   4.194 +              then show ?thesis
   4.195 +                using subUV insert.prems(1) by auto
   4.196 +            qed
   4.197 +          qed
   4.198 +          then show "h \<in> U"
   4.199 +            unfolding g_def using PiE_iff \<open>finite L\<close> h by fastforce
   4.200 +        qed
   4.201 +      qed
   4.202 +      ultimately show ?thesis
   4.203 +        using disj inf_absorb2 \<open>V \<noteq> {}\<close> by fastforce
   4.204 +    qed
   4.205 +    then show ?lhs
   4.206 +      unfolding connected_space_def
   4.207 +      by auto
   4.208 +  qed
   4.209 +  ultimately show ?thesis
   4.210 +    by simp
   4.211 +qed (simp add: connected_space_topspace_empty)
   4.212 +
   4.213 +
   4.214 +lemma connectedin_PiE:
   4.215 +   "connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
   4.216 +        PiE I S = {} \<or> (\<forall>i \<in> I. connectedin (X i) (S i))"
   4.217 +  by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff
   4.218 +      topspace_subtopology_subset)
   4.219 +
   4.220 +lemma path_connected_space_product_topology:
   4.221 +   "path_connected_space(product_topology X I) \<longleftrightarrow>
   4.222 +    topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. path_connected_space(X i))"
   4.223 + (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
   4.224 +proof (cases ?eq)
   4.225 +  case False
   4.226 +  moreover have "?lhs = ?rhs"
   4.227 +  proof
   4.228 +    assume L: ?lhs
   4.229 +    show ?rhs
   4.230 +    proof (clarsimp simp flip: path_connectedin_topspace)
   4.231 +      fix i :: "'a"
   4.232 +      assume "i \<in> I"
   4.233 +      have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
   4.234 +        by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
   4.235 +      show "path_connectedin (X i) (topspace (X i))"
   4.236 +        using path_connectedin_continuous_map_image [OF cm L [unfolded path_connectedin_topspace [symmetric]]]
   4.237 +        by (metis \<open>i \<in> I\<close> False retraction_imp_surjective_map retraction_map_product_projection)
   4.238 +    qed
   4.239 +  next
   4.240 +    assume R [rule_format]: ?rhs
   4.241 +    show ?lhs
   4.242 +      unfolding path_connected_space_def topspace_product_topology
   4.243 +    proof clarify
   4.244 +      fix x y
   4.245 +      assume x: "x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))" and y: "y \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
   4.246 +      have "\<forall>i. \<exists>g. i \<in> I \<longrightarrow> pathin (X i) g \<and> g 0 = x i \<and> g 1 = y i"
   4.247 +        using PiE_mem R path_connected_space_def x y by force
   4.248 +      then obtain g where g: "\<And>i. i \<in> I \<Longrightarrow> pathin (X i) (g i) \<and> g i 0 = x i \<and> g i 1 = y i"
   4.249 +        by metis
   4.250 +      with x y show "\<exists>g. pathin (product_topology X I) g \<and> g 0 = x \<and> g 1 = y"
   4.251 +        apply (rule_tac x="\<lambda>a. \<lambda>i \<in> I. g i a" in exI)
   4.252 +        apply (force simp: pathin_def continuous_map_componentwise)
   4.253 +        done
   4.254 +    qed
   4.255 +  qed
   4.256 +  ultimately show ?thesis
   4.257 +    by simp
   4.258 +qed (simp add: path_connected_space_topspace_empty)
   4.259 +
   4.260 +lemma path_connectedin_PiE:
   4.261 +   "path_connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
   4.262 +    PiE I S = {} \<or> (\<forall>i \<in> I. path_connectedin (X i) (S i))"
   4.263 +  by (fastforce simp add: path_connectedin_def subtopology_PiE path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset)
   4.264 +
   4.265 +
   4.266  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Analysis/Locally.thy	Fri Mar 22 12:34:49 2019 +0000
     5.3 @@ -0,0 +1,449 @@
     5.4 +section \<open>Neigbourhood bases and Locally path-connected spaces\<close>
     5.5 +
     5.6 +theory Locally
     5.7 +  imports
     5.8 +    Path_Connected Function_Topology
     5.9 +begin
    5.10 +
    5.11 +subsection\<open>Neigbourhood bases (useful for "local" properties of various kinds)\<close>
    5.12 +
    5.13 +definition neighbourhood_base_at where
    5.14 + "neighbourhood_base_at x P X \<equiv>
    5.15 +        \<forall>W. openin X W \<and> x \<in> W
    5.16 +            \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)"
    5.17 +
    5.18 +definition neighbourhood_base_of where
    5.19 + "neighbourhood_base_of P X \<equiv>
    5.20 +        \<forall>x \<in> topspace X. neighbourhood_base_at x P X"
    5.21 +
    5.22 +lemma neighbourhood_base_of:
    5.23 +   "neighbourhood_base_of P X \<longleftrightarrow>
    5.24 +        (\<forall>W x. openin X W \<and> x \<in> W
    5.25 +          \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))"
    5.26 +  unfolding neighbourhood_base_at_def neighbourhood_base_of_def
    5.27 +  using openin_subset by blast
    5.28 +
    5.29 +lemma neighbourhood_base_at_mono:
    5.30 +   "\<lbrakk>neighbourhood_base_at x P X; \<And>S. \<lbrakk>P S; x \<in> S\<rbrakk> \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> neighbourhood_base_at x Q X"
    5.31 +  unfolding neighbourhood_base_at_def
    5.32 +  by (meson subset_eq)
    5.33 +
    5.34 +lemma neighbourhood_base_of_mono:
    5.35 +   "\<lbrakk>neighbourhood_base_of P X; \<And>S. P S \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> neighbourhood_base_of Q X"
    5.36 +  unfolding neighbourhood_base_of_def
    5.37 +  using neighbourhood_base_at_mono by force
    5.38 +
    5.39 +lemma open_neighbourhood_base_at:
    5.40 +   "(\<And>S. \<lbrakk>P S; x \<in> S\<rbrakk> \<Longrightarrow> openin X S)
    5.41 +        \<Longrightarrow> neighbourhood_base_at x P X \<longleftrightarrow> (\<forall>W. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> W))"
    5.42 +  unfolding neighbourhood_base_at_def
    5.43 +  by (meson subsetD)
    5.44 +
    5.45 +lemma open_neighbourhood_base_of:
    5.46 +  "(\<forall>S. P S \<longrightarrow> openin X S)
    5.47 +        \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow> (\<forall>W x. openin X W \<and> x \<in> W \<longrightarrow> (\<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> W))"
    5.48 +  apply (simp add: neighbourhood_base_of, safe, blast)
    5.49 +  by meson
    5.50 +
    5.51 +lemma neighbourhood_base_of_open_subset:
    5.52 +   "\<lbrakk>neighbourhood_base_of P X; openin X S\<rbrakk>
    5.53 +        \<Longrightarrow> neighbourhood_base_of P (subtopology X S)"
    5.54 +  apply (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt image_def)
    5.55 +  apply (rename_tac x V)
    5.56 +  apply (drule_tac x="S \<inter> V" in spec)
    5.57 +  apply (simp add: Int_ac)
    5.58 +  by (metis IntI le_infI1 openin_Int)
    5.59 +
    5.60 +lemma neighbourhood_base_of_topology_base:
    5.61 +   "openin X = arbitrary union_of (\<lambda>W. W \<in> \<B>)
    5.62 +        \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow>
    5.63 +             (\<forall>W x. W \<in> \<B> \<and> x \<in> W  \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))"
    5.64 +  apply (auto simp: openin_topology_base_unique neighbourhood_base_of)
    5.65 +  by (meson subset_trans)
    5.66 +
    5.67 +lemma neighbourhood_base_at_unlocalized:
    5.68 +  assumes "\<And>S T. \<lbrakk>P S; openin X T; x \<in> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> P T"
    5.69 +  shows "neighbourhood_base_at x P X
    5.70 +     \<longleftrightarrow> (x \<in> topspace X \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> topspace X))"
    5.71 +         (is "?lhs = ?rhs")
    5.72 +proof
    5.73 +  assume R: ?rhs show ?lhs
    5.74 +    unfolding neighbourhood_base_at_def
    5.75 +  proof clarify
    5.76 +    fix W
    5.77 +    assume "openin X W" "x \<in> W"
    5.78 +    then have "x \<in> topspace X"
    5.79 +      using openin_subset by blast
    5.80 +    with R obtain U V where "openin X U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> topspace X"
    5.81 +      by blast
    5.82 +    then show "\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
    5.83 +      by (metis IntI \<open>openin X W\<close> \<open>x \<in> W\<close> assms inf_le1 inf_le2 openin_Int)
    5.84 +  qed
    5.85 +qed (simp add: neighbourhood_base_at_def)
    5.86 +
    5.87 +lemma neighbourhood_base_at_with_subset:
    5.88 +   "\<lbrakk>openin X U; x \<in> U\<rbrakk>
    5.89 +        \<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow> neighbourhood_base_at x (\<lambda>T. T \<subseteq> U \<and> P T) X)"
    5.90 +  apply (simp add: neighbourhood_base_at_def)
    5.91 +  apply (metis IntI Int_subset_iff openin_Int)
    5.92 +  done
    5.93 +
    5.94 +lemma neighbourhood_base_of_with_subset:
    5.95 +   "neighbourhood_base_of P X \<longleftrightarrow> neighbourhood_base_of (\<lambda>t. t \<subseteq> topspace X \<and> P t) X"
    5.96 +  using neighbourhood_base_at_with_subset
    5.97 +  by (fastforce simp add: neighbourhood_base_of_def)
    5.98 +
    5.99 +subsection\<open>Locally path-connected spaces\<close>
   5.100 +
   5.101 +definition weakly_locally_path_connected_at
   5.102 +  where "weakly_locally_path_connected_at x X \<equiv> neighbourhood_base_at x (path_connectedin X) X"
   5.103 +
   5.104 +definition locally_path_connected_at
   5.105 +  where "locally_path_connected_at x X \<equiv>
   5.106 +    neighbourhood_base_at x (\<lambda>U. openin X U \<and> path_connectedin X U) X"
   5.107 +
   5.108 +definition locally_path_connected_space
   5.109 +  where "locally_path_connected_space X \<equiv> neighbourhood_base_of (path_connectedin X) X"
   5.110 +
   5.111 +lemma locally_path_connected_space_alt:
   5.112 +  "locally_path_connected_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> path_connectedin X U) X"
   5.113 +  (is "?P = ?Q")
   5.114 +  and locally_path_connected_space_eq_open_path_component_of:
   5.115 +  "locally_path_connected_space X \<longleftrightarrow>
   5.116 +        (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (Collect (path_component_of (subtopology X U) x)))"
   5.117 +  (is "?P = ?R")
   5.118 +proof -
   5.119 +  have ?P if ?Q
   5.120 +    using locally_path_connected_space_def neighbourhood_base_of_mono that by auto
   5.121 +  moreover have ?R if P: ?P
   5.122 +  proof -
   5.123 +    show ?thesis
   5.124 +    proof clarify
   5.125 +      fix U y
   5.126 +      assume "openin X U" "y \<in> U"
   5.127 +      have "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> Collect (path_component_of (subtopology X U) y)"
   5.128 +        if "path_component_of (subtopology X U) y x" for x
   5.129 +
   5.130 +      proof -
   5.131 +        have "x \<in> U"
   5.132 +          using path_component_of_equiv that topspace_subtopology by fastforce
   5.133 +        then have "\<exists>Ua. openin X Ua \<and> (\<exists>V. path_connectedin X V \<and> x \<in> Ua \<and> Ua \<subseteq> V \<and> V \<subseteq> U)"
   5.134 +      using P
   5.135 +      by (simp add: \<open>openin X U\<close> locally_path_connected_space_def neighbourhood_base_of)
   5.136 +        then show ?thesis
   5.137 +          by (metis dual_order.trans path_component_of_equiv path_component_of_maximal path_connectedin_subtopology subset_iff that)
   5.138 +      qed
   5.139 +      then show "openin X (Collect (path_component_of (subtopology X U) y))"
   5.140 +        using openin_subopen by force
   5.141 +    qed
   5.142 +  qed
   5.143 +  moreover have ?Q if ?R
   5.144 +    using that
   5.145 +    apply (simp add: open_neighbourhood_base_of)
   5.146 +    by (metis mem_Collect_eq openin_subset path_component_of_refl path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset)
   5.147 +  ultimately show "?P = ?Q" "?P = ?R"
   5.148 +    by blast+
   5.149 +qed
   5.150 +
   5.151 +lemma locally_path_connected_space:
   5.152 +   "locally_path_connected_space X
   5.153 +   \<longleftrightarrow> (\<forall>V x. openin X V \<and> x \<in> V \<longrightarrow> (\<exists>U. openin X U \<and> path_connectedin X U \<and> x \<in> U \<and> U \<subseteq> V))"
   5.154 +  by (simp add: locally_path_connected_space_alt open_neighbourhood_base_of)
   5.155 +
   5.156 +lemma locally_path_connected_space_open_path_components:
   5.157 +   "locally_path_connected_space X \<longleftrightarrow>
   5.158 +        (\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> openin X c)"
   5.159 +  apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def topspace_subtopology)
   5.160 +  by (metis imageI inf.absorb_iff2 openin_closedin_eq)
   5.161 +
   5.162 +lemma openin_path_component_of_locally_path_connected_space:
   5.163 +   "locally_path_connected_space X \<Longrightarrow> openin X (Collect (path_component_of X x))"
   5.164 +  apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
   5.165 +  by (metis openin_empty openin_topspace path_component_of_eq_empty subtopology_topspace)
   5.166 +
   5.167 +lemma openin_path_components_of_locally_path_connected_space:
   5.168 +   "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X c"
   5.169 +  apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
   5.170 +  by (metis (no_types, lifting) imageE openin_topspace path_components_of_def subtopology_topspace)
   5.171 +
   5.172 +lemma closedin_path_components_of_locally_path_connected_space:
   5.173 +   "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X c"
   5.174 +  by (simp add: closedin_def complement_path_components_of_Union openin_path_components_of_locally_path_connected_space openin_clauses(3) path_components_of_subset)
   5.175 +
   5.176 +lemma closedin_path_component_of_locally_path_connected_space:
   5.177 +  assumes "locally_path_connected_space X"
   5.178 +  shows "closedin X (Collect (path_component_of X x))"
   5.179 +proof (cases "x \<in> topspace X")
   5.180 +  case True
   5.181 +  then show ?thesis
   5.182 +    by (simp add: assms closedin_path_components_of_locally_path_connected_space path_component_in_path_components_of)
   5.183 +next
   5.184 +  case False
   5.185 +  then show ?thesis
   5.186 +    by (metis closedin_empty path_component_of_eq_empty)
   5.187 +qed
   5.188 +
   5.189 +lemma weakly_locally_path_connected_at:
   5.190 +   "weakly_locally_path_connected_at x X \<longleftrightarrow>
   5.191 +    (\<forall>V. openin X V \<and> x \<in> V
   5.192 +          \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and>
   5.193 +                  (\<forall>y \<in> U. \<exists>C. path_connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))"
   5.194 +         (is "?lhs = ?rhs")
   5.195 +proof
   5.196 +  assume ?lhs then show ?rhs
   5.197 +    apply (simp add: weakly_locally_path_connected_at_def neighbourhood_base_at_def)
   5.198 +    by (meson order_trans subsetD)
   5.199 +next
   5.200 +  have *: "\<exists>V. path_connectedin X V \<and> U \<subseteq> V \<and> V \<subseteq> W"
   5.201 +    if "(\<forall>y\<in>U. \<exists>C. path_connectedin X C \<and> C \<subseteq> W \<and> x \<in> C \<and> y \<in> C)"
   5.202 +    for W U
   5.203 +  proof (intro exI conjI)
   5.204 +    let ?V = "(Collect (path_component_of (subtopology X W) x))"
   5.205 +      show "path_connectedin X (Collect (path_component_of (subtopology X W) x))"
   5.206 +        by (meson path_connectedin_path_component_of path_connectedin_subtopology)
   5.207 +      show "U \<subseteq> ?V"
   5.208 +        by (auto simp: path_component_of path_connectedin_subtopology that)
   5.209 +      show "?V \<subseteq> W"
   5.210 +        by (meson path_connectedin_path_component_of path_connectedin_subtopology)
   5.211 +    qed
   5.212 +  assume ?rhs
   5.213 +  then show ?lhs
   5.214 +    unfolding weakly_locally_path_connected_at_def neighbourhood_base_at_def by (metis "*")
   5.215 +qed
   5.216 +
   5.217 +lemma locally_path_connected_space_im_kleinen:
   5.218 +   "locally_path_connected_space X \<longleftrightarrow>
   5.219 +      (\<forall>V x. openin X V \<and> x \<in> V
   5.220 +             \<longrightarrow> (\<exists>U. openin X U \<and>
   5.221 +                    x \<in> U \<and> U \<subseteq> V \<and>
   5.222 +                    (\<forall>y \<in> U. \<exists>c. path_connectedin X c \<and>
   5.223 +                                c \<subseteq> V \<and> x \<in> c \<and> y \<in> c)))"
   5.224 +  apply (simp add: locally_path_connected_space_def neighbourhood_base_of_def)
   5.225 +  apply (simp add: weakly_locally_path_connected_at flip: weakly_locally_path_connected_at_def)
   5.226 +  using openin_subset apply force
   5.227 +  done
   5.228 +
   5.229 +lemma locally_path_connected_space_open_subset:
   5.230 +   "\<lbrakk>locally_path_connected_space X; openin X s\<rbrakk>
   5.231 +        \<Longrightarrow> locally_path_connected_space (subtopology X s)"
   5.232 +  apply (simp add: locally_path_connected_space_def neighbourhood_base_of openin_open_subtopology path_connectedin_subtopology)
   5.233 +  by (meson order_trans)
   5.234 +
   5.235 +lemma locally_path_connected_space_quotient_map_image:
   5.236 +  assumes f: "quotient_map X Y f" and X: "locally_path_connected_space X"
   5.237 +  shows "locally_path_connected_space Y"
   5.238 +  unfolding locally_path_connected_space_open_path_components
   5.239 +proof clarify
   5.240 +  fix V C
   5.241 +  assume V: "openin Y V" and c: "C \<in> path_components_of (subtopology Y V)"
   5.242 +  then have sub: "C \<subseteq> topspace Y"
   5.243 +    using path_connectedin_path_components_of path_connectedin_subset_topspace path_connectedin_subtopology by blast
   5.244 +  have "openin X {x \<in> topspace X. f x \<in> C}"
   5.245 +  proof (subst openin_subopen, clarify)
   5.246 +    fix x
   5.247 +    assume x: "x \<in> topspace X" and "f x \<in> C"
   5.248 +    let ?T = "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)"
   5.249 +    show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}"
   5.250 +    proof (intro exI conjI)
   5.251 +      have "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)"
   5.252 +      proof (intro exI conjI)
   5.253 +        show "openin X ({z \<in> topspace X. f z \<in> V})"
   5.254 +          using V f openin_subset quotient_map_def by fastforce
   5.255 +        show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)
   5.256 +        \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})"
   5.257 +          by (metis (no_types, lifting) Int_iff \<open>f x \<in> C\<close> c mem_Collect_eq path_component_in_path_components_of path_components_of_subset topspace_subtopology topspace_subtopology_subset x)
   5.258 +      qed
   5.259 +      with X show "openin X ?T"
   5.260 +        using locally_path_connected_space_open_path_components by blast
   5.261 +      show x: "x \<in> ?T"
   5.262 +        using V \<open>f x \<in> C\<close> c openin_subset path_component_of_equiv path_components_of_subset topspace_subtopology topspace_subtopology_subset x
   5.263 +        by fastforce
   5.264 +      have "f ` ?T \<subseteq> C"
   5.265 +      proof (rule path_components_of_maximal)
   5.266 +        show "C \<in> path_components_of (subtopology Y V)"
   5.267 +          by (simp add: c)
   5.268 +        show "path_connectedin (subtopology Y V) (f ` ?T)"
   5.269 +        proof -
   5.270 +          have "quotient_map (subtopology X {a \<in> topspace X. f a \<in> V}) (subtopology Y V) f"
   5.271 +            by (simp add: V f quotient_map_restriction)
   5.272 +          then show ?thesis
   5.273 +            by (meson path_connectedin_continuous_map_image path_connectedin_path_component_of quotient_imp_continuous_map)
   5.274 +        qed
   5.275 +        show "\<not> disjnt C (f ` ?T)"
   5.276 +          by (metis (no_types, lifting) \<open>f x \<in> C\<close> x disjnt_iff image_eqI)
   5.277 +      qed
   5.278 +      then show "?T \<subseteq> {x \<in> topspace X. f x \<in> C}"
   5.279 +        by (force simp: path_component_of_equiv topspace_subtopology)
   5.280 +    qed
   5.281 +  qed
   5.282 +  then show "openin Y C"
   5.283 +    using f sub by (simp add: quotient_map_def)
   5.284 +qed
   5.285 +
   5.286 +lemma homeomorphic_locally_path_connected_space:
   5.287 +  assumes "X homeomorphic_space Y"
   5.288 +  shows "locally_path_connected_space X \<longleftrightarrow> locally_path_connected_space Y"
   5.289 +proof -
   5.290 +  obtain f g where "homeomorphic_maps X Y f g"
   5.291 +    using assms homeomorphic_space_def by fastforce
   5.292 +  then show ?thesis
   5.293 +    by (metis (no_types) homeomorphic_map_def homeomorphic_maps_map locally_path_connected_space_quotient_map_image)
   5.294 +qed
   5.295 +
   5.296 +lemma locally_path_connected_space_retraction_map_image:
   5.297 +   "\<lbrakk>retraction_map X Y r; locally_path_connected_space X\<rbrakk>
   5.298 +        \<Longrightarrow> locally_path_connected_space Y"
   5.299 +  using Abstract_Topology.retraction_imp_quotient_map locally_path_connected_space_quotient_map_image by blast
   5.300 +
   5.301 +lemma locally_path_connected_space_euclideanreal: "locally_path_connected_space euclideanreal"
   5.302 +  unfolding locally_path_connected_space_def neighbourhood_base_of
   5.303 +  proof clarsimp
   5.304 +  fix W and x :: "real"
   5.305 +  assume "open W" "x \<in> W"
   5.306 +  then obtain e where "e > 0" and e: "\<And>x'. \<bar>x' - x\<bar> < e \<longrightarrow> x' \<in> W"
   5.307 +    by (auto simp: open_real)
   5.308 +  then show "\<exists>U. open U \<and> (\<exists>V. path_connected V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)"
   5.309 +    by (force intro!: convex_imp_path_connected exI [where x = "{x-e<..<x+e}"])
   5.310 +qed
   5.311 +
   5.312 +lemma locally_path_connected_space_discrete_topology:
   5.313 +   "locally_path_connected_space (discrete_topology U)"
   5.314 +  using locally_path_connected_space_open_path_components by fastforce
   5.315 +
   5.316 +lemma path_component_eq_connected_component_of:
   5.317 +  assumes "locally_path_connected_space X"
   5.318 +  shows "(path_component_of_set X x = connected_component_of_set X x)"
   5.319 +proof (cases "x \<in> topspace X")
   5.320 +  case True
   5.321 +  then show ?thesis
   5.322 +    using connectedin_connected_component_of [of X x]
   5.323 +    apply (clarsimp simp add: connectedin_def connected_space_clopen_in topspace_subtopology_subset cong: conj_cong)
   5.324 +    apply (drule_tac x="path_component_of_set X x" in spec)
   5.325 +    by (metis assms closedin_closed_subtopology closedin_connected_component_of closedin_path_component_of_locally_path_connected_space inf.absorb_iff2 inf.orderE openin_path_component_of_locally_path_connected_space openin_subtopology path_component_of_eq_empty path_component_subset_connected_component_of)
   5.326 +next
   5.327 +  case False
   5.328 +  then show ?thesis
   5.329 +    using connected_component_of_eq_empty path_component_of_eq_empty by fastforce
   5.330 +qed
   5.331 +
   5.332 +lemma path_components_eq_connected_components_of:
   5.333 +   "locally_path_connected_space X \<Longrightarrow> (path_components_of X = connected_components_of X)"
   5.334 +  by (simp add: path_components_of_def connected_components_of_def image_def path_component_eq_connected_component_of)
   5.335 +
   5.336 +lemma path_connected_eq_connected_space:
   5.337 +   "locally_path_connected_space X
   5.338 +         \<Longrightarrow> path_connected_space X \<longleftrightarrow> connected_space X"
   5.339 +  by (metis connected_components_of_subset_sing path_components_eq_connected_components_of path_components_of_subset_singleton)
   5.340 +
   5.341 +lemma locally_path_connected_space_product_topology:
   5.342 +   "locally_path_connected_space(product_topology X I) \<longleftrightarrow>
   5.343 +        topspace(product_topology X I) = {} \<or>
   5.344 +        finite {i. i \<in> I \<and> ~path_connected_space(X i)} \<and>
   5.345 +        (\<forall>i \<in> I. locally_path_connected_space(X i))"
   5.346 +    (is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs")
   5.347 +proof (cases ?empty)
   5.348 +  case True
   5.349 +  then show ?thesis
   5.350 +    by (simp add: locally_path_connected_space_def neighbourhood_base_of openin_closedin_eq)
   5.351 +next
   5.352 +  case False
   5.353 +  then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
   5.354 +    by auto
   5.355 +  have ?rhs if L: ?lhs
   5.356 +  proof -
   5.357 +    obtain U C where U: "openin (product_topology X I) U"
   5.358 +      and V: "path_connectedin (product_topology X I) C"
   5.359 +      and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
   5.360 +      using L apply (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
   5.361 +      by (metis openin_topspace topspace_product_topology z)
   5.362 +    then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}"
   5.363 +      and XV: "\<And>i. i\<in>I \<Longrightarrow> openin (X i) (V i)" and "z \<in> Pi\<^sub>E I V" and subU: "Pi\<^sub>E I V \<subseteq> U"
   5.364 +      by (force simp: openin_product_topology_alt)
   5.365 +    show ?thesis
   5.366 +    proof (intro conjI ballI)
   5.367 +      have "path_connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
   5.368 +      proof -
   5.369 +        have pc: "path_connectedin (X i) ((\<lambda>x. x i) ` C)"
   5.370 +          apply (rule path_connectedin_continuous_map_image [OF _ V])
   5.371 +          by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
   5.372 +        moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
   5.373 +        proof
   5.374 +          show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
   5.375 +            by (simp add: pc path_connectedin_subset_topspace)
   5.376 +          have "V i \<subseteq> (\<lambda>x. x i) ` (\<Pi>\<^sub>E i\<in>I. V i)"
   5.377 +            by (metis \<open>z \<in> Pi\<^sub>E I V\<close> empty_iff image_projection_PiE order_refl that(1))
   5.378 +          also have "\<dots> \<subseteq> (\<lambda>x. x i) ` U"
   5.379 +            using subU by blast
   5.380 +          finally show "topspace (X i) \<subseteq> (\<lambda>x. x i) ` C"
   5.381 +            using \<open>U \<subseteq> C\<close> that by blast
   5.382 +        qed
   5.383 +        ultimately show ?thesis
   5.384 +          by (simp add: path_connectedin_topspace)
   5.385 +      qed
   5.386 +      then have "{i \<in> I. \<not> path_connected_space (X i)} \<subseteq> {i \<in> I. V i \<noteq> topspace (X i)}"
   5.387 +        by blast
   5.388 +      with finV show "finite {i \<in> I. \<not> path_connected_space (X i)}"
   5.389 +        using finite_subset by blast
   5.390 +    next
   5.391 +      show "locally_path_connected_space (X i)" if "i \<in> I" for i
   5.392 +        apply (rule locally_path_connected_space_quotient_map_image [OF _ L, where f = "\<lambda>x. x i"])
   5.393 +        by (metis False Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection that)
   5.394 +    qed
   5.395 +  qed
   5.396 +  moreover have ?lhs if R: ?rhs
   5.397 +  proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
   5.398 +    fix F z
   5.399 +    assume "openin (product_topology X I) F" and "z \<in> F"
   5.400 +    then obtain W where finW: "finite {i \<in> I. W i \<noteq> topspace (X i)}"
   5.401 +            and opeW: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (W i)" and "z \<in> Pi\<^sub>E I W" "Pi\<^sub>E I W \<subseteq> F"
   5.402 +      by (auto simp: openin_product_topology_alt)
   5.403 +    have "\<forall>i \<in> I. \<exists>U C. openin (X i) U \<and> path_connectedin (X i) C \<and> z i \<in> U \<and> U \<subseteq> C \<and> C \<subseteq> W i \<and>
   5.404 +                        (W i = topspace (X i) \<and>
   5.405 +                         path_connected_space (X i) \<longrightarrow> U = topspace (X i) \<and> C = topspace (X i))"
   5.406 +          (is "\<forall>i \<in> I. ?\<Phi> i")
   5.407 +    proof
   5.408 +      fix i assume "i \<in> I"
   5.409 +      have "locally_path_connected_space (X i)"
   5.410 +        by (simp add: R \<open>i \<in> I\<close>)
   5.411 +      moreover have "openin (X i) (W i) " "z i \<in> W i"
   5.412 +        using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
   5.413 +      ultimately obtain U C where UC: "openin (X i) U" "path_connectedin (X i) C" "z i \<in> U" "U \<subseteq> C" "C \<subseteq> W i"
   5.414 +        using \<open>i \<in> I\<close> by (force simp: locally_path_connected_space_def neighbourhood_base_of)
   5.415 +      show "?\<Phi> i"
   5.416 +      proof (cases "W i = topspace (X i) \<and> path_connected_space(X i)")
   5.417 +        case True
   5.418 +        then show ?thesis
   5.419 +          using \<open>z i \<in> W i\<close> path_connectedin_topspace by blast
   5.420 +      next
   5.421 +        case False
   5.422 +        then show ?thesis
   5.423 +          by (meson UC)
   5.424 +      qed
   5.425 +    qed
   5.426 +    then obtain U C where
   5.427 +      *: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i) \<and> path_connectedin (X i) (C i) \<and> z i \<in> (U i) \<and> (U i) \<subseteq> (C i) \<and> (C i) \<subseteq> W i \<and>
   5.428 +                        (W i = topspace (X i) \<and> path_connected_space (X i)
   5.429 +                         \<longrightarrow> (U i) = topspace (X i) \<and> (C i) = topspace (X i))"
   5.430 +      by metis
   5.431 +    let ?A = "{i \<in> I. \<not> path_connected_space (X i)} \<union> {i \<in> I. W i \<noteq> topspace (X i)}"
   5.432 +    have "{i \<in> I. U i \<noteq> topspace (X i)} \<subseteq> ?A"
   5.433 +      by (clarsimp simp add: "*")
   5.434 +    moreover have "finite ?A"
   5.435 +      by (simp add: that finW)
   5.436 +    ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}"
   5.437 +      using finite_subset by auto
   5.438 +    then have "openin (product_topology X I) (Pi\<^sub>E I U)"
   5.439 +      using * by (simp add: openin_PiE_gen)
   5.440 +    then show "\<exists>U. openin (product_topology X I) U \<and>
   5.441 +            (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
   5.442 +      apply (rule_tac x="PiE I U" in exI, simp)
   5.443 +      apply (rule_tac x="PiE I C" in exI)
   5.444 +      using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
   5.445 +      apply (simp add: path_connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
   5.446 +      done
   5.447 +  qed
   5.448 +  ultimately show ?thesis
   5.449 +    using False by blast
   5.450 +qed
   5.451 +
   5.452 +end
     6.1 --- a/src/HOL/Analysis/Product_Topology.thy	Thu Mar 21 19:46:26 2019 +0100
     6.2 +++ b/src/HOL/Analysis/Product_Topology.thy	Fri Mar 22 12:34:49 2019 +0000
     6.3 @@ -1,7 +1,7 @@
     6.4  section\<open>The binary product topology\<close>
     6.5  
     6.6  theory Product_Topology
     6.7 -imports Function_Topology   
     6.8 +imports Function_Topology Abstract_Limits
     6.9  begin
    6.10  
    6.11  section \<open>Product Topology\<close> 
    6.12 @@ -519,5 +519,49 @@
    6.13    then show ?thesis by metis
    6.14  qed
    6.15  
    6.16 +lemma limitin_pairwise:
    6.17 +   "limitin (prod_topology X Y) f l F \<longleftrightarrow> limitin X (fst \<circ> f) (fst l) F \<and> limitin Y (snd \<circ> f) (snd l) F"
    6.18 +    (is "?lhs = ?rhs")
    6.19 +proof
    6.20 +  assume ?lhs
    6.21 +  then obtain a b where ev: "\<And>U. \<lbrakk>(a,b) \<in> U; openin (prod_topology X Y) U\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in F. f x \<in> U"
    6.22 +                        and a: "a \<in> topspace X" and b: "b \<in> topspace Y" and l: "l = (a,b)"
    6.23 +    by (auto simp: limitin_def)
    6.24 +  moreover have "\<forall>\<^sub>F x in F. fst (f x) \<in> U" if "openin X U" "a \<in> U" for U
    6.25 +  proof -
    6.26 +    have "\<forall>\<^sub>F c in F. f c \<in> U \<times> topspace Y"
    6.27 +      using b that ev [of "U \<times> topspace Y"] by (auto simp: openin_prod_topology_alt)
    6.28 +    then show ?thesis
    6.29 +      by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
    6.30 +  qed
    6.31 +  moreover have "\<forall>\<^sub>F x in F. snd (f x) \<in> U" if "openin Y U" "b \<in> U" for U
    6.32 +  proof -
    6.33 +    have "\<forall>\<^sub>F c in F. f c \<in> topspace X \<times> U"
    6.34 +      using a that ev [of "topspace X \<times> U"] by (auto simp: openin_prod_topology_alt)
    6.35 +    then show ?thesis
    6.36 +      by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
    6.37 +  qed
    6.38 +  ultimately show ?rhs
    6.39 +    by (simp add: limitin_def)
    6.40 +next
    6.41 +  have "limitin (prod_topology X Y) f (a,b) F"
    6.42 +    if "limitin X (fst \<circ> f) a F" "limitin Y (snd \<circ> f) b F" for a b
    6.43 +    using that
    6.44 +  proof (clarsimp simp: limitin_def)
    6.45 +    fix Z :: "('a \<times> 'b) set"
    6.46 +    assume a: "a \<in> topspace X" "\<forall>U. openin X U \<and> a \<in> U \<longrightarrow> (\<forall>\<^sub>F x in F. fst (f x) \<in> U)"
    6.47 +      and b: "b \<in> topspace Y" "\<forall>U. openin Y U \<and> b \<in> U \<longrightarrow> (\<forall>\<^sub>F x in F. snd (f x) \<in> U)"
    6.48 +      and Z: "openin (prod_topology X Y) Z" "(a, b) \<in> Z"
    6.49 +    then obtain U V where "openin X U" "openin Y V" "a \<in> U" "b \<in> V" "U \<times> V \<subseteq> Z"
    6.50 +      using Z by (force simp: openin_prod_topology_alt)
    6.51 +    then have "\<forall>\<^sub>F x in F. fst (f x) \<in> U" "\<forall>\<^sub>F x in F. snd (f x) \<in> V"
    6.52 +      by (simp_all add: a b)
    6.53 +    then show "\<forall>\<^sub>F x in F. f x \<in> Z"
    6.54 +      by (rule eventually_elim2) (use \<open>U \<times> V \<subseteq> Z\<close> subsetD in auto)
    6.55 +  qed
    6.56 +  then show "?rhs \<Longrightarrow> ?lhs"
    6.57 +    by (metis prod.collapse)
    6.58 +qed
    6.59 +
    6.60  end
    6.61