# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1553258089 0
# Node ID 35ba13ac6e5c5c47074291a4350db162a909b257
# Parent  ab8aad4aa76e11e15da6b17a10de5e0cfa93eefc
New abstract topological material

diff -r ab8aad4aa76e -r 35ba13ac6e5c src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu Mar 21 19:46:26 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Fri Mar 22 12:34:49 2019 +0000
@@ -2761,6 +2761,11 @@
 definition connectedin :: "'a topology \<Rightarrow> 'a set \<Rightarrow> bool" where
   "connectedin X S \<equiv> S \<subseteq> topspace X \<and> connected_space (subtopology X S)"
 
+lemma connected_spaceD:
+  "\<lbrakk>connected_space X;
+    openin X U; openin X V; topspace X \<subseteq> U \<union> V; U \<inter> V = {}; U \<noteq> {}; V \<noteq> {}\<rbrakk> \<Longrightarrow> False"
+  by (auto simp: connected_space_def)
+
 lemma connectedin_subset_topspace: "connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
   by (simp add: connectedin_def)
 
diff -r ab8aad4aa76e -r 35ba13ac6e5c src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Thu Mar 21 19:46:26 2019 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Fri Mar 22 12:34:49 2019 +0000
@@ -6,6 +6,7 @@
   (* Topology *)
   Connected
   Abstract_Limits
+  Locally
   (* Functional Analysis *)
   Elementary_Normed_Spaces
   Norm_Arith
diff -r ab8aad4aa76e -r 35ba13ac6e5c src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Mar 21 19:46:26 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Mar 22 12:34:49 2019 +0000
@@ -84,7 +84,7 @@
     done
 qed
 
-lemma retraction_imp_quotient_map:
+lemma retraction_openin_vimage_iff:
   "openin (top_of_set S) (S \<inter> r -` U) \<longleftrightarrow> openin (top_of_set T) U"
   if retraction: "retraction S T r" and "U \<subseteq> T"
   using retraction apply (rule retractionE)
@@ -110,13 +110,13 @@
   assumes "locally connected T" "S retract_of T"
   shows "locally connected S"
   using assms
-  by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_connected_quotient_image retract_ofE)
+  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_connected_quotient_image retract_ofE)
 
 lemma retract_of_locally_path_connected:
   assumes "locally path_connected T" "S retract_of T"
   shows "locally path_connected S"
   using assms
-  by (auto simp: idempotent_imp_retraction intro!: retraction_imp_quotient_map elim!: locally_path_connected_quotient_image retract_ofE)
+  by (auto simp: idempotent_imp_retraction intro!: retraction_openin_vimage_iff elim!: locally_path_connected_quotient_image retract_ofE)
 
 text \<open>A few simple lemmas about deformation retracts\<close>
 
diff -r ab8aad4aa76e -r 35ba13ac6e5c src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Thu Mar 21 19:46:26 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Fri Mar 22 12:34:49 2019 +0000
@@ -3,7 +3,7 @@
 *)
 
 theory Function_Topology
-imports Topology_Euclidean_Space
+imports Topology_Euclidean_Space Abstract_Limits
 begin
 
 
@@ -1480,6 +1480,8 @@
    "k \<in> I \<Longrightarrow> continuous_map (product_topology X I) (X k) (\<lambda>x. x k)"
   using continuous_map_componentwise [of "product_topology X I" X I id] by simp
 
+declare continuous_map_from_subtopology [OF continuous_map_product_projection, continuous_intros]
+
 proposition open_map_product_projection:
   assumes "i \<in> I"
   shows "open_map (product_topology Y I) (Y i) (\<lambda>f. f i)"
@@ -1752,4 +1754,245 @@
    apply (auto simp: image_iff inj_on_def)
   done
 
+subsection\<open>Relationship with connected spaces, paths, etc.\<close>
+
+proposition connected_space_product_topology:
+   "connected_space(product_topology X I) \<longleftrightarrow>
+    (\<Pi>\<^sub>E i\<in>I. topspace (X i)) = {} \<or> (\<forall>i \<in> I. connected_space(X i))"
+  (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
+proof (cases ?eq)
+  case False
+  moreover have "?lhs = ?rhs"
+  proof
+    assume ?lhs
+    moreover
+    have "connectedin(X i) (topspace(X i))"
+      if "i \<in> I" and ci: "connectedin(product_topology X I) (topspace(product_topology X I))" for i
+    proof -
+      have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
+        by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
+      show ?thesis
+        using connectedin_continuous_map_image [OF cm ci] \<open>i \<in> I\<close>
+        by (simp add: False image_projection_PiE)
+    qed
+    ultimately show ?rhs
+      by (meson connectedin_topspace)
+  next
+    assume cs [rule_format]: ?rhs
+    have False
+      if disj: "U \<inter> V = {}" and subUV: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U \<union> V"
+        and U: "openin (product_topology X I) U"
+        and V: "openin (product_topology X I) V"
+        and "U \<noteq> {}" "V \<noteq> {}"
+      for U V
+    proof -
+      obtain f where "f \<in> U"
+        using \<open>U \<noteq> {}\<close> by blast
+      then have f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+        using U openin_subset by fastforce
+      have "U \<subseteq> topspace(product_topology X I)" "V \<subseteq> topspace(product_topology X I)"
+        using U V openin_subset by blast+
+      moreover have "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<subseteq> U"
+      proof -
+        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
+            (\<Pi>\<^sub>E i\<in>I. topspace (X i))) C" "C \<subseteq> U" "f \<in> C"
+          using U \<open>f \<in> U\<close> unfolding openin_product_topology union_of_def by auto
+        then obtain \<T> where "finite \<T>"
+          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}"
+          and subU: "topspace (product_topology X I) \<inter> \<Inter>\<T> \<subseteq> U"
+          and ftop: "f \<in> topspace (product_topology X I)"
+          and fint: "f \<in> \<Inter> \<T>"
+          by (fastforce simp: relative_to_def intersection_of_def subset_iff)
+        let ?L = "\<Union>C\<in>\<T>. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
+        obtain L where "finite L"
+          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"
+        proof
+          show "finite ?L"
+          proof (rule finite_Union)
+            fix M
+            assume "M \<in> (\<lambda>C. {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}) ` \<T>"
+            then obtain C where "C \<in> \<T>" and C: "M = {i. (\<lambda>x. x i) ` C \<subset> topspace (X i)}"
+              by blast
+            then obtain j V where "j \<in> I" and ope: "openin (X j) V" and Ceq: "C = {x. x j \<in> V}"
+              using t by meson
+            then have "f j \<in> V"
+              using \<open>C \<in> \<T>\<close> fint by force
+            then have "(\<lambda>x. x k) ` {x. x j \<in> V} = UNIV" if "k \<noteq> j" for k
+              using that
+              apply (clarsimp simp add: set_eq_iff)
+              apply (rule_tac x="\<lambda>m. if m = k then x else f m" in image_eqI, auto)
+              done
+            then have "{i. (\<lambda>x. x i) ` C \<subset> topspace (X i)} \<subseteq> {j}"
+              using Ceq by auto
+            then show "finite M"
+              using C finite_subset by fastforce
+          qed (use \<open>finite \<T>\<close> in blast)
+        next
+          fix i U
+          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>"
+          then show "i \<in> ?L"
+            by (rule_tac a="{x. x i \<in> U}" in UN_I) (force+)
+        qed
+        show ?thesis
+        proof
+          fix h
+          assume h: "h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+          define g where "g \<equiv> \<lambda>i. if i \<in> L then f i else h i"
+          have gin: "g \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+            unfolding g_def using f h by auto
+          moreover have "g \<in> X" if "X \<in> \<T>" for X
+            using fint openin_subset t [OF that] L g_def h that by fastforce
+          ultimately have "g \<in> U"
+            using subU by auto
+          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
+            using that
+          proof (induction arbitrary: h)
+            case empty
+            then show ?case
+              using PiE_ext \<open>g \<in> U\<close> gin by force
+          next
+            case (insert i M)
+            define f where "f \<equiv> \<lambda>j. if j = i then g i else h j"
+            have fin: "f \<in> PiE I (topspace \<circ> X)"
+              unfolding f_def using gin insert.prems(1) by auto
+            have subM: "{j \<in> I. f j \<noteq> g j} \<subseteq> M"
+              unfolding f_def using insert.prems(2) by auto
+            have "f \<in> U"
+              using insert.IH [OF fin subM] .
+            show ?case
+            proof (cases "h \<in> V")
+              case True
+              show ?thesis
+              proof (cases "i \<in> I")
+                case True
+                let ?U = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> U}"
+                let ?V = "{x \<in> topspace(X i). (\<lambda>j. if j = i then x else h j) \<in> V}"
+                have False
+                proof (rule connected_spaceD [OF cs [OF \<open>i \<in> I\<close>]])
+                  have "\<And>k. k \<in> I \<Longrightarrow> continuous_map (X i) (X k) (\<lambda>x. if k = i then x else h k)"
+                    using continuous_map_eq_topcontinuous_at insert.prems(1) topcontinuous_at_def by fastforce
+                  then have cm: "continuous_map (X i) (product_topology X I) (\<lambda>x j. if j = i then x else h j)"
+                    using \<open>i \<in> I\<close> insert.prems(1)
+                    by (auto simp: continuous_map_componentwise extensional_def)
+                  show "openin (X i) ?U"
+                    by (rule openin_continuous_map_preimage [OF cm U])
+                  show "openin (X i) ?V"
+                    by (rule openin_continuous_map_preimage [OF cm V])
+                  show "topspace (X i) \<subseteq> ?U \<union> ?V"
+                  proof clarsimp
+                    fix x
+                    assume "x \<in> topspace (X i)" and "(\<lambda>j. if j = i then x else h j) \<notin> V"
+                    with True subUV \<open>h \<in> Pi\<^sub>E I (topspace \<circ> X)\<close>
+                    show "(\<lambda>j. if j = i then x else h j) \<in> U"
+                      by (drule_tac c="(\<lambda>j. if j = i then x else h j)" in subsetD) auto
+                  qed
+                  show "?U \<inter> ?V = {}"
+                    using disj by blast
+                  show "?U \<noteq> {}"
+                    using \<open>U \<noteq> {}\<close> f_def
+                  proof -
+                    have "(\<lambda>j. if j = i then g i else h j) \<in> U"
+                      using \<open>f \<in> U\<close> f_def by blast
+                    moreover have "f i \<in> topspace (X i)"
+                      by (metis PiE_iff True comp_apply fin)
+                    ultimately have "\<exists>b. b \<in> topspace (X i) \<and> (\<lambda>a. if a = i then b else h a) \<in> U"
+                      using f_def by auto
+                    then show ?thesis
+                      by blast
+                  qed
+                  have "(\<lambda>j. if j = i then h i else h j) = h"
+                    by force
+                  moreover have "h i \<in> topspace (X i)"
+                    using True insert.prems(1) by auto
+                  ultimately show "?V \<noteq> {}"
+                    using \<open>h \<in> V\<close>  by force
+                qed
+                then show ?thesis ..
+              next
+                case False
+                show ?thesis
+                proof (cases "h = f")
+                  case True
+                  show ?thesis
+                    by (rule insert.IH [OF insert.prems(1)]) (simp add: True subM)
+                next
+                  case False
+                  then show ?thesis
+                    using gin insert.prems(1) \<open>i \<notin> I\<close> unfolding f_def by fastforce
+                qed
+              qed
+            next
+              case False
+              then show ?thesis
+                using subUV insert.prems(1) by auto
+            qed
+          qed
+          then show "h \<in> U"
+            unfolding g_def using PiE_iff \<open>finite L\<close> h by fastforce
+        qed
+      qed
+      ultimately show ?thesis
+        using disj inf_absorb2 \<open>V \<noteq> {}\<close> by fastforce
+    qed
+    then show ?lhs
+      unfolding connected_space_def
+      by auto
+  qed
+  ultimately show ?thesis
+    by simp
+qed (simp add: connected_space_topspace_empty)
+
+
+lemma connectedin_PiE:
+   "connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
+        PiE I S = {} \<or> (\<forall>i \<in> I. connectedin (X i) (S i))"
+  by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff
+      topspace_subtopology_subset)
+
+lemma path_connected_space_product_topology:
+   "path_connected_space(product_topology X I) \<longleftrightarrow>
+    topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. path_connected_space(X i))"
+ (is "?lhs \<longleftrightarrow> ?eq \<or> ?rhs")
+proof (cases ?eq)
+  case False
+  moreover have "?lhs = ?rhs"
+  proof
+    assume L: ?lhs
+    show ?rhs
+    proof (clarsimp simp flip: path_connectedin_topspace)
+      fix i :: "'a"
+      assume "i \<in> I"
+      have cm: "continuous_map (product_topology X I) (X i) (\<lambda>f. f i)"
+        by (simp add: \<open>i \<in> I\<close> continuous_map_product_projection)
+      show "path_connectedin (X i) (topspace (X i))"
+        using path_connectedin_continuous_map_image [OF cm L [unfolded path_connectedin_topspace [symmetric]]]
+        by (metis \<open>i \<in> I\<close> False retraction_imp_surjective_map retraction_map_product_projection)
+    qed
+  next
+    assume R [rule_format]: ?rhs
+    show ?lhs
+      unfolding path_connected_space_def topspace_product_topology
+    proof clarify
+      fix x y
+      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))"
+      have "\<forall>i. \<exists>g. i \<in> I \<longrightarrow> pathin (X i) g \<and> g 0 = x i \<and> g 1 = y i"
+        using PiE_mem R path_connected_space_def x y by force
+      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"
+        by metis
+      with x y show "\<exists>g. pathin (product_topology X I) g \<and> g 0 = x \<and> g 1 = y"
+        apply (rule_tac x="\<lambda>a. \<lambda>i \<in> I. g i a" in exI)
+        apply (force simp: pathin_def continuous_map_componentwise)
+        done
+    qed
+  qed
+  ultimately show ?thesis
+    by simp
+qed (simp add: path_connected_space_topspace_empty)
+
+lemma path_connectedin_PiE:
+   "path_connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
+    PiE I S = {} \<or> (\<forall>i \<in> I. path_connectedin (X i) (S i))"
+  by (fastforce simp add: path_connectedin_def subtopology_PiE path_connected_space_product_topology subset_PiE PiE_eq_empty_iff topspace_subtopology_subset)
+
+
 end
diff -r ab8aad4aa76e -r 35ba13ac6e5c src/HOL/Analysis/Locally.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Locally.thy	Fri Mar 22 12:34:49 2019 +0000
@@ -0,0 +1,449 @@
+section \<open>Neigbourhood bases and Locally path-connected spaces\<close>
+
+theory Locally
+  imports
+    Path_Connected Function_Topology
+begin
+
+subsection\<open>Neigbourhood bases (useful for "local" properties of various kinds)\<close>
+
+definition neighbourhood_base_at where
+ "neighbourhood_base_at x P X \<equiv>
+        \<forall>W. openin X W \<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)"
+
+definition neighbourhood_base_of where
+ "neighbourhood_base_of P X \<equiv>
+        \<forall>x \<in> topspace X. neighbourhood_base_at x P X"
+
+lemma neighbourhood_base_of:
+   "neighbourhood_base_of P X \<longleftrightarrow>
+        (\<forall>W x. openin X W \<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))"
+  unfolding neighbourhood_base_at_def neighbourhood_base_of_def
+  using openin_subset by blast
+
+lemma neighbourhood_base_at_mono:
+   "\<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"
+  unfolding neighbourhood_base_at_def
+  by (meson subset_eq)
+
+lemma neighbourhood_base_of_mono:
+   "\<lbrakk>neighbourhood_base_of P X; \<And>S. P S \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> neighbourhood_base_of Q X"
+  unfolding neighbourhood_base_of_def
+  using neighbourhood_base_at_mono by force
+
+lemma open_neighbourhood_base_at:
+   "(\<And>S. \<lbrakk>P S; x \<in> S\<rbrakk> \<Longrightarrow> openin X S)
+        \<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))"
+  unfolding neighbourhood_base_at_def
+  by (meson subsetD)
+
+lemma open_neighbourhood_base_of:
+  "(\<forall>S. P S \<longrightarrow> openin X S)
+        \<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))"
+  apply (simp add: neighbourhood_base_of, safe, blast)
+  by meson
+
+lemma neighbourhood_base_of_open_subset:
+   "\<lbrakk>neighbourhood_base_of P X; openin X S\<rbrakk>
+        \<Longrightarrow> neighbourhood_base_of P (subtopology X S)"
+  apply (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt image_def)
+  apply (rename_tac x V)
+  apply (drule_tac x="S \<inter> V" in spec)
+  apply (simp add: Int_ac)
+  by (metis IntI le_infI1 openin_Int)
+
+lemma neighbourhood_base_of_topology_base:
+   "openin X = arbitrary union_of (\<lambda>W. W \<in> \<B>)
+        \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow>
+             (\<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))"
+  apply (auto simp: openin_topology_base_unique neighbourhood_base_of)
+  by (meson subset_trans)
+
+lemma neighbourhood_base_at_unlocalized:
+  assumes "\<And>S T. \<lbrakk>P S; openin X T; x \<in> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> P T"
+  shows "neighbourhood_base_at x P X
+     \<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))"
+         (is "?lhs = ?rhs")
+proof
+  assume R: ?rhs show ?lhs
+    unfolding neighbourhood_base_at_def
+  proof clarify
+    fix W
+    assume "openin X W" "x \<in> W"
+    then have "x \<in> topspace X"
+      using openin_subset by blast
+    with R obtain U V where "openin X U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> topspace X"
+      by blast
+    then show "\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
+      by (metis IntI \<open>openin X W\<close> \<open>x \<in> W\<close> assms inf_le1 inf_le2 openin_Int)
+  qed
+qed (simp add: neighbourhood_base_at_def)
+
+lemma neighbourhood_base_at_with_subset:
+   "\<lbrakk>openin X U; x \<in> U\<rbrakk>
+        \<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow> neighbourhood_base_at x (\<lambda>T. T \<subseteq> U \<and> P T) X)"
+  apply (simp add: neighbourhood_base_at_def)
+  apply (metis IntI Int_subset_iff openin_Int)
+  done
+
+lemma neighbourhood_base_of_with_subset:
+   "neighbourhood_base_of P X \<longleftrightarrow> neighbourhood_base_of (\<lambda>t. t \<subseteq> topspace X \<and> P t) X"
+  using neighbourhood_base_at_with_subset
+  by (fastforce simp add: neighbourhood_base_of_def)
+
+subsection\<open>Locally path-connected spaces\<close>
+
+definition weakly_locally_path_connected_at
+  where "weakly_locally_path_connected_at x X \<equiv> neighbourhood_base_at x (path_connectedin X) X"
+
+definition locally_path_connected_at
+  where "locally_path_connected_at x X \<equiv>
+    neighbourhood_base_at x (\<lambda>U. openin X U \<and> path_connectedin X U) X"
+
+definition locally_path_connected_space
+  where "locally_path_connected_space X \<equiv> neighbourhood_base_of (path_connectedin X) X"
+
+lemma locally_path_connected_space_alt:
+  "locally_path_connected_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> path_connectedin X U) X"
+  (is "?P = ?Q")
+  and locally_path_connected_space_eq_open_path_component_of:
+  "locally_path_connected_space X \<longleftrightarrow>
+        (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (Collect (path_component_of (subtopology X U) x)))"
+  (is "?P = ?R")
+proof -
+  have ?P if ?Q
+    using locally_path_connected_space_def neighbourhood_base_of_mono that by auto
+  moreover have ?R if P: ?P
+  proof -
+    show ?thesis
+    proof clarify
+      fix U y
+      assume "openin X U" "y \<in> U"
+      have "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> Collect (path_component_of (subtopology X U) y)"
+        if "path_component_of (subtopology X U) y x" for x
+
+      proof -
+        have "x \<in> U"
+          using path_component_of_equiv that topspace_subtopology by fastforce
+        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)"
+      using P
+      by (simp add: \<open>openin X U\<close> locally_path_connected_space_def neighbourhood_base_of)
+        then show ?thesis
+          by (metis dual_order.trans path_component_of_equiv path_component_of_maximal path_connectedin_subtopology subset_iff that)
+      qed
+      then show "openin X (Collect (path_component_of (subtopology X U) y))"
+        using openin_subopen by force
+    qed
+  qed
+  moreover have ?Q if ?R
+    using that
+    apply (simp add: open_neighbourhood_base_of)
+    by (metis mem_Collect_eq openin_subset path_component_of_refl path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset)
+  ultimately show "?P = ?Q" "?P = ?R"
+    by blast+
+qed
+
+lemma locally_path_connected_space:
+   "locally_path_connected_space X
+   \<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))"
+  by (simp add: locally_path_connected_space_alt open_neighbourhood_base_of)
+
+lemma locally_path_connected_space_open_path_components:
+   "locally_path_connected_space X \<longleftrightarrow>
+        (\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> openin X c)"
+  apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def topspace_subtopology)
+  by (metis imageI inf.absorb_iff2 openin_closedin_eq)
+
+lemma openin_path_component_of_locally_path_connected_space:
+   "locally_path_connected_space X \<Longrightarrow> openin X (Collect (path_component_of X x))"
+  apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
+  by (metis openin_empty openin_topspace path_component_of_eq_empty subtopology_topspace)
+
+lemma openin_path_components_of_locally_path_connected_space:
+   "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X c"
+  apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
+  by (metis (no_types, lifting) imageE openin_topspace path_components_of_def subtopology_topspace)
+
+lemma closedin_path_components_of_locally_path_connected_space:
+   "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X c"
+  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)
+
+lemma closedin_path_component_of_locally_path_connected_space:
+  assumes "locally_path_connected_space X"
+  shows "closedin X (Collect (path_component_of X x))"
+proof (cases "x \<in> topspace X")
+  case True
+  then show ?thesis
+    by (simp add: assms closedin_path_components_of_locally_path_connected_space path_component_in_path_components_of)
+next
+  case False
+  then show ?thesis
+    by (metis closedin_empty path_component_of_eq_empty)
+qed
+
+lemma weakly_locally_path_connected_at:
+   "weakly_locally_path_connected_at x X \<longleftrightarrow>
+    (\<forall>V. openin X V \<and> x \<in> V
+          \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and>
+                  (\<forall>y \<in> U. \<exists>C. path_connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))"
+         (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    apply (simp add: weakly_locally_path_connected_at_def neighbourhood_base_at_def)
+    by (meson order_trans subsetD)
+next
+  have *: "\<exists>V. path_connectedin X V \<and> U \<subseteq> V \<and> V \<subseteq> W"
+    if "(\<forall>y\<in>U. \<exists>C. path_connectedin X C \<and> C \<subseteq> W \<and> x \<in> C \<and> y \<in> C)"
+    for W U
+  proof (intro exI conjI)
+    let ?V = "(Collect (path_component_of (subtopology X W) x))"
+      show "path_connectedin X (Collect (path_component_of (subtopology X W) x))"
+        by (meson path_connectedin_path_component_of path_connectedin_subtopology)
+      show "U \<subseteq> ?V"
+        by (auto simp: path_component_of path_connectedin_subtopology that)
+      show "?V \<subseteq> W"
+        by (meson path_connectedin_path_component_of path_connectedin_subtopology)
+    qed
+  assume ?rhs
+  then show ?lhs
+    unfolding weakly_locally_path_connected_at_def neighbourhood_base_at_def by (metis "*")
+qed
+
+lemma locally_path_connected_space_im_kleinen:
+   "locally_path_connected_space X \<longleftrightarrow>
+      (\<forall>V x. openin X V \<and> x \<in> V
+             \<longrightarrow> (\<exists>U. openin X U \<and>
+                    x \<in> U \<and> U \<subseteq> V \<and>
+                    (\<forall>y \<in> U. \<exists>c. path_connectedin X c \<and>
+                                c \<subseteq> V \<and> x \<in> c \<and> y \<in> c)))"
+  apply (simp add: locally_path_connected_space_def neighbourhood_base_of_def)
+  apply (simp add: weakly_locally_path_connected_at flip: weakly_locally_path_connected_at_def)
+  using openin_subset apply force
+  done
+
+lemma locally_path_connected_space_open_subset:
+   "\<lbrakk>locally_path_connected_space X; openin X s\<rbrakk>
+        \<Longrightarrow> locally_path_connected_space (subtopology X s)"
+  apply (simp add: locally_path_connected_space_def neighbourhood_base_of openin_open_subtopology path_connectedin_subtopology)
+  by (meson order_trans)
+
+lemma locally_path_connected_space_quotient_map_image:
+  assumes f: "quotient_map X Y f" and X: "locally_path_connected_space X"
+  shows "locally_path_connected_space Y"
+  unfolding locally_path_connected_space_open_path_components
+proof clarify
+  fix V C
+  assume V: "openin Y V" and c: "C \<in> path_components_of (subtopology Y V)"
+  then have sub: "C \<subseteq> topspace Y"
+    using path_connectedin_path_components_of path_connectedin_subset_topspace path_connectedin_subtopology by blast
+  have "openin X {x \<in> topspace X. f x \<in> C}"
+  proof (subst openin_subopen, clarify)
+    fix x
+    assume x: "x \<in> topspace X" and "f x \<in> C"
+    let ?T = "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)"
+    show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}"
+    proof (intro exI conjI)
+      have "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)"
+      proof (intro exI conjI)
+        show "openin X ({z \<in> topspace X. f z \<in> V})"
+          using V f openin_subset quotient_map_def by fastforce
+        show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)
+        \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})"
+          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)
+      qed
+      with X show "openin X ?T"
+        using locally_path_connected_space_open_path_components by blast
+      show x: "x \<in> ?T"
+        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
+        by fastforce
+      have "f ` ?T \<subseteq> C"
+      proof (rule path_components_of_maximal)
+        show "C \<in> path_components_of (subtopology Y V)"
+          by (simp add: c)
+        show "path_connectedin (subtopology Y V) (f ` ?T)"
+        proof -
+          have "quotient_map (subtopology X {a \<in> topspace X. f a \<in> V}) (subtopology Y V) f"
+            by (simp add: V f quotient_map_restriction)
+          then show ?thesis
+            by (meson path_connectedin_continuous_map_image path_connectedin_path_component_of quotient_imp_continuous_map)
+        qed
+        show "\<not> disjnt C (f ` ?T)"
+          by (metis (no_types, lifting) \<open>f x \<in> C\<close> x disjnt_iff image_eqI)
+      qed
+      then show "?T \<subseteq> {x \<in> topspace X. f x \<in> C}"
+        by (force simp: path_component_of_equiv topspace_subtopology)
+    qed
+  qed
+  then show "openin Y C"
+    using f sub by (simp add: quotient_map_def)
+qed
+
+lemma homeomorphic_locally_path_connected_space:
+  assumes "X homeomorphic_space Y"
+  shows "locally_path_connected_space X \<longleftrightarrow> locally_path_connected_space Y"
+proof -
+  obtain f g where "homeomorphic_maps X Y f g"
+    using assms homeomorphic_space_def by fastforce
+  then show ?thesis
+    by (metis (no_types) homeomorphic_map_def homeomorphic_maps_map locally_path_connected_space_quotient_map_image)
+qed
+
+lemma locally_path_connected_space_retraction_map_image:
+   "\<lbrakk>retraction_map X Y r; locally_path_connected_space X\<rbrakk>
+        \<Longrightarrow> locally_path_connected_space Y"
+  using Abstract_Topology.retraction_imp_quotient_map locally_path_connected_space_quotient_map_image by blast
+
+lemma locally_path_connected_space_euclideanreal: "locally_path_connected_space euclideanreal"
+  unfolding locally_path_connected_space_def neighbourhood_base_of
+  proof clarsimp
+  fix W and x :: "real"
+  assume "open W" "x \<in> W"
+  then obtain e where "e > 0" and e: "\<And>x'. \<bar>x' - x\<bar> < e \<longrightarrow> x' \<in> W"
+    by (auto simp: open_real)
+  then show "\<exists>U. open U \<and> (\<exists>V. path_connected V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)"
+    by (force intro!: convex_imp_path_connected exI [where x = "{x-e<..<x+e}"])
+qed
+
+lemma locally_path_connected_space_discrete_topology:
+   "locally_path_connected_space (discrete_topology U)"
+  using locally_path_connected_space_open_path_components by fastforce
+
+lemma path_component_eq_connected_component_of:
+  assumes "locally_path_connected_space X"
+  shows "(path_component_of_set X x = connected_component_of_set X x)"
+proof (cases "x \<in> topspace X")
+  case True
+  then show ?thesis
+    using connectedin_connected_component_of [of X x]
+    apply (clarsimp simp add: connectedin_def connected_space_clopen_in topspace_subtopology_subset cong: conj_cong)
+    apply (drule_tac x="path_component_of_set X x" in spec)
+    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)
+next
+  case False
+  then show ?thesis
+    using connected_component_of_eq_empty path_component_of_eq_empty by fastforce
+qed
+
+lemma path_components_eq_connected_components_of:
+   "locally_path_connected_space X \<Longrightarrow> (path_components_of X = connected_components_of X)"
+  by (simp add: path_components_of_def connected_components_of_def image_def path_component_eq_connected_component_of)
+
+lemma path_connected_eq_connected_space:
+   "locally_path_connected_space X
+         \<Longrightarrow> path_connected_space X \<longleftrightarrow> connected_space X"
+  by (metis connected_components_of_subset_sing path_components_eq_connected_components_of path_components_of_subset_singleton)
+
+lemma locally_path_connected_space_product_topology:
+   "locally_path_connected_space(product_topology X I) \<longleftrightarrow>
+        topspace(product_topology X I) = {} \<or>
+        finite {i. i \<in> I \<and> ~path_connected_space(X i)} \<and>
+        (\<forall>i \<in> I. locally_path_connected_space(X i))"
+    (is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs")
+proof (cases ?empty)
+  case True
+  then show ?thesis
+    by (simp add: locally_path_connected_space_def neighbourhood_base_of openin_closedin_eq)
+next
+  case False
+  then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+    by auto
+  have ?rhs if L: ?lhs
+  proof -
+    obtain U C where U: "openin (product_topology X I) U"
+      and V: "path_connectedin (product_topology X I) C"
+      and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+      using L apply (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
+      by (metis openin_topspace topspace_product_topology z)
+    then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}"
+      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"
+      by (force simp: openin_product_topology_alt)
+    show ?thesis
+    proof (intro conjI ballI)
+      have "path_connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
+      proof -
+        have pc: "path_connectedin (X i) ((\<lambda>x. x i) ` C)"
+          apply (rule path_connectedin_continuous_map_image [OF _ V])
+          by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
+        moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
+        proof
+          show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
+            by (simp add: pc path_connectedin_subset_topspace)
+          have "V i \<subseteq> (\<lambda>x. x i) ` (\<Pi>\<^sub>E i\<in>I. V i)"
+            by (metis \<open>z \<in> Pi\<^sub>E I V\<close> empty_iff image_projection_PiE order_refl that(1))
+          also have "\<dots> \<subseteq> (\<lambda>x. x i) ` U"
+            using subU by blast
+          finally show "topspace (X i) \<subseteq> (\<lambda>x. x i) ` C"
+            using \<open>U \<subseteq> C\<close> that by blast
+        qed
+        ultimately show ?thesis
+          by (simp add: path_connectedin_topspace)
+      qed
+      then have "{i \<in> I. \<not> path_connected_space (X i)} \<subseteq> {i \<in> I. V i \<noteq> topspace (X i)}"
+        by blast
+      with finV show "finite {i \<in> I. \<not> path_connected_space (X i)}"
+        using finite_subset by blast
+    next
+      show "locally_path_connected_space (X i)" if "i \<in> I" for i
+        apply (rule locally_path_connected_space_quotient_map_image [OF _ L, where f = "\<lambda>x. x i"])
+        by (metis False Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection that)
+    qed
+  qed
+  moreover have ?lhs if R: ?rhs
+  proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
+    fix F z
+    assume "openin (product_topology X I) F" and "z \<in> F"
+    then obtain W where finW: "finite {i \<in> I. W i \<noteq> topspace (X i)}"
+            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"
+      by (auto simp: openin_product_topology_alt)
+    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>
+                        (W i = topspace (X i) \<and>
+                         path_connected_space (X i) \<longrightarrow> U = topspace (X i) \<and> C = topspace (X i))"
+          (is "\<forall>i \<in> I. ?\<Phi> i")
+    proof
+      fix i assume "i \<in> I"
+      have "locally_path_connected_space (X i)"
+        by (simp add: R \<open>i \<in> I\<close>)
+      moreover have "openin (X i) (W i) " "z i \<in> W i"
+        using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
+      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"
+        using \<open>i \<in> I\<close> by (force simp: locally_path_connected_space_def neighbourhood_base_of)
+      show "?\<Phi> i"
+      proof (cases "W i = topspace (X i) \<and> path_connected_space(X i)")
+        case True
+        then show ?thesis
+          using \<open>z i \<in> W i\<close> path_connectedin_topspace by blast
+      next
+        case False
+        then show ?thesis
+          by (meson UC)
+      qed
+    qed
+    then obtain U C where
+      *: "\<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>
+                        (W i = topspace (X i) \<and> path_connected_space (X i)
+                         \<longrightarrow> (U i) = topspace (X i) \<and> (C i) = topspace (X i))"
+      by metis
+    let ?A = "{i \<in> I. \<not> path_connected_space (X i)} \<union> {i \<in> I. W i \<noteq> topspace (X i)}"
+    have "{i \<in> I. U i \<noteq> topspace (X i)} \<subseteq> ?A"
+      by (clarsimp simp add: "*")
+    moreover have "finite ?A"
+      by (simp add: that finW)
+    ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}"
+      using finite_subset by auto
+    then have "openin (product_topology X I) (Pi\<^sub>E I U)"
+      using * by (simp add: openin_PiE_gen)
+    then show "\<exists>U. openin (product_topology X I) U \<and>
+            (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
+      apply (rule_tac x="PiE I U" in exI, simp)
+      apply (rule_tac x="PiE I C" in exI)
+      using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
+      apply (simp add: path_connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
+      done
+  qed
+  ultimately show ?thesis
+    using False by blast
+qed
+
+end
diff -r ab8aad4aa76e -r 35ba13ac6e5c src/HOL/Analysis/Product_Topology.thy
--- a/src/HOL/Analysis/Product_Topology.thy	Thu Mar 21 19:46:26 2019 +0100
+++ b/src/HOL/Analysis/Product_Topology.thy	Fri Mar 22 12:34:49 2019 +0000
@@ -1,7 +1,7 @@
 section\<open>The binary product topology\<close>
 
 theory Product_Topology
-imports Function_Topology   
+imports Function_Topology Abstract_Limits
 begin
 
 section \<open>Product Topology\<close> 
@@ -519,5 +519,49 @@
   then show ?thesis by metis
 qed
 
+lemma limitin_pairwise:
+   "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"
+    (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  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"
+                        and a: "a \<in> topspace X" and b: "b \<in> topspace Y" and l: "l = (a,b)"
+    by (auto simp: limitin_def)
+  moreover have "\<forall>\<^sub>F x in F. fst (f x) \<in> U" if "openin X U" "a \<in> U" for U
+  proof -
+    have "\<forall>\<^sub>F c in F. f c \<in> U \<times> topspace Y"
+      using b that ev [of "U \<times> topspace Y"] by (auto simp: openin_prod_topology_alt)
+    then show ?thesis
+      by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
+  qed
+  moreover have "\<forall>\<^sub>F x in F. snd (f x) \<in> U" if "openin Y U" "b \<in> U" for U
+  proof -
+    have "\<forall>\<^sub>F c in F. f c \<in> topspace X \<times> U"
+      using a that ev [of "topspace X \<times> U"] by (auto simp: openin_prod_topology_alt)
+    then show ?thesis
+      by (rule eventually_mono) (metis (mono_tags, lifting) SigmaE2 prod.collapse)
+  qed
+  ultimately show ?rhs
+    by (simp add: limitin_def)
+next
+  have "limitin (prod_topology X Y) f (a,b) F"
+    if "limitin X (fst \<circ> f) a F" "limitin Y (snd \<circ> f) b F" for a b
+    using that
+  proof (clarsimp simp: limitin_def)
+    fix Z :: "('a \<times> 'b) set"
+    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)"
+      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)"
+      and Z: "openin (prod_topology X Y) Z" "(a, b) \<in> Z"
+    then obtain U V where "openin X U" "openin Y V" "a \<in> U" "b \<in> V" "U \<times> V \<subseteq> Z"
+      using Z by (force simp: openin_prod_topology_alt)
+    then have "\<forall>\<^sub>F x in F. fst (f x) \<in> U" "\<forall>\<^sub>F x in F. snd (f x) \<in> V"
+      by (simp_all add: a b)
+    then show "\<forall>\<^sub>F x in F. f x \<in> Z"
+      by (rule eventually_elim2) (use \<open>U \<times> V \<subseteq> Z\<close> subsetD in auto)
+  qed
+  then show "?rhs \<Longrightarrow> ?lhs"
+    by (metis prod.collapse)
+qed
+
 end