The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy Wed Apr 10 13:34:55 2019 +0100
@@ -90,19 +90,19 @@
by (fastforce simp add: continuous_map_componentwise_UNIV continuous_map_diff)
lemma continuous_map_Euclidean_space_iff:
- "continuous_map (Euclidean_space m) euclideanreal g
+ "continuous_map (Euclidean_space m) euclidean g
= continuous_on (topspace (Euclidean_space m)) g"
proof
- assume "continuous_map (Euclidean_space m) euclideanreal g"
- then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclideanreal g"
+ assume "continuous_map (Euclidean_space m) euclidean g"
+ then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclidean g"
by (simp add: Euclidean_space_def euclidean_product_topology)
then show "continuous_on (topspace (Euclidean_space m)) g"
by (metis continuous_map_subtopology_eu subtopology_topspace topspace_Euclidean_space)
next
assume "continuous_on (topspace (Euclidean_space m)) g"
- then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclideanreal g"
+ then have "continuous_map (top_of_set {f. \<forall>n\<ge>m. f n = 0}) euclidean g"
by (metis (lifting) continuous_map_into_fulltopology continuous_map_subtopology_eu order_refl topspace_Euclidean_space)
- then show "continuous_map (Euclidean_space m) euclideanreal g"
+ then show "continuous_map (Euclidean_space m) euclidean g"
by (simp add: Euclidean_space_def euclidean_product_topology)
qed
@@ -201,6 +201,21 @@
by (simp add: nsphere subtopology_subtopology)
qed
+lemma topspace_nsphere_minus1:
+ assumes x: "x \<in> topspace (nsphere n)" and "x n = 0"
+ shows "x \<in> topspace (nsphere (n - Suc 0))"
+proof (cases "n = 0")
+ case True
+ then show ?thesis
+ using x by auto
+next
+ case False
+ have subt_eq: "nsphere (n - Suc 0) = subtopology (nsphere n) {x. x n = 0}"
+ by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator)
+ with x show ?thesis
+ by (simp add: assms)
+qed
+
lemma continuous_map_nsphere_reflection:
"continuous_map (nsphere n) (nsphere n) (\<lambda>x i. if i = k then -x i else x i)"
proof -
--- a/src/HOL/Analysis/Convex.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy Wed Apr 10 13:34:55 2019 +0100
@@ -272,8 +272,8 @@
with *[rule_format, of "2" ?u ?x] have s: "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) \<in> s"
using mu xy by auto
have grarr: "(\<Sum>j \<in> {Suc (Suc 0)..2}. ?u j *\<^sub>R ?x j) = (1 - \<mu>) *\<^sub>R y"
- using sum_head_Suc[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
- from sum_head_Suc[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
+ using sum.atLeast_Suc_atMost[of "Suc (Suc 0)" 2 "\<lambda> j. (1 - \<mu>) *\<^sub>R y"] by auto
+ from sum.atLeast_Suc_atMost[of "Suc 0" 2 "\<lambda> j. ?u j *\<^sub>R ?x j", simplified this]
have "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) = \<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y"
by auto
then have "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x \<in> s"
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Apr 10 13:34:55 2019 +0100
@@ -2090,6 +2090,14 @@
lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
by (simp add: is_interval_convex_1)
+lemma [simp]:
+ fixes r s::real
+ shows is_interval_io: "is_interval {..<r}"
+ and is_interval_oi: "is_interval {r<..}"
+ and is_interval_oo: "is_interval {r<..<s}"
+ and is_interval_oc: "is_interval {r<..s}"
+ and is_interval_co: "is_interval {r..<s}"
+ by (simp_all add: is_interval_convex_1)
subsection%unimportant \<open>Another intermediate value theorem formulation\<close>
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Apr 10 13:34:55 2019 +0100
@@ -1142,7 +1142,7 @@
unfolding nn_integral_sum[OF f] ..
also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
by (intro nn_integral_monotone_convergence_SUP_AE[symmetric])
- (elim AE_mp, auto simp: sum_nonneg simp del: sum_lessThan_Suc intro!: AE_I2 sum_mono2)
+ (elim AE_mp, auto simp: sum_nonneg simp del: sum.lessThan_Suc intro!: AE_I2 sum_mono2)
also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
by (intro nn_integral_cong_AE) (auto simp: suminf_eq_SUP)
finally show ?thesis by simp
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Apr 10 13:34:55 2019 +0100
@@ -221,14 +221,9 @@
by (simp add: cbox_interval)
lemma [simp]:
- fixes a b::"'a::ordered_euclidean_space" and r s::real
- shows is_interval_io: "is_interval {..<r}"
- and is_interval_ic: "is_interval {..a}"
- and is_interval_oi: "is_interval {r<..}"
+ fixes a b::"'a::ordered_euclidean_space"
+ shows is_interval_ic: "is_interval {..a}"
and is_interval_ci: "is_interval {a..}"
- and is_interval_oo: "is_interval {r<..<s}"
- and is_interval_oc: "is_interval {r<..s}"
- and is_interval_co: "is_interval {r..<s}"
and is_interval_cc: "is_interval {b..a}"
by (force simp: is_interval_def eucl_le[where 'a='a])+
--- a/src/HOL/Analysis/Poly_Roots.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Poly_Roots.thy Wed Apr 10 13:34:55 2019 +0100
@@ -174,7 +174,7 @@
have "\<exists>k\<le>n. b k \<noteq> 0"
apply (rule ccontr)
using polyfun_extremal [OF extr_prem, of 1]
- apply (auto simp: eventually_at_infinity b simp del: sum_atMost_Suc)
+ apply (auto simp: eventually_at_infinity b simp del: sum.atMost_Suc)
apply (drule_tac x="of_real ba" in spec, simp)
done
then show ?thesis using Suc.IH [of b] ins_ab
--- a/src/HOL/Analysis/Summation_Tests.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy Wed Apr 10 13:34:55 2019 +0100
@@ -211,7 +211,7 @@
hence "Bseq (\<lambda>n. (\<Sum>k=Suc 0..<Suc n. 2^k * f (2^k)) + f 1)"
by (intro Bseq_add, subst sum_shift_bounds_Suc_ivl) (simp add: atLeast0LessThan)
hence "Bseq (\<lambda>n. (\<Sum>k=0..<Suc n. 2^k * f (2^k)))"
- by (subst sum_head_upt_Suc) (simp_all add: add_ac)
+ by (subst sum.atLeast_Suc_lessThan) (simp_all add: add_ac)
thus "Bseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
by (subst (asm) Bseq_Suc_iff) (simp add: atLeast0LessThan)
next
--- a/src/HOL/Analysis/ex/Approximations.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Analysis/ex/Approximations.thy Wed Apr 10 13:34:55 2019 +0100
@@ -27,7 +27,7 @@
{
fix m :: nat
have "(\<Sum>k<Suc m. f k * x^k) = f 0 + (\<Sum>k=Suc 0..<Suc m. f k * x^k)"
- by (subst atLeast0LessThan [symmetric], subst sum_head_upt_Suc) simp_all
+ by (subst atLeast0LessThan [symmetric], subst sum.atLeast_Suc_lessThan) simp_all
also have "(\<Sum>k=Suc 0..<Suc m. f k * x^k) = (\<Sum>k<m. f (k+1) * x^k) * x"
by (subst sum_shift_bounds_Suc_ivl)
(simp add: sum_distrib_right algebra_simps atLeast0LessThan power_commutes)
@@ -420,7 +420,7 @@
fix m :: nat
have "(\<Sum>k<Suc m. inverse (f k * x^k)) =
inverse (f 0) + (\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k))"
- by (subst atLeast0LessThan [symmetric], subst sum_head_upt_Suc) simp_all
+ by (subst atLeast0LessThan [symmetric], subst sum.atLeast_Suc_lessThan) simp_all
also have "(\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k)) = (\<Sum>k<m. inverse (f (k+1) * x^k)) / x"
by (subst sum_shift_bounds_Suc_ivl)
(simp add: sum_distrib_left divide_inverse algebra_simps
--- a/src/HOL/Binomial.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Binomial.thy Wed Apr 10 13:34:55 2019 +0100
@@ -604,7 +604,7 @@
also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
pochhammer b (Suc n) =
(\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
- apply (subst sum_head_Suc)
+ apply (subst sum.atLeast_Suc_atMost)
apply simp
apply (subst sum_shift_bounds_cl_Suc_ivl)
apply (simp add: atLeast0AtMost)
@@ -858,7 +858,7 @@
unfolding S_def G_def ..
have "S (Suc mm) = G (Suc mm) 0 + (\<Sum>k=Suc 0..Suc mm. G (Suc mm) k)"
- using SG_def by (simp add: sum_head_Suc atLeast0AtMost [symmetric])
+ using SG_def by (simp add: sum.atLeast_Suc_atMost atLeast0AtMost [symmetric])
also have "(\<Sum>k=Suc 0..Suc mm. G (Suc mm) k) = (\<Sum>k=0..mm. G (Suc mm) (Suc k))"
by (subst sum_shift_bounds_cl_Suc_ivl) simp
also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + a gchoose (Suc k)) +
@@ -873,7 +873,7 @@
also have "\<dots> = (\<Sum>k<mm. (of_nat mm + a gchoose Suc k) * x^(Suc k) * y^(mm-k)) +
(of_nat mm + a gchoose (Suc mm)) * x^(Suc mm)"
(is "_ = ?A + ?B")
- by (subst sum_lessThan_Suc) simp
+ by (subst sum.lessThan_Suc) simp
also have "?A = (\<Sum>k=1..mm. (of_nat mm + a gchoose k) * x^k * y^(mm - k + 1))"
proof (subst sum_bounds_lt_plus1 [symmetric], intro sum.cong[OF refl], clarify)
fix k
@@ -894,7 +894,7 @@
y * (G mm 0 + (\<Sum>k=1..mm. (G mm k))) + (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
by (simp add: ring_distribs)
also have "G mm 0 + (\<Sum>k=1..mm. (G mm k)) = S mm"
- by (simp add: sum_head_Suc[symmetric] SG_def atLeast0AtMost)
+ by (simp add: sum.atLeast_Suc_atMost[symmetric] SG_def atLeast0AtMost)
finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + a gchoose (Suc mm)) * x^(Suc mm)"
by (simp add: algebra_simps)
also have "(of_nat mm + a gchoose (Suc mm)) = (-1) ^ (Suc mm) * (- a gchoose (Suc mm))"
@@ -1126,7 +1126,7 @@
also have "{I. I \<subseteq> K \<and> card I = 0} = {{}}"
using assms by (auto simp add: card_eq_0_iff K_def dest: finite_subset)
then have "?rhs = (\<Sum>i = 0..card K. (- 1) ^ (i + 1) * (\<Sum>I | I \<subseteq> K \<and> card I = i. 1 :: int)) + 1"
- by (subst (2) sum_head_Suc) simp_all
+ by (subst (2) sum.atLeast_Suc_atMost) simp_all
also have "\<dots> = (\<Sum>i = 0..card K. (- 1) * ((- 1) ^ i * int (card K choose i))) + 1"
using K by (subst n_subsets[symmetric]) simp_all
also have "\<dots> = - (\<Sum>i = 0..card K. (- 1) ^ i * int (card K choose i)) + 1"
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Apr 10 13:34:55 2019 +0100
@@ -342,7 +342,7 @@
lemma nth_subdegree_mult_right [simp]:
fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
shows "(f * g) $ (subdegree g) = f $ 0 * g $ subdegree g"
- by (cases "subdegree g") (simp_all add: fps_mult_nth nth_less_subdegree_zero sum_head_Suc)
+ by (cases "subdegree g") (simp_all add: fps_mult_nth nth_less_subdegree_zero sum.atLeast_Suc_atMost)
lemma nth_subdegree_mult [simp]:
fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps"
@@ -722,7 +722,7 @@
ultimately show ?case
using ab c fps_mult_nth_conv_upto_subdegree_left[of c a "subdegree c + n"]
fps_mult_nth_conv_upto_subdegree_left[of c b "subdegree c + n"]
- by (simp add: sum_head_Suc)
+ by (simp add: sum.atLeast_Suc_atMost)
qed
qed
thus "c = 0 \<or> a = b" by fast
@@ -814,7 +814,7 @@
by (auto simp: fps_pow_nth_below_subdegree)
with False Suc show ?thesis
using fps_mult_nth_conv_inside_subdegrees[of f "f^n" "Suc n * subdegree f"]
- sum_head_Suc[of
+ sum.atLeast_Suc_atMost[of
"subdegree f"
"Suc n * subdegree f - subdegree (f ^ n)"
"\<lambda>i. f $ i * f ^ n $ (Suc n * subdegree f - i)"
@@ -857,7 +857,7 @@
proof (cases m)
case 0 thus ?thesis using fps_mult_nth_1[of "fps_X" f] by (simp add: fps_X_def)
next
- case (Suc k) thus ?thesis by (simp add: fps_mult_nth fps_X_def sum_head_Suc)
+ case (Suc k) thus ?thesis by (simp add: fps_mult_nth fps_X_def sum.atLeast_Suc_atMost)
qed
ultimately show ?thesis by simp
qed (simp add: fps_X_def)
@@ -949,7 +949,7 @@
lemma fps_X_power_mult_nth:
"(fps_X^k * f) $ n = (if n < k then 0 else f $ (n - k))"
by (cases "n<k")
- (simp_all add: fps_mult_nth_conv_upto_subdegree_left fps_X_power_subdegree sum_head_Suc)
+ (simp_all add: fps_mult_nth_conv_upto_subdegree_left fps_X_power_subdegree sum.atLeast_Suc_atMost)
lemma fps_X_power_mult_right_nth:
"(f * fps_X^k) $ n = (if n < k then 0 else f $ (n - k))"
@@ -1122,7 +1122,7 @@
and n :: nat
assume "1 \<le> subdegree a"
hence "fps_shift 1 (a*b) $ n = (\<Sum>i=Suc 0..Suc n. a$i * b$(n+1-i))"
- using sum_head_Suc[of 0 "n+1" "\<lambda>i. a$i * b$(n+1-i)"]
+ using sum.atLeast_Suc_atMost[of 0 "n+1" "\<lambda>i. a$i * b$(n+1-i)"]
by (simp add: fps_mult_nth nth_less_subdegree_zero)
thus "fps_shift 1 (a*b) $ n = (fps_shift 1 a * b) $ n"
using sum_shift_bounds_cl_Suc_ivl[of "\<lambda>i. a$i * b$(n+1-i)" 0 n]
@@ -1763,7 +1763,7 @@
"(f * fps_right_inverse f y) $ n =
- 1 * sum (\<lambda>i. f$i * fps_right_inverse_constructor f y (n - i)) {1..n} +
sum (\<lambda>i. f$i * (fps_right_inverse_constructor f y (n - i))) {1..n}"
- by (simp add: fps_mult_nth sum_head_Suc mult.assoc f0[symmetric])
+ by (simp add: fps_mult_nth sum.atLeast_Suc_atMost mult.assoc f0[symmetric])
thus "(f * fps_right_inverse f y) $ n = 1 $ n" by (simp add: Suc)
qed (simp add: f0 fps_inverse_def)
qed
@@ -1935,7 +1935,7 @@
using 1 by auto
hence
"fps_right_inverse f (g$0) $ Suc k = 1 * g $ Suc k - g$0 * 1 $ Suc k"
- by (simp add: fps_mult_nth fg(1)[symmetric] algebra_simps fg(2)[symmetric] sum_head_Suc)
+ by (simp add: fps_mult_nth fg(1)[symmetric] algebra_simps fg(2)[symmetric] sum.atLeast_Suc_atMost)
with Suc show ?thesis by simp
qed simp
qed
@@ -2116,7 +2116,7 @@
moreover have "fps_left_inverse ones 1 $ Suc m = ones_inv $ Suc m"
proof (cases m)
case (Suc k) thus ?thesis
- using Suc m 1 by (simp add: ones_def ones_inv_def sum_head_Suc)
+ using Suc m 1 by (simp add: ones_def ones_inv_def sum.atLeast_Suc_atMost)
qed (simp add: ones_def ones_inv_def)
ultimately show ?thesis by simp
qed (simp add: ones_inv_def)
@@ -2183,7 +2183,7 @@
have f2_nth_simps:
"f^2 $ 1 = - of_nat 2" "f^2 $ 2 = 1" "\<And>n. n>2 \<Longrightarrow> f^2 $ n = 0"
- by (simp_all add: power2_eq_square f_def fps_mult_nth sum_head_Suc)
+ by (simp_all add: power2_eq_square f_def fps_mult_nth sum.atLeast_Suc_atMost)
show "fps_left_inverse (f^2) 1 = invf2"
proof (intro fps_ext)
@@ -3086,7 +3086,7 @@
of_nat (Suc n) * f$0 * g$(Suc n) +
(\<Sum>i=1..n. (of_nat (n - i + 1) + of_nat i) * f $ i * g $ (n - i + 1)) +
of_nat (Suc n) * f$(Suc n) * g$0"
- by (simp add: fps_mult_nth algebra_simps mult_of_nat_commute sum_head_Suc sum.distrib)
+ by (simp add: fps_mult_nth algebra_simps mult_of_nat_commute sum.atLeast_Suc_atMost sum.distrib)
moreover have
"\<forall>i\<in>{1..n}.
(of_nat (n - i + 1) + of_nat i) * f $ i * g $ (n - i + 1) =
@@ -3103,7 +3103,7 @@
ultimately have
"(f * fps_deriv g + fps_deriv f * g) $ n =
(\<Sum>i=0..Suc n. of_nat (Suc n) * f $ i * g $ (Suc n - i))"
- by (simp add: sum_head_Suc)
+ by (simp add: sum.atLeast_Suc_atMost)
with LHS show "fps_deriv (f * g) $ n = (f * fps_deriv g + fps_deriv f * g) $ n"
by simp
qed
@@ -3413,7 +3413,7 @@
next
case (Suc i)
with 1 j have "\<forall>m\<in>{0<..j}. a ^ i $ (j - m) = 0" by auto
- with Suc a0 show ?thesis by (simp add: fps_mult_nth sum_head_Suc)
+ with Suc a0 show ?thesis by (simp add: fps_mult_nth sum.atLeast_Suc_atMost)
qed
qed
@@ -3436,8 +3436,8 @@
have "\<forall>i\<in>{Suc 1..Suc n}. a ^ n $ (Suc n - i) = 0"
using a0 startsby_zero_power_prefix[of a n] by auto
thus ?case
- using a0 Suc sum_head_Suc[of 0 "Suc n" "\<lambda>i. a $ i * a ^ n $ (Suc n - i)"]
- sum_head_Suc[of 1 "Suc n" "\<lambda>i. a $ i * a ^ n $ (Suc n - i)"]
+ using a0 Suc sum.atLeast_Suc_atMost[of 0 "Suc n" "\<lambda>i. a $ i * a ^ n $ (Suc n - i)"]
+ sum.atLeast_Suc_atMost[of 1 "Suc n" "\<lambda>i. a $ i * a ^ n $ (Suc n - i)"]
by (simp add: fps_mult_nth)
qed simp
@@ -3806,8 +3806,8 @@
case (Suc m)
hence "(f * g) $ n = g $ Suc m - g $ m"
using fps_mult_nth[of f g "Suc m"]
- sum_head_Suc[of 0 "Suc m" "\<lambda>i. f $ i * g $ (Suc m - i)"]
- sum_head_Suc[of 1 "Suc m" "\<lambda>i. f $ i * g $ (Suc m - i)"]
+ sum.atLeast_Suc_atMost[of 0 "Suc m" "\<lambda>i. f $ i * g $ (Suc m - i)"]
+ sum.atLeast_Suc_atMost[of 1 "Suc m" "\<lambda>i. f $ i * g $ (Suc m - i)"]
by (simp add: f_def)
with Suc show ?thesis by (simp add: g_def)
qed (simp add: f_def g_def)
@@ -6368,7 +6368,7 @@
lemma sum_eq_if: "sum f {(n::nat) .. m} = (if m < n then 0 else f n + sum f {n+1 .. m})"
apply simp
apply (subst sum.insert[symmetric])
- apply (auto simp add: not_less sum_head_Suc)
+ apply (auto simp add: not_less sum.atLeast_Suc_atMost)
done
lemma pochhammer_rec_if: "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
--- a/src/HOL/Computational_Algebra/Polynomial.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Wed Apr 10 13:34:55 2019 +0100
@@ -1000,7 +1000,7 @@
next
case (pCons a p n)
then show ?case
- by (cases n) (simp_all add: sum_atMost_Suc_shift del: sum_atMost_Suc)
+ by (cases n) (simp_all add: sum_atMost_Suc_shift del: sum.atMost_Suc)
qed
lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Apr 10 13:34:55 2019 +0100
@@ -1183,7 +1183,7 @@
by auto
have sum_move0: "\<And>k F. sum F {0..<Suc k} = F 0 + sum (\<lambda> k. F (Suc k)) {0..<k}"
unfolding sum_shift_bounds_Suc_ivl[symmetric]
- unfolding sum_head_upt_Suc[OF zero_less_Suc] ..
+ unfolding sum.atLeast_Suc_lessThan[OF zero_less_Suc] ..
define C where "C = xs!x - c"
{
@@ -1253,7 +1253,7 @@
proof (cases "xs ! x = c")
case True
from True[symmetric] hyp[OF bnd_xs] Suc show ?thesis
- unfolding F_def Suc sum_head_upt_Suc[OF zero_less_Suc] sum_shift_bounds_Suc_ivl
+ unfolding F_def Suc sum.atLeast_Suc_lessThan[OF zero_less_Suc] sum_shift_bounds_Suc_ivl
by auto
next
case False
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Wed Apr 10 13:34:55 2019 +0100
@@ -34,7 +34,7 @@
by auto
show ?thesis
unfolding sum_distrib_left shift_pow uminus_add_conv_diff [symmetric] sum_negf[symmetric]
- sum_head_upt_Suc[OF zero_less_Suc]
+ sum.atLeast_Suc_lessThan[OF zero_less_Suc]
sum.reindex[OF inj_Suc, unfolded comp_def, symmetric, of "\<lambda> n. (-1)^n *a n * x^n"] by auto
qed
--- a/src/HOL/Groups_Big.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Groups_Big.thy Wed Apr 10 13:34:55 2019 +0100
@@ -106,6 +106,11 @@
ultimately show ?thesis by simp
qed
+lemma Int_Diff:
+ assumes "finite A"
+ shows "F g A = F g (A \<inter> B) \<^bold>* F g (A - B)"
+ by (subst subset_diff [where B = "A - B"]) (auto simp: Diff_Diff_Int assms)
+
lemma setdiff_irrelevant:
assumes "finite A"
shows "F g (A - {x. g x = z}) = F g A"
--- a/src/HOL/Hilbert_Choice.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy Wed Apr 10 13:34:55 2019 +0100
@@ -43,6 +43,11 @@
subsection \<open>Hilbert's Epsilon-operator\<close>
+lemma Eps_cong:
+ assumes "\<And>x. P x = Q x"
+ shows "Eps P = Eps Q"
+ using ext[of P Q, OF assms] by simp
+
text \<open>
Easier to apply than \<open>someI\<close> if the witness comes from an
existential formula.
--- a/src/HOL/Homology/Brouwer_Degree.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Homology/Brouwer_Degree.thy Wed Apr 10 13:34:55 2019 +0100
@@ -5,11 +5,6 @@
begin
-lemma Eps_cong:
- assumes "\<And>x. P x = Q x"
- shows "Eps P = Eps Q"
- using ext[of P Q, OF assms] by simp
-
subsection\<open>Reduced Homology\<close>
definition reduced_homology_group :: "int \<Rightarrow> 'a topology \<Rightarrow> 'a chain set monoid"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Homology/Invariance_of_Domain.thy Wed Apr 10 13:34:55 2019 +0100
@@ -0,0 +1,2429 @@
+section\<open>Invariance of Domain\<close>
+
+theory Invariance_of_Domain
+ imports Brouwer_Degree
+
+begin
+
+subsection\<open>Degree invariance mod 2 for map between pairs\<close>
+
+theorem Borsuk_odd_mapping_degree_step:
+ assumes cmf: "continuous_map (nsphere n) (nsphere n) f"
+ and f: "\<And>x. x \<in> topspace(nsphere n) \<Longrightarrow> (f \<circ> (\<lambda>x i. -x i)) x = ((\<lambda>x i. -x i) \<circ> f) x"
+ and fim: "f ` (topspace(nsphere(n - Suc 0))) \<subseteq> topspace(nsphere(n - Suc 0))"
+ shows "even (Brouwer_degree2 n f - Brouwer_degree2 (n - Suc 0) f)"
+proof (cases "n = 0")
+ case False
+ define neg where "neg \<equiv> \<lambda>x::nat\<Rightarrow>real. \<lambda>i. -x i"
+ define upper where "upper \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n \<ge> 0}"
+ define lower where "lower \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n \<le> 0}"
+ define equator where "equator \<equiv> \<lambda>n. {x::nat\<Rightarrow>real. x n = 0}"
+ define usphere where "usphere \<equiv> \<lambda>n. subtopology (nsphere n) (upper n)"
+ define lsphere where "lsphere \<equiv> \<lambda>n. subtopology (nsphere n) (lower n)"
+ have [simp]: "neg x i = -x i" for x i
+ by (force simp: neg_def)
+ have equator_upper: "equator n \<subseteq> upper n"
+ by (force simp: equator_def upper_def)
+ have upper_usphere: "subtopology (nsphere n) (upper n) = usphere n"
+ by (simp add: usphere_def)
+ let ?rhgn = "relative_homology_group n (nsphere n)"
+ let ?hi_ee = "hom_induced n (nsphere n) (equator n) (nsphere n) (equator n)"
+ interpret GE: comm_group "?rhgn (equator n)"
+ by simp
+ interpret HB: group_hom "?rhgn (equator n)"
+ "homology_group (int n - 1) (subtopology (nsphere n) (equator n))"
+ "hom_boundary n (nsphere n) (equator n)"
+ by (simp add: group_hom_axioms_def group_hom_def hom_boundary_hom)
+ interpret HIU: group_hom "?rhgn (equator n)"
+ "?rhgn (upper n)"
+ "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id"
+ by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
+ have subt_eq: "subtopology (nsphere n) {x. x n = 0} = nsphere (n - Suc 0)"
+ by (metis False Suc_pred le_zero_eq not_le subtopology_nsphere_equator)
+ then have equ: "subtopology (nsphere n) (equator n) = nsphere(n - Suc 0)"
+ "subtopology (lsphere n) (equator n) = nsphere(n - Suc 0)"
+ "subtopology (usphere n) (equator n) = nsphere(n - Suc 0)"
+ using False by (auto simp: lsphere_def usphere_def equator_def lower_def upper_def subtopology_subtopology simp flip: Collect_conj_eq cong: rev_conj_cong)
+ have cmr: "continuous_map (nsphere(n - Suc 0)) (nsphere(n - Suc 0)) f"
+ by (metis (no_types, lifting) IntE cmf fim continuous_map_from_subtopology continuous_map_in_subtopology equ(1) image_subset_iff topspace_subtopology)
+
+ have "f x n = 0" if "x \<in> topspace (nsphere n)" "x n = 0" for x
+ proof -
+ have "x \<in> topspace (nsphere (n - Suc 0))"
+ by (simp add: that topspace_nsphere_minus1)
+ moreover have "topspace (nsphere n) \<inter> {f. f n = 0} = topspace (nsphere (n - Suc 0))"
+ by (metis subt_eq topspace_subtopology)
+ ultimately show ?thesis
+ using cmr continuous_map_def by fastforce
+ qed
+ then have fimeq: "f ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
+ using fim cmf by (auto simp: equator_def continuous_map_def image_subset_iff)
+ have "\<And>k. continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. - x k)"
+ by (metis UNIV_I continuous_map_product_projection continuous_map_minus)
+ then have cm_neg: "continuous_map (nsphere m) (nsphere m) neg" for m
+ by (force simp: nsphere continuous_map_in_subtopology neg_def continuous_map_componentwise_UNIV intro: continuous_map_from_subtopology)
+ then have cm_neg_lu: "continuous_map (lsphere n) (usphere n) neg"
+ by (auto simp: lsphere_def usphere_def lower_def upper_def continuous_map_from_subtopology continuous_map_in_subtopology)
+ have neg_in_top_iff: "neg x \<in> topspace(nsphere m) \<longleftrightarrow> x \<in> topspace(nsphere m)" for m x
+ by (simp add: nsphere_def neg_def topspace_Euclidean_space)
+ obtain z where zcarr: "z \<in> carrier (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
+ and zeq: "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z}
+ = reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
+ using cyclic_reduced_homology_group_nsphere [of "int n - 1" "n - Suc 0"] by (auto simp: cyclic_group_def)
+ have "hom_boundary n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0}
+ \<in> Group.iso (relative_homology_group n
+ (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
+ (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
+ using iso_lower_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp
+ then obtain gp where g: "group_isomorphisms
+ (relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
+ (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
+ (hom_boundary n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})
+ gp"
+ by (auto simp: group.iso_iff_group_isomorphisms)
+ then interpret gp: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
+ "relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0}" gp
+ by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def)
+ obtain zp where zpcarr: "zp \<in> carrier(relative_homology_group n (lsphere n) (equator n))"
+ and zp_z: "hom_boundary n (lsphere n) (equator n) zp = z"
+ and zp_sg: "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp}
+ = relative_homology_group n (lsphere n) (equator n)"
+ proof
+ show "gp z \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
+ "hom_boundary n (lsphere n) (equator n) (gp z) = z"
+ using g zcarr by (auto simp: lsphere_def equator_def lower_def group_isomorphisms_def)
+ have giso: "gp \<in> Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
+ (relative_homology_group n (subtopology (nsphere n) {x. x n \<le> 0}) {x. x n = 0})"
+ by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym)
+ show "subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {gp z} =
+ relative_homology_group n (lsphere n) (equator n)"
+ apply (rule monoid.equality)
+ using giso gp.subgroup_generated_by_image [of "{z}"] zcarr
+ by (auto simp: lsphere_def equator_def lower_def zeq gp.iso_iff)
+ qed
+ have hb_iso: "hom_boundary n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0}
+ \<in> iso (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
+ (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))"
+ using iso_upper_hemisphere_reduced_homology_group [of "int n - 1" "n - Suc 0"] False by simp
+ then obtain gn where g: "group_isomorphisms
+ (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
+ (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
+ (hom_boundary n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})
+ gn"
+ by (auto simp: group.iso_iff_group_isomorphisms)
+ then interpret gn: group_hom "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
+ "relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0}" gn
+ by (simp add: group_hom_axioms_def group_hom_def group_isomorphisms_def)
+ obtain zn where zncarr: "zn \<in> carrier(relative_homology_group n (usphere n) (equator n))"
+ and zn_z: "hom_boundary n (usphere n) (equator n) zn = z"
+ and zn_sg: "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn}
+ = relative_homology_group n (usphere n) (equator n)"
+ proof
+ show "gn z \<in> carrier (relative_homology_group n (usphere n) (equator n))"
+ "hom_boundary n (usphere n) (equator n) (gn z) = z"
+ using g zcarr by (auto simp: usphere_def equator_def upper_def group_isomorphisms_def)
+ have giso: "gn \<in> Group.iso (reduced_homology_group (int n - 1) (nsphere (n - Suc 0)))
+ (relative_homology_group n (subtopology (nsphere n) {x. x n \<ge> 0}) {x. x n = 0})"
+ by (metis (mono_tags, lifting) g group_isomorphisms_imp_iso group_isomorphisms_sym)
+ show "subgroup_generated (relative_homology_group n (usphere n) (equator n)) {gn z} =
+ relative_homology_group n (usphere n) (equator n)"
+ apply (rule monoid.equality)
+ using giso gn.subgroup_generated_by_image [of "{z}"] zcarr
+ by (auto simp: usphere_def equator_def upper_def zeq gn.iso_iff)
+ qed
+ let ?hi_lu = "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id"
+ interpret gh_lu: group_hom "relative_homology_group n (lsphere n) (equator n)" "?rhgn (upper n)" ?hi_lu
+ by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
+ interpret gh_eef: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee f"
+ by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
+ define wp where "wp \<equiv> ?hi_lu zp"
+ then have wpcarr: "wp \<in> carrier(?rhgn (upper n))"
+ by (simp add: hom_induced_carrier)
+ have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \<ge> 0} id
+ \<in> iso (reduced_homology_group n (nsphere n))
+ (?rhgn {x. x n \<ge> 0})"
+ using iso_reduced_homology_group_upper_hemisphere [of n n n] by auto
+ then have "carrier(?rhgn {x. x n \<ge> 0})
+ \<subseteq> (hom_induced n (nsphere n) {} (nsphere n) {x. x n \<ge> 0} id)
+ ` carrier(reduced_homology_group n (nsphere n))"
+ by (simp add: iso_iff)
+ then obtain vp where vpcarr: "vp \<in> carrier(reduced_homology_group n (nsphere n))"
+ and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (upper n) id vp = wp"
+ using wpcarr by (auto simp: upper_def)
+ define wn where "wn \<equiv> hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id zn"
+ then have wncarr: "wn \<in> carrier(?rhgn (lower n))"
+ by (simp add: hom_induced_carrier)
+ have "hom_induced n (nsphere n) {} (nsphere n) {x. x n \<le> 0} id
+ \<in> iso (reduced_homology_group n (nsphere n))
+ (?rhgn {x. x n \<le> 0})"
+ using iso_reduced_homology_group_lower_hemisphere [of n n n] by auto
+ then have "carrier(?rhgn {x. x n \<le> 0})
+ \<subseteq> (hom_induced n (nsphere n) {} (nsphere n) {x. x n \<le> 0} id)
+ ` carrier(reduced_homology_group n (nsphere n))"
+ by (simp add: iso_iff)
+ then obtain vn where vpcarr: "vn \<in> carrier(reduced_homology_group n (nsphere n))"
+ and eqwp: "hom_induced n (nsphere n) {} (nsphere n) (lower n) id vn = wn"
+ using wncarr by (auto simp: lower_def)
+ define up where "up \<equiv> hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp"
+ then have upcarr: "up \<in> carrier(?rhgn (equator n))"
+ by (simp add: hom_induced_carrier)
+ define un where "un \<equiv> hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id zn"
+ then have uncarr: "un \<in> carrier(?rhgn (equator n))"
+ by (simp add: hom_induced_carrier)
+ have *: "(\<lambda>(x, y).
+ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
+ \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
+ hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
+ \<in> Group.iso
+ (relative_homology_group n (lsphere n) (equator n) \<times>\<times>
+ relative_homology_group n (usphere n) (equator n))
+ (?rhgn (equator n))"
+ proof (rule conjunct1 [OF exact_sequence_sum_lemma [OF abelian_relative_homology_group]])
+ show "hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id
+ \<in> Group.iso (relative_homology_group n (lsphere n) (equator n))
+ (?rhgn (upper n))"
+ apply (simp add: lsphere_def usphere_def equator_def lower_def upper_def)
+ using iso_relative_homology_group_lower_hemisphere by blast
+ show "hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id
+ \<in> Group.iso (relative_homology_group n (usphere n) (equator n))
+ (?rhgn (lower n))"
+ apply (simp_all add: lsphere_def usphere_def equator_def lower_def upper_def)
+ using iso_relative_homology_group_upper_hemisphere by blast+
+ show "exact_seq
+ ([?rhgn (lower n),
+ ?rhgn (equator n),
+ relative_homology_group n (lsphere n) (equator n)],
+ [hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id,
+ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id])"
+ unfolding lsphere_def usphere_def equator_def lower_def upper_def
+ by (rule homology_exactness_triple_3) force
+ show "exact_seq
+ ([?rhgn (upper n),
+ ?rhgn (equator n),
+ relative_homology_group n (usphere n) (equator n)],
+ [hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id,
+ hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id])"
+ unfolding lsphere_def usphere_def equator_def lower_def upper_def
+ by (rule homology_exactness_triple_3) force
+ next
+ fix x
+ assume "x \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
+ show "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id
+ (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x) =
+ hom_induced n (lsphere n) (equator n) (nsphere n) (upper n) id x"
+ by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def)
+ next
+ fix x
+ assume "x \<in> carrier (relative_homology_group n (usphere n) (equator n))"
+ show "hom_induced n (nsphere n) (equator n) (nsphere n) (lower n) id
+ (hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id x) =
+ hom_induced n (usphere n) (equator n) (nsphere n) (lower n) id x"
+ by (simp add: hom_induced_compose' subset_iff lsphere_def usphere_def equator_def lower_def upper_def)
+ qed
+ then have sb: "carrier (?rhgn (equator n))
+ \<subseteq> (\<lambda>(x, y).
+ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id x
+ \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
+ hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id y)
+ ` carrier (relative_homology_group n (lsphere n) (equator n) \<times>\<times>
+ relative_homology_group n (usphere n) (equator n))"
+ by (simp add: iso_iff)
+ obtain a b::int
+ where up_ab: "?hi_ee f up
+ = up [^]\<^bsub>?rhgn (equator n)\<^esub> a\<otimes>\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b"
+ proof -
+ have hiupcarr: "?hi_ee f up \<in> carrier(?rhgn (equator n))"
+ by (simp add: hom_induced_carrier)
+ obtain u v where u: "u \<in> carrier (relative_homology_group n (lsphere n) (equator n))"
+ and v: "v \<in> carrier (relative_homology_group n (usphere n) (equator n))"
+ and eq: "?hi_ee f up =
+ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id u
+ \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
+ hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id v"
+ using subsetD [OF sb hiupcarr] by auto
+ have "u \<in> carrier (subgroup_generated (relative_homology_group n (lsphere n) (equator n)) {zp})"
+ by (simp_all add: u zp_sg)
+ then obtain a::int where a: "u = zp [^]\<^bsub>relative_homology_group n (lsphere n) (equator n)\<^esub> a"
+ by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zpcarr)
+ have ae: "hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id
+ (pow (relative_homology_group n (lsphere n) (equator n)) zp a)
+ = pow (?rhgn (equator n)) (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp) a"
+ by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zpcarr)
+ have "v \<in> carrier (subgroup_generated (relative_homology_group n (usphere n) (equator n)) {zn})"
+ by (simp_all add: v zn_sg)
+ then obtain b::int where b: "v = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b"
+ by (metis group.carrier_subgroup_generated_by_singleton group_relative_homology_group rangeE zncarr)
+ have be: "hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
+ (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> b)
+ = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
+ zn [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b"
+ by (meson group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced zncarr)
+ show thesis
+ proof
+ show "?hi_ee f up
+ = up [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> un [^]\<^bsub>?rhgn (equator n)\<^esub> b"
+ using a ae b be eq local.up_def un_def by auto
+ qed
+ qed
+ have "(hom_boundary n (nsphere n) (equator n)
+ \<circ> hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id) zp = z"
+ using zp_z equ apply (simp add: lsphere_def naturality_hom_induced)
+ by (metis hom_boundary_carrier hom_induced_id)
+ then have up_z: "hom_boundary n (nsphere n) (equator n) up = z"
+ by (simp add: up_def)
+ have "(hom_boundary n (nsphere n) (equator n)
+ \<circ> hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id) zn = z"
+ using zn_z equ apply (simp add: usphere_def naturality_hom_induced)
+ by (metis hom_boundary_carrier hom_induced_id)
+ then have un_z: "hom_boundary n (nsphere n) (equator n) un = z"
+ by (simp add: un_def)
+ have Bd_ab: "Brouwer_degree2 (n - Suc 0) f = a + b"
+ proof (rule Brouwer_degree2_unique_generator; use False int_ops in simp_all)
+ show "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) f"
+ using cmr by auto
+ show "subgroup_generated (reduced_homology_group (int n - 1) (nsphere (n - Suc 0))) {z} =
+ reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
+ using zeq by blast
+ have "(hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f
+ \<circ> hom_boundary n (nsphere n) (equator n)) up
+ = (hom_boundary n (nsphere n) (equator n) \<circ>
+ ?hi_ee f) up"
+ using naturality_hom_induced [OF cmf fimeq, of n, symmetric]
+ by (simp add: subtopology_restrict equ fun_eq_iff)
+ also have "\<dots> = hom_boundary n (nsphere n) (equator n)
+ (up [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub>
+ a \<otimes>\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub>
+ un [^]\<^bsub>relative_homology_group n (nsphere n) (equator n)\<^esub> b)"
+ by (simp add: o_def up_ab)
+ also have "\<dots> = z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)"
+ using zcarr
+ apply (simp add: HB.hom_int_pow reduced_homology_group_def group.int_pow_subgroup_generated upcarr uncarr)
+ by (metis equ(1) group.int_pow_mult group_relative_homology_group hom_boundary_carrier un_z up_z)
+ finally show "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} f z =
+ z [^]\<^bsub>reduced_homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> (a + b)"
+ by (simp add: up_z)
+ qed
+ define u where "u \<equiv> up \<otimes>\<^bsub>?rhgn (equator n)\<^esub> inv\<^bsub>?rhgn (equator n)\<^esub> un"
+ have ucarr: "u \<in> carrier (?rhgn (equator n))"
+ by (simp add: u_def uncarr upcarr)
+ then have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)
+ \<longleftrightarrow> (GE.ord u) dvd a - b - Brouwer_degree2 n f"
+ by (simp add: GE.int_pow_eq)
+ moreover
+ have "GE.ord u = 0"
+ proof (clarsimp simp add: GE.ord_eq_0 ucarr)
+ fix d :: nat
+ assume "0 < d"
+ and "u [^]\<^bsub>?rhgn (equator n)\<^esub> d = singular_relboundary_set n (nsphere n) (equator n)"
+ then have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u [^]\<^bsub>?rhgn (upper n)\<^esub> d
+ = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
+ by (metis HIU.hom_one HIU.hom_nat_pow one_relative_homology_group ucarr)
+ moreover
+ have "?hi_lu
+ = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id \<circ>
+ hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id"
+ by (simp add: lsphere_def image_subset_iff equator_upper flip: hom_induced_compose)
+ then have p: "wp = hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id up"
+ by (simp add: local.up_def wp_def)
+ have n: "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id un = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
+ using homology_exactness_triple_3 [OF equator_upper, of n "nsphere n"]
+ using un_def zncarr by (auto simp: upper_usphere kernel_def)
+ have "hom_induced n (nsphere n) (equator n) (nsphere n) (upper n) id u = wp"
+ unfolding u_def
+ using p n HIU.inv_one HIU.r_one uncarr upcarr by auto
+ ultimately have "(wp [^]\<^bsub>?rhgn (upper n)\<^esub> d) = \<one>\<^bsub>?rhgn (upper n)\<^esub>"
+ by simp
+ moreover have "infinite (carrier (subgroup_generated (?rhgn (upper n)) {wp}))"
+ proof -
+ have "?rhgn (upper n) \<cong> reduced_homology_group n (nsphere n)"
+ unfolding upper_def
+ using iso_reduced_homology_group_upper_hemisphere [of n n n]
+ by (blast intro: group.iso_sym group_reduced_homology_group is_isoI)
+ also have "\<dots> \<cong> integer_group"
+ by (simp add: reduced_homology_group_nsphere)
+ finally have iso: "?rhgn (upper n) \<cong> integer_group" .
+ have "carrier (subgroup_generated (?rhgn (upper n)) {wp}) = carrier (?rhgn (upper n))"
+ using gh_lu.subgroup_generated_by_image [of "{zp}"] zpcarr HIU.carrier_subgroup_generated_subset
+ gh_lu.iso_iff iso_relative_homology_group_lower_hemisphere zp_sg
+ by (auto simp: lower_def lsphere_def upper_def equator_def wp_def)
+ then show ?thesis
+ using infinite_UNIV_int iso_finite [OF iso] by simp
+ qed
+ ultimately show False
+ using HIU.finite_cyclic_subgroup \<open>0 < d\<close> wpcarr by blast
+ qed
+ ultimately have iff: "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)
+ \<longleftrightarrow> Brouwer_degree2 n f = a - b"
+ by auto
+ have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f = ?hi_ee f u"
+ proof -
+ have ne: "topspace (nsphere n) \<inter> equator n \<noteq> {}"
+ by (metis equ(1) nonempty_nsphere topspace_subtopology)
+ have eq1: "hom_boundary n (nsphere n) (equator n) u
+ = \<one>\<^bsub>reduced_homology_group (int n - 1) (subtopology (nsphere n) (equator n))\<^esub>"
+ using one_reduced_homology_group u_def un_z uncarr up_z upcarr by force
+ then have uhom: "u \<in> hom_induced n (nsphere n) {} (nsphere n) (equator n) id `
+ carrier (reduced_homology_group (int n) (nsphere n))"
+ using homology_exactness_reduced_1 [OF ne, of n] eq1 ucarr by (auto simp: kernel_def)
+ then obtain v where vcarr: "v \<in> carrier (reduced_homology_group (int n) (nsphere n))"
+ and ueq: "u = hom_induced n (nsphere n) {} (nsphere n) (equator n) id v"
+ by blast
+ interpret GH_hi: group_hom "homology_group n (nsphere n)"
+ "?rhgn (equator n)"
+ "hom_induced n (nsphere n) {} (nsphere n) (equator n) id"
+ by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
+ have poweq: "pow (homology_group n (nsphere n)) x i = pow (reduced_homology_group n (nsphere n)) x i"
+ for x and i::int
+ by (simp add: False un_reduced_homology_group)
+ have vcarr': "v \<in> carrier (homology_group n (nsphere n))"
+ using carrier_reduced_homology_group_subset vcarr by blast
+ have "u [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 n f
+ = hom_induced n (nsphere n) {} (nsphere n) (equator n) f v"
+ using vcarr vcarr'
+ by (simp add: ueq poweq hom_induced_compose' cmf flip: GH_hi.hom_int_pow Brouwer_degree2)
+ also have "\<dots> = hom_induced n (nsphere n) (topspace(nsphere n) \<inter> equator n) (nsphere n) (equator n) f
+ (hom_induced n (nsphere n) {} (nsphere n) (topspace(nsphere n) \<inter> equator n) id v)"
+ using fimeq by (simp add: hom_induced_compose' cmf)
+ also have "\<dots> = ?hi_ee f u"
+ by (metis hom_induced inf.left_idem ueq)
+ finally show ?thesis .
+ qed
+ moreover
+ interpret gh_een: group_hom "?rhgn (equator n)" "?rhgn (equator n)" "?hi_ee neg"
+ by (simp add: group_hom_axioms_def group_hom_def hom_induced_hom)
+ have hi_up_eq_un: "?hi_ee neg up = un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
+ proof -
+ have "?hi_ee neg (hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) id zp)
+ = hom_induced n (lsphere n) (equator n) (nsphere n) (equator n) (neg \<circ> id) zp"
+ by (intro hom_induced_compose') (auto simp: lsphere_def equator_def cm_neg)
+ also have "\<dots> = hom_induced n (usphere n) (equator n) (nsphere n) (equator n) id
+ (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)"
+ by (subst hom_induced_compose' [OF cm_neg_lu]) (auto simp: usphere_def equator_def)
+ also have "hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp
+ = zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
+ proof -
+ let ?hb = "hom_boundary n (usphere n) (equator n)"
+ have eq: "subtopology (nsphere n) {x. x n \<ge> 0} = usphere n \<and> {x. x n = 0} = equator n"
+ by (auto simp: usphere_def upper_def equator_def)
+ with hb_iso have inj: "inj_on (?hb) (carrier (relative_homology_group n (usphere n) (equator n)))"
+ by (simp add: iso_iff)
+ interpret hb_hom: group_hom "relative_homology_group n (usphere n) (equator n)"
+ "reduced_homology_group (int n - 1) (nsphere (n - Suc 0))"
+ "?hb"
+ using hb_iso iso_iff eq group_hom_axioms_def group_hom_def by fastforce
+ show ?thesis
+ proof (rule inj_onD [OF inj])
+ have *: "hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg z
+ = z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg"
+ using Brouwer_degree2 [of z "n - Suc 0" neg] False zcarr
+ by (simp add: int_ops group.int_pow_subgroup_generated reduced_homology_group_def)
+ have "?hb \<circ>
+ hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg
+ = hom_induced (int n - 1) (nsphere (n - Suc 0)) {} (nsphere (n - Suc 0)) {} neg \<circ>
+ hom_boundary n (lsphere n) (equator n)"
+ apply (subst naturality_hom_induced [OF cm_neg_lu])
+ apply (force simp: equator_def neg_def)
+ by (simp add: equ)
+ then have "?hb
+ (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp)
+ = (z [^]\<^bsub>homology_group (int n - 1) (nsphere (n - Suc 0))\<^esub> Brouwer_degree2 (n - Suc 0) neg)"
+ by (metis "*" comp_apply zp_z)
+ also have "\<dots> = ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub>
+ Brouwer_degree2 (n - Suc 0) neg)"
+ by (metis group.int_pow_subgroup_generated group_relative_homology_group hb_hom.hom_int_pow reduced_homology_group_def zcarr zn_z zncarr)
+ finally show "?hb (hom_induced n (lsphere n) (equator n) (usphere n) (equator n) neg zp) =
+ ?hb (zn [^]\<^bsub>relative_homology_group n (usphere n) (equator n)\<^esub>
+ Brouwer_degree2 (n - Suc 0) neg)" by simp
+ qed (auto simp: hom_induced_carrier group.int_pow_closed zncarr)
+ qed
+ finally show ?thesis
+ by (metis (no_types, lifting) group_hom.hom_int_pow group_hom_axioms_def group_hom_def group_relative_homology_group hom_induced local.up_def un_def zncarr)
+ qed
+ have "continuous_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg"
+ using cm_neg by blast
+ then have "homeomorphic_map (nsphere (n - Suc 0)) (nsphere (n - Suc 0)) neg"
+ apply (auto simp: homeomorphic_map_maps homeomorphic_maps_def)
+ apply (rule_tac x=neg in exI, auto)
+ done
+ then have Brouwer_degree2_21: "Brouwer_degree2 (n - Suc 0) neg ^ 2 = 1"
+ using Brouwer_degree2_homeomorphic_map power2_eq_1_iff by force
+ have hi_un_eq_up: "?hi_ee neg un = up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" (is "?f un = ?y")
+ proof -
+ have [simp]: "neg \<circ> neg = id"
+ by force
+ have "?f (?f ?y) = ?y"
+ apply (subst hom_induced_compose' [OF cm_neg _ cm_neg])
+ apply(force simp: equator_def)
+ apply (simp add: upcarr hom_induced_id_gen)
+ done
+ moreover have "?f ?y = un"
+ using upcarr apply (simp only: gh_een.hom_int_pow hi_up_eq_un)
+ by (metis (no_types, lifting) Brouwer_degree2_21 GE.group_l_invI GE.l_inv_ex group.int_pow_1 group.int_pow_pow power2_eq_1_iff uncarr zmult_eq_1_iff)
+ ultimately show "?f un = ?y"
+ by simp
+ qed
+ have "?hi_ee f un = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b"
+ proof -
+ let ?TE = "topspace (nsphere n) \<inter> equator n"
+ have fneg: "(f \<circ> neg) x = (neg \<circ> f) x" if "x \<in> topspace (nsphere n)" for x
+ using f [OF that] by (force simp: neg_def)
+ have neg_im: "neg ` (topspace (nsphere n) \<inter> equator n) \<subseteq> topspace (nsphere n) \<inter> equator n"
+ by (metis cm_neg continuous_map_image_subset_topspace equ(1) topspace_subtopology)
+ have 1: "hom_induced n (nsphere n) ?TE (nsphere n) ?TE f \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg
+ = hom_induced n (nsphere n) ?TE (nsphere n) ?TE neg \<circ> hom_induced n (nsphere n) ?TE (nsphere n) ?TE f"
+ using neg_im fimeq cm_neg cmf
+ apply (simp add: flip: hom_induced_compose del: hom_induced_restrict)
+ using fneg by (auto intro: hom_induced_eq)
+ have "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
+ = un [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * a * Brouwer_degree2 (n - 1) neg)
+ \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
+ up [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - 1) neg * b * Brouwer_degree2 (n - 1) neg)"
+ proof -
+ have "Brouwer_degree2 (n - Suc 0) neg = 1 \<or> Brouwer_degree2 (n - Suc 0) neg = - 1"
+ using Brouwer_degree2_21 power2_eq_1_iff by blast
+ then show ?thesis
+ by fastforce
+ qed
+ also have "\<dots> = ((un [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub>
+ (up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - 1) neg) [^]\<^bsub>?rhgn (equator n)\<^esub> b) [^]\<^bsub>?rhgn (equator n)\<^esub>
+ Brouwer_degree2 (n - 1) neg"
+ by (simp add: GE.int_pow_distrib GE.int_pow_pow uncarr upcarr)
+ also have "\<dots> = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
+ by (simp add: gh_een.hom_int_pow hi_un_eq_up hi_up_eq_un uncarr up_ab upcarr)
+ finally have 2: "(un [^]\<^bsub>?rhgn (equator n)\<^esub> a) \<otimes>\<^bsub>?rhgn (equator n)\<^esub> (up [^]\<^bsub>?rhgn (equator n)\<^esub> b)
+ = ?hi_ee neg (?hi_ee f up) [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg" .
+ have "un = ?hi_ee neg up [^]\<^bsub>?rhgn (equator n)\<^esub> Brouwer_degree2 (n - Suc 0) neg"
+ by (metis (no_types, hide_lams) Brouwer_degree2_21 GE.int_pow_1 GE.int_pow_pow hi_up_eq_un power2_eq_1_iff uncarr zmult_eq_1_iff)
+ moreover have "?hi_ee f ((?hi_ee neg up) [^]\<^bsub>?rhgn (equator n)\<^esub> (Brouwer_degree2 (n - Suc 0) neg))
+ = un [^]\<^bsub>?rhgn (equator n)\<^esub> a \<otimes>\<^bsub>?rhgn (equator n)\<^esub> up [^]\<^bsub>?rhgn (equator n)\<^esub> b"
+ using 1 2 by (simp add: hom_induced_carrier gh_eef.hom_int_pow fun_eq_iff)
+ ultimately show ?thesis
+ by blast
+ qed
+ then have "?hi_ee f u = u [^]\<^bsub>?rhgn (equator n)\<^esub> (a - b)"
+ by (simp add: u_def upcarr uncarr up_ab GE.int_pow_diff GE.m_ac GE.int_pow_distrib GE.int_pow_inv GE.inv_mult_group)
+ ultimately
+ have "Brouwer_degree2 n f = a - b"
+ using iff by blast
+ with Bd_ab show ?thesis
+ by simp
+qed simp
+
+
+subsection \<open>General Jordan-Brouwer separation theorem and invariance of dimension\<close>
+
+proposition relative_homology_group_Euclidean_complement_step:
+ assumes "closedin (Euclidean_space n) S"
+ shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
+ \<cong> relative_homology_group (p + k) (Euclidean_space (n+k)) (topspace(Euclidean_space (n+k)) - S)"
+proof -
+ have *: "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
+ \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \<in> S. x n = 0})"
+ (is "?lhs \<cong> ?rhs")
+ if clo: "closedin (Euclidean_space (Suc n)) S" and cong: "\<And>x y. \<lbrakk>x \<in> S; \<And>i. i \<noteq> n \<Longrightarrow> x i = y i\<rbrakk> \<Longrightarrow> y \<in> S"
+ for p n S
+ proof -
+ have Ssub: "S \<subseteq> topspace (Euclidean_space (Suc n))"
+ by (meson clo closedin_def)
+ define lo where "lo \<equiv> {x \<in> topspace(Euclidean_space (Suc n)). x n < (if x \<in> S then 0 else 1)}"
+ define hi where "hi = {x \<in> topspace(Euclidean_space (Suc n)). x n > (if x \<in> S then 0 else -1)}"
+ have lo_hi_Int: "lo \<inter> hi = {x \<in> topspace(Euclidean_space (Suc n)) - S. x n \<in> {-1<..<1}}"
+ by (auto simp: hi_def lo_def)
+ have lo_hi_Un: "lo \<union> hi = topspace(Euclidean_space (Suc n)) - {x \<in> S. x n = 0}"
+ by (auto simp: hi_def lo_def)
+ define ret where "ret \<equiv> \<lambda>c::real. \<lambda>x i. if i = n then c else x i"
+ have cm_ret: "continuous_map (powertop_real UNIV) (powertop_real UNIV) (ret t)" for t
+ by (auto simp: ret_def continuous_map_componentwise_UNIV intro: continuous_map_product_projection)
+ let ?ST = "\<lambda>t. subtopology (Euclidean_space (Suc n)) {x. x n = t}"
+ define squashable where
+ "squashable \<equiv> \<lambda>t S. \<forall>x t'. x \<in> S \<and> (x n \<le> t' \<and> t' \<le> t \<or> t \<le> t' \<and> t' \<le> x n) \<longrightarrow> ret t' x \<in> S"
+ have squashable: "squashable t (topspace(Euclidean_space(Suc n)))" for t
+ by (simp add: squashable_def topspace_Euclidean_space ret_def)
+ have squashableD: "\<lbrakk>squashable t S; x \<in> S; x n \<le> t' \<and> t' \<le> t \<or> t \<le> t' \<and> t' \<le> x n\<rbrakk> \<Longrightarrow> ret t' x \<in> S" for x t' t S
+ by (auto simp: squashable_def)
+ have "squashable 1 hi"
+ by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong)
+ have "squashable t UNIV" for t
+ by (force simp: squashable_def hi_def ret_def topspace_Euclidean_space intro: cong)
+ have squashable_0_lohi: "squashable 0 (lo \<inter> hi)"
+ using Ssub
+ by (auto simp: squashable_def hi_def lo_def ret_def topspace_Euclidean_space intro: cong)
+ have rm_ret: "retraction_maps (subtopology (Euclidean_space (Suc n)) U)
+ (subtopology (Euclidean_space (Suc n)) {x. x \<in> U \<and> x n = t})
+ (ret t) id"
+ if "squashable t U" for t U
+ unfolding retraction_maps_def
+ proof (intro conjI ballI)
+ show "continuous_map (subtopology (Euclidean_space (Suc n)) U)
+ (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t}) (ret t)"
+ apply (simp add: cm_ret continuous_map_in_subtopology continuous_map_from_subtopology Euclidean_space_def)
+ using that by (fastforce simp: squashable_def ret_def)
+ next
+ show "continuous_map (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t})
+ (subtopology (Euclidean_space (Suc n)) U) id"
+ using continuous_map_in_subtopology by fastforce
+ show "ret t (id x) = x"
+ if "x \<in> topspace (subtopology (Euclidean_space (Suc n)) {x \<in> U. x n = t})" for x
+ using that by (simp add: topspace_Euclidean_space ret_def fun_eq_iff)
+ qed
+ have cm_snd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S))
+ euclideanreal (\<lambda>x. snd x k)" for k::nat and S
+ using continuous_map_componentwise_UNIV continuous_map_into_fulltopology continuous_map_snd by fastforce
+ have cm_fstsnd: "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (powertop_real UNIV) S))
+ euclideanreal (\<lambda>x. fst x * snd x k)" for k::nat and S
+ by (intro continuous_intros continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd)
+ have hw_sub: "homotopic_with (\<lambda>k. k ` V \<subseteq> V) (subtopology (Euclidean_space (Suc n)) U)
+ (subtopology (Euclidean_space (Suc n)) U) (ret t) id"
+ if "squashable t U" "squashable t V" for U V t
+ unfolding homotopic_with_def
+ proof (intro exI conjI allI ballI)
+ let ?h = "\<lambda>(z,x). ret ((1 - z) * t + z * x n) x"
+ show "(\<lambda>x. ?h (u, x)) ` V \<subseteq> V" if "u \<in> {0..1}" for u
+ using that
+ by clarsimp (metis squashableD [OF \<open>squashable t V\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
+ have 1: "?h ` ({0..1} \<times> ({x. \<forall>i\<ge>Suc n. x i = 0} \<inter> U)) \<subseteq> U"
+ by clarsimp (metis squashableD [OF \<open>squashable t U\<close>] convex_bound_le diff_ge_0_iff_ge eq_diff_eq' le_cases less_eq_real_def segment_bound_lemma)
+ show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (Euclidean_space (Suc n)) U))
+ (subtopology (Euclidean_space (Suc n)) U) ?h"
+ apply (simp add: continuous_map_in_subtopology Euclidean_space_def subtopology_subtopology 1)
+ apply (auto simp: case_prod_unfold ret_def continuous_map_componentwise_UNIV)
+ apply (intro continuous_map_into_fulltopology [OF continuous_map_fst] cm_snd continuous_intros)
+ by (auto simp: cm_snd)
+ qed (auto simp: ret_def)
+ have cs_hi: "contractible_space(subtopology (Euclidean_space(Suc n)) hi)"
+ proof -
+ have "homotopic_with (\<lambda>x. True) (?ST 1) (?ST 1) id (\<lambda>x. (\<lambda>i. if i = n then 1 else 0))"
+ apply (subst homotopic_with_sym)
+ apply (simp add: homotopic_with)
+ apply (rule_tac x="(\<lambda>(z,x) i. if i=n then 1 else z * x i)" in exI)
+ apply (auto simp: Euclidean_space_def subtopology_subtopology continuous_map_in_subtopology case_prod_unfold continuous_map_componentwise_UNIV cm_fstsnd)
+ done
+ then have "contractible_space (?ST 1)"
+ unfolding contractible_space_def by metis
+ moreover have "?thesis = contractible_space (?ST 1)"
+ proof (intro deformation_retract_imp_homotopy_equivalent_space homotopy_equivalent_space_contractibility)
+ have "{x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x \<in> hi. x n = 1} = {x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x. x n = 1}"
+ by (auto simp: hi_def topspace_Euclidean_space)
+ then have eq: "subtopology (Euclidean_space (Suc n)) {x. x \<in> hi \<and> x n = 1} = ?ST 1"
+ by (simp add: Euclidean_space_def subtopology_subtopology)
+ show "homotopic_with (\<lambda>x. True) (subtopology (Euclidean_space (Suc n)) hi) (subtopology (Euclidean_space (Suc n)) hi) (ret 1) id"
+ using hw_sub [OF \<open>squashable 1 hi\<close> \<open>squashable 1 UNIV\<close>] eq by simp
+ show "retraction_maps (subtopology (Euclidean_space (Suc n)) hi) (?ST 1) (ret 1) id"
+ using rm_ret [OF \<open>squashable 1 hi\<close>] eq by simp
+ qed
+ ultimately show ?thesis by metis
+ qed
+ have "?lhs \<cong> relative_homology_group p (Euclidean_space (Suc n)) (lo \<inter> hi)"
+ proof (rule group.iso_sym [OF _ deformation_retract_imp_isomorphic_relative_homology_groups])
+ have "{x. \<forall>i\<ge>Suc n. x i = 0} \<inter> {x. x n = 0} = {x. \<forall>i\<ge>n. x i = (0::real)}"
+ by auto (metis le_less_Suc_eq not_le)
+ then have "?ST 0 = Euclidean_space n"
+ by (simp add: Euclidean_space_def subtopology_subtopology)
+ then show "retraction_maps (Euclidean_space (Suc n)) (Euclidean_space n) (ret 0) id"
+ using rm_ret [OF \<open>squashable 0 UNIV\<close>] by auto
+ then have "ret 0 x \<in> topspace (Euclidean_space n)"
+ if "x \<in> topspace (Euclidean_space (Suc n))" "-1 < x n" "x n < 1" for x
+ using that by (simp add: continuous_map_def retraction_maps_def)
+ then show "(ret 0) ` (lo \<inter> hi) \<subseteq> topspace (Euclidean_space n) - S"
+ by (auto simp: local.cong ret_def hi_def lo_def)
+ show "homotopic_with (\<lambda>h. h ` (lo \<inter> hi) \<subseteq> lo \<inter> hi) (Euclidean_space (Suc n)) (Euclidean_space (Suc n)) (ret 0) id"
+ using hw_sub [OF squashable squashable_0_lohi] by simp
+ qed (auto simp: lo_def hi_def Euclidean_space_def)
+ also have "\<dots> \<cong> relative_homology_group p (subtopology (Euclidean_space (Suc n)) hi) (lo \<inter> hi)"
+ proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_inclusion_contractible])
+ show "contractible_space (subtopology (Euclidean_space (Suc n)) hi)"
+ by (simp add: cs_hi)
+ show "topspace (Euclidean_space (Suc n)) \<inter> hi \<noteq> {}"
+ apply (simp add: hi_def topspace_Euclidean_space set_eq_iff)
+ apply (rule_tac x="\<lambda>i. if i = n then 1 else 0" in exI, auto)
+ done
+ qed auto
+ also have "\<dots> \<cong> relative_homology_group p (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) lo"
+ proof -
+ have oo: "openin (Euclidean_space (Suc n)) {x \<in> topspace (Euclidean_space (Suc n)). x n \<in> A}"
+ if "open A" for A
+ proof (rule openin_continuous_map_preimage)
+ show "continuous_map (Euclidean_space (Suc n)) euclideanreal (\<lambda>x. x n)"
+ proof -
+ have "\<forall>n f. continuous_map (product_topology f UNIV) (f (n::nat)) (\<lambda>f. f n::real)"
+ by (simp add: continuous_map_product_projection)
+ then show ?thesis
+ using Euclidean_space_def continuous_map_from_subtopology
+ by (metis (mono_tags))
+ qed
+ qed (auto intro: that)
+ have "openin (Euclidean_space(Suc n)) lo"
+ apply (simp add: openin_subopen [of _ lo])
+ apply (simp add: lo_def, safe)
+ apply (force intro: oo [of "lessThan 0", simplified] open_Collect_less)
+ apply (rule_tac x="{x \<in> topspace(Euclidean_space(Suc n)). x n < 1}
+ \<inter> (topspace(Euclidean_space(Suc n)) - S)" in exI)
+ using clo apply (force intro: oo [of "lessThan 1", simplified] open_Collect_less)
+ done
+ moreover have "openin (Euclidean_space(Suc n)) hi"
+ apply (simp add: openin_subopen [of _ hi])
+ apply (simp add: hi_def, safe)
+ apply (force intro: oo [of "greaterThan 0", simplified] open_Collect_less)
+ apply (rule_tac x="{x \<in> topspace(Euclidean_space(Suc n)). x n > -1}
+ \<inter> (topspace(Euclidean_space(Suc n)) - S)" in exI)
+ using clo apply (force intro: oo [of "greaterThan (-1)", simplified] open_Collect_less)
+ done
+ ultimately
+ have *: "subtopology (Euclidean_space (Suc n)) (lo \<union> hi) closure_of
+ (topspace (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) - hi)
+ \<subseteq> subtopology (Euclidean_space (Suc n)) (lo \<union> hi) interior_of lo"
+ by (metis (no_types, lifting) Diff_idemp Diff_subset_conv Un_commute Un_upper2 closure_of_interior_of interior_of_closure_of interior_of_complement interior_of_eq lo_hi_Un openin_Un openin_open_subtopology topspace_subtopology_subset)
+ have eq: "((lo \<union> hi) \<inter> (lo \<union> hi - (topspace (Euclidean_space (Suc n)) \<inter> (lo \<union> hi) - hi))) = hi"
+ "(lo - (topspace (Euclidean_space (Suc n)) \<inter> (lo \<union> hi) - hi)) = lo \<inter> hi"
+ by (auto simp: lo_def hi_def Euclidean_space_def)
+ show ?thesis
+ using homology_excision_axiom [OF *, of "lo \<union> hi" p]
+ by (force simp: subtopology_subtopology eq is_iso_def)
+ qed
+ also have "\<dots> \<cong> relative_homology_group (p + 1 - 1) (subtopology (Euclidean_space (Suc n)) (lo \<union> hi)) lo"
+ by simp
+ also have "\<dots> \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (lo \<union> hi)"
+ proof (rule group.iso_sym [OF _ isomorphic_relative_homology_groups_relboundary_contractible])
+ have proj: "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>f. f n)"
+ by (metis UNIV_I continuous_map_product_projection)
+ have hilo: "\<And>x. x \<in> hi \<Longrightarrow> (\<lambda>i. if i = n then - x i else x i) \<in> lo"
+ "\<And>x. x \<in> lo \<Longrightarrow> (\<lambda>i. if i = n then - x i else x i) \<in> hi"
+ using local.cong
+ by (auto simp: hi_def lo_def topspace_Euclidean_space split: if_split_asm)
+ have "subtopology (Euclidean_space (Suc n)) hi homeomorphic_space subtopology (Euclidean_space (Suc n)) lo"
+ unfolding homeomorphic_space_def
+ apply (rule_tac x="\<lambda>x i. if i = n then -(x i) else x i" in exI)+
+ using proj
+ apply (auto simp: homeomorphic_maps_def Euclidean_space_def continuous_map_in_subtopology
+ hilo continuous_map_componentwise_UNIV continuous_map_from_subtopology continuous_map_minus
+ intro: continuous_map_from_subtopology continuous_map_product_projection)
+ done
+ then have "contractible_space(subtopology (Euclidean_space(Suc n)) hi)
+ \<longleftrightarrow> contractible_space (subtopology (Euclidean_space (Suc n)) lo)"
+ by (rule homeomorphic_space_contractibility)
+ then show "contractible_space (subtopology (Euclidean_space (Suc n)) lo)"
+ using cs_hi by auto
+ show "topspace (Euclidean_space (Suc n)) \<inter> lo \<noteq> {}"
+ apply (simp add: lo_def Euclidean_space_def set_eq_iff)
+ apply (rule_tac x="\<lambda>i. if i = n then -1 else 0" in exI, auto)
+ done
+ qed auto
+ also have "\<dots> \<cong> ?rhs"
+ by (simp flip: lo_hi_Un)
+ finally show ?thesis .
+ qed
+ show ?thesis
+ proof (induction k)
+ case (Suc m)
+ with assms obtain T where cloT: "closedin (powertop_real UNIV) T"
+ and SeqT: "S = T \<inter> {x. \<forall>i\<ge>n. x i = 0}"
+ by (auto simp: Euclidean_space_def closedin_subtopology)
+ then have "closedin (Euclidean_space (m + n)) S"
+ apply (simp add: Euclidean_space_def closedin_subtopology)
+ apply (rule_tac x="T \<inter> topspace(Euclidean_space n)" in exI)
+ using closedin_Euclidean_space topspace_Euclidean_space by force
+ moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
+ \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)"
+ if "closedin (Euclidean_space n) S" for p n
+ proof -
+ define S' where "S' \<equiv> {x \<in> topspace(Euclidean_space(Suc n)). (\<lambda>i. if i < n then x i else 0) \<in> S}"
+ have Ssub_n: "S \<subseteq> topspace (Euclidean_space n)"
+ by (meson that closedin_def)
+ have "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S')
+ \<cong> relative_homology_group (p + 1) (Euclidean_space (Suc n)) (topspace(Euclidean_space (Suc n)) - {x \<in> S'. x n = 0})"
+ proof (rule *)
+ have cm: "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>f. f u)" for u
+ by (metis UNIV_I continuous_map_product_projection)
+ have "continuous_map (subtopology (powertop_real UNIV) {x. \<forall>i>n. x i = 0}) euclideanreal
+ (\<lambda>x. if k \<le> n then x k else 0)" for k
+ by (simp add: continuous_map_from_subtopology [OF cm])
+ moreover have "\<forall>i\<ge>n. (if i < n then x i else 0) = 0"
+ if "x \<in> topspace (subtopology (powertop_real UNIV) {x. \<forall>i>n. x i = 0})" for x
+ using that by simp
+ ultimately have "continuous_map (Euclidean_space (Suc n)) (Euclidean_space n) (\<lambda>x i. if i < n then x i else 0)"
+ by (simp add: Euclidean_space_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
+ continuous_map_from_subtopology [OF cm] image_subset_iff)
+ then show "closedin (Euclidean_space (Suc n)) S'"
+ unfolding S'_def using that by (rule closedin_continuous_map_preimage)
+ next
+ fix x y
+ assume xy: "\<And>i. i \<noteq> n \<Longrightarrow> x i = y i" "x \<in> S'"
+ then have "(\<lambda>i. if i < n then x i else 0) = (\<lambda>i. if i < n then y i else 0)"
+ by (simp add: S'_def Euclidean_space_def fun_eq_iff)
+ with xy show "y \<in> S'"
+ by (simp add: S'_def Euclidean_space_def)
+ qed
+ moreover
+ have abs_eq: "(\<lambda>i. if i < n then x i else 0) = x" if "\<And>i. i \<ge> n \<Longrightarrow> x i = 0" for x :: "nat \<Rightarrow> real" and n
+ using that by auto
+ then have "topspace (Euclidean_space n) - S' = topspace (Euclidean_space n) - S"
+ by (simp add: S'_def Euclidean_space_def set_eq_iff cong: conj_cong)
+ moreover
+ have "topspace (Euclidean_space (Suc n)) - {x \<in> S'. x n = 0} = topspace (Euclidean_space (Suc n)) - S"
+ using Ssub_n
+ apply (auto simp: S'_def subset_iff Euclidean_space_def set_eq_iff abs_eq cong: conj_cong)
+ by (metis abs_eq le_antisym not_less_eq_eq)
+ ultimately show ?thesis
+ by simp
+ qed
+ ultimately have "relative_homology_group (p + m)(Euclidean_space (m + n))(topspace (Euclidean_space (m + n)) - S)
+ \<cong> relative_homology_group (p + m + 1) (Euclidean_space (Suc (m + n))) (topspace (Euclidean_space (Suc (m + n))) - S)"
+ by (metis \<open>closedin (Euclidean_space (m + n)) S\<close>)
+ then show ?case
+ using Suc.IH iso_trans by (force simp: algebra_simps)
+ qed (simp add: iso_refl)
+qed
+
+lemma iso_Euclidean_complements_lemma1:
+ assumes S: "closedin (Euclidean_space m) S" and cmf: "continuous_map(subtopology (Euclidean_space m) S) (Euclidean_space n) f"
+ obtains g where "continuous_map (Euclidean_space m) (Euclidean_space n) g"
+ "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
+proof -
+ have cont: "continuous_on (topspace (Euclidean_space m) \<inter> S) (\<lambda>x. f x i)" for i
+ by (metis (no_types) continuous_on_product_then_coordinatewise
+ cm_Euclidean_space_iff_continuous_on cmf topspace_subtopology)
+ have "f ` (topspace (Euclidean_space m) \<inter> S) \<subseteq> topspace (Euclidean_space n)"
+ using cmf continuous_map_image_subset_topspace by fastforce
+ then
+ have "\<exists>g. continuous_on (topspace (Euclidean_space m)) g \<and> (\<forall>x \<in> S. g x = f x i)" for i
+ using S Tietze_unbounded [OF cont [of i]]
+ by (metis closedin_Euclidean_space_iff closedin_closed_Int topspace_subtopology topspace_subtopology_subset)
+ then obtain g where cmg: "\<And>i. continuous_map (Euclidean_space m) euclideanreal (g i)"
+ and gf: "\<And>i x. x \<in> S \<Longrightarrow> g i x = f x i"
+ unfolding continuous_map_Euclidean_space_iff by metis
+ let ?GG = "\<lambda>x i. if i < n then g i x else 0"
+ show thesis
+ proof
+ show "continuous_map (Euclidean_space m) (Euclidean_space n) ?GG"
+ unfolding Euclidean_space_def [of n]
+ by (auto simp: continuous_map_in_subtopology continuous_map_componentwise cmg)
+ show "?GG x = f x" if "x \<in> S" for x
+ proof -
+ have "S \<subseteq> topspace (Euclidean_space m)"
+ by (meson S closedin_def)
+ then have "f x \<in> topspace (Euclidean_space n)"
+ using cmf that unfolding continuous_map_def topspace_subtopology by blast
+ then show ?thesis
+ by (force simp: topspace_Euclidean_space gf that)
+ qed
+ qed
+qed
+
+
+lemma iso_Euclidean_complements_lemma2:
+ assumes S: "closedin (Euclidean_space m) S"
+ and T: "closedin (Euclidean_space n) T"
+ and hom: "homeomorphic_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f"
+ obtains g where "homeomorphic_map (prod_topology (Euclidean_space m) (Euclidean_space n))
+ (prod_topology (Euclidean_space n) (Euclidean_space m)) g"
+ "\<And>x. x \<in> S \<Longrightarrow> g(x,(\<lambda>i. 0)) = (f x,(\<lambda>i. 0))"
+proof -
+ obtain g where cmf: "continuous_map (subtopology (Euclidean_space m) S) (subtopology (Euclidean_space n) T) f"
+ and cmg: "continuous_map (subtopology (Euclidean_space n) T) (subtopology (Euclidean_space m) S) g"
+ and gf: "\<And>x. x \<in> S \<Longrightarrow> g (f x) = x"
+ and fg: "\<And>y. y \<in> T \<Longrightarrow> f (g y) = y"
+ using hom S T closedin_subset unfolding homeomorphic_map_maps homeomorphic_maps_def
+ by fastforce
+ obtain f' where cmf': "continuous_map (Euclidean_space m) (Euclidean_space n) f'"
+ and f'f: "\<And>x. x \<in> S \<Longrightarrow> f' x = f x"
+ using iso_Euclidean_complements_lemma1 S cmf continuous_map_into_fulltopology by metis
+ obtain g' where cmg': "continuous_map (Euclidean_space n) (Euclidean_space m) g'"
+ and g'g: "\<And>x. x \<in> T \<Longrightarrow> g' x = g x"
+ using iso_Euclidean_complements_lemma1 T cmg continuous_map_into_fulltopology by metis
+ define p where "p \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i + f' x i))"
+ define p' where "p' \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i - f' x i))"
+ define q where "q \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i + g' x i))"
+ define q' where "q' \<equiv> \<lambda>(x,y). (x,(\<lambda>i. y i - g' x i))"
+ have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
+ (prod_topology (Euclidean_space m) (Euclidean_space n))
+ p p'"
+ "homeomorphic_maps (prod_topology (Euclidean_space n) (Euclidean_space m))
+ (prod_topology (Euclidean_space n) (Euclidean_space m))
+ q q'"
+ "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
+ (prod_topology (Euclidean_space n) (Euclidean_space m)) (\<lambda>(x,y). (y,x)) (\<lambda>(x,y). (y,x))"
+ apply (simp_all add: p_def p'_def q_def q'_def homeomorphic_maps_def continuous_map_pairwise)
+ apply (force simp: case_prod_unfold continuous_map_of_fst [unfolded o_def] cmf' cmg' intro: continuous_intros)+
+ done
+ then have "homeomorphic_maps (prod_topology (Euclidean_space m) (Euclidean_space n))
+ (prod_topology (Euclidean_space n) (Euclidean_space m))
+ (q' \<circ> (\<lambda>(x,y). (y,x)) \<circ> p) (p' \<circ> ((\<lambda>(x,y). (y,x)) \<circ> q))"
+ using homeomorphic_maps_compose homeomorphic_maps_sym by (metis (no_types, lifting))
+ moreover
+ have "\<And>x. x \<in> S \<Longrightarrow> (q' \<circ> (\<lambda>(x,y). (y,x)) \<circ> p) (x, \<lambda>i. 0) = (f x, \<lambda>i. 0)"
+ apply (simp add: q'_def p_def f'f)
+ apply (simp add: fun_eq_iff)
+ by (metis S T closedin_subset g'g gf hom homeomorphic_imp_surjective_map image_eqI topspace_subtopology_subset)
+ ultimately
+ show thesis
+ using homeomorphic_map_maps that by blast
+qed
+
+
+proposition isomorphic_relative_homology_groups_Euclidean_complements:
+ assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T"
+ and hom: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
+ shows "relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - S)
+ \<cong> relative_homology_group p (Euclidean_space n) (topspace(Euclidean_space n) - T)"
+proof -
+ have subST: "S \<subseteq> topspace(Euclidean_space n)" "T \<subseteq> topspace(Euclidean_space n)"
+ by (meson S T closedin_def)+
+ have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S)
+ \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)"
+ using relative_homology_group_Euclidean_complement_step [OF S] by blast
+ moreover have "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)
+ \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
+ using relative_homology_group_Euclidean_complement_step [OF T] by blast
+ moreover have "relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - S)
+ \<cong> relative_homology_group (p + int n) (Euclidean_space (n + n)) (topspace (Euclidean_space (n + n)) - T)"
+ proof -
+ obtain f where f: "homeomorphic_map (subtopology (Euclidean_space n) S)
+ (subtopology (Euclidean_space n) T) f"
+ using hom unfolding homeomorphic_space by blast
+ obtain g where g: "homeomorphic_map (prod_topology (Euclidean_space n) (Euclidean_space n))
+ (prod_topology (Euclidean_space n) (Euclidean_space n)) g"
+ and gf: "\<And>x. x \<in> S \<Longrightarrow> g(x,(\<lambda>i. 0)) = (f x,(\<lambda>i. 0))"
+ using S T f iso_Euclidean_complements_lemma2 by blast
+ define h where "h \<equiv> \<lambda>x::nat \<Rightarrow>real. ((\<lambda>i. if i < n then x i else 0), (\<lambda>j. if j < n then x(n + j) else 0))"
+ define k where "k \<equiv> \<lambda>(x,y) i. if i < 2 * n then if i < n then x i else y(i - n) else (0::real)"
+ have hk: "homeomorphic_maps (Euclidean_space(2 * n)) (prod_topology (Euclidean_space n) (Euclidean_space n)) h k"
+ unfolding homeomorphic_maps_def
+ proof safe
+ show "continuous_map (Euclidean_space (2 * n))
+ (prod_topology (Euclidean_space n) (Euclidean_space n)) h"
+ apply (simp add: h_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space)
+ unfolding Euclidean_space_def
+ by (metis (mono_tags) UNIV_I continuous_map_from_subtopology continuous_map_product_projection)
+ have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (\<lambda>p. fst p i)" for i
+ using Euclidean_space_def continuous_map_into_fulltopology continuous_map_fst by fastforce
+ moreover
+ have "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n)) euclideanreal (\<lambda>p. snd p (i - n))" for i
+ using Euclidean_space_def continuous_map_into_fulltopology continuous_map_snd by fastforce
+ ultimately
+ show "continuous_map (prod_topology (Euclidean_space n) (Euclidean_space n))
+ (Euclidean_space (2 * n)) k"
+ by (simp add: k_def continuous_map_pairwise o_def continuous_map_componentwise_Euclidean_space case_prod_unfold)
+ qed (auto simp: k_def h_def fun_eq_iff topspace_Euclidean_space)
+ define kgh where "kgh \<equiv> k \<circ> g \<circ> h"
+ let ?i = "hom_induced (p + n) (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - S)
+ (Euclidean_space(2 * n)) (topspace(Euclidean_space(2 * n)) - T) kgh"
+ have "?i \<in> iso (relative_homology_group (p + int n) (Euclidean_space (2 * n))
+ (topspace (Euclidean_space (2 * n)) - S))
+ (relative_homology_group (p + int n) (Euclidean_space (2 * n))
+ (topspace (Euclidean_space (2 * n)) - T))"
+ proof (rule homeomorphic_map_relative_homology_iso)
+ show hm: "homeomorphic_map (Euclidean_space (2 * n)) (Euclidean_space (2 * n)) kgh"
+ unfolding kgh_def by (meson hk g homeomorphic_map_maps homeomorphic_maps_compose homeomorphic_maps_sym)
+ have Teq: "T = f ` S"
+ using f homeomorphic_imp_surjective_map subST(1) subST(2) topspace_subtopology_subset by blast
+ have khf: "\<And>x. x \<in> S \<Longrightarrow> k(h(f x)) = f x"
+ by (metis (no_types, lifting) Teq hk homeomorphic_maps_def image_subset_iff le_add1 mult_2 subST(2) subsetD subset_Euclidean_space)
+ have gh: "g(h x) = h(f x)" if "x \<in> S" for x
+ proof -
+ have [simp]: "(\<lambda>i. if i < n then x i else 0) = x"
+ using subST(1) that topspace_Euclidean_space by (auto simp: fun_eq_iff)
+ have "f x \<in> topspace(Euclidean_space n)"
+ using Teq subST(2) that by blast
+ moreover have "(\<lambda>j. if j < n then x (n + j) else 0) = (\<lambda>j. 0::real)"
+ using Euclidean_space_def subST(1) that by force
+ ultimately show ?thesis
+ by (simp add: topspace_Euclidean_space h_def gf \<open>x \<in> S\<close> fun_eq_iff)
+ qed
+ have *: "\<lbrakk>S \<subseteq> U; T \<subseteq> U; kgh ` U = U; inj_on kgh U; kgh ` S = T\<rbrakk> \<Longrightarrow> kgh ` (U - S) = U - T" for U
+ unfolding inj_on_def set_eq_iff by blast
+ show "kgh ` (topspace (Euclidean_space (2 * n)) - S) = topspace (Euclidean_space (2 * n)) - T"
+ proof (rule *)
+ show "kgh ` topspace (Euclidean_space (2 * n)) = topspace (Euclidean_space (2 * n))"
+ by (simp add: hm homeomorphic_imp_surjective_map)
+ show "inj_on kgh (topspace (Euclidean_space (2 * n)))"
+ using hm homeomorphic_map_def by auto
+ show "kgh ` S = T"
+ by (simp add: Teq kgh_def gh khf)
+ qed (use subST topspace_Euclidean_space in \<open>fastforce+\<close>)
+ qed auto
+ then show ?thesis
+ by (simp add: is_isoI mult_2)
+ qed
+ ultimately show ?thesis
+ by (meson group.iso_sym iso_trans group_relative_homology_group)
+qed
+
+lemma lemma_iod:
+ assumes "S \<subseteq> T" "S \<noteq> {}" and Tsub: "T \<subseteq> topspace(Euclidean_space n)"
+ and S: "\<And>a b u. \<lbrakk>a \<in> S; b \<in> T; 0 < u; u < 1\<rbrakk> \<Longrightarrow> (\<lambda>i. (1 - u) * a i + u * b i) \<in> S"
+ shows "path_connectedin (Euclidean_space n) T"
+proof -
+ obtain a where "a \<in> S"
+ using assms by blast
+ have "path_component_of (subtopology (Euclidean_space n) T) a b" if "b \<in> T" for b
+ unfolding path_component_of_def
+ proof (intro exI conjI)
+ have [simp]: "\<forall>i\<ge>n. a i = 0"
+ using Tsub \<open>a \<in> S\<close> assms(1) topspace_Euclidean_space by auto
+ have [simp]: "\<forall>i\<ge>n. b i = 0"
+ using Tsub that topspace_Euclidean_space by auto
+ have inT: "(\<lambda>i. (1 - x) * a i + x * b i) \<in> T" if "0 \<le> x" "x \<le> 1" for x
+ proof (cases "x = 0 \<or> x = 1")
+ case True
+ with \<open>a \<in> S\<close> \<open>b \<in> T\<close> \<open>S \<subseteq> T\<close> show ?thesis
+ by force
+ next
+ case False
+ then show ?thesis
+ using subsetD [OF \<open>S \<subseteq> T\<close> S] \<open>a \<in> S\<close> \<open>b \<in> T\<close> that by auto
+ qed
+ have "continuous_on {0..1} (\<lambda>x. (1 - x) * a k + x * b k)" for k
+ by (intro continuous_intros)
+ then show "pathin (subtopology (Euclidean_space n) T) (\<lambda>t i. (1 - t) * a i + t * b i)"
+ apply (simp add: Euclidean_space_def subtopology_subtopology pathin_subtopology)
+ apply (simp add: pathin_def continuous_map_componentwise_UNIV inT)
+ done
+ qed auto
+ then have "path_connected_space (subtopology (Euclidean_space n) T)"
+ by (metis Tsub path_component_of_equiv path_connected_space_iff_path_component topspace_subtopology_subset)
+ then show ?thesis
+ by (simp add: Tsub path_connectedin_def)
+qed
+
+
+lemma invariance_of_dimension_closedin_Euclidean_space:
+ assumes "closedin (Euclidean_space n) S"
+ shows "subtopology (Euclidean_space n) S homeomorphic_space Euclidean_space n
+ \<longleftrightarrow> S = topspace(Euclidean_space n)"
+ (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ have Ssub: "S \<subseteq> topspace (Euclidean_space n)"
+ by (meson assms closedin_def)
+ moreover have False if "a \<notin> S" and "a \<in> topspace (Euclidean_space n)" for a
+ proof -
+ have cl_n: "closedin (Euclidean_space (Suc n)) (topspace(Euclidean_space n))"
+ using Euclidean_space_def closedin_Euclidean_space closedin_subtopology by fastforce
+ then have sub: "subtopology (Euclidean_space(Suc n)) (topspace(Euclidean_space n)) = Euclidean_space n"
+ by (metis (no_types, lifting) Euclidean_space_def closedin_subset subtopology_subtopology topspace_Euclidean_space topspace_subtopology topspace_subtopology_subset)
+ then have cl_S: "closedin (Euclidean_space(Suc n)) S"
+ using cl_n assms closedin_closed_subtopology by fastforce
+ have sub_SucS: "subtopology (Euclidean_space (Suc n)) S = subtopology (Euclidean_space n) S"
+ by (metis Ssub sub subtopology_subtopology topspace_subtopology topspace_subtopology_subset)
+ have non0: "{y. \<exists>x::nat\<Rightarrow>real. (\<forall>i\<ge>Suc n. x i = 0) \<and> (\<exists>i\<ge>n. x i \<noteq> 0) \<and> y = x n} = -{0}"
+ proof safe
+ show "False" if "\<forall>i\<ge>Suc n. f i = 0" "0 = f n" "n \<le> i" "f i \<noteq> 0" for f::"nat\<Rightarrow>real" and i
+ by (metis that le_antisym not_less_eq_eq)
+ show "\<exists>f::nat\<Rightarrow>real. (\<forall>i\<ge>Suc n. f i = 0) \<and> (\<exists>i\<ge>n. f i \<noteq> 0) \<and> a = f n" if "a \<noteq> 0" for a
+ by (rule_tac x="(\<lambda>i. 0)(n:= a)" in exI) (force simp: that)
+ qed
+ have "homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S))
+ \<cong> homology_group 0 (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))"
+ proof (rule isomorphic_relative_contractible_space_imp_homology_groups)
+ show "(topspace (Euclidean_space (Suc n)) - S = {}) =
+ (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n) = {})"
+ using cl_n closedin_subset that by auto
+ next
+ fix p
+ show "relative_homology_group p (Euclidean_space (Suc n))
+ (topspace (Euclidean_space (Suc n)) - S) \<cong>
+ relative_homology_group p (Euclidean_space (Suc n))
+ (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n))"
+ by (simp add: L sub_SucS cl_S cl_n isomorphic_relative_homology_groups_Euclidean_complements sub)
+ qed (auto simp: L)
+ moreover
+ have "continuous_map (powertop_real UNIV) euclideanreal (\<lambda>x. x n)"
+ by (metis (no_types) UNIV_I continuous_map_product_projection)
+ then have cm: "continuous_map (subtopology (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))
+ euclideanreal (\<lambda>x. x n)"
+ by (simp add: Euclidean_space_def continuous_map_from_subtopology)
+ have False if "path_connected_space
+ (subtopology (Euclidean_space (Suc n))
+ (topspace (Euclidean_space (Suc n)) - topspace (Euclidean_space n)))"
+ using path_connectedin_continuous_map_image [OF cm that [unfolded path_connectedin_topspace [symmetric]]]
+ bounded_path_connected_Compl_real [of "{0}"]
+ by (simp add: topspace_Euclidean_space image_def Bex_def non0 flip: path_connectedin_topspace)
+ moreover
+ have eq: "T = T \<inter> {x. x n \<le> 0} \<union> T \<inter> {x. x n \<ge> 0}" for T :: "(nat \<Rightarrow> real) set"
+ by auto
+ have "path_connectedin (Euclidean_space (Suc n)) (topspace (Euclidean_space (Suc n)) - S)"
+ proof (subst eq, rule path_connectedin_Un)
+ have "topspace(Euclidean_space(Suc n)) \<inter> {x. x n = 0} = topspace(Euclidean_space n)"
+ apply (auto simp: topspace_Euclidean_space)
+ by (metis Suc_leI inf.absorb_iff2 inf.orderE leI)
+ let ?S = "topspace(Euclidean_space(Suc n)) \<inter> {x. x n < 0}"
+ show "path_connectedin (Euclidean_space (Suc n))
+ ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0})"
+ proof (rule lemma_iod)
+ show "?S \<subseteq> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0}"
+ using Ssub topspace_Euclidean_space by auto
+ show "?S \<noteq> {}"
+ apply (simp add: topspace_Euclidean_space set_eq_iff)
+ apply (rule_tac x="(\<lambda>i. 0)(n:= -1)" in exI)
+ apply auto
+ done
+ fix a b and u::real
+ assume
+ "a \<in> ?S" "0 < u" "u < 1"
+ "b \<in> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0}"
+ then show "(\<lambda>i. (1 - u) * a i + u * b i) \<in> ?S"
+ by (simp add: topspace_Euclidean_space add_neg_nonpos less_eq_real_def mult_less_0_iff)
+ qed (simp add: topspace_Euclidean_space subset_iff)
+ let ?T = "topspace(Euclidean_space(Suc n)) \<inter> {x. x n > 0}"
+ show "path_connectedin (Euclidean_space (Suc n))
+ ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n})"
+ proof (rule lemma_iod)
+ show "?T \<subseteq> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}"
+ using Ssub topspace_Euclidean_space by auto
+ show "?T \<noteq> {}"
+ apply (simp add: topspace_Euclidean_space set_eq_iff)
+ apply (rule_tac x="(\<lambda>i. 0)(n:= 1)" in exI)
+ apply auto
+ done
+ fix a b and u::real
+ assume "a \<in> ?T" "0 < u" "u < 1" "b \<in> (topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}"
+ then show "(\<lambda>i. (1 - u) * a i + u * b i) \<in> ?T"
+ by (simp add: topspace_Euclidean_space add_pos_nonneg)
+ qed (simp add: topspace_Euclidean_space subset_iff)
+ show "(topspace (Euclidean_space (Suc n)) - S) \<inter> {x. x n \<le> 0} \<inter>
+ ((topspace (Euclidean_space (Suc n)) - S) \<inter> {x. 0 \<le> x n}) \<noteq> {}"
+ using that
+ apply (auto simp: Set.set_eq_iff topspace_Euclidean_space)
+ by (metis Suc_leD order_refl)
+ qed
+ then have "path_connected_space (subtopology (Euclidean_space (Suc n))
+ (topspace (Euclidean_space (Suc n)) - S))"
+ apply (simp add: path_connectedin_subtopology flip: path_connectedin_topspace)
+ by (metis Int_Diff inf_idem)
+ ultimately
+ show ?thesis
+ using isomorphic_homology_imp_path_connectedness by blast
+ qed
+ ultimately show ?rhs
+ by blast
+qed (simp add: homeomorphic_space_refl)
+
+
+
+lemma isomorphic_homology_groups_Euclidean_complements:
+ assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
+ "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
+ shows "homology_group p (subtopology (Euclidean_space n) (topspace(Euclidean_space n) - S))
+ \<cong> homology_group p (subtopology (Euclidean_space n) (topspace(Euclidean_space n) - T))"
+proof (rule isomorphic_relative_contractible_space_imp_homology_groups)
+ show "topspace (Euclidean_space n) - S \<subseteq> topspace (Euclidean_space n)"
+ using assms homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subtopology_superset by fastforce
+ show "topspace (Euclidean_space n) - T \<subseteq> topspace (Euclidean_space n)"
+ using assms invariance_of_dimension_closedin_Euclidean_space subtopology_superset by force
+ show "(topspace (Euclidean_space n) - S = {}) = (topspace (Euclidean_space n) - T = {})"
+ by (metis Diff_eq_empty_iff assms closedin_subset homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subset_antisym subtopology_topspace)
+ show "relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - S) \<cong>
+ relative_homology_group p (Euclidean_space n) (topspace (Euclidean_space n) - T)" for p
+ using assms isomorphic_relative_homology_groups_Euclidean_complements by blast
+qed auto
+
+lemma eqpoll_path_components_Euclidean_complements:
+ assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
+ "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
+ shows "path_components_of
+ (subtopology (Euclidean_space n)
+ (topspace(Euclidean_space n) - S))
+ \<approx> path_components_of
+ (subtopology (Euclidean_space n)
+ (topspace(Euclidean_space n) - T))"
+ by (simp add: assms isomorphic_homology_groups_Euclidean_complements isomorphic_homology_imp_path_components)
+
+lemma path_connectedin_Euclidean_complements:
+ assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
+ "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
+ shows "path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)
+ \<longleftrightarrow> path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - T)"
+ by (meson Diff_subset assms isomorphic_homology_groups_Euclidean_complements isomorphic_homology_imp_path_connectedness path_connectedin_def)
+
+lemma eqpoll_connected_components_Euclidean_complements:
+ assumes S: "closedin (Euclidean_space n) S" and T: "closedin (Euclidean_space n) T"
+ and ST: "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
+ shows "connected_components_of
+ (subtopology (Euclidean_space n)
+ (topspace(Euclidean_space n) - S))
+ \<approx> connected_components_of
+ (subtopology (Euclidean_space n)
+ (topspace(Euclidean_space n) - T))"
+ using eqpoll_path_components_Euclidean_complements [OF assms]
+ by (metis S T closedin_def locally_path_connected_Euclidean_space locally_path_connected_space_open_subset path_components_eq_connected_components_of)
+
+lemma connected_in_Euclidean_complements:
+ assumes "closedin (Euclidean_space n) S" "closedin (Euclidean_space n) T"
+ "(subtopology (Euclidean_space n) S) homeomorphic_space (subtopology (Euclidean_space n) T)"
+ shows "connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)
+ \<longleftrightarrow> connectedin (Euclidean_space n) (topspace(Euclidean_space n) - T)"
+ apply (simp add: connectedin_def connected_space_iff_components_subset_singleton subset_singleton_iff_lepoll)
+ using eqpoll_connected_components_Euclidean_complements [OF assms]
+ by (meson eqpoll_sym lepoll_trans1)
+
+
+theorem invariance_of_dimension_Euclidean_space:
+ "Euclidean_space m homeomorphic_space Euclidean_space n \<longleftrightarrow> m = n"
+proof (cases m n rule: linorder_cases)
+ case less
+ then have *: "topspace (Euclidean_space m) \<subseteq> topspace (Euclidean_space n)"
+ by (meson le_cases not_le subset_Euclidean_space)
+ then have "Euclidean_space m = subtopology (Euclidean_space n) (topspace(Euclidean_space m))"
+ by (simp add: Euclidean_space_def inf.absorb_iff2 subtopology_subtopology)
+ then show ?thesis
+ by (metis (no_types, lifting) * Euclidean_space_def closedin_Euclidean_space closedin_closed_subtopology eq_iff invariance_of_dimension_closedin_Euclidean_space subset_Euclidean_space topspace_Euclidean_space)
+next
+ case equal
+ then show ?thesis
+ by (simp add: homeomorphic_space_refl)
+next
+ case greater
+ then have *: "topspace (Euclidean_space n) \<subseteq> topspace (Euclidean_space m)"
+ by (meson le_cases not_le subset_Euclidean_space)
+ then have "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))"
+ by (simp add: Euclidean_space_def inf.absorb_iff2 subtopology_subtopology)
+ then show ?thesis
+ by (metis (no_types, lifting) "*" Euclidean_space_def closedin_Euclidean_space closedin_closed_subtopology eq_iff homeomorphic_space_sym invariance_of_dimension_closedin_Euclidean_space subset_Euclidean_space topspace_Euclidean_space)
+qed
+
+
+
+lemma biglemma:
+ assumes "n \<noteq> 0" and S: "compactin (Euclidean_space n) S"
+ and cmh: "continuous_map (subtopology (Euclidean_space n) S) (Euclidean_space n) h"
+ and "inj_on h S"
+ shows "path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - h ` S)
+ \<longleftrightarrow> path_connectedin (Euclidean_space n) (topspace(Euclidean_space n) - S)"
+proof (rule path_connectedin_Euclidean_complements)
+ have hS_sub: "h ` S \<subseteq> topspace(Euclidean_space n)"
+ by (metis (no_types) S cmh compactin_subspace continuous_map_image_subset_topspace topspace_subtopology_subset)
+ show clo_S: "closedin (Euclidean_space n) S"
+ using assms by (simp add: continuous_map_in_subtopology Hausdorff_Euclidean_space compactin_imp_closedin)
+ show clo_hS: "closedin (Euclidean_space n) (h ` S)"
+ using Hausdorff_Euclidean_space S cmh compactin_absolute compactin_imp_closedin image_compactin by blast
+ have "homeomorphic_map (subtopology (Euclidean_space n) S) (subtopology (Euclidean_space n) (h ` S)) h"
+ proof (rule continuous_imp_homeomorphic_map)
+ show "compact_space (subtopology (Euclidean_space n) S)"
+ by (simp add: S compact_space_subtopology)
+ show "Hausdorff_space (subtopology (Euclidean_space n) (h ` S))"
+ using hS_sub
+ by (simp add: Hausdorff_Euclidean_space Hausdorff_space_subtopology)
+ show "continuous_map (subtopology (Euclidean_space n) S) (subtopology (Euclidean_space n) (h ` S)) h"
+ using cmh continuous_map_in_subtopology by fastforce
+ show "h ` topspace (subtopology (Euclidean_space n) S) = topspace (subtopology (Euclidean_space n) (h ` S))"
+ using clo_hS clo_S closedin_subset by auto
+ show "inj_on h (topspace (subtopology (Euclidean_space n) S))"
+ by (metis \<open>inj_on h S\<close> clo_S closedin_def topspace_subtopology_subset)
+ qed
+ then show "subtopology (Euclidean_space n) (h ` S) homeomorphic_space subtopology (Euclidean_space n) S"
+ using homeomorphic_space homeomorphic_space_sym by blast
+qed
+
+
+lemma lemmaIOD:
+ assumes
+ "\<exists>T. T \<in> U \<and> c \<subseteq> T" "\<exists>T. T \<in> U \<and> d \<subseteq> T" "\<Union>U = c \<union> d" "\<And>T. T \<in> U \<Longrightarrow> T \<noteq> {}"
+ "pairwise disjnt U" "~(\<exists>T. U \<subseteq> {T})"
+ shows "c \<in> U"
+ using assms
+ apply safe
+ subgoal for C' D'
+ proof (cases "C'=D'")
+ show "c \<in> U"
+ if UU: "\<Union> U = c \<union> d"
+ and U: "\<And>T. T \<in> U \<Longrightarrow> T \<noteq> {}" "disjoint U" and "\<nexists>T. U \<subseteq> {T}" "c \<subseteq> C'" "D' \<in> U" "d \<subseteq> D'" "C' = D'"
+ proof -
+ have "c \<union> d = D'"
+ using Union_upper sup_mono UU that(5) that(6) that(7) that(8) by auto
+ then have "\<Union>U = D'"
+ by (simp add: UU)
+ with U have "U = {D'}"
+ by (metis (no_types, lifting) disjnt_Union1 disjnt_self_iff_empty insertCI pairwiseD subset_iff that(4) that(6))
+ then show ?thesis
+ using that(4) by auto
+ qed
+ show "c \<in> U"
+ if "\<Union> U = c \<union> d""disjoint U" "C' \<in> U" "c \<subseteq> C'""D' \<in> U" "d \<subseteq> D'" "C' \<noteq> D'"
+ proof -
+ have "C' \<inter> D' = {}"
+ using \<open>disjoint U\<close> \<open>C' \<in> U\<close> \<open>D' \<in> U\<close> \<open>C' \<noteq> D'\<close>unfolding disjnt_iff pairwise_def
+ by blast
+ then show ?thesis
+ using subset_antisym that(1) \<open>C' \<in> U\<close> \<open>c \<subseteq> C'\<close> \<open>d \<subseteq> D'\<close> by fastforce
+ qed
+ qed
+ done
+
+
+
+
+theorem invariance_of_domain_Euclidean_space:
+ assumes U: "openin (Euclidean_space n) U"
+ and cmf: "continuous_map (subtopology (Euclidean_space n) U) (Euclidean_space n) f"
+ and "inj_on f U"
+ shows "openin (Euclidean_space n) (f ` U)" (is "openin ?E (f ` U)")
+proof (cases "n = 0")
+ case True
+ have [simp]: "Euclidean_space 0 = discrete_topology {\<lambda>i. 0}"
+ by (auto simp: subtopology_eq_discrete_topology_sing topspace_Euclidean_space)
+ show ?thesis
+ using cmf True U by auto
+next
+ case False
+ define enorm where "enorm \<equiv> \<lambda>x. sqrt(\<Sum>i<n. x i ^ 2)"
+ have enorm_if [simp]: "enorm (\<lambda>i. if i = k then d else 0) = (if k < n then \<bar>d\<bar> else 0)" for k d
+ using \<open>n \<noteq> 0\<close> by (auto simp: enorm_def power2_eq_square if_distrib [of "\<lambda>x. x * _"] cong: if_cong)
+ define zero::"nat\<Rightarrow>real" where "zero \<equiv> \<lambda>i. 0"
+ have zero_in [simp]: "zero \<in> topspace ?E"
+ using False by (simp add: zero_def topspace_Euclidean_space)
+ have enorm_eq_0 [simp]: "enorm x = 0 \<longleftrightarrow> x = zero"
+ if "x \<in> topspace(Euclidean_space n)" for x
+ using that unfolding zero_def enorm_def
+ apply (simp add: sum_nonneg_eq_0_iff fun_eq_iff topspace_Euclidean_space)
+ using le_less_linear by blast
+ have [simp]: "enorm zero = 0"
+ by (simp add: zero_def enorm_def)
+ have cm_enorm: "continuous_map ?E euclideanreal enorm"
+ unfolding enorm_def
+ proof (intro continuous_intros)
+ show "continuous_map ?E euclideanreal (\<lambda>x. x i)"
+ if "i \<in> {..<n}" for i
+ using that by (auto simp: Euclidean_space_def intro: continuous_map_product_projection continuous_map_from_subtopology)
+ qed auto
+ have enorm_ge0: "0 \<le> enorm x" for x
+ by (auto simp: enorm_def sum_nonneg)
+ have le_enorm: "\<bar>x i\<bar> \<le> enorm x" if "i < n" for i x
+ proof -
+ have "\<bar>x i\<bar> \<le> sqrt (\<Sum>k\<in>{i}. (x k)\<^sup>2)"
+ by auto
+ also have "\<dots> \<le> sqrt (\<Sum>k<n. (x k)\<^sup>2)"
+ by (rule real_sqrt_le_mono [OF sum_mono2]) (use that in auto)
+ finally show ?thesis
+ by (simp add: enorm_def)
+ qed
+ define B where "B \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x < r}"
+ define C where "C \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x \<le> r}"
+ define S where "S \<equiv> \<lambda>r. {x \<in> topspace ?E. enorm x = r}"
+ have BC: "B r \<subseteq> C r" and SC: "S r \<subseteq> C r" and disjSB: "disjnt (S r) (B r)" and eqC: "B r \<union> S r = C r" for r
+ by (auto simp: B_def C_def S_def disjnt_def)
+ consider "n = 1" | "n \<ge> 2"
+ using False by linarith
+ then have **: "openin ?E (h ` (B r))"
+ if "r > 0" and cmh: "continuous_map(subtopology ?E (C r)) ?E h" and injh: "inj_on h (C r)" for r h
+ proof cases
+ case 1
+ define e :: "[real,nat]\<Rightarrow>real" where "e \<equiv> \<lambda>x i. if i = 0 then x else 0"
+ define e' :: "(nat\<Rightarrow>real)\<Rightarrow>real" where "e' \<equiv> \<lambda>x. x 0"
+ have "continuous_map euclidean euclideanreal (\<lambda>f. f (0::nat))"
+ by auto
+ then have "continuous_map (subtopology (powertop_real UNIV) {f. \<forall>n\<ge>Suc 0. f n = 0}) euclideanreal (\<lambda>f. f 0)"
+ by (metis (mono_tags) continuous_map_from_subtopology euclidean_product_topology)
+ then have hom_ee': "homeomorphic_maps euclideanreal (Euclidean_space 1) e e'"
+ by (auto simp: homeomorphic_maps_def e_def e'_def continuous_map_in_subtopology Euclidean_space_def)
+ have eBr: "e ` {-r<..<r} = B r"
+ unfolding B_def e_def C_def
+ by(force simp: "1" topspace_Euclidean_space enorm_def power2_eq_square if_distrib [of "\<lambda>x. x * _"] cong: if_cong)
+ have in_Cr: "\<And>x. \<lbrakk>-r < x; x < r\<rbrakk> \<Longrightarrow> (\<lambda>i. if i = 0 then x else 0) \<in> C r"
+ using \<open>n \<noteq> 0\<close> by (auto simp: C_def topspace_Euclidean_space)
+ have inj: "inj_on (e' \<circ> h \<circ> e) {- r<..<r}"
+ proof (clarsimp simp: inj_on_def e_def e'_def)
+ show "(x::real) = y"
+ if f: "h (\<lambda>i. if i = 0 then x else 0) 0 = h (\<lambda>i. if i = 0 then y else 0) 0"
+ and "-r < x" "x < r" "-r < y" "y < r"
+ for x y :: real
+ proof -
+ have x: "(\<lambda>i. if i = 0 then x else 0) \<in> C r" and y: "(\<lambda>i. if i = 0 then y else 0) \<in> C r"
+ by (blast intro: inj_onD [OF \<open>inj_on h (C r)\<close>] that in_Cr)+
+ have "continuous_map (subtopology (Euclidean_space (Suc 0)) (C r)) (Euclidean_space (Suc 0)) h"
+ using cmh by (simp add: 1)
+ then have "h ` ({x. \<forall>i\<ge>Suc 0. x i = 0} \<inter> C r) \<subseteq> {x. \<forall>i\<ge>Suc 0. x i = 0}"
+ by (force simp: Euclidean_space_def subtopology_subtopology continuous_map_def)
+ have "h (\<lambda>i. if i = 0 then x else 0) j = h (\<lambda>i. if i = 0 then y else 0) j" for j
+ proof (cases j)
+ case (Suc j')
+ have "h ` ({x. \<forall>i\<ge>Suc 0. x i = 0} \<inter> C r) \<subseteq> {x. \<forall>i\<ge>Suc 0. x i = 0}"
+ using continuous_map_image_subset_topspace [OF cmh]
+ by (simp add: 1 Euclidean_space_def subtopology_subtopology)
+ with Suc f x y show ?thesis
+ by (simp add: "1" image_subset_iff)
+ qed (use f in blast)
+ then have "(\<lambda>i. if i = 0 then x else 0) = (\<lambda>i::nat. if i = 0 then y else 0)"
+ by (blast intro: inj_onD [OF \<open>inj_on h (C r)\<close>] that in_Cr)
+ then show ?thesis
+ by (simp add: fun_eq_iff) presburger
+ qed
+ qed
+ have hom_e': "homeomorphic_map (Euclidean_space 1) euclideanreal e'"
+ using hom_ee' homeomorphic_maps_map by blast
+ have "openin (Euclidean_space n) (h ` e ` {- r<..<r})"
+ unfolding 1
+ proof (subst homeomorphic_map_openness [OF hom_e', symmetric])
+ show "h ` e ` {- r<..<r} \<subseteq> topspace (Euclidean_space 1)"
+ using "1" C_def \<open>\<And>r. B r \<subseteq> C r\<close> cmh continuous_map_image_subset_topspace eBr by fastforce
+ have cont: "continuous_on {- r<..<r} (e' \<circ> h \<circ> e)"
+ proof (intro continuous_on_compose)
+ have "\<And>i. continuous_on {- r<..<r} (\<lambda>x. if i = 0 then x else 0)"
+ by (auto simp: continuous_on_topological)
+ then show "continuous_on {- r<..<r} e"
+ by (force simp: e_def intro: continuous_on_coordinatewise_then_product)
+ have subCr: "e ` {- r<..<r} \<subseteq> topspace (subtopology ?E (C r))"
+ by (auto simp: eBr \<open>\<And>r. B r \<subseteq> C r\<close>) (auto simp: B_def)
+ with cmh show "continuous_on (e ` {- r<..<r}) h"
+ by (meson cm_Euclidean_space_iff_continuous_on continuous_on_subset)
+ have "h ` (e ` {- r<..<r}) \<subseteq> topspace ?E"
+ using subCr cmh by (simp add: continuous_map_def image_subset_iff)
+ moreover have "continuous_on (topspace ?E) e'"
+ by (metis "1" continuous_map_Euclidean_space_iff hom_ee' homeomorphic_maps_def)
+ ultimately show "continuous_on (h ` e ` {- r<..<r}) e'"
+ by (simp add: e'_def continuous_on_subset)
+ qed
+ show "openin euclideanreal (e' ` h ` e ` {- r<..<r})"
+ using injective_eq_1d_open_map_UNIV [OF cont] inj by (simp add: image_image is_interval_1)
+ qed
+ then show ?thesis
+ by (simp flip: eBr)
+ next
+ case 2
+ have cloC: "\<And>r. closedin (Euclidean_space n) (C r)"
+ unfolding C_def
+ by (rule closedin_continuous_map_preimage [OF cm_enorm, of concl: "{.._}", simplified])
+ have cloS: "\<And>r. closedin (Euclidean_space n) (S r)"
+ unfolding S_def
+ by (rule closedin_continuous_map_preimage [OF cm_enorm, of concl: "{_}", simplified])
+ have C_subset: "C r \<subseteq> UNIV \<rightarrow>\<^sub>E {- \<bar>r\<bar>..\<bar>r\<bar>}"
+ using le_enorm \<open>r > 0\<close>
+ apply (auto simp: C_def topspace_Euclidean_space abs_le_iff)
+ apply (metis add.inverse_neutral le_cases less_minus_iff not_le order_trans)
+ by (metis enorm_ge0 not_le order.trans)
+ have compactinC: "compactin (Euclidean_space n) (C r)"
+ unfolding Euclidean_space_def compactin_subtopology
+ proof
+ show "compactin (powertop_real UNIV) (C r)"
+ proof (rule closed_compactin [OF _ C_subset])
+ show "closedin (powertop_real UNIV) (C r)"
+ by (metis Euclidean_space_def cloC closedin_Euclidean_space closedin_closed_subtopology topspace_Euclidean_space)
+ qed (simp add: compactin_PiE)
+ qed (auto simp: C_def topspace_Euclidean_space)
+ have compactinS: "compactin (Euclidean_space n) (S r)"
+ unfolding Euclidean_space_def compactin_subtopology
+ proof
+ show "compactin (powertop_real UNIV) (S r)"
+ proof (rule closed_compactin)
+ show "S r \<subseteq> UNIV \<rightarrow>\<^sub>E {- \<bar>r\<bar>..\<bar>r\<bar>}"
+ using C_subset \<open>\<And>r. S r \<subseteq> C r\<close> by blast
+ show "closedin (powertop_real UNIV) (S r)"
+ by (metis Euclidean_space_def cloS closedin_Euclidean_space closedin_closed_subtopology topspace_Euclidean_space)
+ qed (simp add: compactin_PiE)
+ qed (auto simp: S_def topspace_Euclidean_space)
+ have h_if_B: "\<And>y. y \<in> B r \<Longrightarrow> h y \<in> topspace ?E"
+ using B_def \<open>\<And>r. B r \<union> S r = C r\<close> cmh continuous_map_image_subset_topspace by fastforce
+ have com_hSr: "compactin (Euclidean_space n) (h ` S r)"
+ by (meson \<open>\<And>r. S r \<subseteq> C r\<close> cmh compactinS compactin_subtopology image_compactin)
+ have ope_comp_hSr: "openin (Euclidean_space n) (topspace (Euclidean_space n) - h ` S r)"
+ proof (rule openin_diff)
+ show "closedin (Euclidean_space n) (h ` S r)"
+ using Hausdorff_Euclidean_space com_hSr compactin_imp_closedin by blast
+ qed auto
+ have h_pcs: "h ` (B r) \<in> path_components_of (subtopology ?E (topspace ?E - h ` (S r)))"
+ proof (rule lemmaIOD)
+ have pc_interval: "path_connectedin (Euclidean_space n) {x \<in> topspace(Euclidean_space n). enorm x \<in> T}"
+ if T: "is_interval T" for T
+ proof -
+ define mul :: "[real, nat \<Rightarrow> real, nat] \<Rightarrow> real" where "mul \<equiv> \<lambda>a x i. a * x i"
+ let ?neg = "mul (-1)"
+ have neg_neg [simp]: "?neg (?neg x) = x" for x
+ by (simp add: mul_def)
+ have enorm_mul [simp]: "enorm(mul a x) = abs a * enorm x" for a x
+ by (simp add: enorm_def mul_def power_mult_distrib) (metis real_sqrt_abs real_sqrt_mult sum_distrib_left)
+ have mul_in_top: "mul a x \<in> topspace ?E"
+ if "x \<in> topspace ?E" for a x
+ using mul_def that topspace_Euclidean_space by auto
+ have neg_in_S: "?neg x \<in> S r"
+ if "x \<in> S r" for x r
+ using that topspace_Euclidean_space S_def by simp (simp add: mul_def)
+ have *: "path_connectedin ?E (S d)"
+ if "d \<ge> 0" for d
+ proof (cases "d = 0")
+ let ?ES = "subtopology ?E (S d)"
+ case False
+ then have "d > 0"
+ using that by linarith
+ moreover have "path_connected_space ?ES"
+ unfolding path_connected_space_iff_path_component
+ proof clarify
+ have **: "path_component_of ?ES x y"
+ if x: "x \<in> topspace ?ES" and y: "y \<in> topspace ?ES" "x \<noteq> ?neg y" for x y
+ proof -
+ show ?thesis
+ unfolding path_component_of_def pathin_def S_def
+ proof (intro exI conjI)
+ let ?g = "(\<lambda>x. mul (d / enorm x) x) \<circ> (\<lambda>t i. (1 - t) * x i + t * y i)"
+ show "continuous_map (top_of_set {0::real..1}) (subtopology ?E {x \<in> topspace ?E. enorm x = d}) ?g"
+ proof (rule continuous_map_compose)
+ let ?Y = "subtopology ?E (- {zero})"
+ have **: False
+ if eq0: "\<And>j. (1 - r) * x j + r * y j = 0"
+ and ne: "x i \<noteq> - y i"
+ and d: "enorm x = d" "enorm y = d"
+ and r: "0 \<le> r" "r \<le> 1"
+ for i r
+ proof -
+ have "mul (1-r) x = ?neg (mul r y)"
+ using eq0 by (simp add: mul_def fun_eq_iff algebra_simps)
+ then have "enorm (mul (1-r) x) = enorm (?neg (mul r y))"
+ by metis
+ with r have "(1-r) * enorm x = r * enorm y"
+ by simp
+ then have r12: "r = 1/2"
+ using \<open>d \<noteq> 0\<close> d by auto
+ show ?thesis
+ using ne eq0 [of i] unfolding r12 by (simp add: algebra_simps)
+ qed
+ show "continuous_map (top_of_set {0..1}) ?Y (\<lambda>t i. (1 - t) * x i + t * y i)"
+ using x y
+ unfolding continuous_map_componentwise_UNIV Euclidean_space_def continuous_map_in_subtopology
+ apply (intro conjI allI continuous_intros)
+ apply (auto simp: zero_def mul_def S_def Euclidean_space_def fun_eq_iff)
+ using ** by blast
+ have cm_enorm': "continuous_map (subtopology (powertop_real UNIV) A) euclideanreal enorm" for A
+ unfolding enorm_def by (intro continuous_intros) auto
+ have "continuous_map ?Y (subtopology ?E {x. enorm x = d}) (\<lambda>x. mul (d / enorm x) x)"
+ unfolding continuous_map_in_subtopology
+ proof (intro conjI)
+ show "continuous_map ?Y (Euclidean_space n) (\<lambda>x. mul (d / enorm x) x)"
+ unfolding continuous_map_in_subtopology Euclidean_space_def mul_def zero_def subtopology_subtopology continuous_map_componentwise_UNIV
+ proof (intro conjI allI cm_enorm' continuous_intros)
+ show "enorm x \<noteq> 0"
+ if "x \<in> topspace (subtopology (powertop_real UNIV) ({x. \<forall>i\<ge>n. x i = 0} \<inter> - {\<lambda>i. 0}))" for x
+ using that by simp (metis abs_le_zero_iff le_enorm not_less)
+ qed auto
+ qed (use \<open>d > 0\<close> enorm_ge0 in auto)
+ moreover have "subtopology ?E {x \<in> topspace ?E. enorm x = d} = subtopology ?E {x. enorm x = d}"
+ by (simp add: subtopology_restrict Collect_conj_eq)
+ ultimately show "continuous_map ?Y (subtopology (Euclidean_space n) {x \<in> topspace (Euclidean_space n). enorm x = d}) (\<lambda>x. mul (d / enorm x) x)"
+ by metis
+ qed
+ show "?g (0::real) = x" "?g (1::real) = y"
+ using that by (auto simp: S_def zero_def mul_def fun_eq_iff)
+ qed
+ qed
+ obtain a b where a: "a \<in> topspace ?ES" and b: "b \<in> topspace ?ES"
+ and "a \<noteq> b" and negab: "?neg a \<noteq> b"
+ proof
+ let ?v = "\<lambda>j i::nat. if i = j then d else 0"
+ show "?v 0 \<in> topspace (subtopology ?E (S d))" "?v 1 \<in> topspace (subtopology ?E (S d))"
+ using \<open>n \<ge> 2\<close> \<open>d \<ge> 0\<close> by (auto simp: S_def topspace_Euclidean_space)
+ show "?v 0 \<noteq> ?v 1" "?neg (?v 0) \<noteq> (?v 1)"
+ using \<open>d > 0\<close> by (auto simp: mul_def fun_eq_iff)
+ qed
+ show "path_component_of ?ES x y"
+ if x: "x \<in> topspace ?ES" and y: "y \<in> topspace ?ES"
+ for x y
+ proof -
+ have "path_component_of ?ES x (?neg x)"
+ proof -
+ have "path_component_of ?ES x a"
+ by (metis (no_types, hide_lams) ** a b \<open>a \<noteq> b\<close> negab path_component_of_trans path_component_of_sym x)
+ moreover
+ have pa_ab: "path_component_of ?ES a b" using "**" a b negab neg_neg by blast
+ then have "path_component_of ?ES a (?neg x)"
+ by (metis "**" \<open>a \<noteq> b\<close> cloS closedin_def neg_in_S path_component_of_equiv topspace_subtopology_subset x)
+ ultimately show ?thesis
+ by (meson path_component_of_trans)
+ qed
+ then show ?thesis
+ using "**" x y by force
+ qed
+ qed
+ ultimately show ?thesis
+ by (simp add: cloS closedin_subset path_connectedin_def)
+ qed (simp add: S_def cong: conj_cong)
+ have "path_component_of (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T}) x y"
+ if "enorm x = a" "x \<in> topspace ?E" "enorm x \<in> T" "enorm y = b" "y \<in> topspace ?E" "enorm y \<in> T"
+ for x y a b
+ using that
+ proof (induction a b arbitrary: x y rule: linorder_less_wlog)
+ case (less a b)
+ then have "a \<ge> 0"
+ using enorm_ge0 by blast
+ with less.hyps have "b > 0"
+ by linarith
+ show ?case
+ proof (rule path_component_of_trans)
+ have y'_ts: "mul (a / b) y \<in> topspace ?E"
+ using \<open>y \<in> topspace ?E\<close> mul_in_top by blast
+ moreover have "enorm (mul (a / b) y) = a"
+ unfolding enorm_mul using \<open>0 < b\<close> \<open>0 \<le> a\<close> less.prems by simp
+ ultimately have y'_S: "mul (a / b) y \<in> S a"
+ using S_def by blast
+ have "x \<in> S a"
+ using S_def less.prems by blast
+ with \<open>x \<in> topspace ?E\<close> y'_ts y'_S
+ have "path_component_of (subtopology ?E (S a)) x (mul (a / b) y)"
+ by (metis * [OF \<open>a \<ge> 0\<close>] path_connected_space_iff_path_component path_connectedin_def topspace_subtopology_subset)
+ moreover
+ have "{f \<in> topspace ?E. enorm f = a} \<subseteq> {f \<in> topspace ?E. enorm f \<in> T}"
+ using \<open>enorm x = a\<close> \<open>enorm x \<in> T\<close> by force
+ ultimately
+ show "path_component_of (subtopology ?E {x. x \<in> topspace ?E \<and> enorm x \<in> T}) x (mul (a / b) y)"
+ by (simp add: S_def path_component_of_mono)
+ have "pathin ?E (\<lambda>t. mul (((1 - t) * b + t * a) / b) y)"
+ using \<open>b > 0\<close> \<open>y \<in> topspace ?E\<close>
+ unfolding pathin_def Euclidean_space_def mul_def continuous_map_in_subtopology continuous_map_componentwise_UNIV
+ by (intro allI conjI continuous_intros) auto
+ moreover have "mul (((1 - t) * b + t * a) / b) y \<in> topspace ?E"
+ if "t \<in> {0..1}" for t
+ using \<open>y \<in> topspace ?E\<close> mul_in_top by blast
+ moreover have "enorm (mul (((1 - t) * b + t * a) / b) y) \<in> T"
+ if "t \<in> {0..1}" for t
+ proof -
+ have "a \<in> T" "b \<in> T"
+ using less.prems by auto
+ then have "\<bar>(1 - t) * b + t * a\<bar> \<in> T"
+ proof (rule mem_is_interval_1_I [OF T])
+ show "a \<le> \<bar>(1 - t) * b + t * a\<bar>"
+ using that \<open>a \<ge> 0\<close> less.hyps segment_bound_lemma by auto
+ show "\<bar>(1 - t) * b + t * a\<bar> \<le> b"
+ using that \<open>a \<ge> 0\<close> less.hyps by (auto intro: convex_bound_le)
+ qed
+ then show ?thesis
+ unfolding enorm_mul \<open>enorm y = b\<close> using that \<open>b > 0\<close> by simp
+ qed
+ ultimately have pa: "pathin (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T})
+ (\<lambda>t. mul (((1 - t) * b + t * a) / b) y)"
+ by (auto simp: pathin_subtopology)
+ have ex_pathin: "\<exists>g. pathin (subtopology ?E {x \<in> topspace ?E. enorm x \<in> T}) g \<and>
+ g 0 = y \<and> g 1 = mul (a / b) y"
+ apply (rule_tac x="\<lambda>t. mul (((1 - t) * b + t * a) / b) y" in exI)
+ using \<open>b > 0\<close> pa by (auto simp: mul_def)
+ show "path_component_of (subtopology ?E {x. x \<in> topspace ?E \<and> enorm x \<in> T}) (mul (a / b) y) y"
+ by (rule path_component_of_sym) (simp add: path_component_of_def ex_pathin)
+ qed
+ next
+ case (refl a)
+ then have pc: "path_component_of (subtopology ?E (S (enorm u))) u v"
+ if "u \<in> topspace ?E \<inter> S (enorm x)" "v \<in> topspace ?E \<inter> S (enorm u)" for u v
+ using * [of a] enorm_ge0 that
+ by (auto simp: path_connectedin_def path_connected_space_iff_path_component S_def)
+ have sub: "{u \<in> topspace ?E. enorm u = enorm x} \<subseteq> {u \<in> topspace ?E. enorm u \<in> T}"
+ using \<open>enorm x \<in> T\<close> by auto
+ show ?case
+ using pc [of x y] refl by (auto simp: S_def path_component_of_mono [OF _ sub])
+ next
+ case (sym a b)
+ then show ?case
+ by (blast intro: path_component_of_sym)
+ qed
+ then show ?thesis
+ by (simp add: path_connectedin_def path_connected_space_iff_path_component)
+ qed
+ have "h ` S r \<subseteq> topspace ?E"
+ by (meson SC cmh compact_imp_compactin_subtopology compactinS compactin_subset_topspace image_compactin)
+ moreover
+ have "\<not> compact_space ?E "
+ by (metis compact_Euclidean_space \<open>n \<noteq> 0\<close>)
+ then have "\<not> compactin ?E (topspace ?E)"
+ by (simp add: compact_space_def topspace_Euclidean_space)
+ then have "h ` S r \<noteq> topspace ?E"
+ using com_hSr by auto
+ ultimately have top_hSr_ne: "topspace (subtopology ?E (topspace ?E - h ` S r)) \<noteq> {}"
+ by auto
+ show pc1: "\<exists>T. T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<and> h ` B r \<subseteq> T"
+ proof (rule exists_path_component_of_superset [OF _ top_hSr_ne])
+ have "path_connectedin ?E (h ` B r)"
+ proof (rule path_connectedin_continuous_map_image)
+ show "continuous_map (subtopology ?E (C r)) ?E h"
+ by (simp add: cmh)
+ have "path_connectedin ?E (B r)"
+ using pc_interval[of "{..<r}"] is_interval_convex_1 unfolding B_def by auto
+ then show "path_connectedin (subtopology ?E (C r)) (B r)"
+ by (simp add: path_connectedin_subtopology BC)
+ qed
+ moreover have "h ` B r \<subseteq> topspace ?E - h ` S r"
+ apply (auto simp: h_if_B)
+ by (metis BC SC disjSB disjnt_iff inj_onD [OF injh] subsetD)
+ ultimately show "path_connectedin (subtopology ?E (topspace ?E - h ` S r)) (h ` B r)"
+ by (simp add: path_connectedin_subtopology)
+ qed metis
+ show "\<exists>T. T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<and> topspace ?E - h ` (C r) \<subseteq> T"
+ proof (rule exists_path_component_of_superset [OF _ top_hSr_ne])
+ have eq: "topspace ?E - {x \<in> topspace ?E. enorm x \<le> r} = {x \<in> topspace ?E. r < enorm x}"
+ by auto
+ have "path_connectedin ?E (topspace ?E - C r)"
+ using pc_interval[of "{r<..}"] is_interval_convex_1 unfolding C_def eq by auto
+ then have "path_connectedin ?E (topspace ?E - h ` C r)"
+ by (metis biglemma [OF \<open>n \<noteq> 0\<close> compactinC cmh injh])
+ then show "path_connectedin (subtopology ?E (topspace ?E - h ` S r)) (topspace ?E - h ` C r)"
+ by (simp add: Diff_mono SC image_mono path_connectedin_subtopology)
+ qed metis
+ have "topspace ?E \<inter> (topspace ?E - h ` S r) = h ` B r \<union> (topspace ?E - h ` C r)" (is "?lhs = ?rhs")
+ proof
+ show "?lhs \<subseteq> ?rhs"
+ using \<open>\<And>r. B r \<union> S r = C r\<close> by auto
+ have "h ` B r \<inter> h ` S r = {}"
+ by (metis Diff_triv \<open>\<And>r. B r \<union> S r = C r\<close> \<open>\<And>r. disjnt (S r) (B r)\<close> disjnt_def inf_commute inj_on_Un injh)
+ then show "?rhs \<subseteq> ?lhs"
+ using path_components_of_subset pc1 \<open>\<And>r. B r \<union> S r = C r\<close>
+ by (fastforce simp add: h_if_B)
+ qed
+ then show "\<Union> (path_components_of (subtopology ?E (topspace ?E - h ` S r))) = h ` B r \<union> (topspace ?E - h ` (C r))"
+ by (simp add: Union_path_components_of)
+ show "T \<noteq> {}"
+ if "T \<in> path_components_of (subtopology ?E (topspace ?E - h ` S r))" for T
+ using that by (simp add: nonempty_path_components_of)
+ show "disjoint (path_components_of (subtopology ?E (topspace ?E - h ` S r)))"
+ by (simp add: pairwise_disjoint_path_components_of)
+ have "\<not> path_connectedin ?E (topspace ?E - h ` S r)"
+ proof (subst biglemma [OF \<open>n \<noteq> 0\<close> compactinS])
+ show "continuous_map (subtopology ?E (S r)) ?E h"
+ by (metis Un_commute Un_upper1 cmh continuous_map_from_subtopology_mono eqC)
+ show "inj_on h (S r)"
+ using SC inj_on_subset injh by blast
+ show "\<not> path_connectedin ?E (topspace ?E - S r)"
+ proof
+ have "topspace ?E - S r = {x \<in> topspace ?E. enorm x \<noteq> r}"
+ by (auto simp: S_def)
+ moreover have "enorm ` {x \<in> topspace ?E. enorm x \<noteq> r} = {0..} - {r}"
+ proof
+ have "\<exists>x. x \<in> topspace ?E \<and> enorm x \<noteq> r \<and> d = enorm x"
+ if "d \<noteq> r" "d \<ge> 0" for d
+ proof (intro exI conjI)
+ show "(\<lambda>i. if i = 0 then d else 0) \<in> topspace ?E"
+ using \<open>n \<noteq> 0\<close> by (auto simp: Euclidean_space_def)
+ show "enorm (\<lambda>i. if i = 0 then d else 0) \<noteq> r" "d = enorm (\<lambda>i. if i = 0 then d else 0)"
+ using \<open>n \<noteq> 0\<close> that by simp_all
+ qed
+ then show "{0..} - {r} \<subseteq> enorm ` {x \<in> topspace ?E. enorm x \<noteq> r}"
+ by (auto simp: image_def)
+ qed (auto simp: enorm_ge0)
+ ultimately have non_r: "enorm ` (topspace ?E - S r) = {0..} - {r}"
+ by simp
+ have "\<exists>x\<ge>0. x \<noteq> r \<and> r \<le> x"
+ by (metis gt_ex le_cases not_le order_trans)
+ then have "\<not> is_interval ({0..} - {r})"
+ unfolding is_interval_1
+ using \<open>r > 0\<close> by (auto simp: Bex_def)
+ then show False
+ if "path_connectedin ?E (topspace ?E - S r)"
+ using path_connectedin_continuous_map_image [OF cm_enorm that] by (simp add: is_interval_path_connected_1 non_r)
+ qed
+ qed
+ then have "\<not> path_connected_space (subtopology ?E (topspace ?E - h ` S r))"
+ by (simp add: path_connectedin_def)
+ then show "\<nexists>T. path_components_of (subtopology ?E (topspace ?E - h ` S r)) \<subseteq> {T}"
+ by (simp add: path_components_of_subset_singleton)
+ qed
+ moreover have "openin ?E A"
+ if "A \<in> path_components_of (subtopology ?E (topspace ?E - h ` (S r)))" for A
+ using locally_path_connected_Euclidean_space [of n] that ope_comp_hSr
+ by (simp add: locally_path_connected_space_open_path_components)
+ ultimately show ?thesis by metis
+ qed
+ have "\<exists>T. openin ?E T \<and> f x \<in> T \<and> T \<subseteq> f ` U"
+ if "x \<in> U" for x
+ proof -
+ have x: "x \<in> topspace ?E"
+ by (meson U in_mono openin_subset that)
+ obtain V where V: "openin (powertop_real UNIV) V" and Ueq: "U = V \<inter> {x. \<forall>i\<ge>n. x i = 0}"
+ using U by (auto simp: openin_subtopology Euclidean_space_def)
+ with \<open>x \<in> U\<close> have "x \<in> V" by blast
+ then obtain T where Tfin: "finite {i. T i \<noteq> UNIV}" and Topen: "\<And>i. open (T i)"
+ and Tx: "x \<in> Pi\<^sub>E UNIV T" and TV: "Pi\<^sub>E UNIV T \<subseteq> V"
+ using V by (force simp: openin_product_topology_alt)
+ have "\<exists>e>0. \<forall>x'. \<bar>x' - x i\<bar> < e \<longrightarrow> x' \<in> T i" for i
+ using Topen [of i] Tx by (auto simp: open_real)
+ then obtain \<beta> where B0: "\<And>i. \<beta> i > 0" and BT: "\<And>i x'. \<bar>x' - x i\<bar> < \<beta> i \<Longrightarrow> x' \<in> T i"
+ by metis
+ define r where "r \<equiv> Min (insert 1 (\<beta> ` {i. T i \<noteq> UNIV}))"
+ have "r > 0"
+ by (simp add: B0 Tfin r_def)
+ have inU: "y \<in> U"
+ if y: "y \<in> topspace ?E" and yxr: "\<And>i. i<n \<Longrightarrow> \<bar>y i - x i\<bar> < r" for y
+ proof -
+ have "y i \<in> T i" for i
+ proof (cases "T i = UNIV")
+ show "y i \<in> T i" if "T i \<noteq> UNIV"
+ proof (cases "i < n")
+ case True
+ then show ?thesis
+ using yxr [OF True] that by (simp add: r_def BT Tfin)
+ next
+ case False
+ then show ?thesis
+ using B0 Ueq \<open>x \<in> U\<close> topspace_Euclidean_space y by (force intro: BT)
+ qed
+ qed auto
+ with TV have "y \<in> V" by auto
+ then show ?thesis
+ using that by (auto simp: Ueq topspace_Euclidean_space)
+ qed
+ have xinU: "(\<lambda>i. x i + y i) \<in> U" if "y \<in> C(r/2)" for y
+ proof (rule inU)
+ have y: "y \<in> topspace ?E"
+ using C_def that by blast
+ show "(\<lambda>i. x i + y i) \<in> topspace ?E"
+ using x y by (simp add: topspace_Euclidean_space)
+ have "enorm y \<le> r/2"
+ using that by (simp add: C_def)
+ then show "\<bar>x i + y i - x i\<bar> < r" if "i < n" for i
+ using le_enorm enorm_ge0 that \<open>0 < r\<close> leI order_trans by fastforce
+ qed
+ show ?thesis
+ proof (intro exI conjI)
+ show "openin ?E ((f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2))"
+ proof (rule **)
+ have "continuous_map (subtopology ?E (C(r/2))) (subtopology ?E U) (\<lambda>y i. x i + y i)"
+ by (auto simp: xinU continuous_map_in_subtopology
+ intro!: continuous_intros continuous_map_Euclidean_space_add x)
+ then show "continuous_map (subtopology ?E (C(r/2))) ?E (f \<circ> (\<lambda>y i. x i + y i))"
+ by (rule continuous_map_compose) (simp add: cmf)
+ show "inj_on (f \<circ> (\<lambda>y i. x i + y i)) (C(r/2))"
+ proof (clarsimp simp add: inj_on_def C_def topspace_Euclidean_space simp del: divide_const_simps)
+ show "y' = y"
+ if ey: "enorm y \<le> r / 2" and ey': "enorm y' \<le> r / 2"
+ and y0: "\<forall>i\<ge>n. y i = 0" and y'0: "\<forall>i\<ge>n. y' i = 0"
+ and feq: "f (\<lambda>i. x i + y' i) = f (\<lambda>i. x i + y i)"
+ for y' y :: "nat \<Rightarrow> real"
+ proof -
+ have "(\<lambda>i. x i + y i) \<in> U"
+ proof (rule inU)
+ show "(\<lambda>i. x i + y i) \<in> topspace ?E"
+ using topspace_Euclidean_space x y0 by auto
+ show "\<bar>x i + y i - x i\<bar> < r" if "i < n" for i
+ using ey le_enorm [of _ y] \<open>r > 0\<close> that by fastforce
+ qed
+ moreover have "(\<lambda>i. x i + y' i) \<in> U"
+ proof (rule inU)
+ show "(\<lambda>i. x i + y' i) \<in> topspace ?E"
+ using topspace_Euclidean_space x y'0 by auto
+ show "\<bar>x i + y' i - x i\<bar> < r" if "i < n" for i
+ using ey' le_enorm [of _ y'] \<open>r > 0\<close> that by fastforce
+ qed
+ ultimately have "(\<lambda>i. x i + y' i) = (\<lambda>i. x i + y i)"
+ using feq by (meson \<open>inj_on f U\<close> inj_on_def)
+ then show ?thesis
+ by (auto simp: fun_eq_iff)
+ qed
+ qed
+ qed (simp add: \<open>0 < r\<close>)
+ have "x \<in> (\<lambda>y i. x i + y i) ` B (r / 2)"
+ proof
+ show "x = (\<lambda>i. x i + zero i)"
+ by (simp add: zero_def)
+ qed (auto simp: B_def \<open>r > 0\<close>)
+ then show "f x \<in> (f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2)"
+ by (metis image_comp image_eqI)
+ show "(f \<circ> (\<lambda>y i. x i + y i)) ` B (r/2) \<subseteq> f ` U"
+ using \<open>\<And>r. B r \<subseteq> C r\<close> xinU by fastforce
+ qed
+ qed
+ then show ?thesis
+ using openin_subopen by force
+qed
+
+
+corollary invariance_of_domain_Euclidean_space_embedding_map:
+ assumes "openin (Euclidean_space n) U"
+ and cmf: "continuous_map(subtopology (Euclidean_space n) U) (Euclidean_space n) f"
+ and "inj_on f U"
+ shows "embedding_map(subtopology (Euclidean_space n) U) (Euclidean_space n) f"
+proof (rule injective_open_imp_embedding_map [OF cmf])
+ show "open_map (subtopology (Euclidean_space n) U) (Euclidean_space n) f"
+ unfolding open_map_def
+ by (meson assms continuous_map_from_subtopology_mono inj_on_subset invariance_of_domain_Euclidean_space openin_imp_subset openin_trans_full)
+ show "inj_on f (topspace (subtopology (Euclidean_space n) U))"
+ using assms openin_subset topspace_subtopology_subset by fastforce
+qed
+
+corollary invariance_of_domain_Euclidean_space_gen:
+ assumes "n \<le> m" and U: "openin (Euclidean_space m) U"
+ and cmf: "continuous_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
+ and "inj_on f U"
+ shows "openin (Euclidean_space n) (f ` U)"
+proof -
+ have *: "Euclidean_space n = subtopology (Euclidean_space m) (topspace(Euclidean_space n))"
+ by (metis Euclidean_space_def \<open>n \<le> m\<close> inf.absorb_iff2 subset_Euclidean_space subtopology_subtopology topspace_Euclidean_space)
+ moreover have "U \<subseteq> topspace (subtopology (Euclidean_space m) U)"
+ by (metis U inf.absorb_iff2 openin_subset openin_subtopology openin_topspace)
+ ultimately show ?thesis
+ by (metis (no_types) U \<open>inj_on f U\<close> cmf continuous_map_in_subtopology inf.absorb_iff2
+ inf.orderE invariance_of_domain_Euclidean_space openin_imp_subset openin_subtopology openin_topspace)
+qed
+
+corollary invariance_of_domain_Euclidean_space_embedding_map_gen:
+ assumes "n \<le> m" and U: "openin (Euclidean_space m) U"
+ and cmf: "continuous_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
+ and "inj_on f U"
+ shows "embedding_map(subtopology (Euclidean_space m) U) (Euclidean_space n) f"
+ proof (rule injective_open_imp_embedding_map [OF cmf])
+ show "open_map (subtopology (Euclidean_space m) U) (Euclidean_space n) f"
+ by (meson U \<open>n \<le> m\<close> \<open>inj_on f U\<close> cmf continuous_map_from_subtopology_mono invariance_of_domain_Euclidean_space_gen open_map_def openin_open_subtopology subset_inj_on)
+ show "inj_on f (topspace (subtopology (Euclidean_space m) U))"
+ using assms openin_subset topspace_subtopology_subset by fastforce
+qed
+
+
+subsection\<open>Relating two variants of Euclidean space, one within product topology. \<close>
+
+proposition homeomorphic_maps_Euclidean_space_euclidean_gen_OLD:
+ fixes B :: "'n::euclidean_space set"
+ assumes "finite B" "independent B" and orth: "pairwise orthogonal B" and n: "card B = n"
+ obtains f g where "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
+proof -
+ note representation_basis [OF \<open>independent B\<close>, simp]
+ obtain b where injb: "inj_on b {..<n}" and beq: "b ` {..<n} = B"
+ using finite_imp_nat_seg_image_inj_on [OF \<open>finite B\<close>]
+ by (metis n card_Collect_less_nat card_image lessThan_def)
+ then have biB: "\<And>i. i < n \<Longrightarrow> b i \<in> B"
+ by force
+ have repr: "\<And>v. v \<in> span B \<Longrightarrow> (\<Sum>i<n. representation B v (b i) *\<^sub>R b i) = v"
+ using real_vector.sum_representation_eq [OF \<open>independent B\<close> _ \<open>finite B\<close>]
+ by (metis (no_types, lifting) injb beq order_refl sum.reindex_cong)
+ let ?f = "\<lambda>x. \<Sum>i<n. x i *\<^sub>R b i"
+ let ?g = "\<lambda>v i. if i < n then representation B v (b i) else 0"
+ show thesis
+ proof
+ show "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) ?f ?g"
+ unfolding homeomorphic_maps_def
+ proof (intro conjI)
+ have *: "continuous_map euclidean (top_of_set (span B)) ?f"
+ by (metis (mono_tags) biB continuous_map_span_sum lessThan_iff)
+ show "continuous_map (Euclidean_space n) (top_of_set (span B)) ?f"
+ unfolding Euclidean_space_def
+ by (rule continuous_map_from_subtopology) (simp add: euclidean_product_topology *)
+ show "continuous_map (top_of_set (span B)) (Euclidean_space n) ?g"
+ unfolding Euclidean_space_def
+ by (auto simp: continuous_map_in_subtopology continuous_map_componentwise_UNIV continuous_on_representation \<open>independent B\<close> biB orth pairwise_orthogonal_imp_finite)
+ have [simp]: "\<And>x i. i<n \<Longrightarrow> x i *\<^sub>R b i \<in> span B"
+ by (simp add: biB span_base span_scale)
+ have "representation B (?f x) (b j) = x j"
+ if 0: "\<forall>i\<ge>n. x i = (0::real)" and "j < n" for x j
+ proof -
+ have "representation B (?f x) (b j) = (\<Sum>i<n. representation B (x i *\<^sub>R b i) (b j))"
+ by (subst real_vector.representation_sum) (auto simp add: \<open>independent B\<close>)
+ also have "... = (\<Sum>i<n. x i * representation B (b i) (b j))"
+ by (simp add: assms(2) biB representation_scale span_base)
+ also have "... = (\<Sum>i<n. if b j = b i then x i else 0)"
+ by (simp add: biB if_distrib cong: if_cong)
+ also have "... = x j"
+ using that inj_on_eq_iff [OF injb] by auto
+ finally show ?thesis .
+ qed
+ then show "\<forall>x\<in>topspace (Euclidean_space n). ?g (?f x) = x"
+ by (auto simp: Euclidean_space_def)
+ show "\<forall>y\<in>topspace (top_of_set (span B)). ?f (?g y) = y"
+ using repr by (auto simp: Euclidean_space_def)
+ qed
+ qed
+qed
+
+proposition homeomorphic_maps_Euclidean_space_euclidean_gen:
+ fixes B :: "'n::euclidean_space set"
+ assumes "independent B" and orth: "pairwise orthogonal B" and n: "card B = n"
+ and 1: "\<And>u. u \<in> B \<Longrightarrow> norm u = 1"
+ obtains f g where "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
+ and "\<And>x. x \<in> topspace (Euclidean_space n) \<Longrightarrow> (norm (f x))\<^sup>2 = (\<Sum>i<n. (x i)\<^sup>2)"
+proof -
+ note representation_basis [OF \<open>independent B\<close>, simp]
+ have "finite B"
+ using \<open>independent B\<close> finiteI_independent by metis
+ obtain b where injb: "inj_on b {..<n}" and beq: "b ` {..<n} = B"
+ using finite_imp_nat_seg_image_inj_on [OF \<open>finite B\<close>]
+ by (metis n card_Collect_less_nat card_image lessThan_def)
+ then have biB: "\<And>i. i < n \<Longrightarrow> b i \<in> B"
+ by force
+ have "0 \<notin> B"
+ using \<open>independent B\<close> dependent_zero by blast
+ have [simp]: "b i \<bullet> b j = (if j = i then 1 else 0)"
+ if "i < n" "j < n" for i j
+ proof (cases "i = j")
+ case True
+ with 1 that show ?thesis
+ by (auto simp: norm_eq_sqrt_inner biB)
+ next
+ case False
+ then have "b i \<noteq> b j"
+ by (meson inj_onD injb lessThan_iff that)
+ then show ?thesis
+ using orth by (auto simp: orthogonal_def pairwise_def norm_eq_sqrt_inner that biB)
+ qed
+ have [simp]: "\<And>x i. i<n \<Longrightarrow> x i *\<^sub>R b i \<in> span B"
+ by (simp add: biB span_base span_scale)
+ have repr: "\<And>v. v \<in> span B \<Longrightarrow> (\<Sum>i<n. representation B v (b i) *\<^sub>R b i) = v"
+ using real_vector.sum_representation_eq [OF \<open>independent B\<close> _ \<open>finite B\<close>]
+ by (metis (no_types, lifting) injb beq order_refl sum.reindex_cong)
+ define f where "f \<equiv> \<lambda>x. \<Sum>i<n. x i *\<^sub>R b i"
+ define g where "g \<equiv> \<lambda>v i. if i < n then representation B v (b i) else 0"
+ show thesis
+ proof
+ show "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
+ unfolding homeomorphic_maps_def
+ proof (intro conjI)
+ have *: "continuous_map euclidean (top_of_set (span B)) f"
+ unfolding f_def
+ by (rule continuous_map_span_sum) (use biB \<open>0 \<notin> B\<close> in auto)
+ show "continuous_map (Euclidean_space n) (top_of_set (span B)) f"
+ unfolding Euclidean_space_def
+ by (rule continuous_map_from_subtopology) (simp add: euclidean_product_topology *)
+ show "continuous_map (top_of_set (span B)) (Euclidean_space n) g"
+ unfolding Euclidean_space_def g_def
+ by (auto simp: continuous_map_in_subtopology continuous_map_componentwise_UNIV continuous_on_representation \<open>independent B\<close> biB orth pairwise_orthogonal_imp_finite)
+ have "representation B (f x) (b j) = x j"
+ if 0: "\<forall>i\<ge>n. x i = (0::real)" and "j < n" for x j
+ proof -
+ have "representation B (f x) (b j) = (\<Sum>i<n. representation B (x i *\<^sub>R b i) (b j))"
+ unfolding f_def
+ by (subst real_vector.representation_sum) (auto simp add: \<open>independent B\<close>)
+ also have "... = (\<Sum>i<n. x i * representation B (b i) (b j))"
+ by (simp add: \<open>independent B\<close> biB representation_scale span_base)
+ also have "... = (\<Sum>i<n. if b j = b i then x i else 0)"
+ by (simp add: biB if_distrib cong: if_cong)
+ also have "... = x j"
+ using that inj_on_eq_iff [OF injb] by auto
+ finally show ?thesis .
+ qed
+ then show "\<forall>x\<in>topspace (Euclidean_space n). g (f x) = x"
+ by (auto simp: Euclidean_space_def f_def g_def)
+ show "\<forall>y\<in>topspace (top_of_set (span B)). f (g y) = y"
+ using repr by (auto simp: Euclidean_space_def f_def g_def)
+ qed
+ show normeq: "(norm (f x))\<^sup>2 = (\<Sum>i<n. (x i)\<^sup>2)" if "x \<in> topspace (Euclidean_space n)" for x
+ unfolding f_def dot_square_norm [symmetric]
+ by (simp add: power2_eq_square inner_sum_left inner_sum_right if_distrib biB cong: if_cong)
+ qed
+qed
+
+corollary homeomorphic_maps_Euclidean_space_euclidean:
+ obtains f :: "(nat \<Rightarrow> real) \<Rightarrow> 'n::euclidean_space" and g
+ where "homeomorphic_maps (Euclidean_space (DIM('n))) euclidean f g"
+ by (force intro: homeomorphic_maps_Euclidean_space_euclidean_gen [OF independent_Basis orthogonal_Basis refl norm_Basis])
+
+lemma homeomorphic_maps_nsphere_euclidean_sphere:
+ fixes B :: "'n::euclidean_space set"
+ assumes B: "independent B" and orth: "pairwise orthogonal B" and n: "card B = n" and "n \<noteq> 0"
+ and 1: "\<And>u. u \<in> B \<Longrightarrow> norm u = 1"
+ obtains f :: "(nat \<Rightarrow> real) \<Rightarrow> 'n::euclidean_space" and g
+ where "homeomorphic_maps (nsphere(n - 1)) (top_of_set (sphere 0 1 \<inter> span B)) f g"
+proof -
+ have "finite B"
+ using \<open>independent B\<close> finiteI_independent by metis
+ obtain f g where fg: "homeomorphic_maps (Euclidean_space n) (top_of_set (span B)) f g"
+ and normf: "\<And>x. x \<in> topspace (Euclidean_space n) \<Longrightarrow> (norm (f x))\<^sup>2 = (\<Sum>i<n. (x i)\<^sup>2)"
+ using homeomorphic_maps_Euclidean_space_euclidean_gen [OF B orth n 1]
+ by blast
+ obtain b where injb: "inj_on b {..<n}" and beq: "b ` {..<n} = B"
+ using finite_imp_nat_seg_image_inj_on [OF \<open>finite B\<close>]
+ by (metis n card_Collect_less_nat card_image lessThan_def)
+ then have biB: "\<And>i. i < n \<Longrightarrow> b i \<in> B"
+ by force
+ have [simp]: "\<And>i. i < n \<Longrightarrow> b i \<noteq> 0"
+ using \<open>independent B\<close> biB dependent_zero by fastforce
+ have [simp]: "b i \<bullet> b j = (if j = i then (norm (b i))\<^sup>2 else 0)"
+ if "i < n" "j < n" for i j
+ proof (cases "i = j")
+ case False
+ then have "b i \<noteq> b j"
+ by (meson inj_onD injb lessThan_iff that)
+ then show ?thesis
+ using orth by (auto simp: orthogonal_def pairwise_def norm_eq_sqrt_inner that biB)
+ qed (auto simp: norm_eq_sqrt_inner)
+ have [simp]: "Suc (n - Suc 0) = n"
+ using Suc_pred \<open>n \<noteq> 0\<close> by blast
+ then have [simp]: "{..card B - Suc 0} = {..<card B}"
+ using n by fastforce
+ show thesis
+ proof
+ have 1: "norm (f x) = 1"
+ if "(\<Sum>i<card B. (x i)\<^sup>2) = (1::real)" "x \<in> topspace (Euclidean_space n)" for x
+ proof -
+ have "norm (f x)^2 = 1"
+ using normf that by (simp add: n)
+ with that show ?thesis
+ by (simp add: power2_eq_imp_eq)
+ qed
+ have "homeomorphic_maps (nsphere (n - 1)) (top_of_set (span B \<inter> sphere 0 1)) f g"
+ unfolding nsphere_def subtopology_subtopology [symmetric]
+ proof (rule homeomorphic_maps_subtopologies_alt)
+ show "homeomorphic_maps (Euclidean_space (Suc (n - 1))) (top_of_set (span B)) f g"
+ using fg by (force simp add: )
+ show "f ` (topspace (Euclidean_space (Suc (n - 1))) \<inter> {x. (\<Sum>i\<le>n - 1. (x i)\<^sup>2) = 1}) \<subseteq> sphere 0 1"
+ using n by (auto simp: image_subset_iff Euclidean_space_def 1)
+ have "(\<Sum>i\<le>n - Suc 0. (g u i)\<^sup>2) = 1"
+ if "u \<in> span B" and "norm (u::'n) = 1" for u
+ proof -
+ obtain v where [simp]: "u = f v" "v \<in> topspace (Euclidean_space n)"
+ using fg unfolding homeomorphic_maps_map subset_iff
+ by (metis \<open>u \<in> span B\<close> homeomorphic_imp_surjective_map image_eqI topspace_euclidean_subtopology)
+ then have [simp]: "g (f v) = v"
+ by (meson fg homeomorphic_maps_map)
+ have fv21: "norm (f v) ^ 2 = 1"
+ using that by simp
+ show ?thesis
+ using that normf fv21 \<open>v \<in> topspace (Euclidean_space n)\<close> n by force
+ qed
+ then show "g ` (topspace (top_of_set (span B)) \<inter> sphere 0 1) \<subseteq> {x. (\<Sum>i\<le>n - 1. (x i)\<^sup>2) = 1}"
+ by auto
+ qed
+ then show "homeomorphic_maps (nsphere(n - 1)) (top_of_set (sphere 0 1 \<inter> span B)) f g"
+ by (simp add: inf_commute)
+ qed
+qed
+
+
+
+subsection\<open> Invariance of dimension and domain in setting of R^n.\<close>
+
+lemma homeomorphic_maps_iff_homeomorphism [simp]:
+ "homeomorphic_maps (top_of_set S) (top_of_set T) f g \<longleftrightarrow> homeomorphism S T f g"
+ unfolding homeomorphic_maps_def homeomorphism_def by force
+
+lemma homeomorphic_space_iff_homeomorphic [simp]:
+ "(top_of_set S) homeomorphic_space (top_of_set T) \<longleftrightarrow> S homeomorphic T"
+ by (simp add: homeomorphic_def homeomorphic_space_def)
+
+lemma homeomorphic_subspace_Euclidean_space:
+ fixes S :: "'a::euclidean_space set"
+ assumes "subspace S"
+ shows "top_of_set S homeomorphic_space Euclidean_space n \<longleftrightarrow> dim S = n"
+proof -
+ obtain B where B: "B \<subseteq> S" "independent B" "span B = S" "card B = dim S"
+ and orth: "pairwise orthogonal B" and 1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
+ by (metis assms orthonormal_basis_subspace)
+ then have "finite B"
+ by (simp add: pairwise_orthogonal_imp_finite)
+ have "top_of_set S homeomorphic_space top_of_set (span B)"
+ unfolding homeomorphic_space_iff_homeomorphic
+ by (auto simp: assms B intro: homeomorphic_subspaces)
+ also have "\<dots> homeomorphic_space Euclidean_space (dim S)"
+ unfolding homeomorphic_space_def
+ using homeomorphic_maps_Euclidean_space_euclidean_gen [OF \<open>independent B\<close> orth] homeomorphic_maps_sym 1 B
+ by metis
+ finally have "top_of_set S homeomorphic_space Euclidean_space (dim S)" .
+ then show ?thesis
+ using homeomorphic_space_sym homeomorphic_space_trans invariance_of_dimension_Euclidean_space by blast
+qed
+
+lemma homeomorphic_subspace_Euclidean_space_dim:
+ fixes S :: "'a::euclidean_space set"
+ assumes "subspace S"
+ shows "top_of_set S homeomorphic_space Euclidean_space (dim S)"
+ by (simp add: homeomorphic_subspace_Euclidean_space assms)
+
+lemma homeomorphic_subspaces_eq:
+ fixes S T:: "'a::euclidean_space set"
+ assumes "subspace S" "subspace T"
+ shows "S homeomorphic T \<longleftrightarrow> dim S = dim T"
+proof
+ show "dim S = dim T"
+ if "S homeomorphic T"
+ proof -
+ have "Euclidean_space (dim S) homeomorphic_space top_of_set S"
+ using \<open>subspace S\<close> homeomorphic_space_sym homeomorphic_subspace_Euclidean_space_dim by blast
+ also have "\<dots> homeomorphic_space top_of_set T"
+ by (simp add: that)
+ also have "\<dots> homeomorphic_space Euclidean_space (dim T)"
+ by (simp add: homeomorphic_subspace_Euclidean_space assms)
+ finally have "Euclidean_space (dim S) homeomorphic_space Euclidean_space (dim T)" .
+ then show ?thesis
+ by (simp add: invariance_of_dimension_Euclidean_space)
+ qed
+next
+ show "S homeomorphic T"
+ if "dim S = dim T"
+ by (metis that assms homeomorphic_subspaces)
+qed
+
+lemma homeomorphic_affine_Euclidean_space:
+ assumes "affine S"
+ shows "top_of_set S homeomorphic_space Euclidean_space n \<longleftrightarrow> aff_dim S = n"
+ (is "?X homeomorphic_space ?E \<longleftrightarrow> aff_dim S = n")
+proof (cases "S = {}")
+ case True
+ with assms show ?thesis
+ using homeomorphic_empty_space nonempty_Euclidean_space by fastforce
+next
+ case False
+ then obtain a where "a \<in> S"
+ by force
+ have "(?X homeomorphic_space ?E)
+ = (top_of_set (image (\<lambda>x. -a + x) S) homeomorphic_space ?E)"
+ proof
+ show "top_of_set ((+) (- a) ` S) homeomorphic_space ?E"
+ if "?X homeomorphic_space ?E"
+ using that
+ by (meson homeomorphic_space_iff_homeomorphic homeomorphic_space_sym homeomorphic_space_trans homeomorphic_translation)
+ show "?X homeomorphic_space ?E"
+ if "top_of_set ((+) (- a) ` S) homeomorphic_space ?E"
+ using that
+ by (meson homeomorphic_space_iff_homeomorphic homeomorphic_space_trans homeomorphic_translation)
+ qed
+ also have "\<dots> \<longleftrightarrow> aff_dim S = n"
+ by (metis \<open>a \<in> S\<close> aff_dim_eq_dim affine_diffs_subspace affine_hull_eq assms homeomorphic_subspace_Euclidean_space of_nat_eq_iff)
+ finally show ?thesis .
+qed
+
+
+corollary invariance_of_domain_subspaces:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes ope: "openin (top_of_set U) S"
+ and "subspace U" "subspace V" and VU: "dim V \<le> dim U"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and injf: "inj_on f S"
+ shows "openin (top_of_set V) (f ` S)"
+proof -
+ have "S \<subseteq> U"
+ using openin_imp_subset [OF ope] .
+ have Uhom: "top_of_set U homeomorphic_space Euclidean_space (dim U)"
+ and Vhom: "top_of_set V homeomorphic_space Euclidean_space (dim V)"
+ by (simp_all add: assms homeomorphic_subspace_Euclidean_space_dim)
+ then obtain \<phi> \<phi>' where hom: "homeomorphic_maps (top_of_set U) (Euclidean_space (dim U)) \<phi> \<phi>'"
+ by (auto simp: homeomorphic_space_def)
+ obtain \<psi> \<psi>' where \<psi>: "homeomorphic_map (top_of_set V) (Euclidean_space (dim V)) \<psi>"
+ and \<psi>'\<psi>: "\<forall>x\<in>V. \<psi>' (\<psi> x) = x"
+ using Vhom by (auto simp: homeomorphic_space_def homeomorphic_maps_map)
+ have "((\<psi> \<circ> f \<circ> \<phi>') o \<phi>) ` S = (\<psi> o f) ` S"
+ proof (rule image_cong [OF refl])
+ show "(\<psi> \<circ> f \<circ> \<phi>' \<circ> \<phi>) x = (\<psi> \<circ> f) x" if "x \<in> S" for x
+ using that unfolding o_def
+ by (metis \<open>S \<subseteq> U\<close> hom homeomorphic_maps_map in_mono topspace_euclidean_subtopology)
+ qed
+ moreover
+ have "openin (Euclidean_space (dim V)) ((\<psi> \<circ> f \<circ> \<phi>') ` \<phi> ` S)"
+ proof (rule invariance_of_domain_Euclidean_space_gen [OF VU])
+ show "openin (Euclidean_space (dim U)) (\<phi> ` S)"
+ using homeomorphic_map_openness_eq hom homeomorphic_maps_map ope by blast
+ show "continuous_map (subtopology (Euclidean_space (dim U)) (\<phi> ` S)) (Euclidean_space (dim V)) (\<psi> \<circ> f \<circ> \<phi>')"
+ proof (intro continuous_map_compose)
+ have "continuous_on ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<phi>'"
+ if "continuous_on {x. \<forall>i\<ge>dim U. x i = 0} \<phi>'"
+ using that by (force elim: continuous_on_subset)
+ moreover have "\<phi>' ` ({x. \<forall>i\<ge>dim U. x i = 0} \<inter> \<phi> ` S) \<subseteq> S"
+ if "\<forall>x\<in>U. \<phi>' (\<phi> x) = x"
+ using that \<open>S \<subseteq> U\<close> by fastforce
+ ultimately show "continuous_map (subtopology (Euclidean_space (dim U)) (\<phi> ` S)) (top_of_set S) \<phi>'"
+ using hom unfolding homeomorphic_maps_def
+ by (simp add: Euclidean_space_def subtopology_subtopology euclidean_product_topology)
+ show "continuous_map (top_of_set S) (top_of_set V) f"
+ by (simp add: contf fim)
+ show "continuous_map (top_of_set V) (Euclidean_space (dim V)) \<psi>"
+ by (simp add: \<psi> homeomorphic_imp_continuous_map)
+ qed
+ show "inj_on (\<psi> \<circ> f \<circ> \<phi>') (\<phi> ` S)"
+ using injf hom
+ unfolding inj_on_def homeomorphic_maps_map
+ by simp (metis \<open>S \<subseteq> U\<close> \<psi>'\<psi> fim imageI subsetD)
+ qed
+ ultimately have "openin (Euclidean_space (dim V)) (\<psi> ` f ` S)"
+ by (simp add: image_comp)
+ then show ?thesis
+ by (simp add: fim homeomorphic_map_openness_eq [OF \<psi>])
+qed
+
+lemma invariance_of_domain:
+ fixes f :: "'a \<Rightarrow> 'a::euclidean_space"
+ assumes "continuous_on S f" "open S" "inj_on f S" shows "open(f ` S)"
+ using invariance_of_domain_subspaces [of UNIV S UNIV] assms by (force simp add: )
+
+corollary invariance_of_dimension_subspaces:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes ope: "openin (top_of_set U) S"
+ and "subspace U" "subspace V"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and injf: "inj_on f S" and "S \<noteq> {}"
+ shows "dim U \<le> dim V"
+proof -
+ have "False" if "dim V < dim U"
+ proof -
+ obtain T where "subspace T" "T \<subseteq> U" "dim T = dim V"
+ using choose_subspace_of_subspace [of "dim V" U]
+ by (metis \<open>dim V < dim U\<close> assms(2) order.strict_implies_order span_eq_iff)
+ then have "V homeomorphic T"
+ by (simp add: \<open>subspace V\<close> homeomorphic_subspaces)
+ then obtain h k where homhk: "homeomorphism V T h k"
+ using homeomorphic_def by blast
+ have "continuous_on S (h \<circ> f)"
+ by (meson contf continuous_on_compose continuous_on_subset fim homeomorphism_cont1 homhk)
+ moreover have "(h \<circ> f) ` S \<subseteq> U"
+ using \<open>T \<subseteq> U\<close> fim homeomorphism_image1 homhk by fastforce
+ moreover have "inj_on (h \<circ> f) S"
+ apply (clarsimp simp: inj_on_def)
+ by (metis fim homeomorphism_apply1 homhk image_subset_iff inj_onD injf)
+ ultimately have ope_hf: "openin (top_of_set U) ((h \<circ> f) ` S)"
+ using invariance_of_domain_subspaces [OF ope \<open>subspace U\<close> \<open>subspace U\<close>] by blast
+ have "(h \<circ> f) ` S \<subseteq> T"
+ using fim homeomorphism_image1 homhk by fastforce
+ then have "dim ((h \<circ> f) ` S) \<le> dim T"
+ by (rule dim_subset)
+ also have "dim ((h \<circ> f) ` S) = dim U"
+ using \<open>S \<noteq> {}\<close> \<open>subspace U\<close>
+ by (blast intro: dim_openin ope_hf)
+ finally show False
+ using \<open>dim V < dim U\<close> \<open>dim T = dim V\<close> by simp
+ qed
+ then show ?thesis
+ using not_less by blast
+qed
+
+corollary invariance_of_domain_affine_sets:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes ope: "openin (top_of_set U) S"
+ and aff: "affine U" "affine V" "aff_dim V \<le> aff_dim U"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and injf: "inj_on f S"
+ shows "openin (top_of_set V) (f ` S)"
+proof (cases "S = {}")
+ case False
+ obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
+ using False fim ope openin_contains_cball by fastforce
+ have "openin (top_of_set ((+) (- b) ` V)) (((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S)"
+ proof (rule invariance_of_domain_subspaces)
+ show "openin (top_of_set ((+) (- a) ` U)) ((+) (- a) ` S)"
+ by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
+ show "subspace ((+) (- a) ` U)"
+ by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace_subtract \<open>affine U\<close> cong: image_cong_simp)
+ show "subspace ((+) (- b) ` V)"
+ by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace_subtract \<open>affine V\<close> cong: image_cong_simp)
+ show "dim ((+) (- b) ` V) \<le> dim ((+) (- a) ` U)"
+ by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
+ show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
+ by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
+ show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
+ using fim by auto
+ show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
+ by (auto simp: inj_on_def) (meson inj_onD injf)
+ qed
+ then show ?thesis
+ by (metis (no_types, lifting) homeomorphism_imp_open_map homeomorphism_translation image_comp translation_galois)
+qed auto
+
+corollary invariance_of_dimension_affine_sets:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes ope: "openin (top_of_set U) S"
+ and aff: "affine U" "affine V"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> V"
+ and injf: "inj_on f S" and "S \<noteq> {}"
+ shows "aff_dim U \<le> aff_dim V"
+proof -
+ obtain a b where "a \<in> S" "a \<in> U" "b \<in> V"
+ using \<open>S \<noteq> {}\<close> fim ope openin_contains_cball by fastforce
+ have "dim ((+) (- a) ` U) \<le> dim ((+) (- b) ` V)"
+ proof (rule invariance_of_dimension_subspaces)
+ show "openin (top_of_set ((+) (- a) ` U)) ((+) (- a) ` S)"
+ by (metis ope homeomorphism_imp_open_map homeomorphism_translation translation_galois)
+ show "subspace ((+) (- a) ` U)"
+ by (simp add: \<open>a \<in> U\<close> affine_diffs_subspace_subtract \<open>affine U\<close> cong: image_cong_simp)
+ show "subspace ((+) (- b) ` V)"
+ by (simp add: \<open>b \<in> V\<close> affine_diffs_subspace_subtract \<open>affine V\<close> cong: image_cong_simp)
+ show "continuous_on ((+) (- a) ` S) ((+) (- b) \<circ> f \<circ> (+) a)"
+ by (metis contf continuous_on_compose homeomorphism_cont2 homeomorphism_translation translation_galois)
+ show "((+) (- b) \<circ> f \<circ> (+) a) ` (+) (- a) ` S \<subseteq> (+) (- b) ` V"
+ using fim by auto
+ show "inj_on ((+) (- b) \<circ> f \<circ> (+) a) ((+) (- a) ` S)"
+ by (auto simp: inj_on_def) (meson inj_onD injf)
+ qed (use \<open>S \<noteq> {}\<close> in auto)
+ then show ?thesis
+ by (metis \<open>a \<in> U\<close> \<open>b \<in> V\<close> aff_dim_eq_dim affine_hull_eq aff of_nat_le_iff)
+qed
+
+corollary invariance_of_dimension:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and "open S"
+ and injf: "inj_on f S" and "S \<noteq> {}"
+ shows "DIM('a) \<le> DIM('b)"
+ using%unimportant invariance_of_dimension_subspaces [of UNIV S UNIV f] assms
+ by auto
+
+corollary continuous_injective_image_subspace_dim_le:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "subspace S" "subspace T"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> T"
+ and injf: "inj_on f S"
+ shows "dim S \<le> dim T"
+ apply (rule invariance_of_dimension_subspaces [of S S _ f])
+ using%unimportant assms by (auto simp: subspace_affine)
+
+lemma invariance_of_dimension_convex_domain:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "convex S"
+ and contf: "continuous_on S f" and fim: "f ` S \<subseteq> affine hull T"
+ and injf: "inj_on f S"
+ shows "aff_dim S \<le> aff_dim T"
+proof (cases "S = {}")
+ case True
+ then show ?thesis by (simp add: aff_dim_geq)
+next
+ case False
+ have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
+ proof (rule invariance_of_dimension_affine_sets)
+ show "openin (top_of_set (affine hull S)) (rel_interior S)"
+ by (simp add: openin_rel_interior)
+ show "continuous_on (rel_interior S) f"
+ using contf continuous_on_subset rel_interior_subset by blast
+ show "f ` rel_interior S \<subseteq> affine hull T"
+ using fim rel_interior_subset by blast
+ show "inj_on f (rel_interior S)"
+ using inj_on_subset injf rel_interior_subset by blast
+ show "rel_interior S \<noteq> {}"
+ by (simp add: False \<open>convex S\<close> rel_interior_eq_empty)
+ qed auto
+ then show ?thesis
+ by simp
+qed
+
+lemma homeomorphic_convex_sets_le:
+ assumes "convex S" "S homeomorphic T"
+ shows "aff_dim S \<le> aff_dim T"
+proof -
+ obtain h k where homhk: "homeomorphism S T h k"
+ using homeomorphic_def assms by blast
+ show ?thesis
+ proof (rule invariance_of_dimension_convex_domain [OF \<open>convex S\<close>])
+ show "continuous_on S h"
+ using homeomorphism_def homhk by blast
+ show "h ` S \<subseteq> affine hull T"
+ by (metis homeomorphism_def homhk hull_subset)
+ show "inj_on h S"
+ by (meson homeomorphism_apply1 homhk inj_on_inverseI)
+ qed
+qed
+
+lemma homeomorphic_convex_sets:
+ assumes "convex S" "convex T" "S homeomorphic T"
+ shows "aff_dim S = aff_dim T"
+ by (meson assms dual_order.antisym homeomorphic_convex_sets_le homeomorphic_sym)
+
+lemma homeomorphic_convex_compact_sets_eq:
+ assumes "convex S" "compact S" "convex T" "compact T"
+ shows "S homeomorphic T \<longleftrightarrow> aff_dim S = aff_dim T"
+ by (meson assms homeomorphic_convex_compact_sets homeomorphic_convex_sets)
+
+lemma invariance_of_domain_gen:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "open S" "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
+ shows "open(f ` S)"
+ using invariance_of_domain_subspaces [of UNIV S UNIV f] assms by auto
+
+lemma injective_into_1d_imp_open_map_UNIV:
+ fixes f :: "'a::euclidean_space \<Rightarrow> real"
+ assumes "open T" "continuous_on S f" "inj_on f S" "T \<subseteq> S"
+ shows "open (f ` T)"
+ apply (rule invariance_of_domain_gen [OF \<open>open T\<close>])
+ using assms apply (auto simp: elim: continuous_on_subset subset_inj_on)
+ done
+
+lemma continuous_on_inverse_open:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" and gf: "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x"
+ shows "continuous_on (f ` S) g"
+proof (clarsimp simp add: continuous_openin_preimage_eq)
+ fix T :: "'a set"
+ assume "open T"
+ have eq: "f ` S \<inter> g -` T = f ` (S \<inter> T)"
+ by (auto simp: gf)
+ have "openin (top_of_set (f ` S)) (f ` (S \<inter> T))"
+ proof (rule open_openin_trans [OF invariance_of_domain_gen])
+ show "inj_on f S"
+ using inj_on_inverseI gf by auto
+ show "open (f ` (S \<inter> T))"
+ by (meson \<open>inj_on f S\<close> \<open>open T\<close> assms(1-3) continuous_on_subset inf_le1 inj_on_subset invariance_of_domain_gen open_Int)
+ qed (use assms in auto)
+ then show "openin (top_of_set (f ` S)) (f ` S \<inter> g -` T)"
+ by (simp add: eq)
+qed
+
+end
\ No newline at end of file
--- a/src/HOL/Homology/Simplices.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Homology/Simplices.thy Wed Apr 10 13:34:55 2019 +0100
@@ -575,9 +575,6 @@
subsection\<open>Show that all boundaries are cycles, the key "chain complex" property.\<close>
-lemma sum_Int_Diff: "finite A \<Longrightarrow> sum f A = sum f (A \<inter> B) + sum f (A - B)"
- by (metis Diff_Diff_Int Diff_subset sum.subset_diff)
-
lemma chain_boundary_boundary:
assumes "singular_chain p X c"
shows "chain_boundary (p - Suc 0) (chain_boundary p c) = 0"
@@ -623,7 +620,7 @@
have *: "(\<Sum>x\<le>p. \<Sum>i\<le>p - Suc 0.
frag_cmul ((-1) ^ (x + i)) (frag_of (singular_face (p - Suc 0) i (singular_face p x g))))
= 0"
- apply (simp add: sum.cartesian_product sum_Int_Diff [of "_ \<times> _" _ "{(x,y). y < x}"])
+ apply (simp add: sum.cartesian_product sum.Int_Diff [of "_ \<times> _" _ "{(x,y). y < x}"])
apply (rule eq0)
apply (simp only: frag_cmul_sum prod.case_distrib [of "frag_cmul (-1)"] frag_cmul_cmul eql eqr flip: power_Suc)
apply (force simp: simp add: inj_on_def sum.reindex add.commute eqf intro: sum.cong)
@@ -1091,26 +1088,6 @@
qed
qed (auto simp: oriented_simplex_def)
-lemma sum_zero_middle:
- fixes g :: "nat \<Rightarrow> 'a::comm_monoid_add"
- assumes "1 \<le> p" "k \<le> p"
- shows "(\<Sum>j\<le>p. if j < k then f j else if j = k then 0 else g (j - Suc 0))
- = (\<Sum>j\<le>p - Suc 0. if j < k then f j else g j)" (is "?lhs = ?rhs")
-proof -
- have [simp]: "{..p - Suc 0} \<inter> {j. j < k} = {..<k}" "{..p - Suc 0} \<inter> - {j. j < k} = {k..p - Suc 0}"
- using assms by auto
- have "?lhs = (\<Sum>j<k. f j) + (\<Sum>j = k..p. if j = k then 0 else g (j - Suc 0))"
- using sum.union_disjoint [of "{..<k}" "{k..p}", where 'a='a] assms
- by (simp add: ivl_disj_int_one ivl_disj_un_one)
- also have "\<dots> = (\<Sum>j<k. f j) + (\<Sum>j = Suc k..p. g (j - Suc 0))"
- by (simp add: sum_head_Suc [of k p] assms)
- also have "\<dots> = (\<Sum>j<k. f j) + (\<Sum>j = k..p - Suc 0. g j)"
- using sum.reindex [of Suc "{k..p - Suc 0}", where 'a='a] assms by simp
- also have "\<dots> = ?rhs"
- by (simp add: comm_monoid_add_class.sum.If_cases)
- finally show ?thesis .
-qed
-
lemma singular_face_oriented_simplex:
assumes "1 \<le> p" "k \<le> p"
shows "singular_face p k (oriented_simplex p l) =
@@ -1122,7 +1099,7 @@
proof -
show ?thesis
unfolding simplical_face_def
- using sum_zero_middle [OF assms, where 'a=real, symmetric]
+ using sum.zero_middle [OF assms, where 'a=real, symmetric]
apply (simp add: if_distrib [of "\<lambda>x. _ * x"] if_distrib [of "\<lambda>f. f i * _"] atLeast0AtMost cong: if_cong)
done
qed
@@ -1144,7 +1121,7 @@
apply (simp add: feq singular_face_def oriented_simplex_def)
apply (simp add: simplical_face_in_standard_simplex [OF p] restrict_compose_left subset_eq)
apply (rule_tac x="\<lambda>i. if i < k then m i else m (Suc i)" in exI)
- using sum_zero_middle [OF p, where 'a=real, symmetric] unfolding simplical_face_def o_def
+ using sum.zero_middle [OF p, where 'a=real, symmetric] unfolding simplical_face_def o_def
apply (simp add: if_distrib [of "\<lambda>x. _ * x"] if_distrib [of "\<lambda>f. f _ * _"] atLeast0AtMost cong: if_cong)
done
ultimately
@@ -1213,7 +1190,7 @@
by (simp add: oriented_simplex_def standard_simplex_def)
have "oriented_simplex (Suc p) (\<lambda>i. if i = 0 then v else l (i -1)) x \<in> T"
if "x \<in> standard_simplex (Suc p)" for x
- proof (simp add: that oriented_simplex_def sum_atMost_Suc_shift del: sum_atMost_Suc)
+ proof (simp add: that oriented_simplex_def sum_atMost_Suc_shift del: sum.atMost_Suc)
have x01: "\<And>i. 0 \<le> x i \<and> x i \<le> 1" and x0: "\<And>i. i > Suc p \<Longrightarrow> x i = 0" and x1: "sum x {..Suc p} = 1"
using that by (auto simp: oriented_simplex_def standard_simplex_def)
obtain a where "a \<in> S"
@@ -1222,7 +1199,7 @@
proof (cases "x 0 = 1")
case True
then have "sum x {Suc 0..Suc p} = 0"
- using x1 by (simp add: atMost_atLeast0 sum_head_Suc)
+ using x1 by (simp add: atMost_atLeast0 sum.atLeast_Suc_atMost)
then have [simp]: "x (Suc j) = 0" if "j\<le>p" for j
unfolding sum.atLeast_Suc_atMost_Suc_shift
using x01 that by (simp add: sum_nonneg_eq_0_iff)
@@ -1318,9 +1295,9 @@
show "chain_boundary (Suc p) (simplicial_cone p v (frag_of f))
= frag_of f - simplicial_cone (p - Suc 0) v (chain_boundary p (frag_of f))"
using \<open>p > 0\<close>
- apply (simp add: assms simplicial_cone_def chain_boundary_of atMost_atLeast0 del: sum_atMost_Suc)
- apply (subst sum_head_Suc [of 0])
- apply (simp_all add: 1 2 del: sum_atMost_Suc)
+ apply (simp add: assms simplicial_cone_def chain_boundary_of atMost_atLeast0 del: sum.atMost_Suc)
+ apply (subst sum.atLeast_Suc_atMost [of 0])
+ apply (simp_all add: 1 2 del: sum.atMost_Suc)
done
qed
@@ -1462,7 +1439,7 @@
moreover
obtain l where l: "\<And>x. x \<in> standard_simplex (Suc p) \<Longrightarrow> (\<lambda>i. (\<Sum>j\<le>Suc p. l j i * x j)) \<in> S"
and feq: "f = oriented_simplex (Suc p) l"
- using f by (fastforce simp: simplicial_simplex oriented_simplex_def simp del: sum_atMost_Suc)
+ using f by (fastforce simp: simplicial_simplex oriented_simplex_def simp del: sum.atMost_Suc)
have "(\<lambda>i. (1 - u) * ((\<Sum>j\<le>Suc p. simplicial_vertex j f i) / (real p + 2)) + u * y i) \<in> S"
if "0 \<le> u" "u \<le> 1" and y: "y \<in> f ` standard_simplex (Suc p)" for y u
proof -
@@ -1474,7 +1451,7 @@
by (simp add: divide_simps)
show "(\<lambda>j. if j \<le> Suc p then (1 - u) * inverse (real (p + 2)) + u * x j else 0) \<in> standard_simplex (Suc p)"
using x \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>
- apply (simp add: sum.distrib standard_simplex_def i2p linepath_le_1 flip: sum_distrib_left del: sum_atMost_Suc)
+ apply (simp add: sum.distrib standard_simplex_def i2p linepath_le_1 flip: sum_distrib_left del: sum.atMost_Suc)
apply (simp add: divide_simps)
done
qed
@@ -1486,7 +1463,7 @@
= (\<Sum>j\<le>Suc p. (1 - u) * l j i / (real p + 2) + u * l j i * x j)" (is "?lhs = _")
by (simp add: field_simps cong: sum.cong)
also have "\<dots> = (1 - u) * (\<Sum>j\<le>Suc p. l j i) / (real p + 2) + u * (\<Sum>j\<le>Suc p. l j i * x j)" (is "_ = ?rhs")
- by (simp add: sum_distrib_left sum.distrib sum_divide_distrib mult.assoc del: sum_atMost_Suc)
+ by (simp add: sum_distrib_left sum.distrib sum_divide_distrib mult.assoc del: sum.atMost_Suc)
finally show "?lhs = ?rhs" .
qed
ultimately show ?thesis
@@ -1589,7 +1566,7 @@
and feq: "f = oriented_simplex (Suc p) l"
using ssf by (auto simp: simplicial_simplex)
show ?thesis
- proof (clarsimp simp add: geq simp del: sum_atMost_Suc)
+ proof (clarsimp simp add: geq simp del: sum.atMost_Suc)
fix x y
assume x: "x \<in> standard_simplex (Suc p)" and y: "y \<in> standard_simplex (Suc p)"
then have x': "(\<forall>i. 0 \<le> x i \<and> x i \<le> 1) \<and> (\<forall>i>Suc p. x i = 0) \<and> (\<Sum>i\<le>Suc p. x i) = 1"
@@ -1633,7 +1610,7 @@
then have "\<bar>\<Sum>j\<le>Suc p. l i k / (p + 2) - l j k / (p + 2)\<bar> \<le> (1 + real p) * d / (p + 2)"
by (rule order_trans [OF sum_abs])
then show "\<bar>l i k - (\<Sum>j\<le>Suc p. l j k) / (2 + real p)\<bar> \<le> (1 + real p) * d / (2 + real p)"
- by (simp add: sum_subtractf sum_divide_distrib del: sum_atMost_Suc)
+ by (simp add: sum_subtractf sum_divide_distrib del: sum.atMost_Suc)
qed (use standard_simplex_def z in auto)
qed
have nonz: "\<bar>m (s - Suc 0) k - m (r - Suc 0) k\<bar> \<le> (1 + real p) * d / (2 + real p)" (is "?lhs \<le> ?rhs")
@@ -1650,7 +1627,7 @@
(if j = 0 then \<lambda>i. (\<Sum>j\<le>Suc p. l j i) / (2 + real p) else m (j -1)) k\<bar>
\<le> (1 + real p) * d / (2 + real p)" for j j'
apply (rule_tac a=j and b = "j'" in linorder_less_wlog)
- apply (force simp: zero nonz \<open>0 \<le> d\<close> simp del: sum_atMost_Suc)+
+ apply (force simp: zero nonz \<open>0 \<le> d\<close> simp del: sum.atMost_Suc)+
done
show ?thesis
apply (rule convex_sum_bound_le)
@@ -1664,8 +1641,8 @@
qed
then show "\<bar>simplex_cone p (Sigp f) (oriented_simplex p m) x k - simplex_cone p (Sigp f) (oriented_simplex p m) y k\<bar>
\<le> (1 + real p) * d / (2 + real p)"
- apply (simp add: feq Sigp_def simplicial_vertex_oriented_simplex simplex_cone del: sum_atMost_Suc)
- apply (simp add: oriented_simplex_def x y del: sum_atMost_Suc)
+ apply (simp add: feq Sigp_def simplicial_vertex_oriented_simplex simplex_cone del: sum.atMost_Suc)
+ apply (simp add: oriented_simplex_def x y del: sum.atMost_Suc)
done
qed
qed
@@ -1678,9 +1655,9 @@
qed
show ?case
using Suc
- apply (simp del: sum_atMost_Suc)
+ apply (simp del: sum.atMost_Suc)
apply (drule subsetD [OF keys_frag_extend])
- apply (simp del: sum_atMost_Suc)
+ apply (simp del: sum.atMost_Suc)
apply clarify (*OBTAIN?*)
apply (rename_tac FFF)
using *
@@ -1831,7 +1808,7 @@
by (metis diff_Suc_1 order_refl simplicial_chain_boundary simplicial_chain_of simplicial_chain_simplicial_subdivision simplicial_simplex_id)
have 2: "(\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2))
\<in> standard_simplex (Suc p)"
- by (simp add: simplicial_vertex_def standard_simplex_def del: sum_atMost_Suc)
+ by (simp add: simplicial_vertex_def standard_simplex_def del: sum.atMost_Suc)
have ss_Sp: "(\<lambda>i. (if i \<le> Suc p then 1 else 0) / (real p + 2)) \<in> standard_simplex (Suc p)"
by (simp add: standard_simplex_def divide_simps)
obtain l where feq: "f = oriented_simplex (Suc p) l"
@@ -1839,7 +1816,7 @@
then have 3: "f (\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j (restrict id (standard_simplex (Suc p))) i) / (real p + 2))
= (\<lambda>i. (\<Sum>j\<le>Suc p. simplicial_vertex j f i) / (real p + 2))"
unfolding simplicial_vertex_def oriented_simplex_def
- by (simp add: ss_Sp if_distrib [of "\<lambda>x. _ * x"] sum_divide_distrib del: sum_atMost_Suc cong: if_cong)
+ by (simp add: ss_Sp if_distrib [of "\<lambda>x. _ * x"] sum_divide_distrib del: sum.atMost_Suc cong: if_cong)
have scp: "singular_chain (Suc p)
(subtopology (powertop_real UNIV) (standard_simplex (Suc p)))
(frag_of (restrict id (standard_simplex (Suc p))))"
@@ -1859,7 +1836,7 @@
flip: singular_simplex_chain_map_id [OF simplicial_imp_singular_simplex [OF ssf]])
by (metis (no_types) scp singular_chain_boundary_alt Suc.IH [OF scps] Suc.IH [OF scpf] naturality_singular_subdivision)
show ?case
- apply (simp add: singular_subdivision_def del: sum_atMost_Suc)
+ apply (simp add: singular_subdivision_def del: sum.atMost_Suc)
apply (simp only: ssf 1 2 3 4 chain_map_simplicial_cone [of "Suc p" S _ p "Suc p"])
done
qed (auto simp: frag_extend_diff singular_subdivision_diff)
@@ -1960,7 +1937,7 @@
have "(\<lambda>i'. \<Sum>j\<le>Suc p. l j i' * (if j = i then 1 else 0)) \<in> standard_simplex s"
using subsetD [OF l] basis_in_standard_simplex that by blast
moreover have "(\<lambda>i'. \<Sum>j\<le>Suc p. l j i' * (if j = i then 1 else 0)) = l i"
- using that by (simp add: if_distrib [of "\<lambda>x. _ * x"] del: sum_atMost_Suc cong: if_cong)
+ using that by (simp add: if_distrib [of "\<lambda>x. _ * x"] del: sum.atMost_Suc cong: if_cong)
ultimately show ?thesis
by simp
qed
@@ -2026,7 +2003,7 @@
apply (rule order_refl)
apply (simp only: chain_map_of frag_extend_of)
apply (rule arg_cong2 [where f = "simplicial_cone (Suc p)"])
- apply (simp add: geq sum_distrib_left oriented_simplex_def ** del: sum_atMost_Suc flip: sum_divide_distrib)
+ apply (simp add: geq sum_distrib_left oriented_simplex_def ** del: sum.atMost_Suc flip: sum_divide_distrib)
using 2 apply (simp only: oriented_simplex_def sum.swap [where A = "{..s}"])
using naturality_simplicial_subdivision scf apply (fastforce simp add: 4 chain_map_diff)
done
@@ -2061,7 +2038,7 @@
apply (simp only: subd.simps frag_extend_of)
apply (subst chain_boundary_simplicial_cone [of "Suc p" "standard_simplex s"])
apply (meson ff scf simplicial_chain_diff simplicial_chain_simplicial_subdivision)
- apply (simp add: simplicial_cone_def del: sum_atMost_Suc simplicial_subdivision.simps)
+ apply (simp add: simplicial_cone_def del: sum.atMost_Suc simplicial_subdivision.simps)
done
qed
next
@@ -2789,7 +2766,7 @@
assumes hom: "homotopic_with (\<lambda>h. h ` T \<subseteq> V) S U f g" and c: "singular_relcycle p S T c"
shows "homologous_rel p U V (chain_map p f c) (chain_map p g c)"
proof -
- note sum_atMost_Suc [simp del]
+ note sum.atMost_Suc [simp del]
have contf: "continuous_map S U f" and contg: "continuous_map S U g"
using homotopic_with_imp_continuous_maps [OF hom] by metis+
obtain h where conth: "continuous_map (prod_topology (top_of_set {0..1::real}) S) U h"
@@ -2986,11 +2963,11 @@
assume x: "x \<in> standard_simplex q"
then have "simp q q (simplical_face (Suc q) x) 0 = 0"
unfolding oriented_simplex_def simp_def
- by (simp add: simplical_face_in_standard_simplex sum_atMost_Suc) (simp add: simplical_face_def vv_def)
+ by (simp add: simplical_face_in_standard_simplex sum.atMost_Suc) (simp add: simplical_face_def vv_def)
moreover have "(\<lambda>n. simp q q (simplical_face (Suc q) x) (Suc n)) = x"
unfolding oriented_simplex_def simp_def vv_def using x
apply (simp add: simplical_face_in_standard_simplex)
- apply (force simp: standard_simplex_def simplical_face_def if_distribR if_distrib [of "\<lambda>x. x * _"] sum_atMost_Suc cong: if_cong)
+ apply (force simp: standard_simplex_def simplical_face_def if_distribR if_distrib [of "\<lambda>x. x * _"] sum.atMost_Suc cong: if_cong)
done
ultimately show "((\<lambda>z. h (z 0, m (z \<circ> Suc))) \<circ> (simp q q \<circ> simplical_face (Suc q))) x = (f \<circ> m) x"
by (simp add: o_def h0)
@@ -3083,7 +3060,7 @@
apply (simp add: simplical_face_in_standard_simplex if_distribR)
apply (simp add: simplical_face_def if_distrib [of "\<lambda>u. u * _"] cong: if_cong)
apply (intro impI conjI)
- apply (force simp: sum_atMost_Suc intro: sum.cong)
+ apply (force simp: sum.atMost_Suc intro: sum.cong)
apply (force simp: q0_eq sum.reindex intro!: sum.cong)
done
qed
@@ -3202,7 +3179,7 @@
show ?thesis
apply (rule ext)
unfolding simplical_face_def using ij
- apply (auto simp: sum_atMost_Suc cong: if_cong)
+ apply (auto simp: sum.atMost_Suc cong: if_cong)
apply (force simp flip: ivl_disj_un(2) intro: sum.neutral)
apply (auto simp: *)
done
--- a/src/HOL/Nonstandard_Analysis/HSeries.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy Wed Apr 10 13:34:55 2019 +0100
@@ -54,7 +54,7 @@
unfolding sumhr_app by transfer (rule sum_distrib_left)
lemma sumhr_split_add: "\<And>n p. n < p \<Longrightarrow> sumhr (0, n, f) + sumhr (n, p, f) = sumhr (0, p, f)"
- unfolding sumhr_app by transfer (simp add: sum_add_nat_ivl)
+ unfolding sumhr_app by transfer (simp add: sum.atLeastLessThan_concat)
lemma sumhr_split_diff: "n < p \<Longrightarrow> sumhr (0, p, f) - sumhr (0, n, f) = sumhr (n, p, f)"
by (drule sumhr_split_add [symmetric, where f = f]) simp
--- a/src/HOL/Probability/Characteristic_Functions.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy Wed Apr 10 13:34:55 2019 +0100
@@ -177,7 +177,7 @@
unfolding of_nat_mult[symmetric]
by (simp add: complex_eq_iff ** of_nat_add[symmetric] del: of_nat_mult of_nat_fact of_nat_add)
show "?P (Suc n)"
- unfolding sum_atMost_Suc ih f_def CLBINT_I0c_power_mirror_iexp[of _ n]
+ unfolding sum.atMost_Suc ih f_def CLBINT_I0c_power_mirror_iexp[of _ n]
by (simp add: divide_simps add_eq_0_iff *) (simp add: field_simps)
qed
--- a/src/HOL/Series.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Series.thy Wed Apr 10 13:34:55 2019 +0100
@@ -305,7 +305,7 @@
unfolding lessThan_Suc_eq_insert_0
by (simp add: ac_simps sum_atLeast1_atMost_eq image_Suc_lessThan)
ultimately show ?thesis
- by (auto simp: sums_def simp del: sum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
+ by (auto simp: sums_def simp del: sum.lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
qed
lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
@@ -460,7 +460,7 @@
apply (drule summable_iff_convergent [THEN iffD1])
apply (drule convergent_Cauchy)
apply (simp only: Cauchy_iff LIMSEQ_iff)
- by (metis add.commute add_diff_cancel_right' diff_zero le_SucI sum_lessThan_Suc)
+ by (metis add.commute add_diff_cancel_right' diff_zero le_SucI sum.lessThan_Suc)
lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
--- a/src/HOL/Set_Interval.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Set_Interval.thy Wed Apr 10 13:34:55 2019 +0100
@@ -1831,19 +1831,41 @@
with the simplifier who adds the unsimplified premise \<^term>\<open>x\<in>B\<close> to
the context.\<close>
-lemmas sum_ivl_cong = sum.ivl_cong
+context comm_monoid_set
+begin
+
+lemma zero_middle:
+ assumes "1 \<le> p" "k \<le> p"
+ shows "F (\<lambda>j. if j < k then g j else if j = k then \<^bold>1 else h (j - Suc 0)) {..p}
+ = F (\<lambda>j. if j < k then g j else h j) {..p - Suc 0}" (is "?lhs = ?rhs")
+proof -
+ have [simp]: "{..p - Suc 0} \<inter> {j. j < k} = {..<k}" "{..p - Suc 0} \<inter> - {j. j < k} = {k..p - Suc 0}"
+ using assms by auto
+ have "?lhs = F g {..<k} \<^bold>* F (\<lambda>j. if j = k then \<^bold>1 else h (j - Suc 0)) {k..p}"
+ using union_disjoint [of "{..<k}" "{k..p}"] assms
+ by (simp add: ivl_disj_int_one ivl_disj_un_one)
+ also have "\<dots> = F g {..<k} \<^bold>* F (\<lambda>j. h (j - Suc 0)) {Suc k..p}"
+ by (simp add: atLeast_Suc_atMost [of k p] assms)
+ also have "\<dots> = F g {..<k} \<^bold>* F h {k .. p - Suc 0}"
+ using reindex [of Suc "{k..p - Suc 0}"] assms by simp
+ also have "\<dots> = ?rhs"
+ by (simp add: If_cases)
+ finally show ?thesis .
+qed
+
+lemma atMost_Suc [simp]:
+ "F g {..Suc n} = F g {..n} \<^bold>* g (Suc n)"
+ by (simp add: atMost_Suc ac_simps)
+
+lemma lessThan_Suc [simp]:
+ "F g {..<Suc n} = F g {..<n} \<^bold>* g n"
+ by (simp add: lessThan_Suc ac_simps)
+
+end
(* FIXME why are the following simp rules but the corresponding eqns
on intervals are not? *)
-lemma sum_atMost_Suc [simp]:
- "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f (Suc n)"
- by (simp add: atMost_Suc ac_simps)
-
-lemma sum_lessThan_Suc [simp]:
- "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n"
- by (simp add: lessThan_Suc ac_simps)
-
lemma sum_cl_ivl_Suc [simp]:
"sum f {m..Suc n} = (if Suc n < m then 0 else sum f {m..n} + f(Suc n))"
by (auto simp: ac_simps atLeastAtMostSuc_conv)
@@ -1851,11 +1873,6 @@
lemma sum_op_ivl_Suc [simp]:
"sum f {m..<Suc n} = (if n < m then 0 else sum f {m..<n} + f(n))"
by (auto simp: ac_simps atLeastLessThanSuc)
-(*
-lemma sum_cl_ivl_add_one_nat: "(n::nat) \<le> m + 1 ==>
- (\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)"
-by (auto simp:ac_simps atLeastAtMostSuc_conv)
-*)
lemma sum_head:
fixes n :: nat
@@ -1871,14 +1888,6 @@
finally show ?thesis .
qed
-lemma sum_head_Suc:
- "m \<le> n \<Longrightarrow> sum f {m..n} = f m + sum f {Suc m..n}"
- by (fact sum.atLeast_Suc_atMost)
-
-lemma sum_head_upt_Suc:
- "m < n \<Longrightarrow> sum f {m..<n} = f m + sum f {Suc m..<n}"
- by (fact sum.atLeast_Suc_lessThan)
-
lemma sum_ub_add_nat: assumes "(m::nat) \<le> n + 1"
shows "sum f {m..n + p} = sum f {m..n} + sum f {n + 1..n + p}"
proof-
@@ -1887,12 +1896,10 @@
atLeastSucAtMost_greaterThanAtMost)
qed
-lemmas sum_add_nat_ivl = sum.atLeastLessThan_concat
-
lemma sum_diff_nat_ivl:
fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> sum f {m..<p} - sum f {m..<n} = sum f {n..<p}"
- using sum_add_nat_ivl [of m n p f,symmetric]
+ using sum.atLeastLessThan_concat [of m n p f,symmetric]
by (simp add: ac_simps)
lemma sum_natinterval_difff:
@@ -1907,7 +1914,7 @@
then have "k > 0"
by auto
then show ?thesis
- by (induct n) (simp_all add: sum_add_nat_ivl add.commute atLeast0LessThan[symmetric])
+ by (induct n) (simp_all add: sum.atLeastLessThan_concat add.commute atLeast0LessThan[symmetric])
qed auto
lemma sum_triangle_reindex:
@@ -2020,14 +2027,14 @@
next
case (Suc n) note IH = this
have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
- by (rule sum_atMost_Suc)
+ by (rule sum.atMost_Suc)
also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
by (rule IH)
also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
by (rule add.assoc)
also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
- by (rule sum_atMost_Suc [symmetric])
+ by (rule sum.atMost_Suc [symmetric])
finally show ?case .
qed
--- a/src/HOL/Transcendental.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/Transcendental.thy Wed Apr 10 13:34:55 2019 +0100
@@ -638,13 +638,13 @@
(\<Sum>i<n. \<Sum>j<n - i. h * ((z + h) ^ j * z ^ (n - Suc j)))"
apply (rule sum.cong [OF refl])
apply (clarsimp simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
- simp del: sum_lessThan_Suc power_Suc)
+ simp del: sum.lessThan_Suc power_Suc)
done
have "h * ?lhs = h * ?rhs"
apply (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
using Suc
apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
- del: power_Suc sum_lessThan_Suc of_nat_Suc)
+ del: power_Suc sum.lessThan_Suc of_nat_Suc)
apply (subst lemma_realpow_rev_sumr)
apply (subst sumr_diff_mult_const2)
apply (simp add: lemma_termdiff1 sum_distrib_left *)
@@ -6227,7 +6227,7 @@
by blast
show ?succase
using Suc.IH [of b k'] bk'
- by (simp add: eq card_insert_if del: sum_atMost_Suc)
+ by (simp add: eq card_insert_if del: sum.atMost_Suc)
qed
qed
@@ -6297,7 +6297,7 @@
fixes z :: "'a::idom"
assumes "1 \<le> n"
shows "z^n = a \<longleftrightarrow> (\<Sum>i\<le>n. (if i = 0 then -a else if i=n then 1 else 0) * z^i) = 0"
- using assms by (cases n) (simp_all add: sum_head_Suc atLeast0AtMost [symmetric])
+ using assms by (cases n) (simp_all add: sum.atLeast_Suc_atMost atLeast0AtMost [symmetric])
lemma
assumes "SORT_CONSTRAINT('a::{idom,real_normed_div_algebra})"
--- a/src/HOL/ex/Sum_of_Powers.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/ex/Sum_of_Powers.thy Wed Apr 10 13:34:55 2019 +0100
@@ -151,7 +151,7 @@
lemma sum_unroll:
"(\<Sum>k\<le>n::nat. f k) = (if n = 0 then f 0 else f n + (\<Sum>k\<le>n - 1. f k))"
-by auto (metis One_nat_def Suc_pred add.commute sum_atMost_Suc)
+by auto (metis One_nat_def Suc_pred add.commute sum.atMost_Suc)
lemma bernoulli_unroll:
"n > 0 \<Longrightarrow> bernoulli n = - 1 / (real n + 1) * (\<Sum>k\<le>n - 1. real (n + 1 choose k) * bernoulli k)"
--- a/src/HOL/ex/ThreeDivides.thy Tue Apr 09 21:05:48 2019 +0100
+++ b/src/HOL/ex/ThreeDivides.thy Wed Apr 10 13:34:55 2019 +0100
@@ -203,7 +203,7 @@
(simp add: atLeast0LessThan)
also have
"\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"
- by (simp add: atLeast0LessThan[symmetric] sum_head_upt_Suc cdef)
+ by (simp add: atLeast0LessThan[symmetric] sum.atLeast_Suc_lessThan cdef)
also note \<open>Suc nd = nlen m\<close>
finally
show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)" .