(* Title: HOL/Analysis/Homeomorphism.thy
Author: LC Paulson (ported from HOL Light)
*)
section \<open>Homeomorphism Theorems\<close>
theory Homeomorphism
imports Homotopy
begin
lemma homeomorphic_spheres':
fixes a ::"'a::euclidean_space" and b ::"'b::euclidean_space"
assumes "0 < \" and dimeq: "DIM('a) = DIM('b)"
shows "(sphere a \) homeomorphic (sphere b \)"
proof -
obtain f :: "'a\'b" and g where "linear f" "linear g"
and fg: "\x. norm(f x) = norm x" "\y. norm(g y) = norm y" "\x. g(f x) = x" "\y. f(g y) = y"
by (blast intro: isomorphisms_UNIV_UNIV [OF dimeq])
then have "continuous_on UNIV f" "continuous_on UNIV g"
using linear_continuous_on linear_linear by blast+
then show ?thesis
unfolding homeomorphic_minimal
apply(rule_tac x="\x. b + f(x - a)" in exI)
apply(rule_tac x="\x. a + g(x - b)" in exI)
using assms
apply (force intro: continuous_intros
continuous_on_compose2 [of _ f] continuous_on_compose2 [of _ g] simp: dist_commute dist_norm fg)
done
qed
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)"
using assms homeomorphic_trans [OF homeomorphic_spheres homeomorphic_spheres'] by auto
subsection \<open>Homeomorphism of all convex compact sets with nonempty interior\<close>
proposition
fixes S :: "'a::euclidean_space set"
assumes "compact S" and 0: "0 \ rel_interior S"
and star: "\x. x \ S \ open_segment 0 x \ rel_interior S"
shows starlike_compact_projective1_0:
"S - rel_interior S homeomorphic sphere 0 1 \ affine hull S"
(is "?SMINUS homeomorphic ?SPHER")
and starlike_compact_projective2_0:
"S homeomorphic cball 0 1 \ affine hull S"
(is "S homeomorphic ?CBALL")
proof -
have starI: "(u *\<^sub>R x) \ rel_interior S" if "x \ S" "0 \ u" "u < 1" for x u
proof (cases "x=0 \ u=0")
case True with 0 show ?thesis by force
next
case False with that show ?thesis
by (auto simp: in_segment intro: star [THEN subsetD])
qed
have "0 \ S" using assms rel_interior_subset by auto
define proj where "proj \ \x::'a. x /\<^sub>R norm x"
have eqI: "x = y" if "proj x = proj y" "norm x = norm y" for x y
using that by (force simp: proj_def)
then have iff_eq: "\x y. (proj x = proj y \ norm x = norm y) \ x = y"
by blast
have projI: "x \ affine hull S \ proj x \ affine hull S" for x
by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_mul proj_def)
have nproj1 [simp]: "x \ 0 \ norm(proj x) = 1" for x
by (simp add: proj_def)
have proj0_iff [simp]: "proj x = 0 \ x = 0" for x
by (simp add: proj_def)
have cont_proj: "continuous_on (UNIV - {0}) proj"
unfolding proj_def by (rule continuous_intros | force)+
have proj_spherI: "\x. \x \ affine hull S; x \ 0\ \ proj x \ ?SPHER"
by (simp add: projI)
have "bounded S" "closed S"
using \<open>compact S\<close> compact_eq_bounded_closed by blast+
have inj_on_proj: "inj_on proj (S - rel_interior S)"
proof
fix x y
assume x: "x \ S - rel_interior S"
and y: "y \ S - rel_interior S" and eq: "proj x = proj y"
then have xynot: "x \ 0" "y \ 0" "x \ S" "y \ S" "x \ rel_interior S" "y \ rel_interior S"
using 0 by auto
consider "norm x = norm y" | "norm x < norm y" | "norm x > norm y" by linarith
then show "x = y"
proof cases
assume "norm x = norm y"
with iff_eq eq show "x = y" by blast
next
assume *: "norm x < norm y"
have "x /\<^sub>R norm x = norm x *\<^sub>R (x /\<^sub>R norm x) /\<^sub>R norm (norm x *\<^sub>R (x /\<^sub>R norm x))"
by force
then have "proj ((norm x / norm y) *\<^sub>R y) = proj x"
by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
then have [simp]: "(norm x / norm y) *\<^sub>R y = x"
by (rule eqI) (simp add: \<open>y \<noteq> 0\<close>)
have no: "0 \ norm x / norm y" "norm x / norm y < 1"
using * by (auto simp: field_split_simps)
then show "x = y"
using starI [OF \<open>y \<in> S\<close> no] xynot by auto
next
assume *: "norm x > norm y"
have "y /\<^sub>R norm y = norm y *\<^sub>R (y /\<^sub>R norm y) /\<^sub>R norm (norm y *\<^sub>R (y /\<^sub>R norm y))"
by force
then have "proj ((norm y / norm x) *\<^sub>R x) = proj y"
by (metis (no_types) divide_inverse local.proj_def eq scaleR_scaleR)
then have [simp]: "(norm y / norm x) *\<^sub>R x = y"
by (rule eqI) (simp add: \<open>x \<noteq> 0\<close>)
have no: "0 \ norm y / norm x" "norm y / norm x < 1"
using * by (auto simp: field_split_simps)
then show "x = y"
using starI [OF \<open>x \<in> S\<close> no] xynot by auto
qed
qed
have "\surf. homeomorphism (S - rel_interior S) ?SPHER proj surf"
proof (rule homeomorphism_compact)
show "compact (S - rel_interior S)"
using \<open>compact S\<close> compact_rel_boundary by blast
show "continuous_on (S - rel_interior S) proj"
using 0 by (blast intro: continuous_on_subset [OF cont_proj])
show "proj ` (S - rel_interior S) = ?SPHER"
proof
show "proj ` (S - rel_interior S) \ ?SPHER"
using 0 by (force simp: hull_inc projI intro: nproj1)
show "?SPHER \ proj ` (S - rel_interior S)"
proof (clarsimp simp: proj_def)
fix x
assume "x \ affine hull S" and nox: "norm x = 1"
then have "x \ 0" by auto
obtain d where "0 < d" and dx: "(d *\<^sub>R x) \ rel_frontier S"
and ri: "\e. \0 \ e; e < d\ \ (e *\<^sub>R x) \ rel_interior S"
using ray_to_rel_frontier [OF \<open>bounded S\<close> 0] \<open>x \<in> affine hull S\<close> \<open>x \<noteq> 0\<close> by auto
show "x \ (\x. x /\<^sub>R norm x) ` (S - rel_interior S)"
proof
show "x = d *\<^sub>R x /\<^sub>R norm (d *\<^sub>R x)"
using \<open>0 < d\<close> by (auto simp: nox)
show "d *\<^sub>R x \ S - rel_interior S"
using dx \<open>closed S\<close> by (auto simp: rel_frontier_def)
qed
qed
qed
qed (rule inj_on_proj)
then obtain surf where surf: "homeomorphism (S - rel_interior S) ?SPHER proj surf"
by blast
then have cont_surf: "continuous_on (proj ` (S - rel_interior S)) surf"
by (auto simp: homeomorphism_def)
have surf_nz: "\x. x \ ?SPHER \ surf x \ 0"
by (metis "0" DiffE homeomorphism_def imageI surf)
have cont_nosp: "continuous_on (?SPHER) (\x. norm x *\<^sub>R ((surf o proj) x))"
proof (intro continuous_intros)
show "continuous_on (sphere 0 1 \ affine hull S) proj"
by (rule continuous_on_subset [OF cont_proj], force)
show "continuous_on (proj ` (sphere 0 1 \ affine hull S)) surf"
by (intro continuous_on_subset [OF cont_surf]) (force simp: homeomorphism_image1 [OF surf] dest: proj_spherI)
qed
have surfpS: "\x. \norm x = 1; x \ affine hull S\ \ surf (proj x) \ S"
by (metis (full_types) DiffE \<open>0 \<in> S\<close> homeomorphism_def image_eqI norm_zero proj_spherI real_vector.scale_zero_left scaleR_one surf)
have *: "\y. norm y = 1 \ y \ affine hull S \ x = surf (proj y)"
if "x \ S" "x \ rel_interior S" for x
proof -
have "proj x \ ?SPHER"
by (metis (full_types) "0" hull_inc proj_spherI that)
moreover have "surf (proj x) = x"
by (metis Diff_iff homeomorphism_def surf that)
ultimately show ?thesis
by (metis \<open>\<And>x. x \<in> ?SPHER \<Longrightarrow> surf x \<noteq> 0\<close> hull_inc inverse_1 local.proj_def norm_sgn projI scaleR_one sgn_div_norm that(1))
qed
have surfp_notin: "\x. \norm x = 1; x \ affine hull S\ \ surf (proj x) \ rel_interior S"
by (metis (full_types) DiffE one_neq_zero homeomorphism_def image_eqI norm_zero proj_spherI surf)
have no_sp_im: "(\x. norm x *\<^sub>R surf (proj x)) ` (?SPHER) = S - rel_interior S"
by (auto simp: surfpS image_def Bex_def surfp_notin *)
have inj_spher: "inj_on (\x. norm x *\<^sub>R surf (proj x)) ?SPHER"
proof
fix x y
assume xy: "x \ ?SPHER" "y \ ?SPHER"
and eq: " norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)"
then have "norm x = 1" "norm y = 1" "x \ affine hull S" "y \ affine hull S"
using 0 by auto
with eq show "x = y"
by (simp add: proj_def) (metis surf xy homeomorphism_def)
qed
have co01: "compact ?SPHER"
by (simp add: compact_Int_closed)
show "?SMINUS homeomorphic ?SPHER"
using homeomorphic_def surf by blast
have proj_scaleR: "\a x. 0 < a \ proj (a *\<^sub>R x) = proj x"
by (simp add: proj_def)
have cont_sp0: "continuous_on (affine hull S - {0}) (surf o proj)"
proof (rule continuous_on_compose [OF continuous_on_subset [OF cont_proj]])
show "continuous_on (proj ` (affine hull S - {0})) surf"
using homeomorphism_image1 proj_spherI surf by (intro continuous_on_subset [OF cont_surf]) fastforce
qed auto
obtain B where "B>0" and B: "\x. x \ S \ norm x \ B"
by (metis compact_imp_bounded \<open>compact S\<close> bounded_pos_less less_eq_real_def)
have cont_nosp: "continuous (at x within ?CBALL) (\x. norm x *\<^sub>R surf (proj x))"
if "norm x \ 1" "x \ affine hull S" for x
proof (cases "x=0")
case True
have "(norm \ 0) (at 0 within cball 0 1 \ affine hull S)"
by (simp add: tendsto_norm_zero eventually_at)
with True show ?thesis
apply (simp add: continuous_within)
apply (rule lim_null_scaleR_bounded [where B=B])
using B \<open>0 < B\<close> local.proj_def projI surfpS by (auto simp: eventually_at)
next
case False
then have "\\<^sub>F x in at x. (x \ affine hull S - {0}) = (x \ affine hull S)"
by (force simp: False eventually_at)
moreover
have "continuous (at x within affine hull S - {0}) (\x. surf (proj x))"
using cont_sp0 False that by (auto simp add: continuous_on_eq_continuous_within)
ultimately have *: "continuous (at x within affine hull S) (\x. surf (proj x))"
by (simp add: continuous_within Lim_transform_within_set continuous_on_eq_continuous_within)
show ?thesis
by (intro continuous_within_subset [where s = "affine hull S", OF _ Int_lower2] continuous_intros *)
qed
have cont_nosp2: "continuous_on ?CBALL (\x. norm x *\<^sub>R ((surf o proj) x))"
by (simp add: continuous_on_eq_continuous_within cont_nosp)
have "norm y *\<^sub>R surf (proj y) \ S" if "y \ cball 0 1" and yaff: "y \ affine hull S" for y
proof (cases "y=0")
case True then show ?thesis
by (simp add: \<open>0 \<in> S\<close>)
next
case False
then have "norm y *\<^sub>R surf (proj y) = norm y *\<^sub>R surf (proj (y /\<^sub>R norm y))"
by (simp add: proj_def)
have "norm y \ 1" using that by simp
have "surf (proj (y /\<^sub>R norm y)) \ S"
using False local.proj_def nproj1 projI surfpS yaff by blast
then have "surf (proj y) \ S"
by (simp add: False proj_def)
then show "norm y *\<^sub>R surf (proj y) \ S"
by (metis dual_order.antisym le_less_linear norm_ge_zero rel_interior_subset scaleR_one
starI subset_eq \<open>norm y \<le> 1\<close>)
qed
moreover have "x \ (\x. norm x *\<^sub>R surf (proj x)) ` (?CBALL)" if "x \ S" for x
proof (cases "x=0")
case True with that hull_inc show ?thesis by fastforce
next
case False
then have psp: "proj (surf (proj x)) = proj x"
by (metis homeomorphism_def hull_inc proj_spherI surf that)
have nxx: "norm x *\<^sub>R proj x = x"
by (simp add: False local.proj_def)
have affineI: "(1 / norm (surf (proj x))) *\<^sub>R x \ affine hull S"
by (metis \<open>0 \<in> S\<close> affine_hull_span_0 hull_inc span_clauses(4) that)
have sproj_nz: "surf (proj x) \ 0"
by (metis False proj0_iff psp)
then have "proj x = proj (proj x)"
by (metis False nxx proj_scaleR zero_less_norm_iff)
moreover have scaleproj: "\a r. r *\<^sub>R proj a = (r / norm a) *\<^sub>R a"
by (simp add: divide_inverse local.proj_def)
ultimately have "(norm (surf (proj x)) / norm x) *\<^sub>R x \ rel_interior S"
by (metis (no_types) sproj_nz divide_self_if hull_inc norm_eq_zero nproj1 projI psp scaleR_one surfp_notin that)
then have "(norm (surf (proj x)) / norm x) \ 1"
using starI [OF that] by (meson starI [OF that] le_less_linear norm_ge_zero zero_le_divide_iff)
then have nole: "norm x \ norm (surf (proj x))"
by (simp add: le_divide_eq_1)
let ?inx = "x /\<^sub>R norm (surf (proj x))"
show ?thesis
proof
show "x = norm ?inx *\<^sub>R surf (proj ?inx)"
by (simp add: field_simps) (metis inverse_eq_divide nxx positive_imp_inverse_positive proj_scaleR psp scaleproj sproj_nz zero_less_norm_iff)
qed (auto simp: field_split_simps nole affineI)
qed
ultimately have im_cball: "(\x. norm x *\<^sub>R surf (proj x)) ` ?CBALL = S"
by blast
have inj_cball: "inj_on (\x. norm x *\<^sub>R surf (proj x)) ?CBALL"
proof
fix x y
assume "x \ ?CBALL" "y \ ?CBALL"
and eq: "norm x *\<^sub>R surf (proj x) = norm y *\<^sub>R surf (proj y)"
then have x: "x \ affine hull S" and y: "y \ affine hull S"
using 0 by auto
show "x = y"
proof (cases "x=0 \ y=0")
case True then show "x = y" using eq proj_spherI surf_nz x y by force
next
case False
with x y have speq: "surf (proj x) = surf (proj y)"
by (metis eq homeomorphism_apply2 proj_scaleR proj_spherI surf zero_less_norm_iff)
then have "norm x = norm y"
by (metis \<open>x \<in> affine hull S\<close> \<open>y \<in> affine hull S\<close> eq proj_spherI real_vector.scale_cancel_right surf_nz)
moreover have "proj x = proj y"
by (metis (no_types) False speq homeomorphism_apply2 proj_spherI surf x y)
ultimately show "x = y"
using eq eqI by blast
qed
qed
have co01: "compact ?CBALL"
by (simp add: compact_Int_closed)
show "S homeomorphic ?CBALL"
using homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball] homeomorphic_sym by blast
qed
corollary
fixes S :: "'a::euclidean_space set"
assumes "compact S" and a: "a \ rel_interior S"
and star: "\x. x \ S \ open_segment a x \ rel_interior S"
shows starlike_compact_projective1:
"S - rel_interior S homeomorphic sphere a 1 \ affine hull S"
and starlike_compact_projective2:
"S homeomorphic cball a 1 \ affine hull S"
proof -
have 1: "compact ((+) (-a) ` S)" by (meson assms compact_translation)
have 2: "0 \ rel_interior ((+) (-a) ` S)"
using a rel_interior_translation [of "- a" S] by (simp cong: image_cong_simp)
have 3: "open_segment 0 x \ rel_interior ((+) (-a) ` S)" if "x \ ((+) (-a) ` S)" for x
proof -
have "x+a \ S" using that by auto
then have "open_segment a (x+a) \ rel_interior S" by (metis star)
then show ?thesis using open_segment_translation [of a 0 x]
using rel_interior_translation [of "- a" S] by (fastforce simp add: ac_simps image_iff cong: image_cong_simp)
qed
have "S - rel_interior S homeomorphic ((+) (-a) ` S) - rel_interior ((+) (-a) ` S)"
by (metis rel_interior_translation translation_diff homeomorphic_translation)
also have "... homeomorphic sphere 0 1 \ affine hull ((+) (-a) ` S)"
by (rule starlike_compact_projective1_0 [OF 1 2 3])
also have "... = (+) (-a) ` (sphere a 1 \ affine hull S)"
by (metis affine_hull_translation left_minus sphere_translation translation_Int)
also have "... homeomorphic sphere a 1 \ affine hull S"
using homeomorphic_translation homeomorphic_sym by blast
finally show "S - rel_interior S homeomorphic sphere a 1 \ affine hull S" .
have "S homeomorphic ((+) (-a) ` S)"
by (metis homeomorphic_translation)
also have "... homeomorphic cball 0 1 \ affine hull ((+) (-a) ` S)"
by (rule starlike_compact_projective2_0 [OF 1 2 3])
also have "... = (+) (-a) ` (cball a 1 \ affine hull S)"
by (metis affine_hull_translation left_minus cball_translation translation_Int)
also have "... homeomorphic cball a 1 \ affine hull S"
using homeomorphic_translation homeomorphic_sym by blast
finally show "S homeomorphic cball a 1 \ affine hull S" .
qed
corollary starlike_compact_projective_special:
assumes "compact S"
and cb01: "cball (0::'a::euclidean_space) 1 \ S"
and scale: "\x u. \x \ S; 0 \ u; u < 1\ \ u *\<^sub>R x \ S - frontier S"
shows "S homeomorphic (cball (0::'a::euclidean_space) 1)"
proof -
have "ball 0 1 \ interior S"
using cb01 interior_cball interior_mono by blast
then have 0: "0 \ rel_interior S"
by (meson centre_in_ball subsetD interior_subset_rel_interior le_numeral_extra(2) not_le)
have [simp]: "affine hull S = UNIV"
using \<open>ball 0 1 \<subseteq> interior S\<close> by (auto intro!: affine_hull_nonempty_interior)
have star: "open_segment 0 x \ rel_interior S" if "x \ S" for x
proof
fix p assume "p \ open_segment 0 x"
then obtain u where "x \ 0" and u: "0 \ u" "u < 1" and p: "u *\<^sub>R x = p"
by (auto simp: in_segment)
then show "p \ rel_interior S"
using scale [OF that u] closure_subset frontier_def interior_subset_rel_interior by fastforce
qed
show ?thesis
using starlike_compact_projective2_0 [OF \<open>compact S\<close> 0 star] by simp
qed
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) \
S homeomorphic T"
proof (cases "rel_interior S = {} \ 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)
next
case False
then obtain a b where a: "a \ rel_interior S" and b: "b \ rel_interior T" by auto
have starS: "\x. x \ S \ open_segment a x \ rel_interior S"
using rel_interior_closure_convex_segment
a \<open>convex S\<close> closure_subset subsetCE by blast
have starT: "\x. x \ T \ open_segment b x \ rel_interior T"
using rel_interior_closure_convex_segment
b \<open>convex T\<close> closure_subset subsetCE by blast
let ?aS = "(+) (-a) ` S" and ?bT = "(+) (-b) ` T"
have 0: "0 \ affine hull ?aS" "0 \ affine hull ?bT"
by (metis a b subsetD hull_inc image_eqI left_minus rel_interior_subset)+
have subs: "subspace (span ?aS)" "subspace (span ?bT)"
by (rule subspace_span)+
moreover
have "dim (span ((+) (- a) ` S)) = dim (span ((+) (- b) ` T))"
by (metis 0 aff_dim_translation_eq aff_dim_zero affeq dim_span nat_int)
ultimately obtain f g where "linear f" "linear g"
and fim: "f ` span ?aS = span ?bT"
and gim: "g ` span ?bT = span ?aS"
and fno: "\x. x \ span ?aS \ norm(f x) = norm x"
and gno: "\x. x \ span ?bT \ norm(g x) = norm x"
and gf: "\x. x \ span ?aS \ g(f x) = x"
and fg: "\x. x \ span ?bT \ f(g x) = x"
by (rule isometries_subspaces) blast
have [simp]: "continuous_on A f" for A
using \<open>linear f\<close> linear_conv_bounded_linear linear_continuous_on by blast
have [simp]: "continuous_on B g" for B
using \<open>linear g\<close> linear_conv_bounded_linear linear_continuous_on by blast
have eqspanS: "affine hull ?aS = span ?aS"
by (metis a affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
have eqspanT: "affine hull ?bT = span ?bT"
by (metis b affine_hull_span_0 subsetD hull_inc image_eqI left_minus rel_interior_subset)
have "S homeomorphic cball a 1 \ affine hull S"
by (rule starlike_compact_projective2 [OF \<open>compact S\<close> a starS])
also have "... homeomorphic (+) (-a) ` (cball a 1 \ affine hull S)"
by (metis homeomorphic_translation)
also have "... = cball 0 1 \ (+) (-a) ` (affine hull S)"
by (auto simp: dist_norm)
also have "... = cball 0 1 \ span ?aS"
using eqspanS affine_hull_translation by blast
also have "... homeomorphic cball 0 1 \ span ?bT"
proof (rule homeomorphicI)
show fim1: "f ` (cball 0 1 \ span ?aS) = cball 0 1 \ span ?bT"
proof
show "f ` (cball 0 1 \ span ?aS) \ cball 0 1 \ span ?bT"
using fim fno by auto
show "cball 0 1 \ span ?bT \ f ` (cball 0 1 \ span ?aS)"
by clarify (metis IntI fg gim gno image_eqI mem_cball_0)
qed
show "g ` (cball 0 1 \ span ?bT) = cball 0 1 \ span ?aS"
proof
show "g ` (cball 0 1 \ span ?bT) \ cball 0 1 \ span ?aS"
using gim gno by auto
show "cball 0 1 \ span ?aS \ g ` (cball 0 1 \ span ?bT)"
by clarify (metis IntI fim1 gf image_eqI)
qed
qed (auto simp: fg gf)
also have "... = cball 0 1 \ (+) (-b) ` (affine hull T)"
using eqspanT affine_hull_translation by blast
also have "... = (+) (-b) ` (cball b 1 \ affine hull T)"
by (auto simp: dist_norm)
also have "... homeomorphic (cball b 1 \ affine hull T)"
by (metis homeomorphic_translation homeomorphic_sym)
also have "... homeomorphic T"
by (metis starlike_compact_projective2 [OF \<open>compact T\<close> b starT] homeomorphic_sym)
finally have 1: "S homeomorphic T" .
have "S - rel_interior S homeomorphic sphere a 1 \ affine hull S"
by (rule starlike_compact_projective1 [OF \<open>compact S\<close> a starS])
also have "... homeomorphic (+) (-a) ` (sphere a 1 \ affine hull S)"
by (metis homeomorphic_translation)
also have "... = sphere 0 1 \ (+) (-a) ` (affine hull S)"
by (auto simp: dist_norm)
also have "... = sphere 0 1 \ span ?aS"
using eqspanS affine_hull_translation by blast
also have "... homeomorphic sphere 0 1 \ span ?bT"
proof (rule homeomorphicI)
show fim1: "f ` (sphere 0 1 \ span ?aS) = sphere 0 1 \ span ?bT"
proof
show "f ` (sphere 0 1 \ span ?aS) \ sphere 0 1 \ span ?bT"
using fim fno by auto
show "sphere 0 1 \ span ?bT \ f ` (sphere 0 1 \ span ?aS)"
by clarify (metis IntI fg gim gno image_eqI mem_sphere_0)
qed
show "g ` (sphere 0 1 \ span ?bT) = sphere 0 1 \ span ?aS"
proof
show "g ` (sphere 0 1 \ span ?bT) \ sphere 0 1 \ span ?aS"
using gim gno by auto
show "sphere 0 1 \ span ?aS \ g ` (sphere 0 1 \ span ?bT)"
by clarify (metis IntI fim1 gf image_eqI)
qed
qed (auto simp: fg gf)
also have "... = sphere 0 1 \ (+) (-b) ` (affine hull T)"
using eqspanT affine_hull_translation by blast
also have "... = (+) (-b) ` (sphere b 1 \ affine hull T)"
by (auto simp: dist_norm)
also have "... homeomorphic (sphere b 1 \ affine hull T)"
by (metis homeomorphic_translation homeomorphic_sym)
also have "... homeomorphic T - rel_interior T"
by (metis starlike_compact_projective1 [OF \<open>compact T\<close> b starT] homeomorphic_sym)
finally have 2: "S - rel_interior S homeomorphic T - rel_interior T" .
show ?thesis
using 1 2 by blast
qed
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"
shows "S homeomorphic T"
using homeomorphic_convex_lemma [OF assms] assms
by (auto simp: rel_frontier_def)
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"
shows "rel_frontier S homeomorphic rel_frontier T"
using assms homeomorphic_convex_lemma [of "closure S" "closure T"]
by (simp add: rel_frontier_def convex_rel_interior_closure)
subsection\<open>Homeomorphisms between punctured spheres and affine sets\<close>
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 homeomorphic_punctured_affine_sphere_affine_01:
assumes "b \ sphere 0 1" "affine T" "0 \ T" "b \ T" "affine p"
and affT: "aff_dim T = aff_dim p + 1"
shows "(sphere 0 1 \ T) - {b} homeomorphic p"
proof -
have [simp]: "norm b = 1" "b\b = 1"
using assms by (auto simp: norm_eq_1)
have [simp]: "T \ {v. b\v = 0} \ {}"
using \<open>0 \<in> T\<close> by auto
have [simp]: "\ T \ {v. b\v = 0}"
using \<open>norm b = 1\<close> \<open>b \<in> T\<close> by auto
define f where "f \ \x. 2 *\<^sub>R b + (2 / (1 - b\x)) *\<^sub>R (x - b)"
define g where "g \ \y. b + (4 / (norm y ^ 2 + 4)) *\<^sub>R (y - 2 *\<^sub>R b)"
have fg[simp]: "\x. \x \ T; b\x = 0\ \ f (g x) = x"
unfolding f_def g_def by (simp add: algebra_simps field_split_simps add_nonneg_eq_0_iff)
have no: "(norm (f x))\<^sup>2 = 4 * (1 + b \ x) / (1 - b \ x)"
if "norm x = 1" and "b \ x \ 1" for x
using that sum_sqs_eq [of 1 "b \ x"]
apply (simp flip: dot_square_norm add: norm_eq_1 nonzero_eq_divide_eq)
apply (simp add: f_def vector_add_divide_simps inner_simps)
apply (auto simp add: field_split_simps inner_commute)
done
have [simp]: "\u::real. 8 + u * (u * 8) = u * 16 \ u=1"
by algebra
have gf[simp]: "\x. \norm x = 1; b \ x \ 1\ \ g (f x) = x"
unfolding g_def no by (auto simp: f_def field_split_simps)
have g1: "norm (g x) = 1" if "x \ T" and "b \ x = 0" for x
using that
apply (simp only: g_def)
apply (rule power2_eq_imp_eq)
apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps)
apply (simp add: algebra_simps inner_commute)
done
have ne1: "b \ g x \ 1" if "x \ T" and "b \ x = 0" for x
using that unfolding g_def
apply (simp_all add: dot_square_norm [symmetric] divide_simps vector_add_divide_simps add_nonneg_eq_0_iff)
apply (auto simp: algebra_simps)
done
have "subspace T"
by (simp add: assms subspace_affine)
have gT: "\x. \x \ T; b \ x = 0\ \ g x \ T"
unfolding g_def
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
have "f ` {x. norm x = 1 \ b\x \ 1} \ {x. b\x = 0}"
unfolding f_def using \<open>norm b = 1\<close> norm_eq_1
by (force simp: field_simps inner_add_right inner_diff_right)
moreover have "f ` T \ T"
unfolding f_def using assms \<open>subspace T\<close>
by (auto simp add: inner_add_right inner_diff_right mem_affine_3_minus subspace_mul)
moreover have "{x. b\x = 0} \ T \ f ` ({x. norm x = 1 \ b\x \ 1} \ T)"
by clarify (metis (mono_tags) IntI ne1 fg gT g1 imageI mem_Collect_eq)
ultimately have imf: "f ` ({x. norm x = 1 \ b\x \ 1} \ T) = {x. b\x = 0} \ T"
by blast
have no4: "\y. b\y = 0 \ norm ((y\y + 4) *\<^sub>R b + 4 *\<^sub>R (y - 2 *\<^sub>R b)) = y\y + 4"
apply (rule power2_eq_imp_eq)
apply (simp_all flip: dot_square_norm)
apply (auto simp: power2_eq_square algebra_simps inner_commute)
done
have [simp]: "\x. \norm x = 1; b \ x \ 1\ \ b \ f x = 0"
by (simp add: f_def algebra_simps field_split_simps)
have [simp]: "\x. \x \ T; norm x = 1; b \ x \ 1\ \ f x \ T"
unfolding f_def
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
have "g ` {x. b\x = 0} \ {x. norm x = 1 \ b\x \ 1}"
unfolding g_def
apply (clarsimp simp: no4 vector_add_divide_simps divide_simps add_nonneg_eq_0_iff dot_square_norm [symmetric])
apply (auto simp: algebra_simps)
done
moreover have "g ` T \ T"
unfolding g_def
by (blast intro: \<open>subspace T\<close> \<open>b \<in> T\<close> subspace_add subspace_mul subspace_diff)
moreover have "{x. norm x = 1 \ b\x \ 1} \ T \ g ` ({x. b\x = 0} \ T)"
by clarify (metis (mono_tags, lifting) IntI gf image_iff imf mem_Collect_eq)
ultimately have img: "g ` ({x. b\x = 0} \ T) = {x. norm x = 1 \ b\x \ 1} \ T"
by blast
have aff: "affine ({x. b\x = 0} \ T)"
by (blast intro: affine_hyperplane assms)
have contf: "continuous_on ({x. norm x = 1 \ b\x \ 1} \ T) f"
unfolding f_def by (rule continuous_intros | force)+
have contg: "continuous_on ({x. b\x = 0} \ T) g"
unfolding g_def by (rule continuous_intros | force simp: add_nonneg_eq_0_iff)+
have "(sphere 0 1 \ T) - {b} = {x. norm x = 1 \ (b\x \ 1)} \ T"
using \<open>norm b = 1\<close> by (auto simp: norm_eq_1) (metis vector_eq \<open>b\<bullet>b = 1\<close>)
also have "... homeomorphic {x. b\x = 0} \ T"
by (rule homeomorphicI [OF imf img contf contg]) auto
also have "... homeomorphic p"
proof (rule homeomorphic_affine_sets [OF aff \<open>affine p\<close>])
show "aff_dim ({x. b \ x = 0} \ T) = aff_dim p"
by (simp add: Int_commute aff_dim_affine_Int_hyperplane [OF \<open>affine T\<close>] affT)
qed
finally show ?thesis .
qed
theorem homeomorphic_punctured_affine_sphere_affine:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" "b \ sphere a r" "affine T" "a \ T" "b \ T" "affine p"
and aff: "aff_dim T = aff_dim p + 1"
shows "(sphere a r \ T) - {b} homeomorphic p"
proof -
have "a \ b" using assms by auto
then have inj: "inj (\x::'a. x /\<^sub>R norm (a - b))"
by (simp add: inj_on_def)
have "((sphere a r \ T) - {b}) homeomorphic
(+) (-a) ` ((sphere a r \<inter> T) - {b})"
by (rule homeomorphic_translation)
also have "... homeomorphic (*\<^sub>R) (inverse r) ` (+) (- a) ` (sphere a r \ T - {b})"
by (metis \<open>0 < r\<close> homeomorphic_scaling inverse_inverse_eq inverse_zero less_irrefl)
also have "... = sphere 0 1 \ ((*\<^sub>R) (inverse r) ` (+) (- a) ` T) - {(b - a) /\<^sub>R r}"
using assms by (auto simp: dist_norm norm_minus_commute divide_simps)
also have "... homeomorphic p"
using assms affine_translation [symmetric, of "- a"] aff_dim_translation_eq [of "- a"]
by (intro homeomorphic_punctured_affine_sphere_affine_01) (auto simp: dist_norm norm_minus_commute affine_scaling inj)
finally show ?thesis .
qed
corollary homeomorphic_punctured_sphere_affine:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" and b: "b \ sphere a r"
and "affine T" and affS: "aff_dim T + 1 = DIM('a)"
shows "(sphere a r - {b}) homeomorphic T"
using homeomorphic_punctured_affine_sphere_affine [of r b a UNIV T] assms by auto
corollary homeomorphic_punctured_sphere_hyperplane:
fixes a :: "'a :: euclidean_space"
assumes "0 < r" and b: "b \ sphere a r"
and "c \ 0"
shows "(sphere a r - {b}) homeomorphic {x::'a. c \ x = d}"
using assms
by (intro homeomorphic_punctured_sphere_affine) (auto simp: affine_hyperplane of_nat_diff)
proposition homeomorphic_punctured_sphere_affine_gen:
fixes a :: "'a :: euclidean_space"
assumes "convex S" "bounded S" and a: "a \ rel_frontier S"
and "affine T" and affS: "aff_dim S = aff_dim T + 1"
shows "rel_frontier S - {a} homeomorphic T"
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)
have "S \ {}" using assms by auto
then obtain z where "z \ U"
by (metis aff_dim_negative_iff equals0I affdS)
then have bne: "ball z 1 \ U \ {}" by force
then have [simp]: "aff_dim(ball z 1 \ U) = aff_dim U"
using aff_dim_convex_Int_open [OF \<open>convex U\<close> open_ball]
by (fastforce simp add: Int_commute)
have "rel_frontier S homeomorphic rel_frontier (ball z 1 \ U)"
by (rule homeomorphic_rel_frontiers_convex_bounded_sets)
(auto simp: \<open>affine U\<close> affine_imp_convex convex_Int affdS assms)
also have "... = sphere z 1 \ U"
using convex_affine_rel_frontier_Int [of "ball z 1" U]
by (simp add: \<open>affine U\<close> bne)
finally have "rel_frontier S homeomorphic sphere z 1 \ U" .
then obtain h k where him: "h ` rel_frontier S = sphere z 1 \ U"
and kim: "k ` (sphere z 1 \ U) = rel_frontier S"
and hcon: "continuous_on (rel_frontier S) h"
and kcon: "continuous_on (sphere z 1 \ U) k"
and kh: "\x. x \ rel_frontier S \ k(h(x)) = x"
and hk: "\y. y \ sphere z 1 \ U \ h(k(y)) = y"
unfolding homeomorphic_def homeomorphism_def by auto
have "rel_frontier S - {a} homeomorphic (sphere z 1 \ U) - {h a}"
proof (rule homeomorphicI)
show h: "h ` (rel_frontier S - {a}) = sphere z 1 \ U - {h a}"
using him a kh by auto metis
show "k ` (sphere z 1 \ U - {h a}) = rel_frontier S - {a}"
by (force simp: h [symmetric] image_comp o_def kh)
qed (auto intro: continuous_on_subset hcon kcon simp: kh hk)
also have "... homeomorphic T"
by (rule homeomorphic_punctured_affine_sphere_affine)
(use a him in \<open>auto simp: affS affdS \<open>affine T\<close> \<open>affine U\<close> \<open>z \<in> U\<close>\<close>)
finally show ?thesis .
qed
text\<open> When dealing with AR, ANR and ANR later, it's useful to know that every set
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 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 \ {}" "closedin (top_of_set U) T"
"S homeomorphic T"
proof (cases "S = {}")
case True then show ?thesis
by (rule_tac U=UNIV and T="{}" in that) auto
next
case False
then obtain a where "a \ S" by auto
obtain i::'n where i: "i \ Basis" "i \ 0"
using SOME_Basis Basis_zero by force
have "0 \ affine hull ((+) (- a) ` S)"
by (simp add: \<open>a \<in> S\<close> hull_inc)
then have "dim ((+) (- a) ` S) = aff_dim ((+) (- a) ` S)"
by (simp add: aff_dim_zero)
also have "... < DIM('n)"
by (simp add: aff_dim_translation_eq_subtract assms cong: image_cong_simp)
finally have dd: "dim ((+) (- a) ` S) < DIM('n)"
by linarith
have span: "span {x. i \ x = 0} = {x. i \ x = 0}"
using span_eq_iff [symmetric, of "{x. i \ x = 0}"] subspace_hyperplane [of i] by simp
have "dim ((+) (- a) ` S) \ dim {x. i \ x = 0}"
using dd by (simp add: dim_hyperplane [OF \<open>i \<noteq> 0\<close>])
then obtain T where "subspace T" and Tsub: "T \ {x. i \ x = 0}"
and dimT: "dim T = dim ((+) (- a) ` S)"
by (rule choose_subspace_of_subspace) (simp add: span)
have "subspace (span ((+) (- a) ` S))"
using subspace_span by blast
then obtain h k where "linear h" "linear k"
and heq: "h ` span ((+) (- a) ` S) = T"
and keq:"k ` T = span ((+) (- a) ` S)"
and hinv [simp]: "\x. x \ span ((+) (- a) ` S) \ k(h x) = x"
and kinv [simp]: "\x. x \ T \ h(k x) = x"
by (auto simp: dimT intro: isometries_subspaces [OF _ \<open>subspace T\<close>] dimT)
have hcont: "continuous_on A h" and kcont: "continuous_on B k" for A B
using \<open>linear h\<close> \<open>linear k\<close> linear_continuous_on linear_conv_bounded_linear by blast+
have ihhhh[simp]: "\x. x \ S \ i \ h (x - a) = 0"
using Tsub [THEN subsetD] heq span_superset by fastforce
have "sphere 0 1 - {i} homeomorphic {x. i \ x = 0}"
proof (rule homeomorphic_punctured_sphere_affine)
show "affine {x. i \ x = 0}"
by (auto simp: affine_hyperplane)
show "aff_dim {x. i \ x = 0} + 1 = int DIM('n)"
using i by clarsimp (metis DIM_positive Suc_pred add.commute of_nat_Suc)
qed (use i in auto)
then obtain f g where fg: "homeomorphism (sphere 0 1 - {i}) {x. i \ x = 0} f g"
by (force simp: homeomorphic_def)
show ?thesis
proof
have "h ` (+) (- a) ` S \ T"
using heq span_superset span_linear_image by blast
then have "g ` h ` (+) (- a) ` S \ g ` {x. i \ x = 0}"
using Tsub by (simp add: image_mono)
also have "... \ sphere 0 1 - {i}"
by (simp add: fg [unfolded homeomorphism_def])
finally have gh_sub_sph: "(g \ h) ` (+) (- a) ` S \ sphere 0 1 - {i}"
by (metis image_comp)
then have gh_sub_cb: "(g \ h) ` (+) (- a) ` S \ cball 0 1"
by (metis Diff_subset order_trans sphere_cball)
have [simp]: "\u. u \ S \ norm (g (h (u - a))) = 1"
using gh_sub_sph [THEN subsetD] by (auto simp: o_def)
show "convex (ball 0 1 \ (g \ h) ` (+) (- a) ` S)"
by (meson ball_subset_cball convex_intermediate_ball gh_sub_cb sup.bounded_iff sup.cobounded1)
show "closedin (top_of_set (ball 0 1 \ (g \ h) ` (+) (- a) ` S)) ((g \ h) ` (+) (- a) ` S)"
unfolding closedin_closed
by (rule_tac x="sphere 0 1" in exI) auto
have ghcont: "continuous_on ((\x. x - a) ` S) (\x. g (h x))"
by (rule continuous_on_compose2 [OF homeomorphism_cont2 [OF fg] hcont], force)
have kfcont: "continuous_on ((\x. g (h (x - a))) ` S) (\x. k (f x))"
proof (rule continuous_on_compose2 [OF kcont])
show "continuous_on ((\x. g (h (x - a))) ` S) f"
using homeomorphism_cont1 [OF fg] gh_sub_sph by (fastforce intro: continuous_on_subset)
qed auto
have "S homeomorphic (+) (- a) ` S"
by (fact homeomorphic_translation)
also have "\ homeomorphic (g \ h) ` (+) (- a) ` S"
apply (simp add: homeomorphic_def homeomorphism_def cong: image_cong_simp)
apply (rule_tac x="g \ h" in exI)
apply (rule_tac x="k \ f" in exI)
apply (auto simp: ghcont kfcont span_base homeomorphism_apply2 [OF fg] image_comp cong: image_cong_simp)
done
finally show "S homeomorphic (g \ h) ` (+) (- a) ` S" .
qed auto
qed
subsection\<open>Locally compact sets in an open set\<close>
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 locally_compact_open_Int_closure:
fixes S :: "'a :: metric_space set"
assumes "locally compact S"
obtains T where "open T" "S = T \ closure S"
proof -
have "\x\S. \T v u. u = S \ T \ x \ u \ u \ v \ v \ S \ open T \ compact v"
by (metis assms locally_compact openin_open)
then obtain t v where
tv: "\x. x \ S
\<Longrightarrow> v x \<subseteq> S \<and> open (t x) \<and> compact (v x) \<and> (\<exists>u. x \<in> u \<and> u \<subseteq> v x \<and> u = S \<inter> t x)"
by metis
then have o: "open (\(t ` S))"
by blast
have "S = \ (v ` S)"
using tv by blast
also have "... = \(t ` S) \ closure S"
proof
show "\(v ` S) \ \(t ` S) \ closure S"
by clarify (meson IntD2 IntI UN_I closure_subset subsetD tv)
have "t x \ closure S \ v x" if "x \ S" for x
proof -
have "t x \ closure S \ closure (t x \ S)"
by (simp add: open_Int_closure_subset that tv)
also have "... \ v x"
by (metis Int_commute closure_minimal compact_imp_closed that tv)
finally show ?thesis .
qed
then show "\(t ` S) \ closure S \ \(v ` S)"
by blast
qed
finally have e: "S = \(t ` S) \ closure S" .
show ?thesis
by (rule that [OF o e])
qed
lemma locally_compact_closedin_open:
fixes S :: "'a :: metric_space set"
assumes "locally compact S"
obtains T where "open T" "closedin (top_of_set T) S"
by (metis locally_compact_open_Int_closure [OF assms] closed_closure closedin_closed_Int)
lemma locally_compact_homeomorphism_projection_closed:
assumes "locally compact S"
obtains T and f :: "'a \ 'a :: euclidean_space \ 'b :: euclidean_space"
where "closed T" "homeomorphism S T f fst"
proof (cases "closed S")
case True
show ?thesis
proof
show "homeomorphism S (S \ {0}) (\x. (x, 0)) fst"
by (auto simp: homeomorphism_def continuous_intros)
qed (use True closed_Times in auto)
next
case False
obtain U where "open U" and US: "U \ closure S = S"
by (metis locally_compact_open_Int_closure [OF assms])
with False have Ucomp: "-U \ {}"
using closure_eq by auto
have [simp]: "closure (- U) = -U"
by (simp add: \<open>open U\<close> closed_Compl)
define f :: "'a \ 'a \ 'b" where "f \ \x. (x, One /\<^sub>R setdist {x} (- U))"
have "continuous_on U (\x. (x, One /\<^sub>R setdist {x} (- U)))"
proof (intro continuous_intros continuous_on_setdist)
show "\x\U. setdist {x} (- U) \ 0"
by (simp add: Ucomp setdist_eq_0_sing_1)
qed
then have homU: "homeomorphism U (f`U) f fst"
by (auto simp: f_def homeomorphism_def image_iff continuous_intros)
have cloS: "closedin (top_of_set U) S"
by (metis US closed_closure closedin_closed_Int)
have cont: "isCont ((\x. setdist {x} (- U)) o fst) z" for z :: "'a \ 'b"
by (rule continuous_at_compose continuous_intros continuous_at_setdist)+
have setdist1D: "setdist {a} (- U) *\<^sub>R b = One \ setdist {a} (- U) \ 0" for a::'a and b::'b
by force
have *: "r *\<^sub>R b = One \ b = (1 / r) *\<^sub>R One" for r and b::'b
by (metis One_non_0 nonzero_divide_eq_eq real_vector.scale_eq_0_iff real_vector.scale_scale scaleR_one)
have "\a b::'b. setdist {a} (- U) *\<^sub>R b = One \ (a,b) \ (\x. (x, (1 / setdist {x} (- U)) *\<^sub>R One)) ` U"
by (metis (mono_tags, lifting) "*" ComplI image_eqI setdist1D setdist_sing_in_set)
then have "f ` U = (\z. (setdist {fst z} (- U) *\<^sub>R snd z)) -` {One}"
by (auto simp: f_def setdist_eq_0_sing_1 field_simps Ucomp)
then have clfU: "closed (f ` U)"
by (force intro: continuous_intros cont [unfolded o_def] continuous_closed_vimage)
have "closed (f ` S)"
by (metis closedin_closed_trans [OF _ clfU] homeomorphism_imp_closed_map [OF homU cloS])
then show ?thesis
by (metis US homU homeomorphism_of_subsets inf_sup_ord(1) that)
qed
lemma locally_compact_closed_Int_open:
fixes S :: "'a :: euclidean_space set"
shows "locally compact S \ (\U V. closed U \ open V \ S = U \ V)" (is "?lhs = ?rhs")
proof
show "?lhs \ ?rhs"
by (metis closed_closure inf_commute locally_compact_open_Int_closure)
show "?rhs \ ?lhs"
by (meson closed_imp_locally_compact locally_compact_Int open_imp_locally_compact)
qed
lemma lowerdim_embeddings:
assumes "DIM('a) < DIM('b)"
obtains f :: "'a::euclidean_space*real \ 'b::euclidean_space"
and g :: "'b \ 'a*real"
and j :: 'b
where "linear f" "linear g" "\z. g (f z) = z" "j \ Basis" "\x. f(x,0) \ j = 0"
proof -
let ?B = "Basis :: ('a*real) set"
have b01: "(0,1) \ ?B"
by (simp add: Basis_prod_def)
have "DIM('a * real) \ DIM('b)"
by (simp add: Suc_leI assms)
then obtain basf :: "'a*real \ 'b" where sbf: "basf ` ?B \ Basis" and injbf: "inj_on basf Basis"
by (metis finite_Basis card_le_inj)
define basg:: "'b \ 'a * real" where
"basg \ \i. if i \ basf ` Basis then inv_into Basis basf i else (0,1)"
have bgf[simp]: "basg (basf i) = i" if "i \ Basis" for i
using inv_into_f_f injbf that by (force simp: basg_def)
have sbg: "basg ` Basis \ ?B"
by (force simp: basg_def injbf b01)
define f :: "'a*real \ 'b" where "f \ \u. \j\Basis. (u \ basg j) *\<^sub>R j"
define g :: "'b \ 'a*real" where "g \ \z. (\i\Basis. (z \ basf i) *\<^sub>R i)"
show ?thesis
proof
show "linear f"
unfolding f_def
by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
show "linear g"
unfolding g_def
by (intro linear_compose_sum linearI ballI) (auto simp: algebra_simps)
have *: "(\a \ Basis. a \ basf b * (x \ basg a)) = x \ b" if "b \ Basis" for x b
using sbf that by auto
show gf: "g (f x) = x" for x
proof (rule euclidean_eqI)
show "\b. b \ Basis \ g (f x) \ b = x \ b"
using f_def g_def sbf by auto
qed
show "basf(0,1) \ Basis"
using b01 sbf by auto
then show "f(x,0) \ basf(0,1) = 0" for x
unfolding f_def inner_sum_left
using b01 inner_not_same_Basis
by (fastforce intro: comm_monoid_add_class.sum.neutral)
qed
qed
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 -
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
obtain f :: "'a*real \ 'b" and g :: "'b \ 'a*real"
where "linear f" "linear g" and gf [simp]: "\z. g (f z) = z"
using lowerdim_embeddings [OF dimlt] by metis
then have "inj f"
by (metis injI)
have gfU: "g ` f ` U = U"
by (simp add: image_comp o_def)
have "S homeomorphic U"
using homU homeomorphic_def by blast
also have "... homeomorphic f ` U"
proof (rule homeomorphicI [OF refl gfU])
show "continuous_on U f"
by (meson \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image)
show "continuous_on (f ` U) g"
using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear by blast
qed (auto simp: o_def)
finally show ?thesis
using \<open>closed U\<close> \<open>inj f\<close> \<open>linear f\<close> closed_injective_linear_image that by blast
qed
lemma homeomorphic_convex_compact_lemma:
fixes S :: "'a::euclidean_space set"
assumes "convex S"
and "compact S"
and "cball 0 1 \ S"
shows "S homeomorphic (cball (0::'a) 1)"
proof (rule starlike_compact_projective_special[OF assms(2-3)])
fix x u
assume "x \ S" and "0 \ u" and "u < (1::real)"
have "open (ball (u *\<^sub>R x) (1 - u))"
by (rule open_ball)
moreover have "u *\<^sub>R x \ ball (u *\<^sub>R x) (1 - u)"
unfolding centre_in_ball using \<open>u < 1\<close> by simp
moreover have "ball (u *\<^sub>R x) (1 - u) \ S"
proof
fix y
assume "y \ ball (u *\<^sub>R x) (1 - u)"
then have "dist (u *\<^sub>R x) y < 1 - u"
unfolding mem_ball .
with \<open>u < 1\<close> have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \ S" ..
with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \ S"
using \<open>x \<in> S\<close> \<open>0 \<le> u\<close> \<open>u < 1\<close> [THEN less_imp_le] by (rule convexD_alt)
then show "y \ S" using \u < 1\
by simp
qed
ultimately have "u *\<^sub>R x \ interior S" ..
then show "u *\<^sub>R x \ S - frontier S"
using frontier_def and interior_subset by auto
qed
proposition homeomorphic_convex_compact_cball:
fixes e :: real
and S :: "'a::euclidean_space set"
assumes S: "convex S" "compact S" "interior S \ {}" and "e > 0"
shows "S homeomorphic (cball (b::'a) e)"
proof (rule homeomorphic_trans[OF _ homeomorphic_balls(2)])
obtain a where "a \ interior S"
using assms by auto
then show "S homeomorphic cball (0::'a) 1"
by (metis (no_types) aff_dim_cball S compact_cball convex_cball
homeomorphic_convex_lemma interior_rel_interior_gen zero_less_one)
qed (use \<open>e>0\<close> in auto)
corollary homeomorphic_convex_compact:
fixes S :: "'a::euclidean_space set"
and T :: "'a set"
assumes "convex S" "compact S" "interior S \ {}"
and "convex T" "compact T" "interior T \ {}"
shows "S homeomorphic T"
using assms
by (meson zero_less_one homeomorphic_trans homeomorphic_convex_compact_cball homeomorphic_sym)
lemma homeomorphic_closed_intervals:
fixes a :: "'a::euclidean_space" and b and c :: "'a::euclidean_space" and d
assumes "box a b \ {}" and "box c d \ {}"
shows "(cbox a b) homeomorphic (cbox c d)"
by (simp add: assms homeomorphic_convex_compact)
lemma homeomorphic_closed_intervals_real:
fixes a::real and b and c::real and d
assumes "a and "c
shows "{a..b} homeomorphic {c..d}"
using assms by (auto intro: homeomorphic_convex_compact)
subsection\<open>Covering spaces and lifting results for them\<close>
definition\<^marker>\<open>tag important\<close> covering_space
:: "'a::topological_space set \ ('a \ 'b) \ 'b::topological_space set \ bool"
where
"covering_space c p S \
continuous_on c p \<and> p ` c = S \<and>
(\<forall>x \<in> S. \<exists>T. x \<in> T \<and> openin (top_of_set S) T \<and>
(\<exists>v. \<Union>v = c \<inter> p -` T \<and>
(\<forall>u \<in> v. openin (top_of_set c) u) \<and>
pairwise disjnt v \<and>
(\<forall>u \<in> v. \<exists>q. homeomorphism u T p q)))"
lemma covering_space_imp_continuous: "covering_space c p S \ continuous_on c p"
by (simp add: covering_space_def)
lemma covering_space_imp_surjective: "covering_space c p S \ p ` c = S"
by (simp add: covering_space_def)
lemma homeomorphism_imp_covering_space: "homeomorphism S T f g \ covering_space S f T"
apply (clarsimp simp add: homeomorphism_def covering_space_def)
apply (rule_tac x=T in exI, simp)
apply (rule_tac x="{S}" in exI, auto)
done
lemma covering_space_local_homeomorphism:
assumes "covering_space c p S" "x \ c"
obtains T u q where "x \ T" "openin (top_of_set c) T"
"p x \ u" "openin (top_of_set S) u"
"homeomorphism T u p q"
using assms
by (clarsimp simp add: covering_space_def) (metis IntI UnionE vimage_eq)
lemma covering_space_local_homeomorphism_alt:
assumes p: "covering_space c p S" and "y \ S"
obtains x T U q where "p x = y"
"x \ T" "openin (top_of_set c) T"
"y \ U" "openin (top_of_set S) U"
"homeomorphism T U p q"
proof -
obtain x where "p x = y" "x \ c"
using assms covering_space_imp_surjective by blast
show ?thesis
using that \<open>p x = y\<close> by (auto intro: covering_space_local_homeomorphism [OF p \<open>x \<in> c\<close>])
qed
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 (top_of_set c) T"
shows "openin (top_of_set S) (p ` T)"
proof -
have pce: "p ` c = S"
and covs:
"\x. x \ S \
\<exists>X VS. x \<in> X \<and> openin (top_of_set S) X \<and>
\<Union>VS = c \<inter> p -` X \<and>
(\<forall>u \<in> VS. openin (top_of_set c) u) \<and>
pairwise disjnt VS \<and>
(\<forall>u \<in> VS. \<exists>q. homeomorphism u X p q)"
using p by (auto simp: covering_space_def)
have "T \ c" by (metis openin_euclidean_subtopology_iff T)
have "\X. openin (top_of_set S) X \ y \ X \ X \ p ` T"
if "y \ p ` T" for y
proof -
have "y \ S" using \T \ c\ pce that by blast
obtain U VS where "y \ U" and U: "openin (top_of_set S) U"
and VS: "\VS = c \ p -` U"
and openVS: "\V \ VS. openin (top_of_set c) V"
and homVS: "\V. V \ VS \ \q. homeomorphism V U p q"
using covs [OF \<open>y \<in> S\<close>] by auto
obtain x where "x \ c" "p x \ U" "x \ T" "p x = y"
using T [unfolded openin_euclidean_subtopology_iff] \<open>y \<in> U\<close> \<open>y \<in> p ` T\<close> by blast
with VS obtain V where "x \ V" "V \ VS" by auto
then obtain q where q: "homeomorphism V U p q" using homVS by blast
then have ptV: "p ` (T \ V) = U \ q -` (T \ V)"
using VS \<open>V \<in> VS\<close> by (auto simp: homeomorphism_def)
have ocv: "openin (top_of_set c) V"
by (simp add: \<open>V \<in> VS\<close> openVS)
have "openin (top_of_set (q ` U)) (T \ V)"
using q unfolding homeomorphism_def
by (metis T inf.absorb_iff2 ocv openin_imp_subset openin_subtopology_Int subtopology_subtopology)
then have "openin (top_of_set U) (U \ q -` (T \ V))"
using continuous_on_open homeomorphism_def q by blast
then have os: "openin (top_of_set S) (U \ q -` (T \ V))"
using openin_trans [of U] by (simp add: Collect_conj_eq U)
show ?thesis
proof (intro exI conjI)
show "openin (top_of_set S) (p ` (T \ V))"
by (simp only: ptV os)
qed (use \<open>p x = y\<close> \<open>x \<in> V\<close> \<open>x \<in> T\<close> in auto)
qed
with openin_subopen show ?thesis by blast
qed
lemma covering_space_lift_unique_gen:
fixes f :: "'a::topological_space \ 'b::topological_space"
fixes g1 :: "'a \ 'c::real_normed_vector"
assumes cov: "covering_space c p S"
and eq: "g1 a = g2 a"
and f: "continuous_on T f" "f ` T \ S"
and g1: "continuous_on T g1" "g1 ` T \ c"
and fg1: "\x. x \ T \ f x = p(g1 x)"
and g2: "continuous_on T g2" "g2 ` T \ c"
and fg2: "\x. x \ T \ f x = p(g2 x)"
and u_compt: "U \ components T" and "a \ U" "x \ U"
shows "g1 x = g2 x"
proof -
have "U \ T" by (rule in_components_subset [OF u_compt])
define G12 where "G12 \ {x \ U. g1 x - g2 x = 0}"
have "connected U" by (rule in_components_connected [OF u_compt])
have contu: "continuous_on U g1" "continuous_on U g2"
using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+
have o12: "openin (top_of_set U) G12"
unfolding G12_def
proof (subst openin_subopen, clarify)
fix z
assume z: "z \ U" "g1 z - g2 z = 0"
obtain v w q where "g1 z \ v" and ocv: "openin (top_of_set c) v"
and "p (g1 z) \ w" and osw: "openin (top_of_set S) w"
and hom: "homeomorphism v w p q"
proof (rule covering_space_local_homeomorphism [OF cov])
show "g1 z \ c"
using \<open>U \<subseteq> T\<close> \<open>z \<in> U\<close> g1(2) by blast
qed auto
have "g2 z \ v" using \g1 z \ v\ z by auto
have gg: "U \ g -` v = U \ g -` (v \ g ` U)" for g
by auto
have "openin (top_of_set (g1 ` U)) (v \ g1 ` U)"
using ocv \<open>U \<subseteq> T\<close> g1 by (fastforce simp add: openin_open)
then have 1: "openin (top_of_set U) (U \ g1 -` v)"
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
have "openin (top_of_set (g2 ` U)) (v \ g2 ` U)"
using ocv \<open>U \<subseteq> T\<close> g2 by (fastforce simp add: openin_open)
then have 2: "openin (top_of_set U) (U \ g2 -` v)"
unfolding gg by (blast intro: contu continuous_on_open [THEN iffD1, rule_format])
let ?T = "(U \ g1 -` v) \ (U \ g2 -` v)"
show "\T. openin (top_of_set U) T \ z \ T \ T \ {z \ U. g1 z - g2 z = 0}"
proof (intro exI conjI)
show "openin (top_of_set U) ?T"
using "1" "2" by blast
show "z \ ?T"
using z by (simp add: \<open>g1 z \<in> v\<close> \<open>g2 z \<in> v\<close>)
show "?T \ {z \ U. g1 z - g2 z = 0}"
using hom
by (clarsimp simp: homeomorphism_def) (metis \<open>U \<subseteq> T\<close> fg1 fg2 subsetD)
qed
qed
have c12: "closedin (top_of_set U) G12"
unfolding G12_def
by (intro continuous_intros continuous_closedin_preimage_constant contu)
have "G12 = {} \ G12 = U"
by (intro connected_clopen [THEN iffD1, rule_format] \<open>connected U\<close> conjI o12 c12)
with eq \<open>a \<in> U\<close> have "\<And>x. x \<in> U \<Longrightarrow> g1 x - g2 x = 0" by (auto simp: G12_def)
then show ?thesis
using \<open>x \<in> U\<close> by force
qed
proposition covering_space_lift_unique:
fixes f :: "'a::topological_space \ 'b::topological_space"
fixes g1 :: "'a \ 'c::real_normed_vector"
assumes "covering_space c p S"
"g1 a = g2 a"
"continuous_on T f" "f ` T \ S"
"continuous_on T g1" "g1 ` T \ c" "\x. x \ T \ f x = p(g1 x)"
"continuous_on T g2" "g2 ` T \ c" "\x. x \ T \ f x = p(g2 x)"
"connected T" "a \ T" "x \ T"
shows "g1 x = g2 x"
using covering_space_lift_unique_gen [of c p S] in_components_self assms ex_in_conv
by blast
lemma covering_space_locally:
fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector"
assumes loc: "locally \ C" and cov: "covering_space C p S"
and pim: "\T. \T \ C; \ T\ \ \(p ` T)"
shows "locally \ S"
proof -
have "locally \ (p ` C)"
proof (rule locally_open_map_image [OF loc])
show "continuous_on C p"
using cov covering_space_imp_continuous by blast
show "\T. openin (top_of_set C) T \ openin (top_of_set (p ` C)) (p ` T)"
using cov covering_space_imp_surjective covering_space_open_map by blast
qed (simp add: pim)
then show ?thesis
using covering_space_imp_surjective [OF cov] by metis
qed
proposition covering_space_locally_eq:
fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector"
assumes cov: "covering_space C p S"
and pim: "\T. \T \ C; \ T\ \ \(p ` T)"
and qim: "\q U. \U \ S; continuous_on U q; \ U\ \ \(q ` U)"
shows "locally \ S \ locally \ C"
(is "?lhs = ?rhs")
proof
assume L: ?lhs
show ?rhs
proof (rule locallyI)
fix V x
assume V: "openin (top_of_set C) V" and "x \ V"
have "p x \ p ` C"
by (metis IntE V \<open>x \<in> V\<close> imageI openin_open)
then obtain T \<V> where "p x \<in> T"
and opeT: "openin (top_of_set S) T"
and veq: "\\ = C \ p -` T"
and ope: "\U\\. openin (top_of_set C) U"
and hom: "\U\\. \q. homeomorphism U T p q"
using cov unfolding covering_space_def by (blast intro: that)
have "x \ \\"
using V veq \<open>p x \<in> T\<close> \<open>x \<in> V\<close> openin_imp_subset by fastforce
then obtain U where "x \ U" "U \ \"
by blast
then obtain q where opeU: "openin (top_of_set C) U" and q: "homeomorphism U T p q"
using ope hom by blast
with V have "openin (top_of_set C) (U \ V)"
by blast
then have UV: "openin (top_of_set S) (p ` (U \ V))"
using cov covering_space_open_map by blast
obtain W W' where opeW: "openin (top_of_set S) W" and "\ W'" "p x \ W" "W \ W'" and W'sub: "W' \ p ` (U \ V)"
using locallyE [OF L UV] \<open>x \<in> U\<close> \<open>x \<in> V\<close> by blast
then have "W \ T"
by (metis Int_lower1 q homeomorphism_image1 image_Int_subset order_trans)
show "\U Z. openin (top_of_set C) U \
\<phi> Z \<and> x \<in> U \<and> U \<subseteq> Z \<and> Z \<subseteq> V"
proof (intro exI conjI)
have "openin (top_of_set T) W"
by (meson opeW opeT openin_imp_subset openin_subset_trans \<open>W \<subseteq> T\<close>)
then have "openin (top_of_set U) (q ` W)"
by (meson homeomorphism_imp_open_map homeomorphism_symD q)
then show "openin (top_of_set C) (q ` W)"
using opeU openin_trans by blast
show "\ (q ` W')"
by (metis (mono_tags, lifting) Int_subset_iff UV W'sub \\ W'\ continuous_on_subset dual_order.trans homeomorphism_def image_Int_subset openin_imp_subset q qim)
show "x \ q ` W"
by (metis \<open>p x \<in> W\<close> \<open>x \<in> U\<close> homeomorphism_def imageI q)
show "q ` W \ q ` W'"
using \<open>W \<subseteq> W'\<close> by blast
have "W' \ p ` V"
using W'sub by blast
then show "q ` W' \ V"
using W'sub homeomorphism_apply1 [OF q] by auto
qed
qed
next
assume ?rhs
then show ?lhs
using cov covering_space_locally pim by blast
qed
lemma covering_space_locally_compact_eq:
fixes p :: "'a::real_normed_vector \ 'b::real_normed_vector"
assumes "covering_space C p S"
shows "locally compact S \ locally compact C"
proof (rule covering_space_locally_eq [OF assms])
show "\T. \T \ C; compact T\ \ compact (p ` T)"
by (meson assms compact_continuous_image continuous_on_subset covering_space_imp_continuous)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
