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