Theory Locally
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
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
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