section ‹Neighbourhood bases and Locally path-connected spaces› theory Locally imports Path_Connected Function_Topology Sum_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))" by (smt (verit) neighbourhood_base_of subsetD) lemma neighbourhood_base_of_open_subset: "⟦neighbourhood_base_of P X; openin X S⟧ ⟹ neighbourhood_base_of P (subtopology X S)" by (smt (verit, ccfv_SIG) neighbourhood_base_of openin_open_subtopology subset_trans) 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))" by (smt (verit, del_insts) neighbourhood_base_of openin_topology_base_unique 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)" unfolding neighbourhood_base_at_def by (metis IntI Int_subset_iff openin_Int) 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 by (smt (verit) mem_Collect_eq open_neighbourhood_base_of 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 (simp add: locally_path_connected_space_eq_open_path_component_of path_components_of_def) by (smt (verit, ccfv_threshold) Int_iff image_iff openin_subset subset_iff) lemma openin_path_component_of_locally_path_connected_space: "locally_path_connected_space X ⟹ openin X (Collect (path_component_of X x))" using locally_path_connected_space_eq_open_path_component_of openin_subopen path_component_of_eq_empty by fastforce lemma openin_path_components_of_locally_path_connected_space: "⟦locally_path_connected_space X; C ∈ path_components_of X⟧ ⟹ openin X C" using locally_path_connected_space_open_path_components by force lemma closedin_path_components_of_locally_path_connected_space: "⟦locally_path_connected_space X; C ∈ path_components_of X⟧ ⟹ closedin X C" unfolding closedin_def by (metis Diff_iff complement_path_components_of_Union openin_clauses(3) openin_closedin_eq openin_path_components_of_locally_path_connected_space) 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 by (smt (verit) neighbourhood_base_at_def subset_iff weakly_locally_path_connected_at_def) 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)))" (is "?lhs = ?rhs") proof show "?lhs ⟹ ?rhs" by (metis locally_path_connected_space) assume ?rhs then show ?lhs unfolding locally_path_connected_space_def neighbourhood_base_of by (metis neighbourhood_base_at_def weakly_locally_path_connected_at weakly_locally_path_connected_at_def) qed lemma locally_path_connected_space_open_subset: "⟦locally_path_connected_space X; openin X S⟧ ⟹ locally_path_connected_space (subtopology X S)" by (smt (verit, best) locally_path_connected_space openin_open_subtopology path_connectedin_subtopology subset_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 have "x ∈ topspace (subtopology X {z ∈ topspace X. f z ∈ V})" using ‹f x ∈ C› c path_components_of_subset x by force then 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 (meson path_component_in_path_components_of) qed with X show "openin X ?T" using locally_path_connected_space_open_path_components by blast show x: "x ∈ ?T" using * nonempty_path_components_of path_component_of_eq path_component_of_eq_empty 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" using assms unfolding homeomorphic_space_def homeomorphic_map_def homeomorphic_maps_map by (metis locally_path_connected_space_quotient_map_image) 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 have "path_component_of_set X x ⊆ connected_component_of_set X x" by (simp add: path_component_subset_connected_component_of) moreover have "closedin X (path_component_of_set X x)" by (simp add: assms closedin_path_component_of_locally_path_connected_space) moreover have "openin X (path_component_of_set X x)" by (simp add: assms openin_path_component_of_locally_path_connected_space) moreover have "path_component_of_set X x ≠ {}" by (meson True path_component_of_eq_empty) ultimately show ?thesis using connectedin_connected_component_of [of X x] unfolding connectedin_def by (metis closedin_subset_topspace connected_space_clopen_in subset_openin_subtopology topspace_subtopology_subset) 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) ⟷ (product_topology X I) = trivial_topology ∨ 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))" using discrete_topology_unique_derived_set by (fastforce iff: null_topspace_iff_trivial) 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))" by (metis L locally_path_connected_space 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)" by (metis V continuous_map_product_projection path_connectedin_continuous_map_image that(1)) 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 by (meson False L locally_path_connected_space_quotient_map_image quotient_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" by (metis UC * openin_subset path_connectedin_topspace) 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 with * have "openin (product_topology X I) (Pi⇩_{E}I U)" 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)" by (metis (no_types, opaque_lifting) subsetI ‹z ∈ Pi⇩_{E}I W› ‹Pi⇩_{E}I W ⊆ F› * path_connectedin_PiE PiE_iff PiE_mono order.trans) qed ultimately show ?thesis using False by blast qed lemma locally_path_connected_is_realinterval: assumes "is_interval S" shows "locally_path_connected_space(subtopology euclideanreal S)" unfolding locally_path_connected_space_def proof (clarsimp simp add: neighbourhood_base_of openin_subtopology_alt) fix a U assume "a ∈ S" and "a ∈ U" and "open U" then obtain r where "r > 0" and r: "ball a r ⊆ U" by (metis open_contains_ball_eq) show "∃W. open W ∧ (∃V. path_connectedin (top_of_set S) V ∧ a ∈ W ∧ S ∩ W ⊆ V ∧ V ⊆ S ∧ V ⊆ U)" proof (intro exI conjI) show "path_connectedin (top_of_set S) (S ∩ ball a r)" by (simp add: assms is_interval_Int is_interval_ball_real is_interval_path_connected path_connectedin_subtopology) show "a ∈ ball a r" by (simp add: ‹0 < r›) qed (use ‹0 < r› r in auto) qed lemma locally_path_connected_real_interval: "locally_path_connected_space (subtopology euclideanreal{a..b})" "locally_path_connected_space (subtopology euclideanreal{a<..<b})" using locally_path_connected_is_realinterval by (auto simp add: is_interval_1) lemma locally_path_connected_space_prod_topology: "locally_path_connected_space (prod_topology X Y) ⟷ (prod_topology X Y) = trivial_topology ∨ locally_path_connected_space X ∧ locally_path_connected_space Y" (is "?lhs=?rhs") proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis using locally_path_connected_space_discrete_topology by force next case False then have ne: "X ≠ trivial_topology" "Y ≠ trivial_topology" by simp_all show ?thesis proof assume ?lhs then show ?rhs by (meson locally_path_connected_space_quotient_map_image ne(1) ne(2) quotient_map_fst quotient_map_snd) next assume ?rhs with False have X: "locally_path_connected_space X" and Y: "locally_path_connected_space Y" by auto show ?lhs unfolding locally_path_connected_space_def neighbourhood_base_of proof clarify fix UV x y assume UV: "openin (prod_topology X Y) UV" and "(x,y) ∈ UV" obtain A B where W12: "openin X A ∧ openin Y B ∧ x ∈ A ∧ y ∈ B ∧ A × B ⊆ UV" using X Y by (metis UV ‹(x,y) ∈ UV› openin_prod_topology_alt) then obtain C D K L where "openin X C" "path_connectedin X K" "x ∈ C" "C ⊆ K" "K ⊆ A" "openin Y D" "path_connectedin Y L" "y ∈ D" "D ⊆ L" "L ⊆ B" by (metis X Y locally_path_connected_space) with W12 ‹openin X C› ‹openin Y D› show "∃U V. openin (prod_topology X Y) U ∧ path_connectedin (prod_topology X Y) V ∧ (x, y) ∈ U ∧ U ⊆ V ∧ V ⊆ UV" apply (rule_tac x="C × D" in exI) apply (rule_tac x="K × L" in exI) apply (fastforce simp: openin_prod_Times_iff path_connectedin_Times) done qed qed qed lemma locally_path_connected_space_sum_topology: "locally_path_connected_space(sum_topology X I) ⟷ (∀i ∈ I. locally_path_connected_space (X i))" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (smt (verit) homeomorphic_locally_path_connected_space locally_path_connected_space_open_subset topological_property_of_sum_component) next assume R: ?rhs show ?lhs proof (clarsimp simp add: locally_path_connected_space_def neighbourhood_base_of forall_openin_sum_topology imp_conjL) fix W i x assume ope: "∀i∈I. openin (X i) (W i)" and "i ∈ I" and "x ∈ W i" then obtain U V where U: "openin (X i) U" and V: "path_connectedin (X i) V" and "x ∈ U" "U ⊆ V" "V ⊆ W i" by (metis R ‹i ∈ I› ‹x ∈ W i› locally_path_connected_space) show "∃U. openin (sum_topology X I) U ∧ (∃V. path_connectedin (sum_topology X I) V ∧ (i, x) ∈ U ∧ U ⊆ V ∧ V ⊆ Sigma I W)" proof (intro exI conjI) show "openin (sum_topology X I) (Pair i ` U)" by (meson U ‹i ∈ I› open_map_component_injection open_map_def) show "path_connectedin (sum_topology X I) (Pair i ` V)" by (meson V ‹i ∈ I› continuous_map_component_injection path_connectedin_continuous_map_image) show "Pair i ` V ⊆ Sigma I W" using ‹V ⊆ W i› ‹i ∈ I› by force qed (use ‹x ∈ U› ‹U ⊆ V› in auto) qed qed subsection‹Locally connected spaces› definition weakly_locally_connected_at where "weakly_locally_connected_at x X ≡ neighbourhood_base_at x (connectedin X) X" definition locally_connected_at where "locally_connected_at x X ≡ neighbourhood_base_at x (λU. openin X U ∧ connectedin X U ) X" definition locally_connected_space where "locally_connected_space X ≡ neighbourhood_base_of (connectedin X) X" lemma locally_connected_A: "(∀U x. openin X U ∧ x ∈ U ⟶ openin X (connected_component_of_set (subtopology X U) x)) ⟹ neighbourhood_base_of (λU. openin X U ∧ connectedin X U) X" unfolding neighbourhood_base_of by (metis (full_types) connected_component_of_refl connectedin_connected_component_of connectedin_subtopology mem_Collect_eq openin_subset topspace_subtopology_subset) lemma locally_connected_B: "locally_connected_space X ⟹ (∀U x. openin X U ∧ x ∈ U ⟶ openin X (connected_component_of_set (subtopology X U) x))" unfolding locally_connected_space_def neighbourhood_base_of apply (erule all_forward) apply clarify apply (subst openin_subopen) by (smt (verit, ccfv_threshold) Ball_Collect connected_component_of_def connected_component_of_equiv connectedin_subtopology in_mono mem_Collect_eq) lemma locally_connected_C: "neighbourhood_base_of (λU. openin X U ∧ connectedin X U) X ⟹ locally_connected_space X" using locally_connected_space_def neighbourhood_base_of_mono by auto lemma locally_connected_space_alt: "locally_connected_space X ⟷ neighbourhood_base_of (λU. openin X U ∧ connectedin X U) X" using locally_connected_A locally_connected_B locally_connected_C by blast lemma locally_connected_space_eq_open_connected_component_of: "locally_connected_space X ⟷ (∀U x. openin X U ∧ x ∈ U ⟶ openin X (connected_component_of_set (subtopology X U) x))" by (meson locally_connected_A locally_connected_B locally_connected_C) lemma locally_connected_space: "locally_connected_space X ⟷ (∀V x. openin X V ∧ x ∈ V ⟶ (∃U. openin X U ∧ connectedin X U ∧ x ∈ U ∧ U ⊆ V))" by (simp add: locally_connected_space_alt open_neighbourhood_base_of) lemma locally_path_connected_imp_locally_connected_space: "locally_path_connected_space X ⟹ locally_connected_space X" by (simp add: locally_connected_space_def locally_path_connected_space_def neighbourhood_base_of_mono path_connectedin_imp_connectedin) lemma locally_connected_space_open_connected_components: "locally_connected_space X ⟷ (∀U C. openin X U ∧ C ∈ connected_components_of(subtopology X U) ⟶ openin X C)" unfolding connected_components_of_def locally_connected_space_eq_open_connected_component_of by (smt (verit, best) image_iff openin_subset topspace_subtopology_subset) lemma openin_connected_component_of_locally_connected_space: "locally_connected_space X ⟹ openin X (connected_component_of_set X x)" by (metis connected_component_of_eq_empty locally_connected_B openin_empty openin_topspace subtopology_topspace) lemma openin_connected_components_of_locally_connected_space: "⟦locally_connected_space X; C ∈ connected_components_of X⟧ ⟹ openin X C" by (metis locally_connected_space_open_connected_components openin_topspace subtopology_topspace) lemma weakly_locally_connected_at: "weakly_locally_connected_at x X ⟷ (∀V. openin X V ∧ x ∈ V ⟶ (∃U. openin X U ∧ x ∈ U ∧ U ⊆ V ∧ (∀y ∈ U. ∃C. connectedin X C ∧ C ⊆ V ∧ x ∈ C ∧ y ∈ C)))" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs unfolding neighbourhood_base_at_def weakly_locally_connected_at_def by (meson subsetD subset_trans) next assume R: ?rhs show ?lhs unfolding neighbourhood_base_at_def weakly_locally_connected_at_def proof clarify fix V assume "openin X V" and "x ∈ V" then obtain U where "openin X U" "x ∈ U" "U ⊆ V" and U: "∀y∈U. ∃C. connectedin X C ∧ C ⊆ V ∧ x ∈ C ∧ y ∈ C" using R by force show "∃A B. openin X A ∧ connectedin X B ∧ x ∈ A ∧ A ⊆ B ∧ B ⊆ V" proof (intro conjI exI) show "connectedin X (connected_component_of_set (subtopology X V) x)" by (meson connectedin_connected_component_of connectedin_subtopology) show "U ⊆ connected_component_of_set (subtopology X V) x" using connected_component_of_maximal U by (simp add: connected_component_of_def connectedin_subtopology subsetI) show "connected_component_of_set (subtopology X V) x ⊆ V" using connected_component_of_subset_topspace by fastforce qed (auto simp: ‹x ∈ U› ‹openin X U›) qed qed lemma locally_connected_space_iff_weak: "locally_connected_space X ⟷ (∀x ∈ topspace X. weakly_locally_connected_at x X)" by (simp add: locally_connected_space_def neighbourhood_base_of_def weakly_locally_connected_at_def) lemma locally_connected_space_im_kleinen: "locally_connected_space X ⟷ (∀V x. openin X V ∧ x ∈ V ⟶ (∃U. openin X U ∧ x ∈ U ∧ U ⊆ V ∧ (∀y ∈ U. ∃C. connectedin X C ∧ C ⊆ V ∧ x ∈ C ∧ y ∈ C)))" unfolding locally_connected_space_iff_weak weakly_locally_connected_at using openin_subset subsetD by fastforce lemma locally_connected_space_open_subset: "⟦locally_connected_space X; openin X S⟧ ⟹ locally_connected_space (subtopology X S)" unfolding locally_connected_space_def neighbourhood_base_of by (smt (verit) connectedin_subtopology openin_open_subtopology subset_trans) lemma locally_connected_space_quotient_map_image: assumes X: "locally_connected_space X" and f: "quotient_map X Y f" shows "locally_connected_space Y" unfolding locally_connected_space_open_connected_components proof clarify fix V C assume "openin Y V" and C: "C ∈ connected_components_of (subtopology Y V)" then have "C ⊆ topspace Y" using connected_components_of_subset by force have ope1: "openin X {a ∈ topspace X. f a ∈ V}" using ‹openin Y V› f openin_continuous_map_preimage quotient_imp_continuous_map by blast define Vf where "Vf ≡ {z ∈ topspace X. f z ∈ V}" have "openin X {x ∈ topspace X. f x ∈ C}" proof (clarsimp simp: openin_subopen [where S = "{x ∈ topspace X. f x ∈ C}"]) fix x assume "x ∈ topspace X" and "f x ∈ C" show "∃T. openin X T ∧ x ∈ T ∧ T ⊆ {x ∈ topspace X. f x ∈ C}" proof (intro exI conjI) show "openin X (connected_component_of_set (subtopology X Vf) x)" by (metis Vf_def X connected_component_of_eq_empty locally_connected_B ope1 openin_empty openin_subset topspace_subtopology_subset) show x_in_conn: "x ∈ connected_component_of_set (subtopology X Vf) x" using C Vf_def ‹f x ∈ C› ‹x ∈ topspace X› connected_component_of_refl connected_components_of_subset by fastforce have "connected_component_of_set (subtopology X Vf) x ⊆ topspace X ∩ Vf" using connected_component_of_subset_topspace by fastforce moreover have "f ` connected_component_of_set (subtopology X Vf) x ⊆ C" proof (rule connected_components_of_maximal [where X = "subtopology Y V"]) show "C ∈ connected_components_of (subtopology Y V)" by (simp add: C) have §: "quotient_map (subtopology X Vf) (subtopology Y V) f" by (simp add: Vf_def ‹openin Y V› f quotient_map_restriction) then show "connectedin (subtopology Y V) (f ` connected_component_of_set (subtopology X Vf) x)" by (metis connectedin_connected_component_of connectedin_continuous_map_image quotient_imp_continuous_map) show "¬ disjnt C (f ` connected_component_of_set (subtopology X Vf) x)" using ‹f x ∈ C› x_in_conn by (auto simp: disjnt_iff) qed ultimately show "connected_component_of_set (subtopology X Vf) x ⊆ {x ∈ topspace X. f x ∈ C}" by blast qed qed then show "openin Y C" using ‹C ⊆ topspace Y› f quotient_map_def by fastforce qed lemma locally_connected_space_retraction_map_image: "⟦retraction_map X Y r; locally_connected_space X⟧ ⟹ locally_connected_space Y" using locally_connected_space_quotient_map_image retraction_imp_quotient_map by blast lemma homeomorphic_locally_connected_space: "X homeomorphic_space Y ⟹ locally_connected_space X ⟷ locally_connected_space Y" by (meson homeomorphic_map_def homeomorphic_space homeomorphic_space_sym locally_connected_space_quotient_map_image) lemma locally_connected_space_euclideanreal: "locally_connected_space euclideanreal" by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_space_euclideanreal) lemma locally_connected_is_realinterval: "is_interval S ⟹ locally_connected_space(subtopology euclideanreal S)" by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_is_realinterval) lemma locally_connected_real_interval: "locally_connected_space (subtopology euclideanreal{a..b})" "locally_connected_space (subtopology euclideanreal{a<..<b})" using connected_Icc is_interval_connected_1 locally_connected_is_realinterval by auto lemma locally_connected_space_discrete_topology: "locally_connected_space (discrete_topology U)" by (simp add: locally_path_connected_imp_locally_connected_space locally_path_connected_space_discrete_topology) lemma locally_path_connected_imp_locally_connected_at: "locally_path_connected_at x X ⟹ locally_connected_at x X" by (simp add: locally_connected_at_def locally_path_connected_at_def neighbourhood_base_at_mono path_connectedin_imp_connectedin) lemma weakly_locally_path_connected_imp_weakly_locally_connected_at: "weakly_locally_path_connected_at x X ⟹ weakly_locally_connected_at x X" by (metis path_connectedin_imp_connectedin weakly_locally_connected_at weakly_locally_path_connected_at) lemma interior_of_locally_connected_subspace_component: assumes X: "locally_connected_space X" and C: "C ∈ connected_components_of (subtopology X S)" shows "X interior_of C = C ∩ X interior_of S" proof - obtain Csub: "C ⊆ topspace X" "C ⊆ S" by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology) show ?thesis proof show "X interior_of C ⊆ C ∩ X interior_of S" by (simp add: Csub interior_of_mono interior_of_subset) have eq: "X interior_of S = ⋃ (connected_components_of (subtopology X (X interior_of S)))" by (metis Union_connected_components_of interior_of_subset_topspace topspace_subtopology_subset) moreover have "C ∩ D ⊆ X interior_of C" if "D ∈ connected_components_of (subtopology X (X interior_of S))" for D proof (cases "C ∩ D = {}") case False have "D ⊆ X interior_of C" proof (rule interior_of_maximal) have "connectedin (subtopology X S) D" by (meson connectedin_connected_components_of connectedin_subtopology interior_of_subset subset_trans that) then show "D ⊆ C" by (meson C False connected_components_of_maximal disjnt_def) show "openin X D" using X locally_connected_space_open_connected_components openin_interior_of that by blast qed then show ?thesis by blast qed auto ultimately show "C ∩ X interior_of S ⊆ X interior_of C" by blast qed qed lemma frontier_of_locally_connected_subspace_component: assumes X: "locally_connected_space X" and "closedin X S" and C: "C ∈ connected_components_of (subtopology X S)" shows "X frontier_of C = C ∩ X frontier_of S" proof - obtain Csub: "C ⊆ topspace X" "C ⊆ S" by (meson C connectedin_connected_components_of connectedin_subset_topspace connectedin_subtopology) then have "X closure_of C - X interior_of C = C ∩ X closure_of S - C ∩ X interior_of S" using assms apply (simp add: closure_of_closedin flip: interior_of_locally_connected_subspace_component) by (metis closedin_connected_components_of closedin_trans_full closure_of_eq inf.orderE) then show ?thesis by (simp add: Diff_Int_distrib frontier_of_def) qed (*Similar proof to locally_connected_space_prod_topology*) lemma locally_connected_space_prod_topology: "locally_connected_space (prod_topology X Y) ⟷ (prod_topology X Y) = trivial_topology ∨ locally_connected_space X ∧ locally_connected_space Y" (is "?lhs=?rhs") proof (cases "(prod_topology X Y) = trivial_topology") case True then show ?thesis using locally_connected_space_iff_weak by force next case False then have ne: "X ≠ trivial_topology" "Y ≠ trivial_topology" by simp_all show ?thesis proof assume ?lhs then show ?rhs by (metis locally_connected_space_quotient_map_image ne quotient_map_fst quotient_map_snd) next assume ?rhs with False have X: "locally_connected_space X" and Y: "locally_connected_space Y" by auto show ?lhs unfolding locally_connected_space_def neighbourhood_base_of proof clarify fix UV x y assume UV: "openin (prod_topology X Y) UV" and "(x,y) ∈ UV" obtain A B where W12: "openin X A ∧ openin Y B ∧ x ∈ A ∧ y ∈ B ∧ A × B ⊆ UV" using X Y by (metis UV ‹(x,y) ∈ UV› openin_prod_topology_alt) then obtain C D K L where "openin X C" "connectedin X K" "x ∈ C" "C ⊆ K" "K ⊆ A" "openin Y D" "connectedin Y L" "y ∈ D" "D ⊆ L" "L ⊆ B" by (metis X Y locally_connected_space) with W12 ‹openin X C› ‹openin Y D› show "∃U V. openin (prod_topology X Y) U ∧ connectedin (prod_topology X Y) V ∧ (x, y) ∈ U ∧ U ⊆ V ∧ V ⊆ UV" apply (rule_tac x="C × D" in exI) apply (rule_tac x="K × L" in exI) apply (auto simp: openin_prod_Times_iff connectedin_Times) done qed qed qed (*Same proof as locally_path_connected_space_product_topology*) lemma locally_connected_space_product_topology: "locally_connected_space(product_topology X I) ⟷ (product_topology X I) = trivial_topology ∨ finite {i. i ∈ I ∧ ~connected_space(X i)} ∧ (∀i ∈ I. locally_connected_space(X i))" (is "?lhs ⟷ ?empty ∨ ?rhs") proof (cases ?empty) case True then show ?thesis by (simp add: locally_connected_space_def neighbourhood_base_of openin_closedin_eq) next case False then obtain z where z: "z ∈ (Π⇩_{E}i∈I. topspace (X i))" using discrete_topology_unique_derived_set by (fastforce iff: null_topspace_iff_trivial) have ?rhs if L: ?lhs proof - obtain U C where U: "openin (product_topology X I) U" and V: "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_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 "connected_space (X i)" if "i ∈ I" "V i = topspace (X i)" for i proof - have pc: "connectedin (X i) ((λx. x i) ` C)" by (metis V connectedin_continuous_map_image continuous_map_product_projection that(1)) moreover have "((λx. x i) ` C) = topspace (X i)" proof show "(λx. x i) ` C ⊆ topspace (X i)" by (simp add: pc 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: connectedin_topspace) qed then have "{i ∈ I. ¬ connected_space (X i)} ⊆ {i ∈ I. V i ≠ topspace (X i)}" by blast with finV show "finite {i ∈ I. ¬ connected_space (X i)}" using finite_subset by blast next show "locally_connected_space (X i)" if "i ∈ I" for i by (meson False L locally_connected_space_quotient_map_image quotient_map_product_projection that) qed qed moreover have ?lhs if R: ?rhs proof (clarsimp simp add: locally_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 ∧ connectedin (X i) C ∧ z i ∈ U ∧ U ⊆ C ∧ C ⊆ W i ∧ (W i = topspace (X i) ∧ connected_space (X i) ⟶ U = topspace (X i) ∧ C = topspace (X i))" (is "∀i ∈ I. ?Φ i") proof fix i assume "i ∈ I" have "locally_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 "openin (X i) U" "connectedin (X i) C" "z i ∈ U" "U ⊆ C" "C ⊆ W i" using ‹i ∈ I› by (force simp: locally_connected_space_def neighbourhood_base_of) then show "?Φ i" by (metis * connectedin_topspace openin_subset) qed then obtain U C where *: "⋀i. i ∈ I ⟹ openin (X i) (U i) ∧ connectedin (X i) (C i) ∧ z i ∈ (U i) ∧ (U i) ⊆ (C i) ∧ (C i) ⊆ W i ∧ (W i = topspace (X i) ∧ connected_space (X i) ⟶ (U i) = topspace (X i) ∧ (C i) = topspace (X i))" by metis let ?A = "{i ∈ I. ¬ 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. connectedin (product_topology X I) V ∧ z ∈ U ∧ U ⊆ V ∧ V ⊆ F)" using ‹z ∈ Pi⇩_{E}I W› ‹Pi⇩_{E}I W ⊆ F› * by (metis (no_types, opaque_lifting) PiE_iff PiE_mono connectedin_PiE subset_iff) qed ultimately show ?thesis using False by blast qed lemma locally_connected_space_sum_topology: "locally_connected_space(sum_topology X I) ⟷ (∀i ∈ I. locally_connected_space (X i))" (is "?lhs=?rhs") proof assume ?lhs then show ?rhs by (smt (verit) homeomorphic_locally_connected_space locally_connected_space_open_subset topological_property_of_sum_component) next assume R: ?rhs show ?lhs proof (clarsimp simp add: locally_connected_space_def neighbourhood_base_of forall_openin_sum_topology imp_conjL) fix W i x assume ope: "∀i∈I. openin (X i) (W i)" and "i ∈ I" and "x ∈ W i" then obtain U V where U: "openin (X i) U" and V: "connectedin (X i) V" and "x ∈ U" "U ⊆ V" "V ⊆ W i" by (metis R ‹i ∈ I› ‹x ∈ W i› locally_connected_space) show "∃U. openin (sum_topology X I) U ∧ (∃V. connectedin (sum_topology X I) V ∧ (i,x) ∈ U ∧ U ⊆ V ∧ V ⊆ Sigma I W)" proof (intro exI conjI) show "openin (sum_topology X I) (Pair i ` U)" by (meson U ‹i ∈ I› open_map_component_injection open_map_def) show "connectedin (sum_topology X I) (Pair i ` V)" by (meson V ‹i ∈ I› continuous_map_component_injection connectedin_continuous_map_image) show "Pair i ` V ⊆ Sigma I W" using ‹V ⊆ W i› ‹i ∈ I› by force qed (use ‹x ∈ U› ‹U ⊆ V› in auto) qed qed subsection ‹Dimension of a topological space› text‹Basic definition of the small inductive dimension relation. Works in any topological space.› inductive dimension_le :: "['a topology, int] ⇒ bool" (infix "dim'_le" 50) where "⟦-1 ≤ n; ⋀V a. ⟦openin X V; a ∈ V⟧ ⟹ ∃U. a ∈ U ∧ U ⊆ V ∧ openin X U ∧ (subtopology X (X frontier_of U)) dim_le (n-1)⟧ ⟹ X dim_le (n::int)" lemma dimension_le_neighbourhood_base: "X dim_le n ⟷ -1 ≤ n ∧ neighbourhood_base_of (λU. openin X U ∧ (subtopology X (X frontier_of U)) dim_le (n-1)) X" by (smt (verit, best) dimension_le.simps open_neighbourhood_base_of) lemma dimension_le_bound: "X dim_le n ⟹-1 ≤ n" using dimension_le.simps by blast lemma dimension_le_mono [rule_format]: assumes "X dim_le m" shows "m ≤ n ⟶ X dim_le n" using assms proof (induction arbitrary: n rule: dimension_le.induct) qed (smt (verit) dimension_le.simps) inductive_simps dim_le_minus2 [simp]: "X dim_le -2" lemma dimension_le_eq_empty [simp]: "X dim_le -1 ⟷ X = trivial_topology" proof show "X dim_le (-1) ⟹ X = trivial_topology" by (force intro: dimension_le.cases) next show "X = trivial_topology ⟹ X dim_le (-1)" using dimension_le.simps openin_subset by fastforce qed lemma dimension_le_0_neighbourhood_base_of_clopen: "X dim_le 0 ⟷ neighbourhood_base_of (λU. closedin X U ∧ openin X U) X" proof - have "(subtopology X (X frontier_of U) dim_le -1) = closedin X U" if "openin X U" for U using that clopenin_eq_frontier_of openin_subset by (fastforce simp add: subtopology_trivial_iff frontier_of_subset_topspace Int_absorb1) then show ?thesis by (smt (verit, del_insts) dimension_le.simps open_neighbourhood_base_of) qed lemma dimension_le_subtopology: "X dim_le n ⟹ subtopology X S dim_le n" proof (induction arbitrary: S rule: dimension_le.induct) case (1 n X) show ?case proof (intro dimension_le.intros) show "- 1 ≤ n" by (simp add: "1.hyps") fix U' a assume U': "openin (subtopology X S) U'" and "a ∈ U'" then obtain U where U: "openin X U" "U' = U ∩ S" by (meson openin_subtopology) then obtain V where "a ∈ V" "V ⊆ U" "openin X V" and subV: "subtopology X (X frontier_of V) dim_le n-1" and dimV: "⋀T. subtopology X (X frontier_of V ∩ T) dim_le n-1" by (metis "1.IH" Int_iff ‹a ∈ U'› subtopology_subtopology) show "∃W. a ∈ W ∧ W ⊆ U' ∧ openin (subtopology X S) W ∧ subtopology (subtopology X S) (subtopology X S frontier_of W) dim_le n-1" proof (intro exI conjI) show "a ∈ S ∩ V" "S ∩ V ⊆ U'" using ‹U' = U ∩ S› ‹a ∈ U'› ‹a ∈ V› ‹V ⊆ U› by blast+ show "openin (subtopology X S) (S ∩ V)" by (simp add: ‹openin X V› openin_subtopology_Int2) have "S ∩ subtopology X S frontier_of V ⊆ X frontier_of V" by (simp add: frontier_of_subtopology_subset) then show "subtopology (subtopology X S) (subtopology X S frontier_of (S ∩ V)) dim_le n-1" by (metis dimV frontier_of_restrict inf.absorb_iff2 inf_left_idem subtopology_subtopology topspace_subtopology) qed qed qed lemma dimension_le_subtopologies: "⟦subtopology X T dim_le n; S ⊆ T⟧ ⟹ (subtopology X S) dim_le n" by (metis dimension_le_subtopology inf.absorb_iff2 subtopology_subtopology) lemma dimension_le_eq_subtopology: "(subtopology X S) dim_le n ⟷ -1 ≤ n ∧ (∀V a. openin X V ∧ a ∈ V ∧ a ∈ S ⟶ (∃U. a ∈ U ∧ U ⊆ V ∧ openin X U ∧ subtopology X (subtopology X S frontier_of (S ∩ U)) dim_le (n-1)))" proof - have *: "(∃T. a ∈ T ∧ T ∩ S ⊆ V ∩ S ∧ openin X T ∧ subtopology X (S ∩ (subtopology X S frontier_of (T ∩ S))) dim_le n-1) ⟷ (∃U. a ∈ U ∧ U ⊆ V ∧ openin X U ∧ subtopology X (subtopology X S frontier_of (S ∩ U)) dim_le n-1)" if "a ∈ V" "a ∈ S" "openin X V" for a V proof - have "∃U. a ∈ U ∧ U ⊆ V ∧ openin X U ∧ subtopology X (subtopology X S frontier_of (S ∩ U)) dim_le n-1" if "a ∈ T" and sub: "T ∩ S ⊆ V ∩ S" and "openin X T" and dim: "subtopology X (S ∩ subtopology X S frontier_of (T ∩ S)) dim_le n-1" for T proof (intro exI conjI) show "openin X (T ∩ V)" using ‹openin X V› ‹openin X T› by blast show "subtopology X (subtopology X S frontier_of (S ∩ (T ∩ V))) dim_le n-1" by (metis dim frontier_of_subset_subtopology inf.boundedE inf_absorb2 inf_assoc inf_commute sub) qed (use ‹a ∈ V› ‹a ∈ T› in auto) moreover have "∃T. a ∈ T ∧ T ∩ S ⊆ V ∩ S ∧ openin X T ∧ subtopology X (S ∩ subtopology X S frontier_of (T ∩ S)) dim_le n-1" if "a ∈ U" and "U ⊆ V" and "openin X U" and dim: "subtopology X (subtopology X S frontier_of (S ∩ U)) dim_le n-1" for U by (metis that frontier_of_subset_subtopology inf_absorb2 inf_commute inf_le1 le_inf_iff) ultimately show ?thesis by safe qed show ?thesis apply (simp add: dimension_le.simps [of _ n] subtopology_subtopology openin_subtopology flip: *) by (safe; metis Int_iff inf_le2 le_inf_iff) qed lemma homeomorphic_space_dimension_le_aux: assumes "X homeomorphic_space Y" "X dim_le of_nat n - 1" shows "Y dim_le of_nat n - 1" using assms proof (induction n arbitrary: X Y) case 0 then show ?case by (simp add: dimension_le_eq_empty homeomorphic_empty_space) next case (Suc n) then have X_dim_n: "X dim_le n" by simp show ?case proof (clarsimp simp add: dimension_le.simps [of Y n]) fix V b assume "openin Y V" and "b ∈ V" obtain f g where fg: "homeomorphic_maps X Y f g" using ‹X homeomorphic_space Y› homeomorphic_space_def by blast then have "openin X (g ` V)" using ‹openin Y V› homeomorphic_map_openness_eq homeomorphic_maps_map by blast then obtain U where "g b ∈ U" "openin X U" and gim: "U ⊆ g ` V" and sub: "subtopology X (X frontier_of U) dim_le int n - int 1" using X_dim_n unfolding dimension_le.simps [of X n] by (metis ‹b ∈ V› imageI of_nat_eq_1_iff) show "∃U. b ∈ U ∧ U ⊆ V ∧ openin Y U ∧ subtopology Y (Y frontier_of U) dim_le int n - 1" proof (intro conjI exI) show "b ∈ f ` U" by (metis (no_types, lifting) ‹b ∈ V› ‹g b ∈ U› ‹openin Y V› fg homeomorphic_maps_map image_iff openin_subset subsetD) show "f ` U ⊆ V" by (smt (verit, ccfv_threshold) ‹openin Y V› fg gim homeomorphic_maps_map image_iff openin_subset subset_iff) show "openin Y (f ` U)" using ‹openin X U› fg homeomorphic_map_openness_eq homeomorphic_maps_map by blast show "subtopology Y (Y frontier_of f ` U) dim_le int n-1" proof (rule Suc.IH) have "homeomorphic_maps (subtopology X (X frontier_of U)) (subtopology Y (Y frontier_of f ` U)) f g" using ‹openin X U› fg by (metis frontier_of_subset_topspace homeomorphic_map_frontier_of homeomorphic_maps_map homeomorphic_maps_subtopologies openin_subset topspace_subtopology topspace_subtopology_subset) then show "subtopology X (X frontier_of U) homeomorphic_space subtopology Y (Y frontier_of f ` U)" using homeomorphic_space_def by blast show "subtopology X (X frontier_of U) dim_le int n-1" using sub by fastforce qed qed qed qed lemma homeomorphic_space_dimension_le: assumes "X homeomorphic_space Y" shows "X dim_le n ⟷ Y dim_le n" proof (cases "n ≥ -1") case True then show ?thesis using homeomorphic_space_dimension_le_aux [of _ _ "nat(n+1)"] by (smt (verit) assms homeomorphic_space_sym nat_eq_iff) next case False then show ?thesis by (metis dimension_le_bound) qed lemma dimension_le_retraction_map_image: "⟦retraction_map X Y r; X dim_le n⟧ ⟹ Y dim_le n" by (meson dimension_le_subtopology homeomorphic_space_dimension_le retraction_map_def retraction_maps_section_image2) lemma dimension_le_discrete_topology [simp]: "(discrete_topology U) dim_le 0" using dimension_le.simps dimension_le_eq_empty by fastforce end