--- a/src/HOL/Analysis/Homeomorphism.thy Thu Jan 17 16:22:21 2019 -0500
+++ b/src/HOL/Analysis/Homeomorphism.thy Thu Jan 17 16:28:07 2019 -0500
@@ -8,7 +8,7 @@
imports Homotopy
begin
-lemma%unimportant homeomorphic_spheres':
+lemma homeomorphic_spheres':
fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
assumes "0 < \<delta>" and dimeq: "DIM('a) = DIM('b)"
shows "(sphere a \<delta>) homeomorphic (sphere b \<delta>)"
@@ -28,7 +28,7 @@
done
qed
-lemma%unimportant homeomorphic_spheres_gen:
+lemma homeomorphic_spheres_gen:
fixes a :: "'a::euclidean_space" and b :: "'b::euclidean_space"
assumes "0 < r" "0 < s" "DIM('a::euclidean_space) = DIM('b::euclidean_space)"
shows "(sphere a r homeomorphic sphere b s)"
@@ -38,7 +38,7 @@
subsection%important \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
-proposition%important ray_to_rel_frontier:
+proposition ray_to_rel_frontier:
fixes a :: "'a::real_inner"
assumes "bounded S"
and a: "a \<in> rel_interior S"
@@ -46,7 +46,7 @@
and "l \<noteq> 0"
obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> rel_frontier S"
"\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> rel_interior S"
-proof%unimportant -
+proof -
have aaff: "a \<in> affine hull S"
by (meson a hull_subset rel_interior_subset rev_subsetD)
let ?D = "{d. 0 < d \<and> a + d *\<^sub>R l \<notin> rel_interior S}"
@@ -139,14 +139,14 @@
by (rule that [OF \<open>0 < d\<close> infront inint])
qed
-corollary%important ray_to_frontier:
+corollary ray_to_frontier:
fixes a :: "'a::euclidean_space"
assumes "bounded S"
and a: "a \<in> interior S"
and "l \<noteq> 0"
obtains d where "0 < d" "(a + d *\<^sub>R l) \<in> frontier S"
"\<And>e. \<lbrakk>0 \<le> e; e < d\<rbrakk> \<Longrightarrow> (a + e *\<^sub>R l) \<in> interior S"
-proof%unimportant -
+proof -
have "interior S = rel_interior S"
using a rel_interior_nonempty_interior by auto
then have "a \<in> rel_interior S"
@@ -158,7 +158,7 @@
qed
-lemma%unimportant segment_to_rel_frontier_aux:
+lemma segment_to_rel_frontier_aux:
fixes x :: "'a::euclidean_space"
assumes "convex S" "bounded S" and x: "x \<in> rel_interior S" and y: "y \<in> S" and xy: "x \<noteq> y"
obtains z where "z \<in> rel_frontier S" "y \<in> closed_segment x z"
@@ -198,7 +198,7 @@
qed
qed
-lemma%unimportant segment_to_rel_frontier:
+lemma segment_to_rel_frontier:
fixes x :: "'a::euclidean_space"
assumes S: "convex S" "bounded S" and x: "x \<in> rel_interior S"
and y: "y \<in> S" and xy: "\<not>(x = y \<and> S = {x})"
@@ -216,11 +216,11 @@
using segment_to_rel_frontier_aux [OF S x y] that by blast
qed
-proposition%important rel_frontier_not_sing:
+proposition rel_frontier_not_sing:
fixes a :: "'a::euclidean_space"
assumes "bounded S"
shows "rel_frontier S \<noteq> {a}"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True then show ?thesis by simp
next
case False
@@ -278,7 +278,7 @@
qed
qed
-proposition%important
+proposition (*FIXME needs name *)
fixes S :: "'a::euclidean_space set"
assumes "compact S" and 0: "0 \<in> rel_interior S"
and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S"
@@ -288,7 +288,7 @@
and starlike_compact_projective2_0:
"S homeomorphic cball 0 1 \<inter> affine hull S"
(is "S homeomorphic ?CBALL")
-proof%unimportant -
+proof -
have starI: "(u *\<^sub>R x) \<in> rel_interior S" if "x \<in> S" "0 \<le> u" "u < 1" for x u
proof (cases "x=0 \<or> u=0")
case True with 0 show ?thesis by force
@@ -540,7 +540,7 @@
done
qed
-corollary%important
+corollary (* FIXME needs name *)
fixes S :: "'a::euclidean_space set"
assumes "compact S" and a: "a \<in> rel_interior S"
and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
@@ -548,7 +548,7 @@
"S - rel_interior S homeomorphic sphere a 1 \<inter> affine hull S"
and starlike_compact_projective2:
"S homeomorphic cball a 1 \<inter> affine hull S"
-proof%unimportant -
+proof -
have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
have 2: "0 \<in> rel_interior ((+) (-a) ` S)"
using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp)
@@ -580,12 +580,12 @@
finally show "S homeomorphic cball a 1 \<inter> affine hull S" .
qed
-corollary%important starlike_compact_projective_special:
+corollary starlike_compact_projective_special:
assumes "compact S"
and cb01: "cball (0::'a::euclidean_space) 1 \<subseteq> S"
and scale: "\<And>x u. \<lbrakk>x \<in> S; 0 \<le> u; u < 1\<rbrakk> \<Longrightarrow> u *\<^sub>R x \<in> S - frontier S"
shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
-proof%unimportant -
+proof -
have "ball 0 1 \<subseteq> interior S"
using cb01 interior_cball interior_mono by blast
then have 0: "0 \<in> rel_interior S"
@@ -604,13 +604,13 @@
using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp
qed
-lemma%important homeomorphic_convex_lemma:
+lemma homeomorphic_convex_lemma:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "compact S" "convex T" "compact T"
and affeq: "aff_dim S = aff_dim T"
shows "(S - rel_interior S) homeomorphic (T - rel_interior T) \<and>
S homeomorphic T"
-proof%unimportant (cases "rel_interior S = {} \<or> rel_interior T = {}")
+proof (cases "rel_interior S = {} \<or> rel_interior T = {}")
case True
then show ?thesis
by (metis Diff_empty affeq \<open>convex S\<close> \<open>convex T\<close> aff_dim_empty homeomorphic_empty rel_interior_eq_empty aff_dim_empty)
@@ -708,7 +708,7 @@
using 1 2 by blast
qed
-lemma%unimportant homeomorphic_convex_compact_sets:
+lemma homeomorphic_convex_compact_sets:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "compact S" "convex T" "compact T"
and affeq: "aff_dim S = aff_dim T"
@@ -716,7 +716,7 @@
using homeomorphic_convex_lemma [OF assms] assms
by (auto simp: rel_frontier_def)
-lemma%unimportant homeomorphic_rel_frontiers_convex_bounded_sets:
+lemma homeomorphic_rel_frontiers_convex_bounded_sets:
fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
assumes "convex S" "bounded S" "convex T" "bounded T"
and affeq: "aff_dim S = aff_dim T"
@@ -729,7 +729,7 @@
text\<open>Including the famous stereoscopic projection of the 3-D sphere to the complex plane\<close>
text\<open>The special case with centre 0 and radius 1\<close>
-lemma%unimportant homeomorphic_punctured_affine_sphere_affine_01:
+lemma homeomorphic_punctured_affine_sphere_affine_01:
assumes "b \<in> sphere 0 1" "affine T" "0 \<in> T" "b \<in> T" "affine p"
and affT: "aff_dim T = aff_dim p + 1"
shows "(sphere 0 1 \<inter> T) - {b} homeomorphic p"
@@ -823,12 +823,12 @@
finally show ?thesis .
qed
-theorem%important homeomorphic_punctured_affine_sphere_affine:
+theorem homeomorphic_punctured_affine_sphere_affine:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" "b \<in> sphere a r" "affine T" "a \<in> T" "b \<in> T" "affine p"
and aff: "aff_dim T = aff_dim p + 1"
shows "(sphere a r \<inter> T) - {b} homeomorphic p"
-proof%unimportant -
+proof -
have "a \<noteq> b" using assms by auto
then have inj: "inj (\<lambda>x::'a. x /\<^sub>R norm (a - b))"
by (simp add: inj_on_def)
@@ -847,14 +847,14 @@
finally show ?thesis .
qed
-corollary%important homeomorphic_punctured_sphere_affine:
+corollary homeomorphic_punctured_sphere_affine:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" and b: "b \<in> sphere a r"
and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
shows "(sphere a r - {b}) homeomorphic T"
using%unimportant homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by%unimportant auto
-corollary%important homeomorphic_punctured_sphere_hyperplane:
+corollary homeomorphic_punctured_sphere_hyperplane:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" and b: "b \<in> sphere a r"
and "c \<noteq> 0"
@@ -864,12 +864,12 @@
apply (auto simp: affine_hyperplane of_nat_diff)
done
-proposition%important homeomorphic_punctured_sphere_affine_gen:
+proposition homeomorphic_punctured_sphere_affine_gen:
fixes a :: "'a :: euclidean_space"
assumes "convex S" "bounded S" and a: "a \<in> rel_frontier S"
and "affine T" and affS: "aff_dim S = aff_dim T + 1"
shows "rel_frontier S - {a} homeomorphic T"
-proof%unimportant -
+proof -
obtain U :: "'a set" where "affine U" "convex U" and affdS: "aff_dim U = aff_dim S"
using choose_affine_subset [OF affine_UNIV aff_dim_geq]
by (meson aff_dim_affine_hull affine_affine_hull affine_imp_convex)
@@ -912,13 +912,13 @@
is homeomorphic to a closed subset of a convex set, and
if the set is locally compact we can take the convex set to be the universe.\<close>
-proposition%important homeomorphic_closedin_convex:
+proposition homeomorphic_closedin_convex:
fixes S :: "'m::euclidean_space set"
assumes "aff_dim S < DIM('n)"
obtains U and T :: "'n::euclidean_space set"
where "convex U" "U \<noteq> {}" "closedin (subtopology euclidean U) T"
"S homeomorphic T"
-proof%unimportant (cases "S = {}")
+proof (cases "S = {}")
case True then show ?thesis
by (rule_tac U=UNIV and T="{}" in that) auto
next
@@ -1009,11 +1009,11 @@
text\<open> Locally compact sets are closed in an open set and are homeomorphic
to an absolutely closed set if we have one more dimension to play with.\<close>
-lemma%important locally_compact_open_Int_closure:
+lemma locally_compact_open_Int_closure:
fixes S :: "'a :: metric_space set"
assumes "locally compact S"
obtains T where "open T" "S = T \<inter> closure S"
-proof%unimportant -
+proof -
have "\<forall>x\<in>S. \<exists>T v u. u = S \<inter> T \<and> x \<in> u \<and> u \<subseteq> v \<and> v \<subseteq> S \<and> open T \<and> compact v"
by (metis assms locally_compact openin_open)
then obtain t v where
@@ -1048,14 +1048,14 @@
qed
-lemma%unimportant locally_compact_closedin_open:
+lemma locally_compact_closedin_open:
fixes S :: "'a :: metric_space set"
assumes "locally compact S"
obtains T where "open T" "closedin (subtopology euclidean T) S"
by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)
-lemma%unimportant locally_compact_homeomorphism_projection_closed:
+lemma locally_compact_homeomorphism_projection_closed:
assumes "locally compact S"
obtains T and f :: "'a \<Rightarrow> 'a :: euclidean_space \<times> 'b :: euclidean_space"
where "closed T" "homeomorphism S T f fst"
@@ -1108,14 +1108,14 @@
done
qed
-lemma%unimportant locally_compact_closed_Int_open:
+lemma locally_compact_closed_Int_open:
fixes S :: "'a :: euclidean_space set"
shows
"locally compact S \<longleftrightarrow> (\<exists>U u. closed U \<and> open u \<and> S = U \<inter> u)"
by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact)
-lemma%unimportant lowerdim_embeddings:
+lemma lowerdim_embeddings:
assumes "DIM('a) < DIM('b)"
obtains f :: "'a::euclidean_space*real \<Rightarrow> 'b::euclidean_space"
and g :: "'b \<Rightarrow> 'a*real"
@@ -1161,11 +1161,11 @@
qed
qed
-proposition%important locally_compact_homeomorphic_closed:
+proposition locally_compact_homeomorphic_closed:
fixes S :: "'a::euclidean_space set"
assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)"
obtains T :: "'b::euclidean_space set" where "closed T" "S homeomorphic T"
-proof%unimportant -
+proof -
obtain U:: "('a*real)set" and h
where "closed U" and homU: "homeomorphism S U h fst"
using locally_compact_homeomorphism_projection_closed assms by metis
@@ -1191,13 +1191,13 @@
qed
-lemma%important homeomorphic_convex_compact_lemma:
+lemma homeomorphic_convex_compact_lemma:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "compact S"
and "cball 0 1 \<subseteq> S"
shows "S homeomorphic (cball (0::'a) 1)"
-proof%unimportant (rule starlike_compact_projective_special[OF assms(2-3)])
+proof (rule starlike_compact_projective_special[OF assms(2-3)])
fix x u
assume "x \<in> S" and "0 \<le> u" and "u < (1::real)"
have "open (ball (u *\<^sub>R x) (1 - u))"
@@ -1223,7 +1223,7 @@
using frontier_def and interior_subset by auto
qed
-proposition%important homeomorphic_convex_compact_cball:
+proposition homeomorphic_convex_compact_cball:
fixes e :: real
and S :: "'a::euclidean_space set"
assumes "convex S"
@@ -1231,7 +1231,7 @@
and "interior S \<noteq> {}"
and "e > 0"
shows "S homeomorphic (cball (b::'a) e)"
-proof%unimportant -
+proof -
obtain a where "a \<in> interior S"
using assms(3) by auto
then obtain d where "d > 0" and d: "cball a d \<subseteq> S"
@@ -1259,7 +1259,7 @@
done
qed
-corollary%important homeomorphic_convex_compact:
+corollary homeomorphic_convex_compact:
fixes S :: "'a::euclidean_space set"
and T :: "'a set"
assumes "convex S" "compact S" "interior S \<noteq> {}"
@@ -1268,7 +1268,7 @@
using assms
by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
-subsection%important\<open>Covering spaces and lifting results for them\<close>
+subsection\<open>Covering spaces and lifting results for them\<close>
definition%important covering_space
:: "'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
@@ -1281,19 +1281,19 @@
pairwise disjnt v \<and>
(\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
-lemma%unimportant covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
+lemma covering_space_imp_continuous: "covering_space c p S \<Longrightarrow> continuous_on c p"
by (simp add: covering_space_def)
-lemma%unimportant covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
+lemma covering_space_imp_surjective: "covering_space c p S \<Longrightarrow> p ` c = S"
by (simp add: covering_space_def)
-lemma%unimportant homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
+lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \<Longrightarrow> covering_space S f T"
apply (simp add: homeomorphism_def covering_space_def, clarify)
apply (rule_tac x=T in exI, simp)
apply (rule_tac x="{S}" in exI, auto)
done
-lemma%unimportant covering_space_local_homeomorphism:
+lemma covering_space_local_homeomorphism:
assumes "covering_space c p S" "x \<in> c"
obtains T u q where "x \<in> T" "openin (subtopology euclidean c) T"
"p x \<in> u" "openin (subtopology euclidean S) u"
@@ -1304,13 +1304,13 @@
by (metis IntI UnionE vimage_eq)
-lemma%important covering_space_local_homeomorphism_alt:
+lemma covering_space_local_homeomorphism_alt:
assumes p: "covering_space c p S" and "y \<in> S"
obtains x T U q where "p x = y"
"x \<in> T" "openin (subtopology euclidean c) T"
"y \<in> U" "openin (subtopology euclidean S) U"
"homeomorphism T U p q"
-proof%unimportant -
+proof -
obtain x where "p x = y" "x \<in> c"
using assms covering_space_imp_surjective by blast
show ?thesis
@@ -1318,11 +1318,11 @@
using that \<open>p x = y\<close> by blast
qed
-proposition%important covering_space_open_map:
+proposition covering_space_open_map:
fixes S :: "'a :: metric_space set" and T :: "'b :: metric_space set"
assumes p: "covering_space c p S" and T: "openin (subtopology euclidean c) T"
shows "openin (subtopology euclidean S) (p ` T)"
-proof%unimportant -
+proof -
have pce: "p ` c = S"
and covs:
"\<And>x. x \<in> S \<Longrightarrow>
@@ -1368,7 +1368,7 @@
with openin_subopen show ?thesis by blast
qed
-lemma%important covering_space_lift_unique_gen:
+lemma covering_space_lift_unique_gen:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes cov: "covering_space c p S"
@@ -1380,7 +1380,7 @@
and fg2: "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
and u_compt: "U \<in> components T" and "a \<in> U" "x \<in> U"
shows "g1 x = g2 x"
-proof%unimportant -
+proof -
have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}"
have "connected U" by (rule in_components_connected [OF u_compt])
@@ -1427,7 +1427,7 @@
using \<open>x \<in> U\<close> by force
qed
-proposition%important covering_space_lift_unique:
+proposition covering_space_lift_unique:
fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
fixes g1 :: "'a \<Rightarrow> 'c::real_normed_vector"
assumes "covering_space c p S"
@@ -1437,10 +1437,10 @@
"continuous_on T g2" "g2 ` T \<subseteq> c" "\<And>x. x \<in> T \<Longrightarrow> f x = p(g2 x)"
"connected T" "a \<in> T" "x \<in> T"
shows "g1 x = g2 x"
- using%unimportant covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
- by%unimportant blast
+ using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
+ by blast
-lemma%unimportant covering_space_locally:
+lemma covering_space_locally:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes loc: "locally \<phi> C" and cov: "covering_space C p S"
and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
@@ -1456,14 +1456,14 @@
qed
-proposition%important covering_space_locally_eq:
+proposition covering_space_locally_eq:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and pim: "\<And>T. \<lbrakk>T \<subseteq> C; \<phi> T\<rbrakk> \<Longrightarrow> \<psi>(p ` T)"
and qim: "\<And>q U. \<lbrakk>U \<subseteq> S; continuous_on U q; \<psi> U\<rbrakk> \<Longrightarrow> \<phi>(q ` U)"
shows "locally \<psi> S \<longleftrightarrow> locally \<phi> C"
(is "?lhs = ?rhs")
-proof%unimportant
+proof
assume L: ?lhs
show ?rhs
proof (rule locallyI)
@@ -1518,7 +1518,7 @@
using cov covering_space_locally pim by blast
qed
-lemma%unimportant covering_space_locally_compact_eq:
+lemma covering_space_locally_compact_eq:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally compact S \<longleftrightarrow> locally compact C"
@@ -1526,7 +1526,7 @@
apply (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
using compact_continuous_image by blast
-lemma%unimportant covering_space_locally_connected_eq:
+lemma covering_space_locally_connected_eq:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally connected S \<longleftrightarrow> locally connected C"
@@ -1534,7 +1534,7 @@
apply (meson connected_continuous_image assms continuous_on_subset covering_space_imp_continuous)
using connected_continuous_image by blast
-lemma%unimportant covering_space_locally_path_connected_eq:
+lemma covering_space_locally_path_connected_eq:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally path_connected S \<longleftrightarrow> locally path_connected C"
@@ -1543,26 +1543,26 @@
using path_connected_continuous_image by blast
-lemma%unimportant covering_space_locally_compact:
+lemma covering_space_locally_compact:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "locally compact C" "covering_space C p S"
shows "locally compact S"
using assms covering_space_locally_compact_eq by blast
-lemma%unimportant covering_space_locally_connected:
+lemma covering_space_locally_connected:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "locally connected C" "covering_space C p S"
shows "locally connected S"
using assms covering_space_locally_connected_eq by blast
-lemma%unimportant covering_space_locally_path_connected:
+lemma covering_space_locally_path_connected:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes "locally path_connected C" "covering_space C p S"
shows "locally path_connected S"
using assms covering_space_locally_path_connected_eq by blast
-proposition%important covering_space_lift_homotopy:
+proposition covering_space_lift_homotopy:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and h :: "real \<times> 'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
@@ -1574,7 +1574,7 @@
"k ` ({0..1} \<times> U) \<subseteq> C"
"\<And>y. y \<in> U \<Longrightarrow> k(0, y) = f y"
"\<And>z. z \<in> {0..1} \<times> U \<Longrightarrow> h z = p(k z)"
-proof%unimportant -
+proof -
have "\<exists>V k. openin (subtopology euclidean U) V \<and> y \<in> V \<and>
continuous_on ({0..1} \<times> V) k \<and> k ` ({0..1} \<times> V) \<subseteq> C \<and>
(\<forall>z \<in> V. k(0, z) = f z) \<and> (\<forall>z \<in> {0..1} \<times> V. h z = p(k z))"
@@ -1912,7 +1912,7 @@
qed (auto simp: contk)
qed
-corollary%important covering_space_lift_homotopy_alt:
+corollary covering_space_lift_homotopy_alt:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and h :: "'c::real_normed_vector \<times> real \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
@@ -1924,7 +1924,7 @@
"k ` (U \<times> {0..1}) \<subseteq> C"
"\<And>y. y \<in> U \<Longrightarrow> k(y, 0) = f y"
"\<And>z. z \<in> U \<times> {0..1} \<Longrightarrow> h z = p(k z)"
-proof%unimportant -
+proof -
have "continuous_on ({0..1} \<times> U) (h \<circ> (\<lambda>z. (snd z, fst z)))"
by (intro continuous_intros continuous_on_subset [OF conth]) auto
then obtain k where contk: "continuous_on ({0..1} \<times> U) k"
@@ -1940,7 +1940,7 @@
done
qed
-corollary%important covering_space_lift_homotopic_function:
+corollary covering_space_lift_homotopic_function:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and g:: "'c::real_normed_vector \<Rightarrow> 'a"
assumes cov: "covering_space C p S"
and contg: "continuous_on U g"
@@ -1948,7 +1948,7 @@
and pgeq: "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
and hom: "homotopic_with (\<lambda>x. True) U S f f'"
obtains g' where "continuous_on U g'" "image g' U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g' y) = f' y"
-proof%unimportant -
+proof -
obtain h where conth: "continuous_on ({0..1::real} \<times> U) h"
and him: "h ` ({0..1} \<times> U) \<subseteq> S"
and h0: "\<And>x. h(0, x) = f x"
@@ -1972,12 +1972,12 @@
qed
qed
-corollary%important covering_space_lift_inessential_function:
+corollary covering_space_lift_inessential_function:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" and U :: "'c::real_normed_vector set"
assumes cov: "covering_space C p S"
and hom: "homotopic_with (\<lambda>x. True) U S f (\<lambda>x. a)"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (cases "U = {}")
+proof (cases "U = {}")
case True
then show ?thesis
using that continuous_on_empty by blast
@@ -1997,14 +1997,14 @@
subsection%important\<open> Lifting of general functions to covering space\<close>
-proposition%important covering_space_lift_path_strong:
+proposition covering_space_lift_path_strong:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" and "a \<in> C"
and "path g" and pag: "path_image g \<subseteq> S" and pas: "pathstart g = p a"
obtains h where "path h" "path_image h \<subseteq> C" "pathstart h = a"
and "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
-proof%unimportant -
+proof -
obtain k:: "real \<times> 'c \<Rightarrow> 'a"
where contk: "continuous_on ({0..1} \<times> {undefined}) k"
and kim: "k ` ({0..1} \<times> {undefined}) \<subseteq> C"
@@ -2033,11 +2033,11 @@
qed
qed
-corollary%important covering_space_lift_path:
+corollary covering_space_lift_path:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S" and "path g" and pig: "path_image g \<subseteq> S"
obtains h where "path h" "path_image h \<subseteq> C" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h t) = g t"
-proof%unimportant -
+proof -
obtain a where "a \<in> C" "pathstart g = p a"
by (metis pig cov covering_space_imp_surjective imageE pathstart_in_path_image subsetCE)
show ?thesis
@@ -2046,7 +2046,7 @@
qed
-proposition%important covering_space_lift_homotopic_paths:
+proposition covering_space_lift_homotopic_paths:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and "path g1" and pig1: "path_image g1 \<subseteq> S"
@@ -2056,7 +2056,7 @@
and "path h2" and pih2: "path_image h2 \<subseteq> C" and ph2: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(h2 t) = g2 t"
and h1h2: "pathstart h1 = pathstart h2"
shows "homotopic_paths C h1 h2"
-proof%unimportant -
+proof -
obtain h :: "real \<times> real \<Rightarrow> 'b"
where conth: "continuous_on ({0..1} \<times> {0..1}) h"
and him: "h ` ({0..1} \<times> {0..1}) \<subseteq> S"
@@ -2117,7 +2117,7 @@
qed
-corollary%important covering_space_monodromy:
+corollary covering_space_monodromy:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and "path g1" and pig1: "path_image g1 \<subseteq> S"
@@ -2131,7 +2131,7 @@
by%unimportant blast
-corollary%important covering_space_lift_homotopic_path:
+corollary covering_space_lift_homotopic_path:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and hom: "homotopic_paths S f f'"
@@ -2140,7 +2140,7 @@
and pgeq: "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g t) = f t"
obtains g' where "path g'" "path_image g' \<subseteq> C"
"pathstart g' = a" "pathfinish g' = b" "\<And>t. t \<in> {0..1} \<Longrightarrow> p(g' t) = f' t"
-proof%unimportant (rule covering_space_lift_path_strong [OF cov, of a f'])
+proof (rule covering_space_lift_path_strong [OF cov, of a f'])
show "a \<in> C"
using a pig by auto
show "path f'" "path_image f' \<subseteq> S"
@@ -2150,7 +2150,7 @@
qed (metis (mono_tags, lifting) assms cov covering_space_monodromy hom homotopic_paths_imp_path homotopic_paths_imp_subset pgeq pig)
-proposition%important covering_space_lift_general:
+proposition covering_space_lift_general:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" and "a \<in> C" "z \<in> U"
@@ -2162,7 +2162,7 @@
pathstart q = a \<and> pathfinish q = a \<and>
homotopic_paths S (f \<circ> r) (p \<circ> q)"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant -
+proof -
have *: "\<exists>g h. path g \<and> path_image g \<subseteq> U \<and>
pathstart g = z \<and> pathfinish g = y \<and>
path h \<and> path_image h \<subseteq> C \<and> pathstart h = a \<and>
@@ -2405,7 +2405,7 @@
qed
-corollary%important covering_space_lift_stronger:
+corollary covering_space_lift_stronger:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
@@ -2415,7 +2415,7 @@
and hom: "\<And>r. \<lbrakk>path r; path_image r \<subseteq> U; pathstart r = z; pathfinish r = z\<rbrakk>
\<Longrightarrow> \<exists>b. homotopic_paths S (f \<circ> r) (linepath b b)"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (rule covering_space_lift_general [OF cov U contf fim feq])
+proof (rule covering_space_lift_general [OF cov U contf fim feq])
fix r
assume "path r" "path_image r \<subseteq> U" "pathstart r = z" "pathfinish r = z"
then obtain b where b: "homotopic_paths S (f \<circ> r) (linepath b b)"
@@ -2432,7 +2432,7 @@
by (force simp: \<open>a \<in> C\<close>)
qed auto
-corollary%important covering_space_lift_strong:
+corollary covering_space_lift_strong:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S" "a \<in> C" "z \<in> U"
@@ -2440,7 +2440,7 @@
and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
and feq: "f z = p a"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "g z = a" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
+proof (rule covering_space_lift_stronger [OF cov _ lpcU contf fim feq])
show "path_connected U"
using scU simply_connected_eq_contractible_loop_some by blast
fix r
@@ -2453,14 +2453,14 @@
by blast
qed blast
-corollary%important covering_space_lift:
+corollary covering_space_lift:
fixes p :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
and f :: "'c::real_normed_vector \<Rightarrow> 'b"
assumes cov: "covering_space C p S"
and U: "simply_connected U" "locally path_connected U"
and contf: "continuous_on U f" and fim: "f ` U \<subseteq> S"
obtains g where "continuous_on U g" "g ` U \<subseteq> C" "\<And>y. y \<in> U \<Longrightarrow> p(g y) = f y"
-proof%unimportant (cases "U = {}")
+proof (cases "U = {}")
case True
with that show ?thesis by auto
next