Theory Locally

section ‹Neighbourhood bases and Locally path-connected spaces›

theory Locally
  imports
    Path_Connected Function_Topology
begin

subsection‹Neighbourhood Bases›

text ‹Useful for "local" properties of various kinds›

definition neighbourhood_base_at where
 "neighbourhood_base_at x P X ≡
        ∀W. openin X W ∧ x ∈ W
            ⟶ (∃U V. openin X U ∧ P V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ W)"

definition neighbourhood_base_of where
 "neighbourhood_base_of P X ≡
        ∀x ∈ topspace X. neighbourhood_base_at x P X"

lemma neighbourhood_base_of:
   "neighbourhood_base_of P X ⟷
        (∀W x. openin X W ∧ x ∈ W
          ⟶ (∃U V. openin X U ∧ P V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ W))"
  unfolding neighbourhood_base_at_def neighbourhood_base_of_def
  using openin_subset by blast

lemma neighbourhood_base_at_mono:
   "⟦neighbourhood_base_at x P X; ⋀S. ⟦P S; x ∈ S⟧ ⟹ Q S⟧ ⟹ neighbourhood_base_at x Q X"
  unfolding neighbourhood_base_at_def
  by (meson subset_eq)

lemma neighbourhood_base_of_mono:
   "⟦neighbourhood_base_of P X; ⋀S. P S ⟹ Q S⟧ ⟹ neighbourhood_base_of Q X"
  unfolding neighbourhood_base_of_def
  using neighbourhood_base_at_mono by force

lemma open_neighbourhood_base_at:
   "(⋀S. ⟦P S; x ∈ S⟧ ⟹ openin X S)
        ⟹ neighbourhood_base_at x P X ⟷ (∀W. openin X W ∧ x ∈ W ⟶ (∃U. P U ∧ x ∈ U ∧ U ⊆ W))"
  unfolding neighbourhood_base_at_def
  by (meson subsetD)

lemma open_neighbourhood_base_of:
  "(∀S. P S ⟶ openin X S)
        ⟹ neighbourhood_base_of P X ⟷ (∀W x. openin X W ∧ x ∈ W ⟶ (∃U. P U ∧ x ∈ U ∧ U ⊆ W))"
  apply (simp add: neighbourhood_base_of, safe, blast)
  by meson

lemma neighbourhood_base_of_open_subset:
   "⟦neighbourhood_base_of P X; openin X S⟧
        ⟹ 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 ∩ 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 (λW. W ∈ ℬ)
        ⟹ neighbourhood_base_of P X ⟷
             (∀W x. W ∈ ℬ ∧ x ∈ W  ⟶ (∃U V. openin X U ∧ P V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ W))"
  apply (auto simp: openin_topology_base_unique neighbourhood_base_of)
  by (meson subset_trans)

lemma neighbourhood_base_at_unlocalized:
  assumes "⋀S T. ⟦P S; openin X T; x ∈ T; T ⊆ S⟧ ⟹ P T"
  shows "neighbourhood_base_at x P X
     ⟷ (x ∈ topspace X ⟶ (∃U V. openin X U ∧ P V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ 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 ∈ W"
    then have "x ∈ topspace X"
      using openin_subset by blast
    with R obtain U V where "openin X U" "P V" "x ∈ U" "U ⊆ V" "V ⊆ topspace X"
      by blast
    then show "∃U V. openin X U ∧ P V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ W"
      by (metis IntI ‹openin X W› ‹x ∈ W› assms inf_le1 inf_le2 openin_Int)
  qed
qed (simp add: neighbourhood_base_at_def)

lemma neighbourhood_base_at_with_subset:
   "⟦openin X U; x ∈ U⟧
        ⟹ (neighbourhood_base_at x P X ⟷ neighbourhood_base_at x (λT. T ⊆ U ∧ 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 ⟷ neighbourhood_base_of (λt. t ⊆ topspace X ∧ P t) X"
  using neighbourhood_base_at_with_subset
  by (fastforce simp add: neighbourhood_base_of_def)

subsection‹Locally path-connected spaces›

definition weakly_locally_path_connected_at
  where "weakly_locally_path_connected_at x X ≡ neighbourhood_base_at x (path_connectedin X) X"

definition locally_path_connected_at
  where "locally_path_connected_at x X ≡
    neighbourhood_base_at x (λU. openin X U ∧ path_connectedin X U) X"

definition locally_path_connected_space
  where "locally_path_connected_space X ≡ neighbourhood_base_of (path_connectedin X) X"

lemma locally_path_connected_space_alt:
  "locally_path_connected_space X ⟷ neighbourhood_base_of (λU. openin X U ∧ path_connectedin X U) X"
  (is "?P = ?Q")
  and locally_path_connected_space_eq_open_path_component_of:
  "locally_path_connected_space X ⟷
        (∀U x. openin X U ∧ x ∈ U ⟶ 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 ∈ U"
      have "∃T. openin X T ∧ x ∈ T ∧ T ⊆ Collect (path_component_of (subtopology X U) y)"
        if "path_component_of (subtopology X U) y x" for x

      proof -
        have "x ∈ U"
          using path_component_of_equiv that topspace_subtopology by fastforce
        then have "∃Ua. openin X Ua ∧ (∃V. path_connectedin X V ∧ x ∈ Ua ∧ Ua ⊆ V ∧ V ⊆ U)"
      using P
      by (simp add: ‹openin X U› 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
   ⟷ (∀V x. openin X V ∧ x ∈ V ⟶ (∃U. openin X U ∧ path_connectedin X U ∧ x ∈ U ∧ U ⊆ 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 ⟷
        (∀U c. openin X U ∧ c ∈ path_components_of(subtopology X U) ⟶ openin X c)"
  apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def)
  by (metis imageI inf.absorb_iff2 openin_closedin_eq)

lemma openin_path_component_of_locally_path_connected_space:
   "locally_path_connected_space X ⟹ 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:
   "⟦locally_path_connected_space X; c ∈ path_components_of X⟧ ⟹ 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:
   "⟦locally_path_connected_space X; c ∈ path_components_of X⟧ ⟹ 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 ∈ 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 ⟷
    (∀V. openin X V ∧ x ∈ V
          ⟶ (∃U. openin X U ∧ x ∈ U ∧ U ⊆ V ∧
                  (∀y ∈ U. ∃C. path_connectedin X C ∧ C ⊆ V ∧ x ∈ C ∧ y ∈ 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 *: "∃V. path_connectedin X V ∧ U ⊆ V ∧ V ⊆ W"
    if "(∀y∈U. ∃C. path_connectedin X C ∧ C ⊆ W ∧ x ∈ C ∧ y ∈ 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 ⊆ ?V"
        by (auto simp: path_component_of path_connectedin_subtopology that)
      show "?V ⊆ 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 ⟷
      (∀V x. openin X V ∧ x ∈ V
             ⟶ (∃U. openin X U ∧
                    x ∈ U ∧ U ⊆ V ∧
                    (∀y ∈ U. ∃c. path_connectedin X c ∧
                                c ⊆ V ∧ x ∈ c ∧ y ∈ 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:
   "⟦locally_path_connected_space X; openin X s⟧
        ⟹ 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 ∈ path_components_of (subtopology Y V)"
  then have sub: "C ⊆ topspace Y"
    using path_connectedin_path_components_of path_connectedin_subset_topspace path_connectedin_subtopology by blast
  have "openin X {x ∈ topspace X. f x ∈ C}"
  proof (subst openin_subopen, clarify)
    fix x
    assume x: "x ∈ topspace X" and "f x ∈ C"
    let ?T = "Collect (path_component_of (subtopology X {z ∈ topspace X. f z ∈ V}) x)"
    show "∃T. openin X T ∧ x ∈ T ∧ T ⊆ {x ∈ topspace X. f x ∈ C}"
    proof (intro exI conjI)
      have "∃U. openin X U ∧ ?T ∈ path_components_of (subtopology X U)"
      proof (intro exI conjI)
        show "openin X ({z ∈ topspace X. f z ∈ V})"
          using V f openin_subset quotient_map_def by fastforce
        show "Collect (path_component_of (subtopology X {z ∈ topspace X. f z ∈ V}) x)
        ∈ path_components_of (subtopology X {z ∈ topspace X. f z ∈ V})"
          by (metis (no_types, lifting) Int_iff ‹f x ∈ C› 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 ∈ ?T"
        using V ‹f x ∈ C› c openin_subset path_component_of_equiv path_components_of_subset topspace_subtopology topspace_subtopology_subset x
        by fastforce
      have "f ` ?T ⊆ C"
      proof (rule path_components_of_maximal)
        show "C ∈ 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 ∈ topspace X. f a ∈ 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 "¬ disjnt C (f ` ?T)"
          by (metis (no_types, lifting) ‹f x ∈ C› x disjnt_iff image_eqI)
      qed
      then show "?T ⊆ {x ∈ topspace X. f x ∈ C}"
        by (force simp: path_component_of_equiv)
    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 ⟷ 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:
   "⟦retraction_map X Y r; locally_path_connected_space X⟧
        ⟹ 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 ∈ W"
  then obtain e where "e > 0" and e: "⋀x'. ¦x' - x¦ < e ⟶ x' ∈ W"
    by (auto simp: open_real)
  then show "∃U. open U ∧ (∃V. path_connected V ∧ x ∈ U ∧ U ⊆ V ∧ V ⊆ 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 ∈ 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 ⟹ (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
         ⟹ path_connected_space X ⟷ 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) ⟷
        topspace(product_topology X I) = {} ∨
        finite {i. i ∈ I ∧ ~path_connected_space(X i)} ∧
        (∀i ∈ I. locally_path_connected_space(X i))"
    (is "?lhs ⟷ ?empty ∨ ?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 ∈ (Π⇩E i∈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 ∈ U" "U ⊆ C" and Csub: "C ⊆ (Π⇩E i∈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 ∈ I. V i ≠ topspace (X i)}"
      and XV: "⋀i. i∈I ⟹ openin (X i) (V i)" and "z ∈ Pi⇩E I V" and subU: "Pi⇩E I V ⊆ U"
      by (force simp: openin_product_topology_alt)
    show ?thesis
    proof (intro conjI ballI)
      have "path_connected_space (X i)" if "i ∈ I" "V i = topspace (X i)" for i
      proof -
        have pc: "path_connectedin (X i) ((λx. x i) ` C)"
          apply (rule path_connectedin_continuous_map_image [OF _ V])
          by (simp add: continuous_map_product_projection ‹i ∈ I›)
        moreover have "((λx. x i) ` C) = topspace (X i)"
        proof
          show "(λx. x i) ` C ⊆ topspace (X i)"
            by (simp add: pc path_connectedin_subset_topspace)
          have "V i ⊆ (λx. x i) ` (Π⇩E i∈I. V i)"
            by (metis ‹z ∈ Pi⇩E I V› empty_iff image_projection_PiE order_refl that(1))
          also have "… ⊆ (λx. x i) ` U"
            using subU by blast
          finally show "topspace (X i) ⊆ (λx. x i) ` C"
            using ‹U ⊆ C› that by blast
        qed
        ultimately show ?thesis
          by (simp add: path_connectedin_topspace)
      qed
      then have "{i ∈ I. ¬ path_connected_space (X i)} ⊆ {i ∈ I. V i ≠ topspace (X i)}"
        by blast
      with finV show "finite {i ∈ I. ¬ path_connected_space (X i)}"
        using finite_subset by blast
    next
      show "locally_path_connected_space (X i)" if "i ∈ I" for i
        apply (rule locally_path_connected_space_quotient_map_image [OF _ L, where f = "λ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 ∈ F"
    then obtain W where finW: "finite {i ∈ I. W i ≠ topspace (X i)}"
            and opeW: "⋀i. i ∈ I ⟹ openin (X i) (W i)" and "z ∈ Pi⇩E I W" "Pi⇩E I W ⊆ F"
      by (auto simp: openin_product_topology_alt)
    have "∀i ∈ I. ∃U C. openin (X i) U ∧ path_connectedin (X i) C ∧ z i ∈ U ∧ U ⊆ C ∧ C ⊆ W i ∧
                        (W i = topspace (X i) ∧
                         path_connected_space (X i) ⟶ U = topspace (X i) ∧ C = topspace (X i))"
          (is "∀i ∈ I. ?Φ i")
    proof
      fix i assume "i ∈ I"
      have "locally_path_connected_space (X i)"
        by (simp add: R ‹i ∈ I›)
      moreover have "openin (X i) (W i) " "z i ∈ W i"
        using ‹z ∈ Pi⇩E I W› opeW ‹i ∈ I› by auto
      ultimately obtain U C where UC: "openin (X i) U" "path_connectedin (X i) C" "z i ∈ U" "U ⊆ C" "C ⊆ W i"
        using ‹i ∈ I› by (force simp: locally_path_connected_space_def neighbourhood_base_of)
      show "?Φ i"
      proof (cases "W i = topspace (X i) ∧ path_connected_space(X i)")
        case True
        then show ?thesis
          using ‹z i ∈ W i› path_connectedin_topspace by blast
      next
        case False
        then show ?thesis
          by (meson UC)
      qed
    qed
    then obtain U C where
      *: "⋀i. i ∈ I ⟹ openin (X i) (U i) ∧ path_connectedin (X i) (C i) ∧ z i ∈ (U i) ∧ (U i) ⊆ (C i) ∧ (C i) ⊆ W i ∧
                        (W i = topspace (X i) ∧ path_connected_space (X i)
                         ⟶ (U i) = topspace (X i) ∧ (C i) = topspace (X i))"
      by metis
    let ?A = "{i ∈ I. ¬ path_connected_space (X i)} ∪ {i ∈ I. W i ≠ topspace (X i)}"
    have "{i ∈ I. U i ≠ topspace (X i)} ⊆ ?A"
      by (clarsimp simp add: "*")
    moreover have "finite ?A"
      by (simp add: that finW)
    ultimately have "finite {i ∈ I. U i ≠ topspace (X i)}"
      using finite_subset by auto
    then have "openin (product_topology X I) (Pi⇩E I U)"
      using * by (simp add: openin_PiE_gen)
    then show "∃U. openin (product_topology X I) U ∧
            (∃V. path_connectedin (product_topology X I) V ∧ z ∈ U ∧ U ⊆ V ∧ V ⊆ F)"
      apply (rule_tac x="PiE I U" in exI, simp)
      apply (rule_tac x="PiE I C" in exI)
      using ‹z ∈ Pi⇩E I W› ‹Pi⇩E I W ⊆ F› *
      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