--- a/src/HOL/Analysis/Homotopy.thy Sun Apr 12 10:51:51 2020 +0100
+++ b/src/HOL/Analysis/Homotopy.thy Sun Apr 12 21:53:58 2020 +0100
@@ -578,7 +578,7 @@
text\<open> A slightly ad-hoc but useful lemma in constructing homotopies.\<close>
-lemma homotopic_join_lemma:
+lemma continuous_on_homotopic_join_lemma:
fixes q :: "[real,real] \<Rightarrow> 'a::topological_space"
assumes p: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>y. p (fst y) (snd y))" (is "continuous_on ?A ?p")
and q: "continuous_on ({0..1} \<times> {0..1}) (\<lambda>y. q (fst y) (snd y))" (is "continuous_on ?A ?q")
@@ -621,7 +621,7 @@
apply (clarsimp simp add: homotopic_paths_def homotopic_with_def)
apply (rename_tac k1 k2)
apply (rule_tac x="(\<lambda>y. ((k1 \<circ> Pair (fst y)) +++ (k2 \<circ> Pair (fst y))) (snd y))" in exI)
- apply (intro conjI continuous_intros homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
+ apply (intro conjI continuous_intros continuous_on_homotopic_join_lemma; force simp: joinpaths_def pathstart_def pathfinish_def path_image_def)
done
proposition homotopic_paths_continuous_image:
@@ -806,10 +806,10 @@
have "c * 3 \<le> c * (d * 4)" using that less_eq_real_def by auto
with \<open>c \<le> 1\<close> show ?thesis by fastforce
qed
- have *: "\<And>p x. (path p \<and> path(reversepath p)) \<and>
- (path_image p \<subseteq> s \<and> path_image(reversepath p) \<subseteq> s) \<and>
- (pathfinish p = pathstart(linepath a a +++ reversepath p) \<and>
- pathstart(reversepath p) = a) \<and> pathstart p = x
+ have *: "\<And>p x. \<lbrakk>path p \<and> path(reversepath p);
+ path_image p \<subseteq> s \<and> path_image(reversepath p) \<subseteq> s;
+ pathfinish p = pathstart(linepath a a +++ reversepath p) \<and>
+ pathstart(reversepath p) = a \<and> pathstart p = x\<rbrakk>
\<Longrightarrow> homotopic_paths s (p +++ linepath a a +++ reversepath p) (linepath x x)"
by (metis homotopic_paths_lid homotopic_paths_join
homotopic_paths_trans homotopic_paths_sym homotopic_paths_rinv)
@@ -825,20 +825,23 @@
((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))"
unfolding homotopic_paths_def homotopic_with_def
proof (intro exI strip conjI)
- let ?h = "\<lambda>y. (subpath 0 (fst y) (\<lambda>u. h (u, 0)) +++ (\<lambda>u. h (Pair (fst y) u)) +++ subpath (fst y) 0 (\<lambda>u. h (u, 0))) (snd y)"
- show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
+ let ?h = "\<lambda>y. (subpath 0 (fst y) (\<lambda>u. h (u, 0)) +++ (\<lambda>u. h (Pair (fst y) u))
+ +++ subpath (fst y) 0 (\<lambda>u. h (u, 0))) (snd y)"
+ have "continuous_on ?A ?h"
+ by (intro continuous_on_homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2)
+ moreover have "?h ` ?A \<subseteq> s"
+ unfolding joinpaths_def subpath_def
+ by (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le)
+ ultimately show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1}))
(top_of_set s) ?h"
- apply (simp add: subpath_reversepath)
- apply (intro conjI homotopic_join_lemma; simp add: path_defs joinpaths_def subpath_def conth c1 c2)
- apply (force simp: algebra_simps mult_le_one mult_left_le intro: hs [THEN subsetD] adhoc_le)
- done
+ by (simp add: subpath_reversepath)
qed (use ploop in \<open>simp_all add: reversepath_def path_defs joinpaths_def o_def subpath_def conth c1 c2\<close>)
moreover have "homotopic_paths s ((\<lambda>u. h (u, 0)) +++ linepath a a +++ reversepath (\<lambda>u. h (u, 0)))
(linepath (pathstart p) (pathstart p))"
- apply (rule *)
- apply (simp add: pih0 pathstart_def pathfinish_def conth0)
- apply (simp add: reversepath_def joinpaths_def)
- done
+ proof (rule *; simp add: pih0 pathstart_def pathfinish_def conth0)
+ show "a = (linepath a a +++ reversepath (\<lambda>u. h (u, 0))) 0 \<and> reversepath (\<lambda>u. h (u, 0)) 0 = a"
+ by (simp_all add: reversepath_def joinpaths_def)
+ qed
ultimately show ?thesis
by (blast intro: homotopic_paths_trans)
qed
@@ -846,7 +849,7 @@
proposition homotopic_loops_conjugate:
fixes s :: "'a::real_normed_vector set"
assumes "path p" "path q" and pip: "path_image p \<subseteq> s" and piq: "path_image q \<subseteq> s"
- and papp: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
+ and pq: "pathfinish p = pathstart q" and qloop: "pathfinish q = pathstart q"
shows "homotopic_loops s (p +++ q +++ reversepath p) q"
proof -
have contp: "continuous_on {0..1} p" using \<open>path p\<close> [unfolded path_def] by blast
@@ -876,15 +879,20 @@
using path_image_def piq by fastforce
have "homotopic_loops s (p +++ q +++ reversepath p)
(linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q))"
- apply (simp add: homotopic_loops_def homotopic_with_def)
- apply (rule_tac x="(\<lambda>y. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))" in exI)
- apply (simp add: subpath_refl subpath_reversepath)
- apply (intro conjI homotopic_join_lemma)
- using papp qloop
- apply (simp_all add: path_defs joinpaths_def o_def subpath_def c1 c2)
- apply (force simp: contq intro: continuous_on_compose [of _ _ q, unfolded o_def] continuous_on_id continuous_on_snd)
- apply (auto simp: ps1 ps2 qs)
- done
+ unfolding homotopic_loops_def homotopic_with_def
+ proof (intro exI strip conjI)
+ let ?h = "(\<lambda>y. (subpath (fst y) 1 p +++ q +++ subpath 1 (fst y) p) (snd y))"
+ have "continuous_on ?A (\<lambda>y. q (snd y))"
+ by (force simp: contq intro: continuous_on_compose [of _ _ q, unfolded o_def] continuous_on_id continuous_on_snd)
+ then have "continuous_on ?A ?h"
+ apply (intro continuous_on_homotopic_join_lemma)
+ using pq qloop
+ by (auto simp: path_defs joinpaths_def subpath_def c1 c2)
+ then show "continuous_map (prod_topology (top_of_set {0..1}) (top_of_set {0..1})) (top_of_set s) ?h"
+ by (auto simp: joinpaths_def subpath_def ps1 ps2 qs)
+ show "?h (1,x) = (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) x" for x
+ using pq by (simp add: pathfinish_def subpath_refl)
+ qed (auto simp: subpath_reversepath)
moreover have "homotopic_loops s (linepath (pathstart q) (pathstart q) +++ q +++ linepath (pathstart q) (pathstart q)) q"
proof -
have "homotopic_paths s (linepath (pathfinish q) (pathfinish q) +++ q) q"
@@ -944,10 +952,10 @@
lemma homotopic_with_linear:
fixes f g :: "_ \<Rightarrow> 'b::real_normed_vector"
- assumes contf: "continuous_on s f"
- and contg:"continuous_on s g"
- and sub: "\<And>x. x \<in> s \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> t"
- shows "homotopic_with_canon (\<lambda>z. True) s t f g"
+ assumes contf: "continuous_on S f"
+ and contg:"continuous_on S g"
+ and sub: "\<And>x. x \<in> S \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> t"
+ shows "homotopic_with_canon (\<lambda>z. True) S t f g"
apply (simp add: homotopic_with_def)
apply (rule_tac x="\<lambda>y. ((1 - (fst y)) *\<^sub>R f(snd y) + (fst y) *\<^sub>R g(snd y))" in exI)
apply (intro conjI)
@@ -959,8 +967,8 @@
lemma homotopic_paths_linear:
fixes g h :: "real \<Rightarrow> 'a::real_normed_vector"
assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
- "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
- shows "homotopic_paths s g h"
+ "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> S"
+ shows "homotopic_paths S g h"
using assms
unfolding path_def
apply (simp add: closed_segment_def pathstart_def pathfinish_def homotopic_paths_def homotopic_with_def)
@@ -971,8 +979,8 @@
lemma homotopic_loops_linear:
fixes g h :: "real \<Rightarrow> 'a::real_normed_vector"
assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
- "\<And>t x. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> s"
- shows "homotopic_loops s g h"
+ "\<And>t x. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> S"
+ shows "homotopic_loops S g h"
using assms
unfolding path_def
apply (simp add: pathstart_def pathfinish_def homotopic_loops_def homotopic_with_def)
@@ -982,29 +990,33 @@
done
lemma homotopic_paths_nearby_explicit:
- assumes "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
- and no: "\<And>t x. \<lbrakk>t \<in> {0..1}; x \<notin> s\<rbrakk> \<Longrightarrow> norm(h t - g t) < norm(g t - x)"
- shows "homotopic_paths s g h"
- apply (rule homotopic_paths_linear [OF assms(1-4)])
+ assumes \<section>: "path g" "path h" "pathstart h = pathstart g" "pathfinish h = pathfinish g"
+ and no: "\<And>t x. \<lbrakk>t \<in> {0..1}; x \<notin> S\<rbrakk> \<Longrightarrow> norm(h t - g t) < norm(g t - x)"
+ shows "homotopic_paths S g h"
+proof (rule homotopic_paths_linear [OF \<section>])
+ show "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> S"
by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
+qed
lemma homotopic_loops_nearby_explicit:
- assumes "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
- and no: "\<And>t x. \<lbrakk>t \<in> {0..1}; x \<notin> s\<rbrakk> \<Longrightarrow> norm(h t - g t) < norm(g t - x)"
- shows "homotopic_loops s g h"
- apply (rule homotopic_loops_linear [OF assms(1-4)])
+ assumes \<section>: "path g" "path h" "pathfinish g = pathstart g" "pathfinish h = pathstart h"
+ and no: "\<And>t x. \<lbrakk>t \<in> {0..1}; x \<notin> S\<rbrakk> \<Longrightarrow> norm(h t - g t) < norm(g t - x)"
+ shows "homotopic_loops S g h"
+proof (rule homotopic_loops_linear [OF \<section>])
+ show "\<And>t. t \<in> {0..1} \<Longrightarrow> closed_segment (g t) (h t) \<subseteq> S"
by (metis no segment_bound(1) subsetI norm_minus_commute not_le)
+qed
lemma homotopic_nearby_paths:
fixes g h :: "real \<Rightarrow> 'a::euclidean_space"
- assumes "path g" "open s" "path_image g \<subseteq> s"
+ assumes "path g" "open S" "path_image g \<subseteq> S"
shows "\<exists>e. 0 < e \<and>
(\<forall>h. path h \<and>
pathstart h = pathstart g \<and> pathfinish h = pathfinish g \<and>
- (\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> homotopic_paths s g h)"
+ (\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> homotopic_paths S g h)"
proof -
- obtain e where "e > 0" and e: "\<And>x y. x \<in> path_image g \<Longrightarrow> y \<in> - s \<Longrightarrow> e \<le> dist x y"
- using separate_compact_closed [of "path_image g" "-s"] assms by force
+ obtain e where "e > 0" and e: "\<And>x y. x \<in> path_image g \<Longrightarrow> y \<in> - S \<Longrightarrow> e \<le> dist x y"
+ using separate_compact_closed [of "path_image g" "-S"] assms by force
show ?thesis
apply (intro exI conjI)
using e [unfolded dist_norm]
@@ -1014,13 +1026,13 @@
lemma homotopic_nearby_loops:
fixes g h :: "real \<Rightarrow> 'a::euclidean_space"
- assumes "path g" "open s" "path_image g \<subseteq> s" "pathfinish g = pathstart g"
+ assumes "path g" "open S" "path_image g \<subseteq> S" "pathfinish g = pathstart g"
shows "\<exists>e. 0 < e \<and>
(\<forall>h. path h \<and> pathfinish h = pathstart h \<and>
- (\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> homotopic_loops s g h)"
+ (\<forall>t \<in> {0..1}. norm(h t - g t) < e) \<longrightarrow> homotopic_loops S g h)"
proof -
- obtain e where "e > 0" and e: "\<And>x y. x \<in> path_image g \<Longrightarrow> y \<in> - s \<Longrightarrow> e \<le> dist x y"
- using separate_compact_closed [of "path_image g" "-s"] assms by force
+ obtain e where "e > 0" and e: "\<And>x y. x \<in> path_image g \<Longrightarrow> y \<in> - S \<Longrightarrow> e \<le> dist x y"
+ using separate_compact_closed [of "path_image g" "-S"] assms by force
show ?thesis
apply (intro exI conjI)
using e [unfolded dist_norm]
@@ -1041,28 +1053,34 @@
have 2: "t * 2 > 1 \<Longrightarrow> u + (2*t - 1) * v \<le> v + (2*t - 1) * w" for t
by (metis add_mono_thms_linordered_semiring(1) diff_gt_0_iff_gt less_eq_real_def mult.commute mult_right_mono \<open>u \<le> v\<close> \<open>v \<le> w\<close>)
have t2: "\<And>t::real. t*2 = 1 \<Longrightarrow> t = 1/2" by auto
- show ?thesis
- apply (rule homotopic_paths_subset [OF _ pag])
- using assms
- apply (cases "w = u")
- using homotopic_paths_rinv [of "subpath u v g" "path_image g"]
- apply (force simp: closed_segment_eq_real_ivl image_mono path_image_def subpath_refl)
- apply (rule homotopic_paths_sym)
- apply (rule homotopic_paths_reparametrize
- [where f = "\<lambda>t. if t \<le> 1/2
- then inverse((w - u)) *\<^sub>R (2 * (v - u)) *\<^sub>R t
- else inverse((w - u)) *\<^sub>R ((v - u) + (w - v) *\<^sub>R (2 *\<^sub>R t - 1))"])
- using \<open>path g\<close> path_subpath u w apply blast
- using \<open>path g\<close> path_image_subpath_subset u w(1) apply blast
- apply simp_all
- apply (subst split_01)
- apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
- apply (simp_all add: field_simps not_le)
- apply (force dest!: t2)
- apply (force simp: algebra_simps mult_left_mono affine_ineq dest!: 1 2)
- apply (simp add: joinpaths_def subpath_def)
- apply (force simp: algebra_simps)
- done
+ have "homotopic_paths (path_image g) (subpath u v g +++ subpath v w g) (subpath u w g)"
+ proof (cases "w = u")
+ case True
+ then show ?thesis
+ by (metis \<open>path g\<close> homotopic_paths_rinv path_image_subpath_subset path_subpath pathstart_subpath reversepath_subpath subpath_refl u v)
+ next
+ case False
+ let ?f = "\<lambda>t. if t \<le> 1/2 then inverse((w - u)) *\<^sub>R (2 * (v - u)) *\<^sub>R t
+ else inverse((w - u)) *\<^sub>R ((v - u) + (w - v) *\<^sub>R (2 *\<^sub>R t - 1))"
+ show ?thesis
+ proof (rule homotopic_paths_sym [OF homotopic_paths_reparametrize [where f = ?f]])
+ show "path (subpath u w g)"
+ using assms(1) path_subpath u w(1) by blast
+ show "path_image (subpath u w g) \<subseteq> path_image g"
+ by (meson path_image_subpath_subset u w(1))
+ show "continuous_on {0..1} ?f"
+ unfolding split_01
+ by (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def dest!: t2)+
+ show "?f ` {0..1} \<subseteq> {0..1}"
+ using False assms
+ by (force simp: field_simps not_le mult_left_mono affine_ineq dest!: 1 2)
+ show "(subpath u v g +++ subpath v w g) t = subpath u w g (?f t)" if "t \<in> {0..1}" for t
+ using assms
+ unfolding joinpaths_def subpath_def by (auto simp add: divide_simps add.commute mult.commute mult.left_commute)
+ qed (use False in auto)
+ qed
+ then show ?thesis
+ by (rule homotopic_paths_subset [OF _ pag])
qed
lemma homotopic_join_subpaths2:
@@ -1077,25 +1095,30 @@
shows "homotopic_paths s (subpath v w g +++ subpath w u g) (subpath v u g)"
proof -
have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
- apply (rule homotopic_paths_join)
- using hom homotopic_paths_sym_eq apply blast
- apply (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w, simp)
- done
+ proof (rule homotopic_paths_join)
+ show "homotopic_paths s (subpath u w g) (subpath u v g +++ subpath v w g)"
+ using hom homotopic_paths_sym_eq by blast
+ show "homotopic_paths s (subpath w v g) (subpath w v g)"
+ by (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w)
+ qed auto
also have "homotopic_paths s ((subpath u v g +++ subpath v w g) +++ subpath w v g) (subpath u v g +++ subpath v w g +++ subpath w v g)"
- apply (rule homotopic_paths_sym [OF homotopic_paths_assoc])
- using assms by (simp_all add: path_image_subpath_subset [THEN order_trans])
+ by (rule homotopic_paths_sym [OF homotopic_paths_assoc])
+ (use assms in \<open>simp_all add: path_image_subpath_subset [THEN order_trans]\<close>)
also have "homotopic_paths s (subpath u v g +++ subpath v w g +++ subpath w v g)
(subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
- apply (rule homotopic_paths_join)
- apply (metis \<open>path g\<close> homotopic_paths_eq order.trans pag path_image_subpath_subset path_subpath u v)
- apply (metis (no_types, lifting) \<open>path g\<close> homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w)
- apply simp
- done
+ proof (rule homotopic_paths_join; simp)
+ show "path (subpath u v g) \<and> path_image (subpath u v g) \<subseteq> s"
+ by (metis \<open>path g\<close> order.trans pag path_image_subpath_subset path_subpath u v)
+ show "homotopic_paths s (subpath v w g +++ subpath w v g) (linepath (g v) (g v))"
+ by (metis (no_types, lifting) \<open>path g\<close> homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w)
+ qed
also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
- apply (rule homotopic_paths_rid)
- using \<open>path g\<close> path_subpath u v apply blast
- apply (meson \<open>path g\<close> order.trans pag path_image_subpath_subset u v)
- done
+ proof (rule homotopic_paths_rid)
+ show "path (subpath u v g)"
+ using \<open>path g\<close> path_subpath u v by blast
+ show "path_image (subpath u v g) \<subseteq> s"
+ by (meson \<open>path g\<close> order.trans pag path_image_subpath_subset u v)
+ qed
finally have "homotopic_paths s (subpath u w g +++ subpath w v g) (subpath u v g)" .
then show ?thesis
using homotopic_join_subpaths2 by blast
@@ -1104,8 +1127,8 @@
proposition homotopic_join_subpaths:
"\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
\<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
- apply (rule le_cases3 [of u v w])
-using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
+ using le_cases3 [of u v w] homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3
+ by metis
text\<open>Relating homotopy of trivial loops to path-connectedness.\<close>
@@ -1169,11 +1192,10 @@
(\<forall>p a. path p \<and> path_image p \<subseteq> S \<and>
pathfinish p = pathstart p \<and> a \<in> S
\<longrightarrow> homotopic_loops S p (linepath a a))"
-apply (simp add: simply_connected_def)
+ unfolding simply_connected_def
apply (rule iffI, force, clarify)
-apply (rule_tac q = "linepath (pathstart p) (pathstart p)" in homotopic_loops_trans)
-apply (fastforce simp add:)
-using homotopic_loops_sym apply blast
+ apply (rule_tac q = "linepath (pathstart p) (pathstart p)" in homotopic_loops_trans)
+using homotopic_loops_sym apply blast+
done
lemma simply_connected_eq_contractible_loop_some:
@@ -1182,13 +1204,23 @@
path_connected S \<and>
(\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
\<longrightarrow> (\<exists>a. a \<in> S \<and> homotopic_loops S p (linepath a a)))"
-apply (rule iffI)
- apply (fastforce simp: simply_connected_imp_path_connected simply_connected_eq_contractible_loop_any)
-apply (clarsimp simp add: simply_connected_eq_contractible_loop_any)
-apply (drule_tac x=p in spec)
-using homotopic_loops_trans path_connected_eq_homotopic_points
- apply blast
-done
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ using simply_connected_eq_contractible_loop_any by (blast intro: simply_connected_imp_path_connected)
+next
+ assume r: ?rhs
+ note pa = r [THEN conjunct2, rule_format]
+ show ?lhs
+ proof (clarsimp simp add: simply_connected_eq_contractible_loop_any)
+ fix p a
+ assume "path p" and "path_image p \<subseteq> S" "pathfinish p = pathstart p"
+ and "a \<in> S"
+ with pa [of p] show "homotopic_loops S p (linepath a a)"
+ using homotopic_loops_trans path_connected_eq_homotopic_points r by blast
+ qed
+qed
lemma simply_connected_eq_contractible_loop_all:
fixes S :: "_::real_normed_vector set"
@@ -1211,9 +1243,9 @@
next
assume ?rhs
then show "simply_connected S"
- apply (simp add: simply_connected_eq_contractible_loop_any False)
- by (meson homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans
- path_component_imp_homotopic_points path_component_refl)
+ unfolding simply_connected_eq_contractible_loop_any
+ by (meson False homotopic_loops_refl homotopic_loops_sym homotopic_loops_trans
+ path_component_imp_homotopic_points path_component_refl)
qed
qed
@@ -1223,11 +1255,17 @@
path_connected S \<and>
(\<forall>p. path p \<and> path_image p \<subseteq> S \<and> pathfinish p = pathstart p
\<longrightarrow> homotopic_paths S p (linepath (pathstart p) (pathstart p)))"
-apply (rule iffI)
- apply (simp add: simply_connected_imp_path_connected)
- apply (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null)
-by (meson homotopic_paths_imp_homotopic_loops pathfinish_linepath pathstart_in_path_image
- simply_connected_eq_contractible_loop_some subset_iff)
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ unfolding simply_connected_imp_path_connected
+ by (metis simply_connected_eq_contractible_loop_some homotopic_loops_imp_homotopic_paths_null)
+next
+ assume ?rhs
+ then show ?lhs
+ using homotopic_paths_imp_homotopic_loops simply_connected_eq_contractible_loop_some by fastforce
+qed
lemma simply_connected_eq_homotopic_paths:
fixes S :: "_::real_normed_vector set"
@@ -1285,38 +1323,25 @@
for p a b
proof -
have "path (fst \<circ> p)"
- apply (rule Path_Connected.path_continuous_image [OF \<open>path p\<close>])
- apply (rule continuous_intros)+
- done
+ by (simp add: continuous_on_fst Path_Connected.path_continuous_image [OF \<open>path p\<close>])
moreover have "path_image (fst \<circ> p) \<subseteq> S"
using that apply (simp add: path_image_def) by force
ultimately have p1: "homotopic_loops S (fst \<circ> p) (linepath a a)"
using S that
- apply (simp add: simply_connected_eq_contractible_loop_any)
- apply (drule_tac x="fst \<circ> p" in spec)
- apply (drule_tac x=a in spec)
- apply (auto simp: pathstart_def pathfinish_def)
- done
+ by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
have "path (snd \<circ> p)"
- apply (rule Path_Connected.path_continuous_image [OF \<open>path p\<close>])
- apply (rule continuous_intros)+
- done
+ by (simp add: continuous_on_snd Path_Connected.path_continuous_image [OF \<open>path p\<close>])
moreover have "path_image (snd \<circ> p) \<subseteq> T"
using that apply (simp add: path_image_def) by force
ultimately have p2: "homotopic_loops T (snd \<circ> p) (linepath b b)"
using T that
- apply (simp add: simply_connected_eq_contractible_loop_any)
- apply (drule_tac x="snd \<circ> p" in spec)
- apply (drule_tac x=b in spec)
- apply (auto simp: pathstart_def pathfinish_def)
- done
+ by (simp add: simply_connected_eq_contractible_loop_any pathfinish_def pathstart_def)
show ?thesis
- using p1 p2
- apply (simp add: homotopic_loops, clarify)
+ using p1 p2 unfolding homotopic_loops
+ apply clarify
apply (rename_tac h k)
apply (rule_tac x="\<lambda>z. Pair (h z) (k z)" in exI)
- apply (intro conjI continuous_intros | assumption)+
- apply (auto simp: pathstart_def pathfinish_def)
+ apply (force intro: continuous_intros simp: pathstart_def pathfinish_def)+
done
qed
with assms show ?thesis
@@ -1340,14 +1365,15 @@
using assms by (force simp: contractible_def)
then have "a \<in> S"
by (metis False homotopic_constant_maps homotopic_with_symD homotopic_with_trans path_component_in_topspace topspace_euclidean_subtopology)
- show ?thesis
- apply (simp add: simply_connected_eq_contractible_loop_all False)
- apply (rule bexI [OF _ \<open>a \<in> S\<close>])
+ have "\<forall>p. path p \<and>
+ path_image p \<subseteq> S \<and> pathfinish p = pathstart p \<longrightarrow>
+ homotopic_loops S p (linepath a a)"
using a apply (simp add: homotopic_loops_def homotopic_with_def path_def path_image_def pathfinish_def pathstart_def, clarify)
apply (rule_tac x="(h \<circ> (\<lambda>y. (fst y, (p \<circ> snd) y)))" in exI)
- apply (intro conjI continuous_on_compose continuous_intros)
- apply (erule continuous_on_subset | force)+
+ apply (intro conjI continuous_on_compose continuous_intros; force elim: continuous_on_subset)
done
+ with \<open>a \<in> S\<close> show ?thesis
+ by (auto simp add: simply_connected_eq_contractible_loop_all False)
qed
corollary contractible_imp_connected:
@@ -1381,19 +1407,14 @@
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
and T: "contractible T"
obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
-apply (rule nullhomotopic_through_contractible [OF f, of id T])
-using assms
-apply (auto)
-done
+ by (rule nullhomotopic_through_contractible [OF f, of id T]) (use assms in auto)
lemma nullhomotopic_from_contractible:
assumes f: "continuous_on S f" "f ` S \<subseteq> T"
and S: "contractible S"
obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
-apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
-using assms
-apply (auto simp: comp_def)
-done
+ apply (rule nullhomotopic_through_contractible [OF continuous_on_id _ f S, of S])
+ using assms by (auto simp: comp_def)
lemma homotopic_through_contractible:
fixes S :: "_::real_normed_vector set"
@@ -1405,14 +1426,10 @@
shows "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (g2 \<circ> f2)"
proof -
obtain c1 where c1: "homotopic_with_canon (\<lambda>h. True) S U (g1 \<circ> f1) (\<lambda>x. c1)"
- apply (rule nullhomotopic_through_contractible [of S f1 T g1 U])
- using assms apply auto
- done
+ by (rule nullhomotopic_through_contractible [of S f1 T g1 U]) (use assms in auto)
obtain c2 where c2: "homotopic_with_canon (\<lambda>h. True) S U (g2 \<circ> f2) (\<lambda>x. c2)"
- apply (rule nullhomotopic_through_contractible [of S f2 T g2 U])
- using assms apply auto
- done
- have *: "S = {} \<or> (\<exists>t. path_connected t \<and> t \<subseteq> U \<and> c2 \<in> t \<and> c1 \<in> t)"
+ by (rule nullhomotopic_through_contractible [of S f2 T g2 U]) (use assms in auto)
+ have "S = {} \<or> (\<exists>t. path_connected t \<and> t \<subseteq> U \<and> c2 \<in> t \<and> c1 \<in> t)"
proof (cases "S = {}")
case True then show ?thesis by force
next
@@ -1421,12 +1438,10 @@
using homotopic_with_imp_continuous_maps by fastforce+
with \<open>path_connected U\<close> show ?thesis by blast
qed
- show ?thesis
- apply (rule homotopic_with_trans [OF c1])
- apply (rule homotopic_with_symD)
- apply (rule homotopic_with_trans [OF c2])
- apply (simp add: path_component homotopic_constant_maps *)
- done
+ then have "homotopic_with_canon (\<lambda>h. True) S U (\<lambda>x. c2) (\<lambda>x. c1)"
+ by (simp add: path_component homotopic_constant_maps)
+ then show ?thesis
+ using c1 c2 homotopic_with_symD homotopic_with_trans by blast
qed
lemma homotopic_into_contractible:
@@ -1467,16 +1482,14 @@
by (simp add: assms rel_interior_eq_empty)
then obtain a where a: "a \<in> rel_interior S" by blast
with ST have "a \<in> T" by blast
- have *: "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
- apply (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
- using assms by blast
- show ?thesis
- unfolding starlike_def
- apply (rule bexI [OF _ \<open>a \<in> T\<close>])
- apply (simp add: closed_segment_eq_open)
+ have "\<And>x. x \<in> T \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
+ by (rule rel_interior_closure_convex_segment [OF \<open>convex S\<close> a]) (use assms in auto)
+ then have "\<forall>x\<in>T. a \<in> T \<and> open_segment a x \<subseteq> T"
apply (intro conjI ballI a \<open>a \<in> T\<close> rel_interior_closure_convex_segment [OF \<open>convex S\<close> a])
- apply (simp add: order_trans [OF * ST])
- done
+ using ST by blast
+ then show ?thesis
+ unfolding starlike_def using bexI [OF _ \<open>a \<in> T\<close>]
+ by (simp add: closed_segment_eq_open)
qed
lemma starlike_imp_contractible_gen:
@@ -1492,14 +1505,14 @@
apply (erule a [unfolded closed_segment_def, THEN subsetD], simp)
apply (metis add_diff_cancel_right' diff_ge_0_iff_ge le_add_diff_inverse pth_c(1))
done
- then show ?thesis
- apply (rule_tac a=a in that)
+ then have "homotopic_with_canon P S S (\<lambda>x. x) (\<lambda>x. a)"
using \<open>a \<in> S\<close>
apply (simp add: homotopic_with_def)
apply (rule_tac x="\<lambda>y. (1 - (fst y)) *\<^sub>R snd y + (fst y) *\<^sub>R a" in exI)
- apply (intro conjI ballI continuous_on_compose continuous_intros)
- apply (simp_all add: P)
+ apply (intro conjI ballI continuous_on_compose continuous_intros; simp add: P)
done
+ then show ?thesis
+ using that by blast
qed
lemma starlike_imp_contractible:
@@ -1549,9 +1562,7 @@
next
case False
show ?thesis
- apply (rule starlike_imp_contractible)
- apply (rule starlike_convex_tweak_boundary_points [OF \<open>convex S\<close> False TS])
- done
+ by (meson False assms starlike_convex_tweak_boundary_points starlike_imp_contractible)
qed
lemma convex_imp_contractible:
@@ -1627,14 +1638,10 @@
lemma locally_open_subset:
assumes "locally P S" "openin (top_of_set S) t"
shows "locally P t"
-using assms
-apply (simp add: locally_def)
-apply (erule all_forward)+
-apply (rule impI)
-apply (erule impCE)
- using openin_trans apply blast
-apply (erule ex_forward)
-by (metis (no_types, hide_lams) Int_absorb1 Int_lower1 Int_subset_iff openin_open openin_subtopology_Int_subset)
+ using assms
+ unfolding locally_def
+ apply (elim all_forward)
+ by (meson dual_order.trans openin_imp_subset openin_subset_trans openin_trans)
lemma locally_diff_closed:
"\<lbrakk>locally P S; closedin (top_of_set S) t\<rbrakk> \<Longrightarrow> locally P (S - t)"
@@ -1651,27 +1658,32 @@
lemma locally_iff:
"locally P S \<longleftrightarrow>
- (\<forall>T x. open T \<and> x \<in> S \<inter> T \<longrightarrow> (\<exists>U. open U \<and> (\<exists>v. P v \<and> x \<in> S \<inter> U \<and> S \<inter> U \<subseteq> v \<and> v \<subseteq> S \<inter> T)))"
+ (\<forall>T x. open T \<and> x \<in> S \<inter> T \<longrightarrow> (\<exists>U. open U \<and> (\<exists>V. P V \<and> x \<in> S \<inter> U \<and> S \<inter> U \<subseteq> V \<and> V \<subseteq> S \<inter> T)))"
apply (simp add: le_inf_iff locally_def openin_open, safe)
apply (metis IntE IntI le_inf_iff)
apply (metis IntI Int_subset_iff)
done
lemma locally_Int:
- assumes S: "locally P S" and t: "locally P t"
- and P: "\<And>S t. P S \<and> P t \<Longrightarrow> P(S \<inter> t)"
- shows "locally P (S \<inter> t)"
-using S t unfolding locally_iff
-apply clarify
-apply (drule_tac x=T in spec)+
-apply (drule_tac x=x in spec)+
-apply clarsimp
-apply (rename_tac U1 U2 V1 V2)
-apply (rule_tac x="U1 \<inter> U2" in exI)
-apply (simp add: open_Int)
-apply (rule_tac x="V1 \<inter> V2" in exI)
-apply (auto intro: P)
- done
+ assumes S: "locally P S" and T: "locally P T"
+ and P: "\<And>S T. P S \<and> P T \<Longrightarrow> P(S \<inter> T)"
+ shows "locally P (S \<inter> T)"
+ unfolding locally_iff
+proof clarify
+ fix A x
+ assume "open A" "x \<in> A" "x \<in> S" "x \<in> T"
+ then obtain U1 V1 U2 V2
+ where "open U1" "P V1" "x \<in> S \<inter> U1" "S \<inter> U1 \<subseteq> V1 \<and> V1 \<subseteq> S \<inter> A"
+ "open U2" "P V2" "x \<in> T \<inter> U2" "T \<inter> U2 \<subseteq> V2 \<and> V2 \<subseteq> T \<inter> A"
+ using S T unfolding locally_iff by (meson IntI)
+ then have "S \<inter> T \<inter> (U1 \<inter> U2) \<subseteq> V1 \<inter> V2" "V1 \<inter> V2 \<subseteq> S \<inter> T \<inter> A" "x \<in> S \<inter> T \<inter> (U1 \<inter> U2)"
+ by blast+
+ moreover have "P (V1 \<inter> V2)"
+ by (simp add: P \<open>P V1\<close> \<open>P V2\<close>)
+ ultimately show "\<exists>U. open U \<and> (\<exists>V. P V \<and> x \<in> S \<inter> T \<inter> U \<and> S \<inter> T \<inter> U \<subseteq> V \<and> V \<subseteq> S \<inter> T \<inter> A)"
+ using \<open>open U1\<close> \<open>open U2\<close> by blast
+qed
+
lemma locally_Times:
fixes S :: "('a::metric_space) set" and T :: "('b::metric_space) set"
@@ -1697,73 +1709,73 @@
proposition homeomorphism_locally_imp:
- fixes S :: "'a::metric_space set" and t :: "'b::t2_space set"
- assumes S: "locally P S" and hom: "homeomorphism S t f g"
+ fixes S :: "'a::metric_space set" and T :: "'b::t2_space set"
+ assumes S: "locally P S" and hom: "homeomorphism S T f g"
and Q: "\<And>S S'. \<lbrakk>P S; homeomorphism S S' f g\<rbrakk> \<Longrightarrow> Q S'"
- shows "locally Q t"
+ shows "locally Q T"
proof (clarsimp simp: locally_def)
fix W y
- assume "y \<in> W" and "openin (top_of_set t) W"
- then obtain T where T: "open T" "W = t \<inter> T"
+ assume "y \<in> W" and "openin (top_of_set T) W"
+ then obtain A where T: "open A" "W = T \<inter> A"
by (force simp: openin_open)
- then have "W \<subseteq> t" by auto
- have f: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "f ` S = t" "continuous_on S f"
- and g: "\<And>y. y \<in> t \<Longrightarrow> f(g y) = y" "g ` t = S" "continuous_on t g"
+ then have "W \<subseteq> T" by auto
+ have f: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "f ` S = T" "continuous_on S f"
+ and g: "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y" "g ` T = S" "continuous_on T g"
using hom by (auto simp: homeomorphism_def)
have gw: "g ` W = S \<inter> f -` W"
- using \<open>W \<subseteq> t\<close>
- apply auto
- using \<open>g ` t = S\<close> \<open>W \<subseteq> t\<close> apply blast
- using g \<open>W \<subseteq> t\<close> apply auto[1]
- by (simp add: f rev_image_eqI)
+ using \<open>W \<subseteq> T\<close> g by force
have \<circ>: "openin (top_of_set S) (g ` W)"
proof -
have "continuous_on S f"
using f(3) by blast
then show "openin (top_of_set S) (g ` W)"
- by (simp add: gw Collect_conj_eq \<open>openin (top_of_set t) W\<close> continuous_on_open f(2))
+ by (simp add: gw Collect_conj_eq \<open>openin (top_of_set T) W\<close> continuous_on_open f(2))
qed
- then obtain u v
- where osu: "openin (top_of_set S) u" and uv: "P v" "g y \<in> u" "u \<subseteq> v" "v \<subseteq> g ` W"
+ then obtain U V
+ where osu: "openin (top_of_set S) U" and uv: "P V" "g y \<in> U" "U \<subseteq> V" "V \<subseteq> g ` W"
using S [unfolded locally_def, rule_format, of "g ` W" "g y"] \<open>y \<in> W\<close> by force
- have "v \<subseteq> S" using uv by (simp add: gw)
- have fv: "f ` v = t \<inter> {x. g x \<in> v}"
- using \<open>f ` S = t\<close> f \<open>v \<subseteq> S\<close> by auto
- have "f ` v \<subseteq> W"
+ have "V \<subseteq> S" using uv by (simp add: gw)
+ have fv: "f ` V = T \<inter> {x. g x \<in> V}"
+ using \<open>f ` S = T\<close> f \<open>V \<subseteq> S\<close> by auto
+ have "f ` V \<subseteq> W"
using uv using Int_lower2 gw image_subsetI mem_Collect_eq subset_iff by auto
- have contvf: "continuous_on v f"
- using \<open>v \<subseteq> S\<close> continuous_on_subset f(3) by blast
- have contvg: "continuous_on (f ` v) g"
- using \<open>f ` v \<subseteq> W\<close> \<open>W \<subseteq> t\<close> continuous_on_subset [OF g(3)] by blast
- have homv: "homeomorphism v (f ` v) f g"
- using \<open>v \<subseteq> S\<close> \<open>W \<subseteq> t\<close> f
- apply (simp add: homeomorphism_def contvf contvg, auto)
- by (metis f(1) rev_image_eqI rev_subsetD)
- have 1: "openin (top_of_set t) (t \<inter> g -` u)"
- apply (rule continuous_on_open [THEN iffD1, rule_format])
- apply (rule \<open>continuous_on t g\<close>)
- using \<open>g ` t = S\<close> apply (simp add: osu)
+ have contvf: "continuous_on V f"
+ using \<open>V \<subseteq> S\<close> continuous_on_subset f(3) by blast
+ have contvg: "continuous_on (f ` V) g"
+ using \<open>f ` V \<subseteq> W\<close> \<open>W \<subseteq> T\<close> continuous_on_subset [OF g(3)] by blast
+ have "V \<subseteq> g ` f ` V"
+ by (metis hom homeomorphism_def homeomorphism_of_subsets set_eq_subset \<open>V \<subseteq> S\<close>)
+ then have homv: "homeomorphism V (f ` V) f g"
+ using \<open>V \<subseteq> S\<close> f by (auto simp add: homeomorphism_def contvf contvg)
+ have "openin (top_of_set (g ` T)) U"
+ using \<open>g ` T = S\<close> by (simp add: osu)
+ then have 1: "openin (top_of_set T) (T \<inter> g -` U)"
+ using \<open>continuous_on T g\<close> continuous_on_open [THEN iffD1] by blast
+ have 2: "\<exists>V. Q V \<and> y \<in> (T \<inter> g -` U) \<and> (T \<inter> g -` U) \<subseteq> V \<and> V \<subseteq> W"
+ apply (rule_tac x="f ` V" in exI)
+ apply (intro conjI Q [OF \<open>P V\<close> homv])
+ using \<open>W \<subseteq> T\<close> \<open>y \<in> W\<close> \<open>f ` V \<subseteq> W\<close> uv apply (auto simp: fv)
done
- have 2: "\<exists>V. Q V \<and> y \<in> (t \<inter> g -` u) \<and> (t \<inter> g -` u) \<subseteq> V \<and> V \<subseteq> W"
- apply (rule_tac x="f ` v" in exI)
- apply (intro conjI Q [OF \<open>P v\<close> homv])
- using \<open>W \<subseteq> t\<close> \<open>y \<in> W\<close> \<open>f ` v \<subseteq> W\<close> uv apply (auto simp: fv)
- done
- show "\<exists>U. openin (top_of_set t) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
+ show "\<exists>U. openin (top_of_set T) U \<and> (\<exists>v. Q v \<and> y \<in> U \<and> U \<subseteq> v \<and> v \<subseteq> W)"
by (meson 1 2)
qed
lemma homeomorphism_locally:
fixes f:: "'a::metric_space \<Rightarrow> 'b::metric_space"
- assumes hom: "homeomorphism S t f g"
- and eq: "\<And>S t. homeomorphism S t f g \<Longrightarrow> (P S \<longleftrightarrow> Q t)"
- shows "locally P S \<longleftrightarrow> locally Q t"
-apply (rule iffI)
-apply (erule homeomorphism_locally_imp [OF _ hom])
-apply (simp add: eq)
-apply (erule homeomorphism_locally_imp)
-using eq homeomorphism_sym homeomorphism_symD [OF hom] apply blast+
-done
+ assumes hom: "homeomorphism S T f g"
+ and eq: "\<And>S T. homeomorphism S T f g \<Longrightarrow> (P S \<longleftrightarrow> Q T)"
+ shows "locally P S \<longleftrightarrow> locally Q T"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ using eq hom homeomorphism_locally_imp by blast
+next
+ assume ?rhs
+ then show ?lhs
+ using eq homeomorphism_sym homeomorphism_symD [OF hom]
+ by (blast intro: homeomorphism_locally_imp)
+qed
lemma homeomorphic_locally:
fixes S:: "'a::metric_space set" and T:: "'b::metric_space set"
@@ -1785,28 +1797,23 @@
lemma locally_translation:
fixes P :: "'a :: real_normed_vector set \<Rightarrow> bool"
- shows
- "(\<And>S. P (image (\<lambda>x. a + x) S) \<longleftrightarrow> P S)
- \<Longrightarrow> locally P (image (\<lambda>x. a + x) S) \<longleftrightarrow> locally P S"
+ shows "(\<And>S. P ((+) a ` S) = P S) \<Longrightarrow> locally P ((+) a ` S) = locally P S"
apply (rule homeomorphism_locally [OF homeomorphism_translation])
-apply (simp add: homeomorphism_def)
-by metis
+ by (metis (no_types) homeomorphism_def)
lemma locally_injective_linear_image:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
assumes f: "linear f" "inj f" and iff: "\<And>S. P (f ` S) \<longleftrightarrow> Q S"
- shows "locally P (f ` S) \<longleftrightarrow> locally Q S"
-apply (rule linear_homeomorphism_image [OF f])
-apply (rule_tac f=g and g = f in homeomorphism_locally, assumption)
-by (metis iff homeomorphism_def)
+ shows "locally P (f ` S) \<longleftrightarrow> locally Q S"
+ using homeomorphism_locally [of "f`S" _ _ f] linear_homeomorphism_image [OF f]
+ by (metis (no_types, lifting) homeomorphism_image2 iff)
lemma locally_open_map_image:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes P: "locally P S"
and f: "continuous_on S f"
- and oo: "\<And>t. openin (top_of_set S) t
- \<Longrightarrow> openin (top_of_set (f ` S)) (f ` t)"
- and Q: "\<And>t. \<lbrakk>t \<subseteq> S; P t\<rbrakk> \<Longrightarrow> Q(f ` t)"
+ and oo: "\<And>T. openin (top_of_set S) T \<Longrightarrow> openin (top_of_set (f ` S)) (f ` T)"
+ and Q: "\<And>T. \<lbrakk>T \<subseteq> S; P T\<rbrakk> \<Longrightarrow> Q(f ` T)"
shows "locally Q (f ` S)"
proof (clarsimp simp add: locally_def)
fix W y
@@ -1820,12 +1827,10 @@
where "openin (top_of_set S) U" "P V" "x \<in> U" "U \<subseteq> V" "V \<subseteq> S \<inter> f -` W"
using P [unfolded locally_def, rule_format, of "(S \<inter> f -` W)" x] oivf \<open>y \<in> W\<close>
by auto
+ then have "openin (top_of_set (f ` S)) (f ` U)"
+ by (simp add: oo)
then show "\<exists>X. openin (top_of_set (f ` S)) X \<and> (\<exists>Y. Q Y \<and> y \<in> X \<and> X \<subseteq> Y \<and> Y \<subseteq> W)"
- apply (rule_tac x="f ` U" in exI)
- apply (rule conjI, blast intro!: oo)
- apply (rule_tac x="f ` V" in exI)
- apply (force simp: \<open>f x = y\<close> rev_image_eqI intro: Q)
- done
+ using Q \<open>P V\<close> \<open>U \<subseteq> V\<close> \<open>V \<subseteq> S \<inter> f -` W\<close> \<open>f x = y\<close> \<open>x \<in> U\<close> by blast
qed
@@ -1840,28 +1845,25 @@
and etc: "a \<in> S" "b \<in> S" "P a" "P b" "Q a"
shows "Q b"
proof -
- have 1: "openin (top_of_set S)
- {b. \<exists>T. openin (top_of_set S) T \<and>
- b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
+ let ?A = "{b. \<exists>T. openin (top_of_set S) T \<and> b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> Q x)}"
+ let ?B = "{b. \<exists>T. openin (top_of_set S) T \<and> b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> \<not> Q x)}"
+ have 1: "openin (top_of_set S) ?A"
+ apply (subst openin_subopen, clarify)
+ apply (rule_tac x=T in exI, auto)
+ done
+ have 2: "openin (top_of_set S) ?B"
apply (subst openin_subopen, clarify)
apply (rule_tac x=T in exI, auto)
done
- have 2: "openin (top_of_set S)
- {b. \<exists>T. openin (top_of_set S) T \<and>
- b \<in> T \<and> (\<forall>x\<in>T. P x \<longrightarrow> \<not> Q x)}"
- apply (subst openin_subopen, clarify)
- apply (rule_tac x=T in exI, auto)
- done
- show ?thesis
- using \<open>connected S\<close>
- apply (simp only: connected_openin HOL.not_ex HOL.de_Morgan_conj)
- apply (elim disjE allE)
- apply (blast intro: 1)
- apply (blast intro: 2, simp_all)
- apply clarify apply (metis opI)
- using opD apply (blast intro: etc elim: dest:)
- using opI etc apply meson+
- done
+ have \<section>: "?A \<inter> ?B = {}"
+ by (clarsimp simp: set_eq_iff) (metis (no_types, hide_lams) Int_iff opD openin_Int)
+ have *: "S \<subseteq> ?A \<union> ?B"
+ by clarsimp (meson opI)
+ have "?A = {} \<or> ?B = {}"
+ using \<open>connected S\<close> [unfolded connected_openin, simplified, rule_format, OF 1 \<section> * 2]
+ by blast
+ then show ?thesis
+ by clarsimp (meson opI etc)
qed
lemma connected_equivalence_relation_gen:
@@ -1969,26 +1971,25 @@
qed
lemma locally_compactE:
- fixes s :: "'a :: metric_space set"
- assumes "locally compact s"
- obtains u v where "\<And>x. x \<in> s \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> s \<and>
- openin (top_of_set s) (u x) \<and> compact (v x)"
-using assms
-unfolding locally_compact by metis
+ fixes S :: "'a :: metric_space set"
+ assumes "locally compact S"
+ obtains u v where "\<And>x. x \<in> S \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> S \<and>
+ openin (top_of_set S) (u x) \<and> compact (v x)"
+ using assms unfolding locally_compact by metis
lemma locally_compact_alt:
- fixes s :: "'a :: heine_borel set"
- shows "locally compact s \<longleftrightarrow>
- (\<forall>x \<in> s. \<exists>u. x \<in> u \<and>
- openin (top_of_set s) u \<and> compact(closure u) \<and> closure u \<subseteq> s)"
-apply (simp add: locally_compact)
-apply (intro ball_cong ex_cong refl iffI)
-apply (metis bounded_subset closure_eq closure_mono compact_eq_bounded_closed dual_order.trans)
-by (meson closure_subset compact_closure)
+ fixes S :: "'a :: heine_borel set"
+ shows "locally compact S \<longleftrightarrow>
+ (\<forall>x \<in> S. \<exists>u. x \<in> u \<and>
+ openin (top_of_set S) u \<and> compact(closure u) \<and> closure u \<subseteq> S)"
+ apply (simp add: locally_compact)
+ apply (intro ball_cong ex_cong refl iffI)
+ apply (meson bounded_subset closure_minimal compact_eq_bounded_closed dual_order.trans)
+ by (meson closure_subset compact_closure)
lemma locally_compact_Int_cball:
- fixes s :: "'a :: heine_borel set"
- shows "locally compact s \<longleftrightarrow> (\<forall>x \<in> s. \<exists>e. 0 < e \<and> closed(cball x e \<inter> s))"
+ fixes S :: "'a :: heine_borel set"
+ shows "locally compact S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>e. 0 < e \<and> closed(cball x e \<inter> S))"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -2001,8 +2002,8 @@
then show ?lhs
apply (simp add: locally_compact openin_contains_cball)
apply (clarify | assumption | drule bspec)+
- apply (rule_tac x="ball x e \<inter> s" in exI, simp)
- apply (rule_tac x="cball x e \<inter> s" in exI)
+ apply (rule_tac x="ball x e \<inter> S" in exI, simp)
+ apply (rule_tac x="cball x e \<inter> S" in exI)
using compact_eq_bounded_closed
apply auto
apply (metis open_ball le_infI1 mem_ball open_contains_cball_eq)
@@ -2010,20 +2011,20 @@
qed
lemma locally_compact_compact:
- fixes s :: "'a :: heine_borel set"
- shows "locally compact s \<longleftrightarrow>
- (\<forall>k. k \<subseteq> s \<and> compact k
- \<longrightarrow> (\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
- openin (top_of_set s) u \<and> compact v))"
+ fixes S :: "'a :: heine_borel set"
+ shows "locally compact S \<longleftrightarrow>
+ (\<forall>k. k \<subseteq> S \<and> compact k
+ \<longrightarrow> (\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and>
+ openin (top_of_set S) u \<and> compact v))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then obtain u v where
- uv: "\<And>x. x \<in> s \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> s \<and>
- openin (top_of_set s) (u x) \<and> compact (v x)"
+ uv: "\<And>x. x \<in> S \<Longrightarrow> x \<in> u x \<and> u x \<subseteq> v x \<and> v x \<subseteq> S \<and>
+ openin (top_of_set S) (u x) \<and> compact (v x)"
by (metis locally_compactE)
- have *: "\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (top_of_set s) u \<and> compact v"
- if "k \<subseteq> s" "compact k" for k
+ have *: "\<exists>u v. k \<subseteq> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and> openin (top_of_set S) u \<and> compact v"
+ if "k \<subseteq> S" "compact k" for k
proof -
have "\<And>C. (\<forall>c\<in>C. openin (top_of_set k) c) \<and> k \<subseteq> \<Union>C \<Longrightarrow>
\<exists>D\<subseteq>C. finite D \<and> k \<subseteq> \<Union>D"
@@ -2041,9 +2042,7 @@
show ?thesis
apply (rule_tac x="\<Union>(u ` T)" in exI)
apply (rule_tac x="\<Union>(v ` T)" in exI)
- apply (simp add: Tuv)
- using T that
- apply (auto simp: dest!: uv)
+ using T that apply (auto simp: Tuv dest!: uv)
done
qed
show ?rhs
@@ -2057,43 +2056,42 @@
qed
lemma open_imp_locally_compact:
- fixes s :: "'a :: heine_borel set"
- assumes "open s"
- shows "locally compact s"
+ fixes S :: "'a :: heine_borel set"
+ assumes "open S"
+ shows "locally compact S"
proof -
- have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and> openin (top_of_set s) u \<and> compact v"
- if "x \<in> s" for x
+ have *: "\<exists>U V. x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> S \<and> openin (top_of_set S) U \<and> compact V"
+ if "x \<in> S" for x
proof -
- obtain e where "e>0" and e: "cball x e \<subseteq> s"
- using open_contains_cball assms \<open>x \<in> s\<close> by blast
- have ope: "openin (top_of_set s) (ball x e)"
+ obtain e where "e>0" and e: "cball x e \<subseteq> S"
+ using open_contains_cball assms \<open>x \<in> S\<close> by blast
+ have ope: "openin (top_of_set S) (ball x e)"
by (meson e open_ball ball_subset_cball dual_order.trans open_subset)
show ?thesis
- apply (rule_tac x="ball x e" in exI)
- apply (rule_tac x="cball x e" in exI)
- using \<open>e > 0\<close> e apply (auto simp: ope)
- done
+ proof (intro exI conjI)
+ let ?U = "ball x e"
+ let ?V = "cball x e"
+ show "x \<in> ?U" "?U \<subseteq> ?V" "?V \<subseteq> S" "compact ?V"
+ using \<open>e > 0\<close> e by auto
+ show "openin (top_of_set S) ?U"
+ using ope by blast
+ qed
qed
show ?thesis
- unfolding locally_compact
- by (blast intro: *)
+ unfolding locally_compact by (blast intro: *)
qed
lemma closed_imp_locally_compact:
- fixes s :: "'a :: heine_borel set"
- assumes "closed s"
- shows "locally compact s"
+ fixes S :: "'a :: heine_borel set"
+ assumes "closed S"
+ shows "locally compact S"
proof -
- have *: "\<exists>u v. x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> s \<and>
- openin (top_of_set s) u \<and> compact v"
- if "x \<in> s" for x
- proof -
- show ?thesis
- apply (rule_tac x = "s \<inter> ball x 1" in exI)
- apply (rule_tac x = "s \<inter> cball x 1" in exI)
- using \<open>x \<in> s\<close> assms apply auto
- done
- qed
+ have *: "\<exists>U V. x \<in> U \<and> U \<subseteq> V \<and> V \<subseteq> S \<and> openin (top_of_set S) U \<and> compact V"
+ if "x \<in> S" for x
+ apply (rule_tac x = "S \<inter> ball x 1" in exI)
+ apply (rule_tac x = "S \<inter> cball x 1" in exI)
+ using \<open>x \<in> S\<close> assms apply auto
+ done
show ?thesis
unfolding locally_compact
by (blast intro: *)
@@ -2103,25 +2101,25 @@
by (simp add: closed_imp_locally_compact)
lemma locally_compact_Int:
- fixes s :: "'a :: t2_space set"
- shows "\<lbrakk>locally compact s; locally compact t\<rbrakk> \<Longrightarrow> locally compact (s \<inter> t)"
+ fixes S :: "'a :: t2_space set"
+ shows "\<lbrakk>locally compact S; locally compact t\<rbrakk> \<Longrightarrow> locally compact (S \<inter> t)"
by (simp add: compact_Int locally_Int)
lemma locally_compact_closedin:
- fixes s :: "'a :: heine_borel set"
- shows "\<lbrakk>closedin (top_of_set s) t; locally compact s\<rbrakk>
+ fixes S :: "'a :: heine_borel set"
+ shows "\<lbrakk>closedin (top_of_set S) t; locally compact S\<rbrakk>
\<Longrightarrow> locally compact t"
-unfolding closedin_closed
-using closed_imp_locally_compact locally_compact_Int by blast
+ unfolding closedin_closed
+ using closed_imp_locally_compact locally_compact_Int by blast
lemma locally_compact_delete:
- fixes s :: "'a :: t1_space set"
- shows "locally compact s \<Longrightarrow> locally compact (s - {a})"
+ fixes S :: "'a :: t1_space set"
+ shows "locally compact S \<Longrightarrow> locally compact (S - {a})"
by (auto simp: openin_delete locally_open_subset)
lemma locally_closed:
- fixes s :: "'a :: heine_borel set"
- shows "locally closed s \<longleftrightarrow> locally compact s"
+ fixes S :: "'a :: heine_borel set"
+ shows "locally closed S \<longleftrightarrow> locally compact S"
(is "?lhs = ?rhs")
proof
assume ?lhs
@@ -2345,10 +2343,8 @@
and cloV2: "closedin (top_of_set D) (D \<inter> closure V2)"
by (simp_all add: closedin_closed_Int)
moreover have "D \<inter> closure V1 = D \<inter> V1" "D \<inter> closure V2 = D \<inter> V2"
- apply safe
using \<open>D \<subseteq> V1 \<union> V2\<close> \<open>open V1\<close> \<open>open V2\<close> V12
- apply (simp_all add: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
- done
+ by (auto simp add: closure_subset [THEN subsetD] closure_iff_nhds_not_empty, blast+)
ultimately have cloDV1: "closedin (top_of_set D) (D \<inter> V1)"
and cloDV2: "closedin (top_of_set D) (D \<inter> V2)"
by metis+
@@ -2360,10 +2356,12 @@
assume "D \<inter> U1 \<inter> C = {}"
then have *: "C \<subseteq> D \<inter> V2"
using D1 DV12 \<open>C \<subseteq> D\<close> by auto
- have "\<Inter>?\<T> \<subseteq> D \<inter> V2"
- apply (rule Inter_lower)
- using * apply simp
- by (meson cloDV2 \<open>open V2\<close> cloD closedin_trans le_inf_iff opeD openin_Int_open)
+ have 1: "openin (top_of_set S) (D \<inter> V2)"
+ by (simp add: \<open>open V2\<close> opeD openin_Int_open)
+ have 2: "closedin (top_of_set S) (D \<inter> V2)"
+ using cloD cloDV2 closedin_trans by blast
+ have "\<Inter> ?\<T> \<subseteq> D \<inter> V2"
+ by (rule Inter_lower) (use * 1 2 in simp)
then show False
using K1 V12 \<open>K1 \<noteq> {}\<close> \<open>K1 \<subseteq> V1\<close> closedin_imp_subset by blast
qed
@@ -2372,18 +2370,17 @@
assume "D \<inter> U2 \<inter> C = {}"
then have *: "C \<subseteq> D \<inter> V1"
using D2 DV12 \<open>C \<subseteq> D\<close> by auto
+ have 1: "openin (top_of_set S) (D \<inter> V1)"
+ by (simp add: \<open>open V1\<close> opeD openin_Int_open)
+ have 2: "closedin (top_of_set S) (D \<inter> V1)"
+ using cloD cloDV1 closedin_trans by blast
have "\<Inter>?\<T> \<subseteq> D \<inter> V1"
- apply (rule Inter_lower)
- using * apply simp
- by (meson cloDV1 \<open>open V1\<close> cloD closedin_trans le_inf_iff opeD openin_Int_open)
+ by (rule Inter_lower) (use * 1 2 in simp)
then show False
using K2 V12 \<open>K2 \<noteq> {}\<close> \<open>K2 \<subseteq> V2\<close> closedin_imp_subset by blast
qed
ultimately show False
- using \<open>connected C\<close> unfolding connected_closed
- apply (simp only: not_ex)
- apply (drule_tac x="D \<inter> U1" in spec)
- apply (drule_tac x="D \<inter> U2" in spec)
+ using \<open>connected C\<close> [unfolded connected_closed, simplified, rule_format, of concl: "D \<inter> U1" "D \<inter> U2"]
using \<open>C \<subseteq> D\<close> D1 D2 V12 DV12 \<open>closed U1\<close> \<open>closed U2\<close> \<open>closed D\<close>
by blast
qed
@@ -2617,7 +2614,7 @@
have "path_component v x x"
by (meson assms(3) path_component_refl)
then show ?thesis
- by (metis assms(1) assms(2) assms(3) mem_Collect_eq path_component_subset path_connected_path_component)
+ by (metis assms mem_Collect_eq path_component_subset path_connected_path_component)
qed
proposition locally_path_connected:
@@ -3415,10 +3412,11 @@
apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
using Q by (auto simp: contk imk)
then show ?thesis
- apply (rule homotopic_with_eq)
- using feq apply auto[1]
- using geq apply auto[1]
- using Qeq topspace_euclidean_subtopology by blast
+ proof (rule homotopic_with_eq)
+ show "f x = (f \<circ> h \<circ> k) x" "g x = (g \<circ> h \<circ> k) x"
+ if "x \<in> topspace (top_of_set t)" for x
+ using feq geq that by force+
+ qed (use Qeq topspace_euclidean_subtopology in blast)
qed
lemma cohomotopically_trivial_retraction_null_gen:
@@ -3439,15 +3437,15 @@
by (simp add: P Qf contf imf)
ultimately obtain c where "homotopic_with_canon P s u (f \<circ> h) (\<lambda>x. c)"
by (metis hom)
- then have "homotopic_with_canon Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
- apply (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
- using Q by (auto simp: contk imk)
- then show ?thesis
- apply (rule_tac c = c in that)
- apply (erule homotopic_with_eq)
- using feq apply auto[1]
- apply simp
- using Qeq topspace_euclidean_subtopology by blast
+ then have \<section>: "homotopic_with_canon Q t u (f \<circ> h \<circ> k) ((\<lambda>x. c) \<circ> k)"
+ proof (rule homotopic_with_compose_continuous_right [OF homotopic_with_mono])
+ show "\<And>h. \<lbrakk>continuous_map (top_of_set s) (top_of_set u) h; P h\<rbrakk> \<Longrightarrow> Q (h \<circ> k)"
+ using Q by auto
+ qed (auto simp: contk imk)
+ moreover have "homotopic_with_canon Q t u f (\<lambda>x. c)"
+ using homotopic_with_eq [OF \<section>] feq Qeq by fastforce
+ ultimately show ?thesis
+ using that by blast
qed
end