author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 69945 35ba13ac6e5c
permissions -rw-r--r--
more strict AFP properties;
     1 section \<open>Neigbourhood bases and Locally path-connected spaces\<close>
     3 theory Locally
     4   imports
     5     Path_Connected Function_Topology
     6 begin
     8 subsection\<open>Neigbourhood bases (useful for "local" properties of various kinds)\<close>
    10 definition neighbourhood_base_at where
    11  "neighbourhood_base_at x P X \<equiv>
    12         \<forall>W. openin X W \<and> x \<in> W
    13             \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)"
    15 definition neighbourhood_base_of where
    16  "neighbourhood_base_of P X \<equiv>
    17         \<forall>x \<in> topspace X. neighbourhood_base_at x P X"
    19 lemma neighbourhood_base_of:
    20    "neighbourhood_base_of P X \<longleftrightarrow>
    21         (\<forall>W x. openin X W \<and> x \<in> W
    22           \<longrightarrow> (\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W))"
    23   unfolding neighbourhood_base_at_def neighbourhood_base_of_def
    24   using openin_subset by blast
    26 lemma neighbourhood_base_at_mono:
    27    "\<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"
    28   unfolding neighbourhood_base_at_def
    29   by (meson subset_eq)
    31 lemma neighbourhood_base_of_mono:
    32    "\<lbrakk>neighbourhood_base_of P X; \<And>S. P S \<Longrightarrow> Q S\<rbrakk> \<Longrightarrow> neighbourhood_base_of Q X"
    33   unfolding neighbourhood_base_of_def
    34   using neighbourhood_base_at_mono by force
    36 lemma open_neighbourhood_base_at:
    37    "(\<And>S. \<lbrakk>P S; x \<in> S\<rbrakk> \<Longrightarrow> openin X S)
    38         \<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))"
    39   unfolding neighbourhood_base_at_def
    40   by (meson subsetD)
    42 lemma open_neighbourhood_base_of:
    43   "(\<forall>S. P S \<longrightarrow> openin X S)
    44         \<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))"
    45   apply (simp add: neighbourhood_base_of, safe, blast)
    46   by meson
    48 lemma neighbourhood_base_of_open_subset:
    49    "\<lbrakk>neighbourhood_base_of P X; openin X S\<rbrakk>
    50         \<Longrightarrow> neighbourhood_base_of P (subtopology X S)"
    51   apply (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt image_def)
    52   apply (rename_tac x V)
    53   apply (drule_tac x="S \<inter> V" in spec)
    54   apply (simp add: Int_ac)
    55   by (metis IntI le_infI1 openin_Int)
    57 lemma neighbourhood_base_of_topology_base:
    58    "openin X = arbitrary union_of (\<lambda>W. W \<in> \<B>)
    59         \<Longrightarrow> neighbourhood_base_of P X \<longleftrightarrow>
    60              (\<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))"
    61   apply (auto simp: openin_topology_base_unique neighbourhood_base_of)
    62   by (meson subset_trans)
    64 lemma neighbourhood_base_at_unlocalized:
    65   assumes "\<And>S T. \<lbrakk>P S; openin X T; x \<in> T; T \<subseteq> S\<rbrakk> \<Longrightarrow> P T"
    66   shows "neighbourhood_base_at x P X
    67      \<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))"
    68          (is "?lhs = ?rhs")
    69 proof
    70   assume R: ?rhs show ?lhs
    71     unfolding neighbourhood_base_at_def
    72   proof clarify
    73     fix W
    74     assume "openin X W" "x \<in> W"
    75     then have "x \<in> topspace X"
    76       using openin_subset by blast
    77     with R obtain U V where "openin X U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> topspace X"
    78       by blast
    79     then show "\<exists>U V. openin X U \<and> P V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W"
    80       by (metis IntI \<open>openin X W\<close> \<open>x \<in> W\<close> assms inf_le1 inf_le2 openin_Int)
    81   qed
    82 qed (simp add: neighbourhood_base_at_def)
    84 lemma neighbourhood_base_at_with_subset:
    85    "\<lbrakk>openin X U; x \<in> U\<rbrakk>
    86         \<Longrightarrow> (neighbourhood_base_at x P X \<longleftrightarrow> neighbourhood_base_at x (\<lambda>T. T \<subseteq> U \<and> P T) X)"
    87   apply (simp add: neighbourhood_base_at_def)
    88   apply (metis IntI Int_subset_iff openin_Int)
    89   done
    91 lemma neighbourhood_base_of_with_subset:
    92    "neighbourhood_base_of P X \<longleftrightarrow> neighbourhood_base_of (\<lambda>t. t \<subseteq> topspace X \<and> P t) X"
    93   using neighbourhood_base_at_with_subset
    94   by (fastforce simp add: neighbourhood_base_of_def)
    96 subsection\<open>Locally path-connected spaces\<close>
    98 definition weakly_locally_path_connected_at
    99   where "weakly_locally_path_connected_at x X \<equiv> neighbourhood_base_at x (path_connectedin X) X"
   101 definition locally_path_connected_at
   102   where "locally_path_connected_at x X \<equiv>
   103     neighbourhood_base_at x (\<lambda>U. openin X U \<and> path_connectedin X U) X"
   105 definition locally_path_connected_space
   106   where "locally_path_connected_space X \<equiv> neighbourhood_base_of (path_connectedin X) X"
   108 lemma locally_path_connected_space_alt:
   109   "locally_path_connected_space X \<longleftrightarrow> neighbourhood_base_of (\<lambda>U. openin X U \<and> path_connectedin X U) X"
   110   (is "?P = ?Q")
   111   and locally_path_connected_space_eq_open_path_component_of:
   112   "locally_path_connected_space X \<longleftrightarrow>
   113         (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (Collect (path_component_of (subtopology X U) x)))"
   114   (is "?P = ?R")
   115 proof -
   116   have ?P if ?Q
   117     using locally_path_connected_space_def neighbourhood_base_of_mono that by auto
   118   moreover have ?R if P: ?P
   119   proof -
   120     show ?thesis
   121     proof clarify
   122       fix U y
   123       assume "openin X U" "y \<in> U"
   124       have "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> Collect (path_component_of (subtopology X U) y)"
   125         if "path_component_of (subtopology X U) y x" for x
   127       proof -
   128         have "x \<in> U"
   129           using path_component_of_equiv that topspace_subtopology by fastforce
   130         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)"
   131       using P
   132       by (simp add: \<open>openin X U\<close> locally_path_connected_space_def neighbourhood_base_of)
   133         then show ?thesis
   134           by (metis dual_order.trans path_component_of_equiv path_component_of_maximal path_connectedin_subtopology subset_iff that)
   135       qed
   136       then show "openin X (Collect (path_component_of (subtopology X U) y))"
   137         using openin_subopen by force
   138     qed
   139   qed
   140   moreover have ?Q if ?R
   141     using that
   142     apply (simp add: open_neighbourhood_base_of)
   143     by (metis mem_Collect_eq openin_subset path_component_of_refl path_connectedin_path_component_of path_connectedin_subtopology that topspace_subtopology_subset)
   144   ultimately show "?P = ?Q" "?P = ?R"
   145     by blast+
   146 qed
   148 lemma locally_path_connected_space:
   149    "locally_path_connected_space X
   150    \<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))"
   151   by (simp add: locally_path_connected_space_alt open_neighbourhood_base_of)
   153 lemma locally_path_connected_space_open_path_components:
   154    "locally_path_connected_space X \<longleftrightarrow>
   155         (\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> openin X c)"
   156   apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def topspace_subtopology)
   157   by (metis imageI inf.absorb_iff2 openin_closedin_eq)
   159 lemma openin_path_component_of_locally_path_connected_space:
   160    "locally_path_connected_space X \<Longrightarrow> openin X (Collect (path_component_of X x))"
   161   apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
   162   by (metis openin_empty openin_topspace path_component_of_eq_empty subtopology_topspace)
   164 lemma openin_path_components_of_locally_path_connected_space:
   165    "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> openin X c"
   166   apply (auto simp: locally_path_connected_space_eq_open_path_component_of)
   167   by (metis (no_types, lifting) imageE openin_topspace path_components_of_def subtopology_topspace)
   169 lemma closedin_path_components_of_locally_path_connected_space:
   170    "\<lbrakk>locally_path_connected_space X; c \<in> path_components_of X\<rbrakk> \<Longrightarrow> closedin X c"
   171   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)
   173 lemma closedin_path_component_of_locally_path_connected_space:
   174   assumes "locally_path_connected_space X"
   175   shows "closedin X (Collect (path_component_of X x))"
   176 proof (cases "x \<in> topspace X")
   177   case True
   178   then show ?thesis
   179     by (simp add: assms closedin_path_components_of_locally_path_connected_space path_component_in_path_components_of)
   180 next
   181   case False
   182   then show ?thesis
   183     by (metis closedin_empty path_component_of_eq_empty)
   184 qed
   186 lemma weakly_locally_path_connected_at:
   187    "weakly_locally_path_connected_at x X \<longleftrightarrow>
   188     (\<forall>V. openin X V \<and> x \<in> V
   189           \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> U \<subseteq> V \<and>
   190                   (\<forall>y \<in> U. \<exists>C. path_connectedin X C \<and> C \<subseteq> V \<and> x \<in> C \<and> y \<in> C)))"
   191          (is "?lhs = ?rhs")
   192 proof
   193   assume ?lhs then show ?rhs
   194     apply (simp add: weakly_locally_path_connected_at_def neighbourhood_base_at_def)
   195     by (meson order_trans subsetD)
   196 next
   197   have *: "\<exists>V. path_connectedin X V \<and> U \<subseteq> V \<and> V \<subseteq> W"
   198     if "(\<forall>y\<in>U. \<exists>C. path_connectedin X C \<and> C \<subseteq> W \<and> x \<in> C \<and> y \<in> C)"
   199     for W U
   200   proof (intro exI conjI)
   201     let ?V = "(Collect (path_component_of (subtopology X W) x))"
   202       show "path_connectedin X (Collect (path_component_of (subtopology X W) x))"
   203         by (meson path_connectedin_path_component_of path_connectedin_subtopology)
   204       show "U \<subseteq> ?V"
   205         by (auto simp: path_component_of path_connectedin_subtopology that)
   206       show "?V \<subseteq> W"
   207         by (meson path_connectedin_path_component_of path_connectedin_subtopology)
   208     qed
   209   assume ?rhs
   210   then show ?lhs
   211     unfolding weakly_locally_path_connected_at_def neighbourhood_base_at_def by (metis "*")
   212 qed
   214 lemma locally_path_connected_space_im_kleinen:
   215    "locally_path_connected_space X \<longleftrightarrow>
   216       (\<forall>V x. openin X V \<and> x \<in> V
   217              \<longrightarrow> (\<exists>U. openin X U \<and>
   218                     x \<in> U \<and> U \<subseteq> V \<and>
   219                     (\<forall>y \<in> U. \<exists>c. path_connectedin X c \<and>
   220                                 c \<subseteq> V \<and> x \<in> c \<and> y \<in> c)))"
   221   apply (simp add: locally_path_connected_space_def neighbourhood_base_of_def)
   222   apply (simp add: weakly_locally_path_connected_at flip: weakly_locally_path_connected_at_def)
   223   using openin_subset apply force
   224   done
   226 lemma locally_path_connected_space_open_subset:
   227    "\<lbrakk>locally_path_connected_space X; openin X s\<rbrakk>
   228         \<Longrightarrow> locally_path_connected_space (subtopology X s)"
   229   apply (simp add: locally_path_connected_space_def neighbourhood_base_of openin_open_subtopology path_connectedin_subtopology)
   230   by (meson order_trans)
   232 lemma locally_path_connected_space_quotient_map_image:
   233   assumes f: "quotient_map X Y f" and X: "locally_path_connected_space X"
   234   shows "locally_path_connected_space Y"
   235   unfolding locally_path_connected_space_open_path_components
   236 proof clarify
   237   fix V C
   238   assume V: "openin Y V" and c: "C \<in> path_components_of (subtopology Y V)"
   239   then have sub: "C \<subseteq> topspace Y"
   240     using path_connectedin_path_components_of path_connectedin_subset_topspace path_connectedin_subtopology by blast
   241   have "openin X {x \<in> topspace X. f x \<in> C}"
   242   proof (subst openin_subopen, clarify)
   243     fix x
   244     assume x: "x \<in> topspace X" and "f x \<in> C"
   245     let ?T = "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)"
   246     show "\<exists>T. openin X T \<and> x \<in> T \<and> T \<subseteq> {x \<in> topspace X. f x \<in> C}"
   247     proof (intro exI conjI)
   248       have "\<exists>U. openin X U \<and> ?T \<in> path_components_of (subtopology X U)"
   249       proof (intro exI conjI)
   250         show "openin X ({z \<in> topspace X. f z \<in> V})"
   251           using V f openin_subset quotient_map_def by fastforce
   252         show "Collect (path_component_of (subtopology X {z \<in> topspace X. f z \<in> V}) x)
   253         \<in> path_components_of (subtopology X {z \<in> topspace X. f z \<in> V})"
   254           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)
   255       qed
   256       with X show "openin X ?T"
   257         using locally_path_connected_space_open_path_components by blast
   258       show x: "x \<in> ?T"
   259         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
   260         by fastforce
   261       have "f ` ?T \<subseteq> C"
   262       proof (rule path_components_of_maximal)
   263         show "C \<in> path_components_of (subtopology Y V)"
   264           by (simp add: c)
   265         show "path_connectedin (subtopology Y V) (f ` ?T)"
   266         proof -
   267           have "quotient_map (subtopology X {a \<in> topspace X. f a \<in> V}) (subtopology Y V) f"
   268             by (simp add: V f quotient_map_restriction)
   269           then show ?thesis
   270             by (meson path_connectedin_continuous_map_image path_connectedin_path_component_of quotient_imp_continuous_map)
   271         qed
   272         show "\<not> disjnt C (f ` ?T)"
   273           by (metis (no_types, lifting) \<open>f x \<in> C\<close> x disjnt_iff image_eqI)
   274       qed
   275       then show "?T \<subseteq> {x \<in> topspace X. f x \<in> C}"
   276         by (force simp: path_component_of_equiv topspace_subtopology)
   277     qed
   278   qed
   279   then show "openin Y C"
   280     using f sub by (simp add: quotient_map_def)
   281 qed
   283 lemma homeomorphic_locally_path_connected_space:
   284   assumes "X homeomorphic_space Y"
   285   shows "locally_path_connected_space X \<longleftrightarrow> locally_path_connected_space Y"
   286 proof -
   287   obtain f g where "homeomorphic_maps X Y f g"
   288     using assms homeomorphic_space_def by fastforce
   289   then show ?thesis
   290     by (metis (no_types) homeomorphic_map_def homeomorphic_maps_map locally_path_connected_space_quotient_map_image)
   291 qed
   293 lemma locally_path_connected_space_retraction_map_image:
   294    "\<lbrakk>retraction_map X Y r; locally_path_connected_space X\<rbrakk>
   295         \<Longrightarrow> locally_path_connected_space Y"
   296   using Abstract_Topology.retraction_imp_quotient_map locally_path_connected_space_quotient_map_image by blast
   298 lemma locally_path_connected_space_euclideanreal: "locally_path_connected_space euclideanreal"
   299   unfolding locally_path_connected_space_def neighbourhood_base_of
   300   proof clarsimp
   301   fix W and x :: "real"
   302   assume "open W" "x \<in> W"
   303   then obtain e where "e > 0" and e: "\<And>x'. \<bar>x' - x\<bar> < e \<longrightarrow> x' \<in> W"
   304     by (auto simp: open_real)
   305   then show "\<exists>U. open U \<and> (\<exists>V. path_connected V \<and> x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> W)"
   306     by (force intro!: convex_imp_path_connected exI [where x = "{x-e<..<x+e}"])
   307 qed
   309 lemma locally_path_connected_space_discrete_topology:
   310    "locally_path_connected_space (discrete_topology U)"
   311   using locally_path_connected_space_open_path_components by fastforce
   313 lemma path_component_eq_connected_component_of:
   314   assumes "locally_path_connected_space X"
   315   shows "(path_component_of_set X x = connected_component_of_set X x)"
   316 proof (cases "x \<in> topspace X")
   317   case True
   318   then show ?thesis
   319     using connectedin_connected_component_of [of X x]
   320     apply (clarsimp simp add: connectedin_def connected_space_clopen_in topspace_subtopology_subset cong: conj_cong)
   321     apply (drule_tac x="path_component_of_set X x" in spec)
   322     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)
   323 next
   324   case False
   325   then show ?thesis
   326     using connected_component_of_eq_empty path_component_of_eq_empty by fastforce
   327 qed
   329 lemma path_components_eq_connected_components_of:
   330    "locally_path_connected_space X \<Longrightarrow> (path_components_of X = connected_components_of X)"
   331   by (simp add: path_components_of_def connected_components_of_def image_def path_component_eq_connected_component_of)
   333 lemma path_connected_eq_connected_space:
   334    "locally_path_connected_space X
   335          \<Longrightarrow> path_connected_space X \<longleftrightarrow> connected_space X"
   336   by (metis connected_components_of_subset_sing path_components_eq_connected_components_of path_components_of_subset_singleton)
   338 lemma locally_path_connected_space_product_topology:
   339    "locally_path_connected_space(product_topology X I) \<longleftrightarrow>
   340         topspace(product_topology X I) = {} \<or>
   341         finite {i. i \<in> I \<and> ~path_connected_space(X i)} \<and>
   342         (\<forall>i \<in> I. locally_path_connected_space(X i))"
   343     (is "?lhs \<longleftrightarrow> ?empty \<or> ?rhs")
   344 proof (cases ?empty)
   345   case True
   346   then show ?thesis
   347     by (simp add: locally_path_connected_space_def neighbourhood_base_of openin_closedin_eq)
   348 next
   349   case False
   350   then obtain z where z: "z \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
   351     by auto
   352   have ?rhs if L: ?lhs
   353   proof -
   354     obtain U C where U: "openin (product_topology X I) U"
   355       and V: "path_connectedin (product_topology X I) C"
   356       and "z \<in> U" "U \<subseteq> C" and Csub: "C \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
   357       using L apply (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
   358       by (metis openin_topspace topspace_product_topology z)
   359     then obtain V where finV: "finite {i \<in> I. V i \<noteq> topspace (X i)}"
   360       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"
   361       by (force simp: openin_product_topology_alt)
   362     show ?thesis
   363     proof (intro conjI ballI)
   364       have "path_connected_space (X i)" if "i \<in> I" "V i = topspace (X i)" for i
   365       proof -
   366         have pc: "path_connectedin (X i) ((\<lambda>x. x i) ` C)"
   367           apply (rule path_connectedin_continuous_map_image [OF _ V])
   368           by (simp add: continuous_map_product_projection \<open>i \<in> I\<close>)
   369         moreover have "((\<lambda>x. x i) ` C) = topspace (X i)"
   370         proof
   371           show "(\<lambda>x. x i) ` C \<subseteq> topspace (X i)"
   372             by (simp add: pc path_connectedin_subset_topspace)
   373           have "V i \<subseteq> (\<lambda>x. x i) ` (\<Pi>\<^sub>E i\<in>I. V i)"
   374             by (metis \<open>z \<in> Pi\<^sub>E I V\<close> empty_iff image_projection_PiE order_refl that(1))
   375           also have "\<dots> \<subseteq> (\<lambda>x. x i) ` U"
   376             using subU by blast
   377           finally show "topspace (X i) \<subseteq> (\<lambda>x. x i) ` C"
   378             using \<open>U \<subseteq> C\<close> that by blast
   379         qed
   380         ultimately show ?thesis
   381           by (simp add: path_connectedin_topspace)
   382       qed
   383       then have "{i \<in> I. \<not> path_connected_space (X i)} \<subseteq> {i \<in> I. V i \<noteq> topspace (X i)}"
   384         by blast
   385       with finV show "finite {i \<in> I. \<not> path_connected_space (X i)}"
   386         using finite_subset by blast
   387     next
   388       show "locally_path_connected_space (X i)" if "i \<in> I" for i
   389         apply (rule locally_path_connected_space_quotient_map_image [OF _ L, where f = "\<lambda>x. x i"])
   390         by (metis False Abstract_Topology.retraction_imp_quotient_map retraction_map_product_projection that)
   391     qed
   392   qed
   393   moreover have ?lhs if R: ?rhs
   394   proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of)
   395     fix F z
   396     assume "openin (product_topology X I) F" and "z \<in> F"
   397     then obtain W where finW: "finite {i \<in> I. W i \<noteq> topspace (X i)}"
   398             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"
   399       by (auto simp: openin_product_topology_alt)
   400     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>
   401                         (W i = topspace (X i) \<and>
   402                          path_connected_space (X i) \<longrightarrow> U = topspace (X i) \<and> C = topspace (X i))"
   403           (is "\<forall>i \<in> I. ?\<Phi> i")
   404     proof
   405       fix i assume "i \<in> I"
   406       have "locally_path_connected_space (X i)"
   407         by (simp add: R \<open>i \<in> I\<close>)
   408       moreover have "openin (X i) (W i) " "z i \<in> W i"
   409         using \<open>z \<in> Pi\<^sub>E I W\<close> opeW \<open>i \<in> I\<close> by auto
   410       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"
   411         using \<open>i \<in> I\<close> by (force simp: locally_path_connected_space_def neighbourhood_base_of)
   412       show "?\<Phi> i"
   413       proof (cases "W i = topspace (X i) \<and> path_connected_space(X i)")
   414         case True
   415         then show ?thesis
   416           using \<open>z i \<in> W i\<close> path_connectedin_topspace by blast
   417       next
   418         case False
   419         then show ?thesis
   420           by (meson UC)
   421       qed
   422     qed
   423     then obtain U C where
   424       *: "\<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>
   425                         (W i = topspace (X i) \<and> path_connected_space (X i)
   426                          \<longrightarrow> (U i) = topspace (X i) \<and> (C i) = topspace (X i))"
   427       by metis
   428     let ?A = "{i \<in> I. \<not> path_connected_space (X i)} \<union> {i \<in> I. W i \<noteq> topspace (X i)}"
   429     have "{i \<in> I. U i \<noteq> topspace (X i)} \<subseteq> ?A"
   430       by (clarsimp simp add: "*")
   431     moreover have "finite ?A"
   432       by (simp add: that finW)
   433     ultimately have "finite {i \<in> I. U i \<noteq> topspace (X i)}"
   434       using finite_subset by auto
   435     then have "openin (product_topology X I) (Pi\<^sub>E I U)"
   436       using * by (simp add: openin_PiE_gen)
   437     then show "\<exists>U. openin (product_topology X I) U \<and>
   438             (\<exists>V. path_connectedin (product_topology X I) V \<and> z \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> F)"
   439       apply (rule_tac x="PiE I U" in exI, simp)
   440       apply (rule_tac x="PiE I C" in exI)
   441       using \<open>z \<in> Pi\<^sub>E I W\<close> \<open>Pi\<^sub>E I W \<subseteq> F\<close> *
   442       apply (simp add: path_connectedin_PiE subset_PiE PiE_iff PiE_mono dual_order.trans)
   443       done
   444   qed
   445   ultimately show ?thesis
   446     using False by blast
   447 qed
   449 end