author  paulson <lp15@cam.ac.uk> 
Mon, 03 Oct 2016 13:01:01 +0100  
changeset 64006  0de4736dad8b 
child 64122  74fde524799e 
permissions  rwrr 
64006
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1 
section \<open>Extending Continous Maps, etc..\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

2 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

3 
text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

4 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

5 
theory "FurtherTopology" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

6 
imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

7 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

8 
begin 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

9 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

10 
subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

11 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

12 
lemma spheremap_lemma1: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

13 
fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

14 
assumes "subspace S" "subspace T" and dimST: "dim S < dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

15 
and "S \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

16 
and diff_f: "f differentiable_on sphere 0 1 \<inter> S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

17 
shows "f ` (sphere 0 1 \<inter> S) \<noteq> sphere 0 1 \<inter> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

18 
proof 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

19 
assume fim: "f ` (sphere 0 1 \<inter> S) = sphere 0 1 \<inter> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

20 
have inS: "\<And>x. \<lbrakk>x \<in> S; x \<noteq> 0\<rbrakk> \<Longrightarrow> (x /\<^sub>R norm x) \<in> S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

21 
using subspace_mul \<open>subspace S\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

22 
have subS01: "(\<lambda>x. x /\<^sub>R norm x) ` (S  {0}) \<subseteq> sphere 0 1 \<inter> S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

23 
using \<open>subspace S\<close> subspace_mul by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

24 
then have diff_f': "f differentiable_on (\<lambda>x. x /\<^sub>R norm x) ` (S  {0})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

25 
by (rule differentiable_on_subset [OF diff_f]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

26 
define g where "g \<equiv> \<lambda>x. norm x *\<^sub>R f(inverse(norm x) *\<^sub>R x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

27 
have gdiff: "g differentiable_on S  {0}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

28 
unfolding g_def 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

29 
by (rule diff_f' derivative_intros differentiable_on_compose [where f=f]  force)+ 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

30 
have geq: "g ` (S  {0}) = T  {0}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

31 
proof 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

32 
have "g ` (S  {0}) \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

33 
apply (auto simp: g_def subspace_mul [OF \<open>subspace T\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

34 
apply (metis (mono_tags, lifting) DiffI subS01 subspace_mul [OF \<open>subspace T\<close>] fim image_subset_iff inf_le2 singletonD) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

35 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

36 
moreover have "g ` (S  {0}) \<subseteq> UNIV  {0}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

37 
proof (clarsimp simp: g_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

38 
fix y 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

39 
assume "y \<in> S" and f0: "f (y /\<^sub>R norm y) = 0" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

40 
then have "y \<noteq> 0 \<Longrightarrow> y /\<^sub>R norm y \<in> sphere 0 1 \<inter> S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

41 
by (auto simp: subspace_mul [OF \<open>subspace S\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

42 
then show "y = 0" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

43 
by (metis fim f0 Int_iff image_iff mem_sphere_0 norm_eq_zero zero_neq_one) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

44 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

45 
ultimately show "g ` (S  {0}) \<subseteq> T  {0}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

46 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

47 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

48 
have *: "sphere 0 1 \<inter> T \<subseteq> f ` (sphere 0 1 \<inter> S)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

49 
using fim by (simp add: image_subset_iff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

50 
have "x \<in> (\<lambda>x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S  {0})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

51 
if "x \<in> T" "x \<noteq> 0" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

52 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

53 
have "x /\<^sub>R norm x \<in> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

54 
using \<open>subspace T\<close> subspace_mul that by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

55 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

56 
using * [THEN subsetD, of "x /\<^sub>R norm x"] that apply clarsimp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

57 
apply (rule_tac x="norm x *\<^sub>R xa" in image_eqI, simp) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

58 
apply (metis norm_eq_zero right_inverse scaleR_one scaleR_scaleR) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

59 
using \<open>subspace S\<close> subspace_mul apply force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

60 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

61 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

62 
then have "T  {0} \<subseteq> (\<lambda>x. norm x *\<^sub>R f (x /\<^sub>R norm x)) ` (S  {0})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

63 
by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

64 
then show "T  {0} \<subseteq> g ` (S  {0})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

65 
by (simp add: g_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

66 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

67 
define T' where "T' \<equiv> {y. \<forall>x \<in> T. orthogonal x y}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

68 
have "subspace T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

69 
by (simp add: subspace_orthogonal_to_vectors T'_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

70 
have dim_eq: "dim T' + dim T = DIM('a)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

71 
using dim_subspace_orthogonal_to_vectors [of T UNIV] \<open>subspace T\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

72 
by (simp add: dim_UNIV T'_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

73 
have "\<exists>v1 v2. v1 \<in> span T \<and> (\<forall>w \<in> span T. orthogonal v2 w) \<and> x = v1 + v2" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

74 
by (force intro: orthogonal_subspace_decomp_exists [of T x]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

75 
then obtain p1 p2 where p1span: "p1 x \<in> span T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

76 
and "\<And>w. w \<in> span T \<Longrightarrow> orthogonal (p2 x) w" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

77 
and eq: "p1 x + p2 x = x" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

78 
by metis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

79 
then have p1: "\<And>z. p1 z \<in> T" and ortho: "\<And>w. w \<in> T \<Longrightarrow> orthogonal (p2 x) w" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

80 
using span_eq \<open>subspace T\<close> by blast+ 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

81 
then have p2: "\<And>z. p2 z \<in> T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

82 
by (simp add: T'_def orthogonal_commute) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

83 
have p12_eq: "\<And>x y. \<lbrakk>x \<in> T; y \<in> T'\<rbrakk> \<Longrightarrow> p1(x + y) = x \<and> p2(x + y) = y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

84 
proof (rule orthogonal_subspace_decomp_unique [OF eq p1span, where T=T']) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

85 
show "\<And>x y. \<lbrakk>x \<in> T; y \<in> T'\<rbrakk> \<Longrightarrow> p2 (x + y) \<in> span T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

86 
using span_eq p2 \<open>subspace T'\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

87 
show "\<And>a b. \<lbrakk>a \<in> T; b \<in> T'\<rbrakk> \<Longrightarrow> orthogonal a b" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

88 
using T'_def by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

89 
qed (auto simp: span_superset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

90 
then have "\<And>c x. p1 (c *\<^sub>R x) = c *\<^sub>R p1 x \<and> p2 (c *\<^sub>R x) = c *\<^sub>R p2 x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

91 
by (metis eq \<open>subspace T\<close> \<open>subspace T'\<close> p1 p2 scaleR_add_right subspace_mul) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

92 
moreover have lin_add: "\<And>x y. p1 (x + y) = p1 x + p1 y \<and> p2 (x + y) = p2 x + p2 y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

93 
proof (rule orthogonal_subspace_decomp_unique [OF _ p1span, where T=T']) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

94 
show "\<And>x y. p1 (x + y) + p2 (x + y) = p1 x + p1 y + (p2 x + p2 y)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

95 
by (simp add: add.assoc add.left_commute eq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

96 
show "\<And>a b. \<lbrakk>a \<in> T; b \<in> T'\<rbrakk> \<Longrightarrow> orthogonal a b" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

97 
using T'_def by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

98 
qed (auto simp: p1span p2 span_superset subspace_add) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

99 
ultimately have "linear p1" "linear p2" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

100 
by unfold_locales auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

101 
have "(\<lambda>z. g (p1 z)) differentiable_on {x + y x y. x \<in> S  {0} \<and> y \<in> T'}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

102 
apply (rule differentiable_on_compose [where f=g]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

103 
apply (rule linear_imp_differentiable_on [OF \<open>linear p1\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

104 
apply (rule differentiable_on_subset [OF gdiff]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

105 
using p12_eq \<open>S \<subseteq> T\<close> apply auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

106 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

107 
then have diff: "(\<lambda>x. g (p1 x) + p2 x) differentiable_on {x + y x y. x \<in> S  {0} \<and> y \<in> T'}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

108 
by (intro derivative_intros linear_imp_differentiable_on [OF \<open>linear p2\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

109 
have "dim {x + y x y. x \<in> S  {0} \<and> y \<in> T'} \<le> dim {x + y x y. x \<in> S \<and> y \<in> T'}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

110 
by (blast intro: dim_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

111 
also have "... = dim S + dim T'  dim (S \<inter> T')" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

112 
using dim_sums_Int [OF \<open>subspace S\<close> \<open>subspace T'\<close>] 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

113 
by (simp add: algebra_simps) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

114 
also have "... < DIM('a)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

115 
using dimST dim_eq by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

116 
finally have neg: "negligible {x + y x y. x \<in> S  {0} \<and> y \<in> T'}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

117 
by (rule negligible_lowdim) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

118 
have "negligible ((\<lambda>x. g (p1 x) + p2 x) ` {x + y x y. x \<in> S  {0} \<and> y \<in> T'})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

119 
by (rule negligible_differentiable_image_negligible [OF order_refl neg diff]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

120 
then have "negligible {x + y x y. x \<in> g ` (S  {0}) \<and> y \<in> T'}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

121 
proof (rule negligible_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

122 
have "\<lbrakk>t' \<in> T'; s \<in> S; s \<noteq> 0\<rbrakk> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

123 
\<Longrightarrow> g s + t' \<in> (\<lambda>x. g (p1 x) + p2 x) ` 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

124 
{x + t' x t'. x \<in> S \<and> x \<noteq> 0 \<and> t' \<in> T'}" for t' s 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

125 
apply (rule_tac x="s + t'" in image_eqI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

126 
using \<open>S \<subseteq> T\<close> p12_eq by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

127 
then show "{x + y x y. x \<in> g ` (S  {0}) \<and> y \<in> T'} 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

128 
\<subseteq> (\<lambda>x. g (p1 x) + p2 x) ` {x + y x y. x \<in> S  {0} \<and> y \<in> T'}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

129 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

130 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

131 
moreover have " T' \<subseteq> {x + y x y. x \<in> g ` (S  {0}) \<and> y \<in> T'}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

132 
proof clarsimp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

133 
fix z assume "z \<notin> T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

134 
show "\<exists>x y. z = x + y \<and> x \<in> g ` (S  {0}) \<and> y \<in> T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

135 
apply (rule_tac x="p1 z" in exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

136 
apply (rule_tac x="p2 z" in exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

137 
apply (simp add: p1 eq p2 geq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

138 
by (metis \<open>z \<notin> T'\<close> add.left_neutral eq p2) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

139 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

140 
ultimately have "negligible (T')" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

141 
using negligible_subset by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

142 
moreover have "negligible T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

143 
using negligible_lowdim 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

144 
by (metis add.commute assms(3) diff_add_inverse2 diff_self_eq_0 dim_eq le_add1 le_antisym linordered_semidom_class.add_diff_inverse not_less0) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

145 
ultimately have "negligible (T' \<union> T')" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

146 
by (metis negligible_Un_eq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

147 
then show False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

148 
using negligible_Un_eq non_negligible_UNIV by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

149 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

150 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

151 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

152 
lemma spheremap_lemma2: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

153 
fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

154 
assumes ST: "subspace S" "subspace T" "dim S < dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

155 
and "S \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

156 
and contf: "continuous_on (sphere 0 1 \<inter> S) f" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

157 
and fim: "f ` (sphere 0 1 \<inter> S) \<subseteq> sphere 0 1 \<inter> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

158 
shows "\<exists>c. homotopic_with (\<lambda>x. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) f (\<lambda>x. c)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

159 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

160 
have [simp]: "\<And>x. \<lbrakk>norm x = 1; x \<in> S\<rbrakk> \<Longrightarrow> norm (f x) = 1" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

161 
using fim by (simp add: image_subset_iff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

162 
have "compact (sphere 0 1 \<inter> S)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

163 
by (simp add: \<open>subspace S\<close> closed_subspace compact_Int_closed) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

164 
then obtain g where pfg: "polynomial_function g" and gim: "g ` (sphere 0 1 \<inter> S) \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

165 
and g12: "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> norm(f x  g x) < 1/2" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

166 
apply (rule Stone_Weierstrass_polynomial_function_subspace [OF _ contf _ \<open>subspace T\<close>, of "1/2"]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

167 
using fim apply auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

168 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

169 
have gnz: "g x \<noteq> 0" if "x \<in> sphere 0 1 \<inter> S" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

170 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

171 
have "norm (f x) = 1" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

172 
using fim that by (simp add: image_subset_iff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

173 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

174 
using g12 [OF that] by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

175 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

176 
have diffg: "g differentiable_on sphere 0 1 \<inter> S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

177 
by (metis pfg differentiable_on_polynomial_function) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

178 
define h where "h \<equiv> \<lambda>x. inverse(norm(g x)) *\<^sub>R g x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

179 
have h: "x \<in> sphere 0 1 \<inter> S \<Longrightarrow> h x \<in> sphere 0 1 \<inter> T" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

180 
unfolding h_def 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

181 
using gnz [of x] 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

182 
by (auto simp: subspace_mul [OF \<open>subspace T\<close>] subsetD [OF gim]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

183 
have diffh: "h differentiable_on sphere 0 1 \<inter> S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

184 
unfolding h_def 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

185 
apply (intro derivative_intros diffg differentiable_on_compose [OF diffg]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

186 
using gnz apply auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

187 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

188 
have homfg: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (T  {0}) f g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

189 
proof (rule homotopic_with_linear [OF contf]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

190 
show "continuous_on (sphere 0 1 \<inter> S) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

191 
using pfg by (simp add: differentiable_imp_continuous_on diffg) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

192 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

193 
have non0fg: "0 \<notin> closed_segment (f x) (g x)" if "norm x = 1" "x \<in> S" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

194 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

195 
have "f x \<in> sphere 0 1" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

196 
using fim that by (simp add: image_subset_iff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

197 
moreover have "norm(f x  g x) < 1/2" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

198 
apply (rule g12) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

199 
using that by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

200 
ultimately show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

201 
by (auto simp: norm_minus_commute dest: segment_bound) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

202 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

203 
show "\<And>x. x \<in> sphere 0 1 \<inter> S \<Longrightarrow> closed_segment (f x) (g x) \<subseteq> T  {0}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

204 
apply (simp add: subset_Diff_insert non0fg) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

205 
apply (simp add: segment_convex_hull) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

206 
apply (rule hull_minimal) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

207 
using fim image_eqI gim apply force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

208 
apply (rule subspace_imp_convex [OF \<open>subspace T\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

209 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

210 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

211 
obtain d where d: "d \<in> (sphere 0 1 \<inter> T)  h ` (sphere 0 1 \<inter> S)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

212 
using h spheremap_lemma1 [OF ST \<open>S \<subseteq> T\<close> diffh] by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

213 
then have non0hd: "0 \<notin> closed_segment (h x) ( d)" if "norm x = 1" "x \<in> S" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

214 
using midpoint_between [of 0 "h x" "d"] that h [of x] 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

215 
by (auto simp: between_mem_segment midpoint_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

216 
have conth: "continuous_on (sphere 0 1 \<inter> S) h" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

217 
using differentiable_imp_continuous_on diffh by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

218 
have hom_hd: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (T  {0}) h (\<lambda>x. d)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

219 
apply (rule homotopic_with_linear [OF conth continuous_on_const]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

220 
apply (simp add: subset_Diff_insert non0hd) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

221 
apply (simp add: segment_convex_hull) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

222 
apply (rule hull_minimal) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

223 
using h d apply (force simp: subspace_neg [OF \<open>subspace T\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

224 
apply (rule subspace_imp_convex [OF \<open>subspace T\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

225 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

226 
have conT0: "continuous_on (T  {0}) (\<lambda>y. inverse(norm y) *\<^sub>R y)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

227 
by (intro continuous_intros) auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

228 
have sub0T: "(\<lambda>y. y /\<^sub>R norm y) ` (T  {0}) \<subseteq> sphere 0 1 \<inter> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

229 
by (fastforce simp: assms(2) subspace_mul) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

230 
obtain c where homhc: "homotopic_with (\<lambda>z. True) (sphere 0 1 \<inter> S) (sphere 0 1 \<inter> T) h (\<lambda>x. c)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

231 
apply (rule_tac c="d" in that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

232 
apply (rule homotopic_with_eq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

233 
apply (rule homotopic_compose_continuous_left [OF hom_hd conT0 sub0T]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

234 
using d apply (auto simp: h_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

235 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

236 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

237 
apply (rule_tac x=c in exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

238 
apply (rule homotopic_with_trans [OF _ homhc]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

239 
apply (rule homotopic_with_eq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

240 
apply (rule homotopic_compose_continuous_left [OF homfg conT0 sub0T]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

241 
apply (auto simp: h_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

242 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

243 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

244 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

245 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

246 
lemma spheremap_lemma3: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

247 
assumes "bounded S" "convex S" "subspace U" and affSU: "aff_dim S \<le> dim U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

248 
obtains T where "subspace T" "T \<subseteq> U" "S \<noteq> {} \<Longrightarrow> aff_dim T = aff_dim S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

249 
"(rel_frontier S) homeomorphic (sphere 0 1 \<inter> T)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

250 
proof (cases "S = {}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

251 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

252 
with \<open>subspace U\<close> subspace_0 show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

253 
by (rule_tac T = "{0}" in that) auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

254 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

255 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

256 
then obtain a where "a \<in> S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

257 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

258 
then have affS: "aff_dim S = int (dim ((\<lambda>x. a+x) ` S))" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

259 
by (metis hull_inc aff_dim_eq_dim) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

260 
with affSU have "dim ((\<lambda>x. a+x) ` S) \<le> dim U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

261 
by linarith 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

262 
with choose_subspace_of_subspace 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

263 
obtain T where "subspace T" "T \<subseteq> span U" and dimT: "dim T = dim ((\<lambda>x. a+x) ` S)" . 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

264 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

265 
proof (rule that [OF \<open>subspace T\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

266 
show "T \<subseteq> U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

267 
using span_eq \<open>subspace U\<close> \<open>T \<subseteq> span U\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

268 
show "aff_dim T = aff_dim S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

269 
using dimT \<open>subspace T\<close> affS aff_dim_subspace by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

270 
show "rel_frontier S homeomorphic sphere 0 1 \<inter> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

271 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

272 
have "aff_dim (ball 0 1 \<inter> T) = aff_dim (T)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

273 
by (metis IntI interior_ball \<open>subspace T\<close> aff_dim_convex_Int_nonempty_interior centre_in_ball empty_iff inf_commute subspace_0 subspace_imp_convex zero_less_one) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

274 
then have affS_eq: "aff_dim S = aff_dim (ball 0 1 \<inter> T)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

275 
using \<open>aff_dim T = aff_dim S\<close> by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

276 
have "rel_frontier S homeomorphic rel_frontier(ball 0 1 \<inter> T)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

277 
apply (rule homeomorphic_rel_frontiers_convex_bounded_sets [OF \<open>convex S\<close> \<open>bounded S\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

278 
apply (simp add: \<open>subspace T\<close> convex_Int subspace_imp_convex) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

279 
apply (simp add: bounded_Int) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

280 
apply (rule affS_eq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

281 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

282 
also have "... = frontier (ball 0 1) \<inter> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

283 
apply (rule convex_affine_rel_frontier_Int [OF convex_ball]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

284 
apply (simp add: \<open>subspace T\<close> subspace_imp_affine) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

285 
using \<open>subspace T\<close> subspace_0 by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

286 
also have "... = sphere 0 1 \<inter> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

287 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

288 
finally show ?thesis . 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

289 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

290 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

291 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

292 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

293 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

294 
proposition inessential_spheremap_lowdim_gen: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

295 
fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

296 
assumes "convex S" "bounded S" "convex T" "bounded T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

297 
and affST: "aff_dim S < aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

298 
and contf: "continuous_on (rel_frontier S) f" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

299 
and fim: "f ` (rel_frontier S) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

300 
obtains c where "homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

301 
proof (cases "S = {}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

302 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

303 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

304 
by (simp add: that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

305 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

306 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

307 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

308 
proof (cases "T = {}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

309 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

310 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

311 
using fim that by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

312 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

313 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

314 
obtain T':: "'a set" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

315 
where "subspace T'" and affT': "aff_dim T' = aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

316 
and homT: "rel_frontier T homeomorphic sphere 0 1 \<inter> T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

317 
apply (rule spheremap_lemma3 [OF \<open>bounded T\<close> \<open>convex T\<close> subspace_UNIV, where 'b='a]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

318 
apply (simp add: dim_UNIV aff_dim_le_DIM) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

319 
using \<open>T \<noteq> {}\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

320 
with homeomorphic_imp_homotopy_eqv 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

321 
have relT: "sphere 0 1 \<inter> T' homotopy_eqv rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

322 
using homotopy_eqv_sym by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

323 
have "aff_dim S \<le> int (dim T')" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

324 
using affT' \<open>subspace T'\<close> affST aff_dim_subspace by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

325 
with spheremap_lemma3 [OF \<open>bounded S\<close> \<open>convex S\<close> \<open>subspace T'\<close>] \<open>S \<noteq> {}\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

326 
obtain S':: "'a set" where "subspace S'" "S' \<subseteq> T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

327 
and affS': "aff_dim S' = aff_dim S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

328 
and homT: "rel_frontier S homeomorphic sphere 0 1 \<inter> S'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

329 
by metis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

330 
with homeomorphic_imp_homotopy_eqv 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

331 
have relS: "sphere 0 1 \<inter> S' homotopy_eqv rel_frontier S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

332 
using homotopy_eqv_sym by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

333 
have dimST': "dim S' < dim T'" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

334 
by (metis \<open>S' \<subseteq> T'\<close> \<open>subspace S'\<close> \<open>subspace T'\<close> affS' affST affT' less_irrefl not_le subspace_dim_equal) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

335 
have "\<exists>c. homotopic_with (\<lambda>z. True) (rel_frontier S) (rel_frontier T) f (\<lambda>x. c)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

336 
apply (rule homotopy_eqv_homotopic_triviality_null_imp [OF relT contf fim]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

337 
apply (rule homotopy_eqv_cohomotopic_triviality_null[OF relS, THEN iffD1, rule_format]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

338 
apply (metis dimST' \<open>subspace S'\<close> \<open>subspace T'\<close> \<open>S' \<subseteq> T'\<close> spheremap_lemma2, blast) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

339 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

340 
with that show ?thesis by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

341 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

342 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

343 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

344 
lemma inessential_spheremap_lowdim: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

345 
fixes f :: "'M::euclidean_space \<Rightarrow> 'a::euclidean_space" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

346 
assumes 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

347 
"DIM('M) < DIM('a)" and f: "continuous_on (sphere a r) f" "f ` (sphere a r) \<subseteq> (sphere b s)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

348 
obtains c where "homotopic_with (\<lambda>z. True) (sphere a r) (sphere b s) f (\<lambda>x. c)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

349 
proof (cases "s \<le> 0") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

350 
case True then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

351 
by (meson nullhomotopic_into_contractible f contractible_sphere that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

352 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

353 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

354 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

355 
proof (cases "r \<le> 0") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

356 
case True then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

357 
by (meson f nullhomotopic_from_contractible contractible_sphere that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

358 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

359 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

360 
with \<open>~ s \<le> 0\<close> have "r > 0" "s > 0" by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

361 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

362 
apply (rule inessential_spheremap_lowdim_gen [of "cball a r" "cball b s" f]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

363 
using \<open>0 < r\<close> \<open>0 < s\<close> assms(1) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

364 
apply (simp_all add: f aff_dim_cball) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

365 
using that by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

366 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

367 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

368 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

369 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

370 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

371 
subsection\<open> Some technical lemmas about extending maps from cell complexes.\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

372 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

373 
lemma extending_maps_Union_aux: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

374 
assumes fin: "finite \<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

375 
and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

376 
and "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>; S \<noteq> T\<rbrakk> \<Longrightarrow> S \<inter> T \<subseteq> K" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

377 
and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

378 
shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

379 
using assms 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

380 
proof (induction \<F>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

381 
case empty show ?case by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

382 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

383 
case (insert S \<F>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

384 
then obtain f where contf: "continuous_on (S) f" and fim: "f ` S \<subseteq> T" and feq: "\<forall>x \<in> S \<inter> K. f x = h x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

385 
by (meson insertI1) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

386 
obtain g where contg: "continuous_on (\<Union>\<F>) g" and gim: "g ` \<Union>\<F> \<subseteq> T" and geq: "\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

387 
using insert by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

388 
have fg: "f x = g x" if "x \<in> T" "T \<in> \<F>" "x \<in> S" for x T 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

389 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

390 
have "T \<inter> S \<subseteq> K \<or> S = T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

391 
using that by (metis (no_types) insert.prems(2) insertCI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

392 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

393 
using UnionI feq geq \<open>S \<notin> \<F>\<close> subsetD that by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

394 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

395 
show ?case 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

396 
apply (rule_tac x="\<lambda>x. if x \<in> S then f x else g x" in exI, simp) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

397 
apply (intro conjI continuous_on_cases) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

398 
apply (simp_all add: insert closed_Union contf contg) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

399 
using fim gim feq geq 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

400 
apply (force simp: insert closed_Union contf contg inf_commute intro: fg)+ 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

401 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

402 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

403 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

404 
lemma extending_maps_Union: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

405 
assumes fin: "finite \<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

406 
and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>g. continuous_on S g \<and> g ` S \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

407 
and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

408 
and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; ~ X \<subseteq> Y; ~ Y \<subseteq> X\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

409 
shows "\<exists>g. continuous_on (\<Union>\<F>) g \<and> g ` (\<Union>\<F>) \<subseteq> T \<and> (\<forall>x \<in> \<Union>\<F> \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

410 
apply (simp add: Union_maximal_sets [OF fin, symmetric]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

411 
apply (rule extending_maps_Union_aux) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

412 
apply (simp_all add: Union_maximal_sets [OF fin] assms) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

413 
by (metis K psubsetI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

414 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

415 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

416 
lemma extend_map_lemma: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

417 
assumes "finite \<F>" "\<G> \<subseteq> \<F>" "convex T" "bounded T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

418 
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

419 
and aff: "\<And>X. X \<in> \<F>  \<G> \<Longrightarrow> aff_dim X < aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

420 
and face: "\<And>S T. \<lbrakk>S \<in> \<F>; T \<in> \<F>\<rbrakk> \<Longrightarrow> (S \<inter> T) face_of S \<and> (S \<inter> T) face_of T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

421 
and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

422 
obtains g where "continuous_on (\<Union>\<F>) g" "g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

423 
proof (cases "\<F>  \<G> = {}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

424 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

425 
then have "\<Union>\<F> \<subseteq> \<Union>\<G>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

426 
by (simp add: Union_mono) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

427 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

428 
apply (rule_tac g=f in that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

429 
using contf continuous_on_subset apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

430 
using fim apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

431 
by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

432 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

433 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

434 
then have "0 \<le> aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

435 
by (metis aff aff_dim_empty aff_dim_geq aff_dim_negative_iff all_not_in_conv not_less) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

436 
then obtain i::nat where i: "int i = aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

437 
by (metis nonneg_eq_int) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

438 
have Union_empty_eq: "\<Union>{D. D = {} \<and> P D} = {}" for P :: "'a set \<Rightarrow> bool" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

439 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

440 
have extendf: "\<exists>g. continuous_on (\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i})) g \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

441 
g ` (\<Union> (\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i})) \<subseteq> rel_frontier T \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

442 
(\<forall>x \<in> \<Union>\<G>. g x = f x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

443 
if "i \<le> aff_dim T" for i::nat 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

444 
using that 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

445 
proof (induction i) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

446 
case 0 then show ?case 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

447 
apply (simp add: Union_empty_eq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

448 
apply (rule_tac x=f in exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

449 
apply (intro conjI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

450 
using contf continuous_on_subset apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

451 
using fim apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

452 
by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

453 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

454 
case (Suc p) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

455 
with \<open>bounded T\<close> have "rel_frontier T \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

456 
by (auto simp: rel_frontier_eq_empty affine_bounded_eq_lowdim [of T]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

457 
then obtain t where t: "t \<in> rel_frontier T" by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

458 
have ple: "int p \<le> aff_dim T" using Suc.prems by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

459 
obtain h where conth: "continuous_on (\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})) h" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

460 
and him: "h ` (\<Union> (\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

461 
\<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

462 
and heq: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

463 
using Suc.IH [OF ple] by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

464 
let ?Faces = "{D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D \<le> p}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

465 
have extendh: "\<exists>g. continuous_on D g \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

466 
g ` D \<subseteq> rel_frontier T \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

467 
(\<forall>x \<in> D \<inter> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p}). g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

468 
if D: "D \<in> \<G> \<union> ?Faces" for D 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

469 
proof (cases "D \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p})") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

470 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

471 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

472 
apply (rule_tac x=h in exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

473 
apply (intro conjI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

474 
apply (blast intro: continuous_on_subset [OF conth]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

475 
using him apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

476 
by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

477 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

478 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

479 
note notDsub = False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

480 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

481 
proof (cases "\<exists>a. D = {a}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

482 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

483 
then obtain a where "D = {a}" by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

484 
with notDsub t show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

485 
by (rule_tac x="\<lambda>x. t" in exI) simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

486 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

487 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

488 
have "D \<noteq> {}" using notDsub by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

489 
have Dnotin: "D \<notin> \<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

490 
using notDsub by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

491 
then have "D \<notin> \<G>" by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

492 
have "D \<in> ?Faces  {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < p}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

493 
using Dnotin that by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

494 
then obtain C where "C \<in> \<F>" "D face_of C" and affD: "aff_dim D = int p" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

495 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

496 
then have "bounded D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

497 
using face_of_polytope_polytope poly polytope_imp_bounded by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

498 
then have [simp]: "\<not> affine D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

499 
using affine_bounded_eq_trivial False \<open>D \<noteq> {}\<close> \<open>bounded D\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

500 
have "{F. F facet_of D} \<subseteq> {E. E face_of C \<and> aff_dim E < int p}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

501 
apply clarify 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

502 
apply (metis \<open>D face_of C\<close> affD eq_iff face_of_trans facet_of_def zle_diff1_eq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

503 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

504 
moreover have "polyhedron D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

505 
using \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face_of_polytope_polytope poly polytope_imp_polyhedron by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

506 
ultimately have relf_sub: "rel_frontier D \<subseteq> \<Union> {E. E face_of C \<and> aff_dim E < p}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

507 
by (simp add: rel_frontier_of_polyhedron Union_mono) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

508 
then have him_relf: "h ` rel_frontier D \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

509 
using \<open>C \<in> \<F>\<close> him by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

510 
have "convex D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

511 
by (simp add: \<open>polyhedron D\<close> polyhedron_imp_convex) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

512 
have affD_lessT: "aff_dim D < aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

513 
using Suc.prems affD by linarith 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

514 
have contDh: "continuous_on (rel_frontier D) h" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

515 
using \<open>C \<in> \<F>\<close> relf_sub by (blast intro: continuous_on_subset [OF conth]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

516 
then have *: "(\<exists>c. homotopic_with (\<lambda>x. True) (rel_frontier D) (rel_frontier T) h (\<lambda>x. c)) = 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

517 
(\<exists>g. continuous_on UNIV g \<and> range g \<subseteq> rel_frontier T \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

518 
(\<forall>x\<in>rel_frontier D. g x = h x))" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

519 
apply (rule nullhomotopic_into_rel_frontier_extension [OF closed_rel_frontier]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

520 
apply (simp_all add: assms rel_frontier_eq_empty him_relf) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

521 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

522 
have "(\<exists>c. homotopic_with (\<lambda>x. True) (rel_frontier D) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

523 
(rel_frontier T) h (\<lambda>x. c))" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

524 
by (metis inessential_spheremap_lowdim_gen 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

525 
[OF \<open>convex D\<close> \<open>bounded D\<close> \<open>convex T\<close> \<open>bounded T\<close> affD_lessT contDh him_relf]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

526 
then obtain g where contg: "continuous_on UNIV g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

527 
and gim: "range g \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

528 
and gh: "\<And>x. x \<in> rel_frontier D \<Longrightarrow> g x = h x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

529 
by (metis *) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

530 
have "D \<inter> E \<subseteq> rel_frontier D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

531 
if "E \<in> \<G> \<union> {D. Bex \<F> (op face_of D) \<and> aff_dim D < int p}" for E 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

532 
proof (rule face_of_subset_rel_frontier) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

533 
show "D \<inter> E face_of D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

534 
using that \<open>C \<in> \<F>\<close> \<open>D face_of C\<close> face 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

535 
apply auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

536 
apply (meson face_of_Int_subface \<open>\<G> \<subseteq> \<F>\<close> face_of_refl_eq poly polytope_imp_convex subsetD) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

537 
using face_of_Int_subface apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

538 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

539 
show "D \<inter> E \<noteq> D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

540 
using that notDsub by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

541 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

542 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

543 
apply (rule_tac x=g in exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

544 
apply (intro conjI ballI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

545 
using continuous_on_subset contg apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

546 
using gim apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

547 
using gh by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

548 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

549 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

550 
have intle: "i < 1 + int j \<longleftrightarrow> i \<le> int j" for i j 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

551 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

552 
have "finite \<G>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

553 
using \<open>finite \<F>\<close> \<open>\<G> \<subseteq> \<F>\<close> rev_finite_subset by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

554 
then have fin: "finite (\<G> \<union> ?Faces)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

555 
apply simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

556 
apply (rule_tac B = "\<Union>{{D. D face_of C} C. C \<in> \<F>}" in finite_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

557 
by (auto simp: \<open>finite \<F>\<close> finite_polytope_faces poly) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

558 
have clo: "closed S" if "S \<in> \<G> \<union> ?Faces" for S 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

559 
using that \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly polytope_imp_closed by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

560 
have K: "X \<inter> Y \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int p})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

561 
if "X \<in> \<G> \<union> ?Faces" "Y \<in> \<G> \<union> ?Faces" "~ Y \<subseteq> X" for X Y 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

562 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

563 
have ff: "X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

564 
if XY: "X face_of D" "Y face_of E" and DE: "D \<in> \<F>" "E \<in> \<F>" for D E 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

565 
apply (rule face_of_Int_subface [OF _ _ XY]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

566 
apply (auto simp: face DE) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

567 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

568 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

569 
using that 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

570 
apply auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

571 
apply (drule_tac x="X \<inter> Y" in spec, safe) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

572 
using ff face_of_imp_convex [of X] face_of_imp_convex [of Y] 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

573 
apply (fastforce dest: face_of_aff_dim_lt) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

574 
by (meson face_of_trans ff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

575 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

576 
obtain g where "continuous_on (\<Union>(\<G> \<union> ?Faces)) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

577 
"g ` \<Union>(\<G> \<union> ?Faces) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

578 
"(\<forall>x \<in> \<Union>(\<G> \<union> ?Faces) \<inter> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

579 
\<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < p}). g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

580 
apply (rule exE [OF extending_maps_Union [OF fin extendh clo K]], blast+) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

581 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

582 
then show ?case 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

583 
apply (simp add: intle local.heq [symmetric], blast) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

584 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

585 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

586 
have eq: "\<Union>(\<G> \<union> {D. \<exists>C \<in> \<F>. D face_of C \<and> aff_dim D < i}) = \<Union>\<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

587 
proof 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

588 
show "\<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < int i}) \<subseteq> \<Union>\<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

589 
apply (rule Union_subsetI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

590 
using \<open>\<G> \<subseteq> \<F>\<close> face_of_imp_subset apply force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

591 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

592 
show "\<Union>\<F> \<subseteq> \<Union>(\<G> \<union> {D. \<exists>C\<in>\<F>. D face_of C \<and> aff_dim D < i})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

593 
apply (rule Union_mono) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

594 
using face apply (fastforce simp: aff i) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

595 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

596 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

597 
have "int i \<le> aff_dim T" by (simp add: i) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

598 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

599 
using extendf [of i] unfolding eq by (metis that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

600 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

601 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

602 
lemma extend_map_lemma_cofinite0: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

603 
assumes "finite \<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

604 
and "pairwise (\<lambda>S T. S \<inter> T \<subseteq> K) \<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

605 
and "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S  {a}) g \<and> g ` (S  {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

606 
and "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

607 
shows "\<exists>C g. finite C \<and> disjnt C U \<and> card C \<le> card \<F> \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

608 
continuous_on (\<Union>\<F>  C) g \<and> g ` (\<Union>\<F>  C) \<subseteq> T 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

609 
\<and> (\<forall>x \<in> (\<Union>\<F>  C) \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

610 
using assms 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

611 
proof induction 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

612 
case empty then show ?case 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

613 
by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

614 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

615 
case (insert X \<F>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

616 
then have "closed X" and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

617 
and \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (S  {a}) g \<and> g ` (S  {a}) \<subseteq> T \<and> (\<forall>x \<in> S \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

618 
and pwX: "\<And>Y. Y \<in> \<F> \<and> Y \<noteq> X \<longrightarrow> X \<inter> Y \<subseteq> K \<and> Y \<inter> X \<subseteq> K" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

619 
and pwF: "pairwise (\<lambda> S T. S \<inter> T \<subseteq> K) \<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

620 
by (simp_all add: pairwise_insert) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

621 
obtain C g where C: "finite C" "disjnt C U" "card C \<le> card \<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

622 
and contg: "continuous_on (\<Union>\<F>  C) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

623 
and gim: "g ` (\<Union>\<F>  C) \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

624 
and gh: "\<And>x. x \<in> (\<Union>\<F>  C) \<inter> K \<Longrightarrow> g x = h x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

625 
using insert.IH [OF pwF \<F> clo] by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

626 
obtain a f where "a \<notin> U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

627 
and contf: "continuous_on (X  {a}) f" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

628 
and fim: "f ` (X  {a}) \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

629 
and fh: "(\<forall>x \<in> X \<inter> K. f x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

630 
using insert.prems by (meson insertI1) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

631 
show ?case 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

632 
proof (intro exI conjI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

633 
show "finite (insert a C)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

634 
by (simp add: C) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

635 
show "disjnt (insert a C) U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

636 
using C \<open>a \<notin> U\<close> by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

637 
show "card (insert a C) \<le> card (insert X \<F>)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

638 
by (simp add: C card_insert_if insert.hyps le_SucI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

639 
have "closed (\<Union>\<F>)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

640 
using clo insert.hyps by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

641 
have "continuous_on (X  insert a C \<union> (\<Union>\<F>  insert a C)) (\<lambda>x. if x \<in> X then f x else g x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

642 
apply (rule continuous_on_cases_local) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

643 
apply (simp_all add: closedin_closed) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

644 
using \<open>closed X\<close> apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

645 
using \<open>closed (\<Union>\<F>)\<close> apply blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

646 
using contf apply (force simp: elim: continuous_on_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

647 
using contg apply (force simp: elim: continuous_on_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

648 
using fh gh insert.hyps pwX by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

649 
then show "continuous_on (\<Union>insert X \<F>  insert a C) (\<lambda>a. if a \<in> X then f a else g a)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

650 
by (blast intro: continuous_on_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

651 
show "\<forall>x\<in>(\<Union>insert X \<F>  insert a C) \<inter> K. (if x \<in> X then f x else g x) = h x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

652 
using gh by (auto simp: fh) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

653 
show "(\<lambda>a. if a \<in> X then f a else g a) ` (\<Union>insert X \<F>  insert a C) \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

654 
using fim gim by auto force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

655 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

656 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

657 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

658 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

659 
lemma extend_map_lemma_cofinite1: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

660 
assumes "finite \<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

661 
and \<F>: "\<And>X. X \<in> \<F> \<Longrightarrow> \<exists>a g. a \<notin> U \<and> continuous_on (X  {a}) g \<and> g ` (X  {a}) \<subseteq> T \<and> (\<forall>x \<in> X \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

662 
and clo: "\<And>X. X \<in> \<F> \<Longrightarrow> closed X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

663 
and K: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>; ~(X \<subseteq> Y); ~(Y \<subseteq> X)\<rbrakk> \<Longrightarrow> X \<inter> Y \<subseteq> K" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

664 
obtains C g where "finite C" "disjnt C U" "card C \<le> card \<F>" "continuous_on (\<Union>\<F>  C) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

665 
"g ` (\<Union>\<F>  C) \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

666 
"\<And>x. x \<in> (\<Union>\<F>  C) \<inter> K \<Longrightarrow> g x = h x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

667 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

668 
let ?\<F> = "{X \<in> \<F>. \<forall>Y\<in>\<F>. \<not> X \<subset> Y}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

669 
have [simp]: "\<Union>?\<F> = \<Union>\<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

670 
by (simp add: Union_maximal_sets assms) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

671 
have fin: "finite ?\<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

672 
by (force intro: finite_subset [OF _ \<open>finite \<F>\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

673 
have pw: "pairwise (\<lambda> S T. S \<inter> T \<subseteq> K) ?\<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

674 
by (simp add: pairwise_def) (metis K psubsetI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

675 
have "card {X \<in> \<F>. \<forall>Y\<in>\<F>. \<not> X \<subset> Y} \<le> card \<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

676 
by (simp add: \<open>finite \<F>\<close> card_mono) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

677 
moreover 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

678 
obtain C g where "finite C \<and> disjnt C U \<and> card C \<le> card ?\<F> \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

679 
continuous_on (\<Union>?\<F>  C) g \<and> g ` (\<Union>?\<F>  C) \<subseteq> T 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

680 
\<and> (\<forall>x \<in> (\<Union>?\<F>  C) \<inter> K. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

681 
apply (rule exE [OF extend_map_lemma_cofinite0 [OF fin pw, of U T h]]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

682 
apply (fastforce intro!: clo \<F>)+ 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

683 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

684 
ultimately show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

685 
by (rule_tac C=C and g=g in that) auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

686 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

687 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

688 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

689 
lemma extend_map_lemma_cofinite: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

690 
assumes "finite \<F>" "\<G> \<subseteq> \<F>" and T: "convex T" "bounded T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

691 
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

692 
and contf: "continuous_on (\<Union>\<G>) f" and fim: "f ` (\<Union>\<G>) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

693 
and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

694 
and aff: "\<And>X. X \<in> \<F>  \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

695 
obtains C g where 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

696 
"finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F>  C) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

697 
"g ` (\<Union> \<F>  C) \<subseteq> rel_frontier T" "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

698 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

699 
define \<H> where "\<H> \<equiv> \<G> \<union> {D. \<exists>C \<in> \<F>  \<G>. D face_of C \<and> aff_dim D < aff_dim T}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

700 
have "finite \<G>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

701 
using assms finite_subset by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

702 
moreover have "finite (\<Union>{{D. D face_of C} C. C \<in> \<F>})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

703 
apply (rule finite_Union) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

704 
apply (simp add: \<open>finite \<F>\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

705 
using finite_polytope_faces poly by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

706 
ultimately have "finite \<H>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

707 
apply (simp add: \<H>_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

708 
apply (rule finite_subset [of _ "\<Union> {{D. D face_of C}  C. C \<in> \<F>}"], auto) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

709 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

710 
have *: "\<And>X Y. \<lbrakk>X \<in> \<H>; Y \<in> \<H>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

711 
unfolding \<H>_def 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

712 
apply (elim UnE bexE CollectE DiffE) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

713 
using subsetD [OF \<open>\<G> \<subseteq> \<F>\<close>] apply (simp_all add: face) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

714 
apply (meson subsetD [OF \<open>\<G> \<subseteq> \<F>\<close>] face face_of_Int_subface face_of_imp_subset face_of_refl poly polytope_imp_convex)+ 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

715 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

716 
obtain h where conth: "continuous_on (\<Union>\<H>) h" and him: "h ` (\<Union>\<H>) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

717 
and hf: "\<And>x. x \<in> \<Union>\<G> \<Longrightarrow> h x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

718 
using \<open>finite \<H>\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

719 
unfolding \<H>_def 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

720 
apply (rule extend_map_lemma [OF _ Un_upper1 T _ _ _ contf fim]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

721 
using \<open>\<G> \<subseteq> \<F>\<close> face_of_polytope_polytope poly apply fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

722 
using * apply (auto simp: \<H>_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

723 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

724 
have "bounded (\<Union>\<G>)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

725 
using \<open>finite \<G>\<close> \<open>\<G> \<subseteq> \<F>\<close> poly polytope_imp_bounded by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

726 
then have "\<Union>\<G> \<noteq> UNIV" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

727 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

728 
then obtain a where a: "a \<notin> \<Union>\<G>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

729 
by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

730 
have \<F>: "\<exists>a g. a \<notin> \<Union>\<G> \<and> continuous_on (D  {a}) g \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

731 
g ` (D  {a}) \<subseteq> rel_frontier T \<and> (\<forall>x \<in> D \<inter> \<Union>\<H>. g x = h x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

732 
if "D \<in> \<F>" for D 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

733 
proof (cases "D \<subseteq> \<Union>\<H>") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

734 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

735 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

736 
apply (rule_tac x=a in exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

737 
apply (rule_tac x=h in exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

738 
using him apply (blast intro!: \<open>a \<notin> \<Union>\<G>\<close> continuous_on_subset [OF conth]) + 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

739 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

740 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

741 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

742 
note D_not_subset = False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

743 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

744 
proof (cases "D \<in> \<G>") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

745 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

746 
with D_not_subset show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

747 
by (auto simp: \<H>_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

748 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

749 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

750 
then have affD: "aff_dim D \<le> aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

751 
by (simp add: \<open>D \<in> \<F>\<close> aff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

752 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

753 
proof (cases "rel_interior D = {}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

754 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

755 
with \<open>D \<in> \<F>\<close> poly a show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

756 
by (force simp: rel_interior_eq_empty polytope_imp_convex) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

757 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

758 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

759 
then obtain b where brelD: "b \<in> rel_interior D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

760 
by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

761 
have "polyhedron D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

762 
by (simp add: poly polytope_imp_polyhedron that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

763 
have "rel_frontier D retract_of affine hull D  {b}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

764 
by (simp add: rel_frontier_retract_of_punctured_affine_hull poly polytope_imp_bounded polytope_imp_convex that brelD) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

765 
then obtain r where relfD: "rel_frontier D \<subseteq> affine hull D  {b}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

766 
and contr: "continuous_on (affine hull D  {b}) r" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

767 
and rim: "r ` (affine hull D  {b}) \<subseteq> rel_frontier D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

768 
and rid: "\<And>x. x \<in> rel_frontier D \<Longrightarrow> r x = x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

769 
by (auto simp: retract_of_def retraction_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

770 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

771 
proof (intro exI conjI ballI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

772 
show "b \<notin> \<Union>\<G>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

773 
proof clarify 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

774 
fix E 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

775 
assume "b \<in> E" "E \<in> \<G>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

776 
then have "E \<inter> D face_of E \<and> E \<inter> D face_of D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

777 
using \<open>\<G> \<subseteq> \<F>\<close> face that by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

778 
with face_of_subset_rel_frontier \<open>E \<in> \<G>\<close> \<open>b \<in> E\<close> brelD rel_interior_subset [of D] 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

779 
D_not_subset rel_frontier_def \<H>_def 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

780 
show False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

781 
by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

782 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

783 
have "r ` (D  {b}) \<subseteq> r ` (affine hull D  {b})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

784 
by (simp add: Diff_mono hull_subset image_mono) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

785 
also have "... \<subseteq> rel_frontier D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

786 
by (rule rim) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

787 
also have "... \<subseteq> \<Union>{E. E face_of D \<and> aff_dim E < aff_dim T}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

788 
using affD 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

789 
by (force simp: rel_frontier_of_polyhedron [OF \<open>polyhedron D\<close>] facet_of_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

790 
also have "... \<subseteq> \<Union>(\<H>)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

791 
using D_not_subset \<H>_def that by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

792 
finally have rsub: "r ` (D  {b}) \<subseteq> \<Union>(\<H>)" . 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

793 
show "continuous_on (D  {b}) (h \<circ> r)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

794 
apply (intro conjI \<open>b \<notin> \<Union>\<G>\<close> continuous_on_compose) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

795 
apply (rule continuous_on_subset [OF contr]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

796 
apply (simp add: Diff_mono hull_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

797 
apply (rule continuous_on_subset [OF conth rsub]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

798 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

799 
show "(h \<circ> r) ` (D  {b}) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

800 
using brelD him rsub by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

801 
show "(h \<circ> r) x = h x" if x: "x \<in> D \<inter> \<Union>\<H>" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

802 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

803 
consider A where "x \<in> D" "A \<in> \<G>" "x \<in> A" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

804 
 A B where "x \<in> D" "A face_of B" "B \<in> \<F>" "B \<notin> \<G>" "aff_dim A < aff_dim T" "x \<in> A" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

805 
using x by (auto simp: \<H>_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

806 
then have xrel: "x \<in> rel_frontier D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

807 
proof cases 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

808 
case 1 show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

809 
proof (rule face_of_subset_rel_frontier [THEN subsetD]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

810 
show "D \<inter> A face_of D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

811 
using \<open>A \<in> \<G>\<close> \<open>\<G> \<subseteq> \<F>\<close> face \<open>D \<in> \<F>\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

812 
show "D \<inter> A \<noteq> D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

813 
using \<open>A \<in> \<G>\<close> D_not_subset \<H>_def by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

814 
qed (auto simp: 1) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

815 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

816 
case 2 show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

817 
proof (rule face_of_subset_rel_frontier [THEN subsetD]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

818 
show "D \<inter> A face_of D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

819 
apply (rule face_of_Int_subface [of D B _ A, THEN conjunct1]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

820 
apply (simp_all add: 2 \<open>D \<in> \<F>\<close> face) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

821 
apply (simp add: \<open>polyhedron D\<close> polyhedron_imp_convex face_of_refl) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

822 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

823 
show "D \<inter> A \<noteq> D" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

824 
using "2" D_not_subset \<H>_def by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

825 
qed (auto simp: 2) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

826 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

827 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

828 
by (simp add: rid xrel) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

829 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

830 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

831 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

832 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

833 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

834 
have clo: "\<And>S. S \<in> \<F> \<Longrightarrow> closed S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

835 
by (simp add: poly polytope_imp_closed) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

836 
obtain C g where "finite C" "disjnt C (\<Union>\<G>)" "card C \<le> card \<F>" "continuous_on (\<Union>\<F>  C) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

837 
"g ` (\<Union>\<F>  C) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

838 
and gh: "\<And>x. x \<in> (\<Union>\<F>  C) \<inter> \<Union>\<H> \<Longrightarrow> g x = h x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

839 
proof (rule extend_map_lemma_cofinite1 [OF \<open>finite \<F>\<close> \<F> clo]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

840 
show "X \<inter> Y \<subseteq> \<Union>\<H>" if XY: "X \<in> \<F>" "Y \<in> \<F>" and "\<not> X \<subseteq> Y" "\<not> Y \<subseteq> X" for X Y 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

841 
proof (cases "X \<in> \<G>") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

842 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

843 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

844 
by (auto simp: \<H>_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

845 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

846 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

847 
have "X \<inter> Y \<noteq> X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

848 
using \<open>\<not> X \<subseteq> Y\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

849 
with XY 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

850 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

851 
by (clarsimp simp: \<H>_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

852 
(metis Diff_iff Int_iff aff antisym_conv face face_of_aff_dim_lt face_of_refl 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

853 
not_le poly polytope_imp_convex) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

854 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

855 
qed (blast)+ 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

856 
with \<open>\<G> \<subseteq> \<F>\<close> show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

857 
apply (rule_tac C=C and g=g in that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

858 
apply (auto simp: disjnt_def hf [symmetric] \<H>_def intro!: gh) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

859 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

860 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

861 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

862 
text\<open>The next two proofs are similar\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

863 
theorem extend_map_cell_complex_to_sphere: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

864 
assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

865 
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

866 
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X < aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

867 
and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

868 
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

869 
obtains g where "continuous_on (\<Union>\<F>) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

870 
"g ` (\<Union>\<F>) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

871 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

872 
obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

873 
using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

874 
have "compact S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

875 
by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

876 
then obtain d where "d > 0" and d: "\<And>x y. \<lbrakk>x \<in> S; y \<in>  V\<rbrakk> \<Longrightarrow> d \<le> dist x y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

877 
using separate_compact_closed [of S "V"] \<open>open V\<close> \<open>S \<subseteq> V\<close> by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

878 
obtain \<G> where "finite \<G>" "\<Union>\<G> = \<Union>\<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

879 
and diaG: "\<And>X. X \<in> \<G> \<Longrightarrow> diameter X < d" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

880 
and polyG: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

881 
and affG: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T  1" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

882 
and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

883 
proof (rule cell_complex_subdivision_exists [OF \<open>d>0\<close> \<open>finite \<F>\<close> poly _ face]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

884 
show "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T  1" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

885 
by (simp add: aff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

886 
qed auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

887 
obtain h where conth: "continuous_on (\<Union>\<G>) h" and him: "h ` \<Union>\<G> \<subseteq> rel_frontier T" and hg: "\<And>x. x \<in> \<Union>(\<G> \<inter> Pow V) \<Longrightarrow> h x = g x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

888 
proof (rule extend_map_lemma [of \<G> "\<G> \<inter> Pow V" T g]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

889 
show "continuous_on (\<Union>(\<G> \<inter> Pow V)) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

890 
by (metis Union_Int_subset Union_Pow_eq \<open>continuous_on V g\<close> continuous_on_subset le_inf_iff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

891 
qed (use \<open>finite \<G>\<close> T polyG affG faceG gim in fastforce)+ 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

892 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

893 
proof 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

894 
show "continuous_on (\<Union>\<F>) h" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

895 
using \<open>\<Union>\<G> = \<Union>\<F>\<close> conth by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

896 
show "h ` \<Union>\<F> \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

897 
using \<open>\<Union>\<G> = \<Union>\<F>\<close> him by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

898 
show "h x = f x" if "x \<in> S" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

899 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

900 
have "x \<in> \<Union>\<G>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

901 
using \<open>\<Union>\<G> = \<Union>\<F>\<close> \<open>S \<subseteq> \<Union>\<F>\<close> that by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

902 
then obtain X where "x \<in> X" "X \<in> \<G>" by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

903 
then have "diameter X < d" "bounded X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

904 
by (auto simp: diaG \<open>X \<in> \<G>\<close> polyG polytope_imp_bounded) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

905 
then have "X \<subseteq> V" using d [OF \<open>x \<in> S\<close>] diameter_bounded_bound [OF \<open>bounded X\<close> \<open>x \<in> X\<close>] 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

906 
by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

907 
have "h x = g x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

908 
apply (rule hg) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

909 
using \<open>X \<in> \<G>\<close> \<open>X \<subseteq> V\<close> \<open>x \<in> X\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

910 
also have "... = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

911 
by (simp add: gf that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

912 
finally show "h x = f x" . 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

913 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

914 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

915 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

916 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

917 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

918 
theorem extend_map_cell_complex_to_sphere_cofinite: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

919 
assumes "finite \<F>" and S: "S \<subseteq> \<Union>\<F>" "closed S" and T: "convex T" "bounded T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

920 
and poly: "\<And>X. X \<in> \<F> \<Longrightarrow> polytope X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

921 
and aff: "\<And>X. X \<in> \<F> \<Longrightarrow> aff_dim X \<le> aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

922 
and face: "\<And>X Y. \<lbrakk>X \<in> \<F>; Y \<in> \<F>\<rbrakk> \<Longrightarrow> (X \<inter> Y) face_of X \<and> (X \<inter> Y) face_of Y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

923 
and contf: "continuous_on S f" and fim: "f ` S \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

924 
obtains C g where "finite C" "disjnt C S" "continuous_on (\<Union>\<F>  C) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

925 
"g ` (\<Union>\<F>  C) \<subseteq> rel_frontier T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

926 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

927 
obtain V g where "S \<subseteq> V" "open V" "continuous_on V g" and gim: "g ` V \<subseteq> rel_frontier T" and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

928 
using neighbourhood_extension_into_ANR [OF contf fim _ \<open>closed S\<close>] ANR_rel_frontier_convex T by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

929 
have "compact S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

930 
by (meson assms compact_Union poly polytope_imp_compact seq_compact_closed_subset seq_compact_eq_compact) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

931 
then obtain d where "d > 0" and d: "\<And>x y. \<lbrakk>x \<in> S; y \<in>  V\<rbrakk> \<Longrightarrow> d \<le> dist x y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

932 
using separate_compact_closed [of S "V"] \<open>open V\<close> \<open>S \<subseteq> V\<close> by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

933 
obtain \<G> where "finite \<G>" "\<Union>\<G> = \<Union>\<F>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

934 
and diaG: "\<And>X. X \<in> \<G> \<Longrightarrow> diameter X < d" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

935 
and polyG: "\<And>X. X \<in> \<G> \<Longrightarrow> polytope X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

936 
and affG: "\<And>X. X \<in> \<G> \<Longrightarrow> aff_dim X \<le> aff_dim T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

937 
and faceG: "\<And>X Y. \<lbrakk>X \<in> \<G>; Y \<in> \<G>\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

938 
by (rule cell_complex_subdivision_exists [OF \<open>d>0\<close> \<open>finite \<F>\<close> poly aff face]) auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

939 
obtain C h where "finite C" and dis: "disjnt C (\<Union>(\<G> \<inter> Pow V))" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

940 
and card: "card C \<le> card \<G>" and conth: "continuous_on (\<Union>\<G>  C) h" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

941 
and him: "h ` (\<Union>\<G>  C) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

942 
and hg: "\<And>x. x \<in> \<Union>(\<G> \<inter> Pow V) \<Longrightarrow> h x = g x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

943 
proof (rule extend_map_lemma_cofinite [of \<G> "\<G> \<inter> Pow V" T g]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

944 
show "continuous_on (\<Union>(\<G> \<inter> Pow V)) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

945 
by (metis Union_Int_subset Union_Pow_eq \<open>continuous_on V g\<close> continuous_on_subset le_inf_iff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

946 
show "g ` \<Union>(\<G> \<inter> Pow V) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

947 
using gim by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

948 
qed (auto intro: \<open>finite \<G>\<close> T polyG affG dest: faceG) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

949 
have Ssub: "S \<subseteq> \<Union>(\<G> \<inter> Pow V)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

950 
proof 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

951 
fix x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

952 
assume "x \<in> S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

953 
then have "x \<in> \<Union>\<G>" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

954 
using \<open>\<Union>\<G> = \<Union>\<F>\<close> \<open>S \<subseteq> \<Union>\<F>\<close> by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

955 
then obtain X where "x \<in> X" "X \<in> \<G>" by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

956 
then have "diameter X < d" "bounded X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

957 
by (auto simp: diaG \<open>X \<in> \<G>\<close> polyG polytope_imp_bounded) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

958 
then have "X \<subseteq> V" using d [OF \<open>x \<in> S\<close>] diameter_bounded_bound [OF \<open>bounded X\<close> \<open>x \<in> X\<close>] 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

959 
by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

960 
then show "x \<in> \<Union>(\<G> \<inter> Pow V)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

961 
using \<open>X \<in> \<G>\<close> \<open>x \<in> X\<close> by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

962 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

963 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

964 
proof 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

965 
show "continuous_on (\<Union>\<F>C) h" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

966 
using \<open>\<Union>\<G> = \<Union>\<F>\<close> conth by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

967 
show "h ` (\<Union>\<F>  C) \<subseteq> rel_frontier T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

968 
using \<open>\<Union>\<G> = \<Union>\<F>\<close> him by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

969 
show "h x = f x" if "x \<in> S" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

970 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

971 
have "h x = g x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

972 
apply (rule hg) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

973 
using Ssub that by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

974 
also have "... = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

975 
by (simp add: gf that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

976 
finally show "h x = f x" . 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

977 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

978 
show "disjnt C S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

979 
using dis Ssub by (meson disjnt_iff subset_eq) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

980 
qed (intro \<open>finite C\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

981 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

982 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

983 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

984 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

985 
subsection\<open> Special cases and corollaries involving spheres.\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

986 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

987 
lemma disjnt_Diff1: "X \<subseteq> Y' \<Longrightarrow> disjnt (X  Y) (X'  Y')" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

988 
by (auto simp: disjnt_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

989 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

990 
proposition extend_map_affine_to_sphere_cofinite_simple: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

991 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

992 
assumes "compact S" "convex U" "bounded U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

993 
and aff: "aff_dim T \<le> aff_dim U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

994 
and "S \<subseteq> T" and contf: "continuous_on S f" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

995 
and fim: "f ` S \<subseteq> rel_frontier U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

996 
obtains K g where "finite K" "K \<subseteq> T" "disjnt K S" "continuous_on (T  K) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

997 
"g ` (T  K) \<subseteq> rel_frontier U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

998 
"\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

999 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1000 
have "\<exists>K g. finite K \<and> disjnt K S \<and> continuous_on (T  K) g \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1001 
g ` (T  K) \<subseteq> rel_frontier U \<and> (\<forall>x \<in> S. g x = f x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1002 
if "affine T" "S \<subseteq> T" and aff: "aff_dim T \<le> aff_dim U" for T 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1003 
proof (cases "S = {}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1004 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1005 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1006 
proof (cases "rel_frontier U = {}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1007 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1008 
with \<open>bounded U\<close> have "aff_dim U \<le> 0" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1009 
using affine_bounded_eq_lowdim rel_frontier_eq_empty by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1010 
with aff have "aff_dim T \<le> 0" by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1011 
then obtain a where "T \<subseteq> {a}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1012 
using \<open>affine T\<close> affine_bounded_eq_lowdim affine_bounded_eq_trivial by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1013 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1014 
using \<open>S = {}\<close> fim 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1015 
by (metis Diff_cancel contf disjnt_empty2 finite.emptyI finite_insert finite_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1016 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1017 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1018 
then obtain a where "a \<in> rel_frontier U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1019 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1020 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1021 
using continuous_on_const [of _ a] \<open>S = {}\<close> by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1022 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1023 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1024 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1025 
have "bounded S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1026 
by (simp add: \<open>compact S\<close> compact_imp_bounded) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1027 
then obtain b where b: "S \<subseteq> cbox (b) b" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1028 
using bounded_subset_cbox_symmetric by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1029 
define bbox where "bbox \<equiv> cbox ((b+One)) (b+One)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1030 
have "cbox (b) b \<subseteq> bbox" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1031 
by (auto simp: bbox_def algebra_simps intro!: subset_box_imp) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1032 
with b \<open>S \<subseteq> T\<close> have "S \<subseteq> bbox \<inter> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1033 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1034 
then have Ssub: "S \<subseteq> \<Union>{bbox \<inter> T}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1035 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1036 
then have "aff_dim (bbox \<inter> T) \<le> aff_dim U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1037 
by (metis aff aff_dim_subset inf_commute inf_le1 order_trans) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1038 
obtain K g where K: "finite K" "disjnt K S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1039 
and contg: "continuous_on (\<Union>{bbox \<inter> T}  K) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1040 
and gim: "g ` (\<Union>{bbox \<inter> T}  K) \<subseteq> rel_frontier U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1041 
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1042 
proof (rule extend_map_cell_complex_to_sphere_cofinite 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1043 
[OF _ Ssub _ \<open>convex U\<close> \<open>bounded U\<close> _ _ _ contf fim]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1044 
show "closed S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1045 
using \<open>compact S\<close> compact_eq_bounded_closed by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1046 
show poly: "\<And>X. X \<in> {bbox \<inter> T} \<Longrightarrow> polytope X" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1047 
by (simp add: polytope_Int_polyhedron bbox_def polytope_interval affine_imp_polyhedron \<open>affine T\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1048 
show "\<And>X Y. \<lbrakk>X \<in> {bbox \<inter> T}; Y \<in> {bbox \<inter> T}\<rbrakk> \<Longrightarrow> X \<inter> Y face_of X \<and> X \<inter> Y face_of Y" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1049 
by (simp add:poly face_of_refl polytope_imp_convex) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1050 
show "\<And>X. X \<in> {bbox \<inter> T} \<Longrightarrow> aff_dim X \<le> aff_dim U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1051 
by (simp add: \<open>aff_dim (bbox \<inter> T) \<le> aff_dim U\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1052 
qed auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1053 
define fro where "fro \<equiv> \<lambda>d. frontier(cbox ((b + d *\<^sub>R One)) (b + d *\<^sub>R One))" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1054 
obtain d where d12: "1/2 \<le> d" "d \<le> 1" and dd: "disjnt K (fro d)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1055 
proof (rule disjoint_family_elem_disjnt [OF _ \<open>finite K\<close>]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1056 
show "infinite {1/2..1::real}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1057 
by (simp add: infinite_Icc) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1058 
have dis1: "disjnt (fro x) (fro y)" if "x<y" for x y 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1059 
by (auto simp: algebra_simps that subset_box_imp disjnt_Diff1 frontier_def fro_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1060 
then show "disjoint_family_on fro {1/2..1}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1061 
by (auto simp: disjoint_family_on_def disjnt_def neq_iff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1062 
qed auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1063 
define c where "c \<equiv> b + d *\<^sub>R One" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1064 
have cbsub: "cbox (b) b \<subseteq> box (c) c" "cbox (b) b \<subseteq> cbox (c) c" "cbox (c) c \<subseteq> bbox" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1065 
using d12 by (auto simp: algebra_simps subset_box_imp c_def bbox_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1066 
have clo_cbT: "closed (cbox ( c) c \<inter> T)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1067 
by (simp add: affine_closed closed_Int closed_cbox \<open>affine T\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1068 
have cpT_ne: "cbox ( c) c \<inter> T \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1069 
using \<open>S \<noteq> {}\<close> b cbsub(2) \<open>S \<subseteq> T\<close> by fastforce 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1070 
have "closest_point (cbox ( c) c \<inter> T) x \<notin> K" if "x \<in> T" "x \<notin> K" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1071 
proof (cases "x \<in> cbox (c) c") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1072 
case True with that show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1073 
by (simp add: closest_point_self) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1074 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1075 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1076 
have int_ne: "interior (cbox (c) c) \<inter> T \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1077 
using \<open>S \<noteq> {}\<close> \<open>S \<subseteq> T\<close> b \<open>cbox ( b) b \<subseteq> box ( c) c\<close> by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1078 
have "convex T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1079 
by (meson \<open>affine T\<close> affine_imp_convex) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1080 
then have "x \<in> affine hull (cbox ( c) c \<inter> T)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1081 
by (metis Int_commute Int_iff \<open>S \<noteq> {}\<close> \<open>S \<subseteq> T\<close> cbsub(1) \<open>x \<in> T\<close> affine_hull_convex_Int_nonempty_interior all_not_in_conv b hull_inc inf.orderE interior_cbox) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1082 
then have "x \<in> affine hull (cbox ( c) c \<inter> T)  rel_interior (cbox ( c) c \<inter> T)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1083 
by (meson DiffI False Int_iff rel_interior_subset subsetCE) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1084 
then have "closest_point (cbox ( c) c \<inter> T) x \<in> rel_frontier (cbox ( c) c \<inter> T)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1085 
by (rule closest_point_in_rel_frontier [OF clo_cbT cpT_ne]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1086 
moreover have "(rel_frontier (cbox ( c) c \<inter> T)) \<subseteq> fro d" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1087 
apply (subst convex_affine_rel_frontier_Int [OF _ \<open>affine T\<close> int_ne]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1088 
apply (auto simp: fro_def c_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1089 
done 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1090 
ultimately show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1091 
using dd by (force simp: disjnt_def) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1092 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1093 
then have cpt_subset: "closest_point (cbox ( c) c \<inter> T) ` (T  K) \<subseteq> \<Union>{bbox \<inter> T}  K" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1094 
using closest_point_in_set [OF clo_cbT cpT_ne] cbsub(3) by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1095 
show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1096 
proof (intro conjI ballI exI) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1097 
have "continuous_on (T  K) (closest_point (cbox ( c) c \<inter> T))" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1098 
apply (rule continuous_on_closest_point) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1099 
using \<open>S \<noteq> {}\<close> cbsub(2) b that 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1100 
by (auto simp: affine_imp_convex convex_Int affine_closed closed_Int closed_cbox \<open>affine T\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1101 
then show "continuous_on (T  K) (g \<circ> closest_point (cbox ( c) c \<inter> T))" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1102 
by (metis continuous_on_compose continuous_on_subset [OF contg cpt_subset]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1103 
have "(g \<circ> closest_point (cbox ( c) c \<inter> T)) ` (T  K) \<subseteq> g ` (\<Union>{bbox \<inter> T}  K)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1104 
by (metis image_comp image_mono cpt_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1105 
also have "... \<subseteq> rel_frontier U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1106 
by (rule gim) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1107 
finally show "(g \<circ> closest_point (cbox ( c) c \<inter> T)) ` (T  K) \<subseteq> rel_frontier U" . 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1108 
show "(g \<circ> closest_point (cbox ( c) c \<inter> T)) x = f x" if "x \<in> S" for x 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1109 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1110 
have "(g \<circ> closest_point (cbox ( c) c \<inter> T)) x = g x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1111 
unfolding o_def 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1112 
by (metis IntI \<open>S \<subseteq> T\<close> b cbsub(2) closest_point_self subset_eq that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1113 
also have "... = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1114 
by (simp add: that gf) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1115 
finally show ?thesis . 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1116 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1117 
qed (auto simp: K) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1118 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1119 
then obtain K g where "finite K" "disjnt K S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1120 
and contg: "continuous_on (affine hull T  K) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1121 
and gim: "g ` (affine hull T  K) \<subseteq> rel_frontier U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1122 
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1123 
by (metis aff affine_affine_hull aff_dim_affine_hull 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1124 
order_trans [OF \<open>S \<subseteq> T\<close> hull_subset [of T affine]]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1125 
then obtain K g where "finite K" "disjnt K S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1126 
and contg: "continuous_on (T  K) g" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1127 
and gim: "g ` (T  K) \<subseteq> rel_frontier U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1128 
and gf: "\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1129 
by (rule_tac K=K and g=g in that) (auto simp: hull_inc elim: continuous_on_subset) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1130 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1131 
by (rule_tac K="K \<inter> T" and g=g in that) (auto simp: disjnt_iff Diff_Int contg) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1132 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1133 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1134 
subsection\<open>Extending maps to spheres\<close> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1135 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1136 
(*Up to extend_map_affine_to_sphere_cofinite_gen*) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1137 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1138 
lemma closedin_closed_subset: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1139 
"\<lbrakk>closedin (subtopology euclidean U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1140 
\<Longrightarrow> closedin (subtopology euclidean T) S" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1141 
by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1142 

0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1143 
lemma extend_map_affine_to_sphere1: 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1144 
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::topological_space" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1145 
assumes "finite K" "affine U" and contf: "continuous_on (U  K) f" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1146 
and fim: "f ` (U  K) \<subseteq> T" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1147 
and comps: "\<And>C. \<lbrakk>C \<in> components(U  S); C \<inter> K \<noteq> {}\<rbrakk> \<Longrightarrow> C \<inter> L \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1148 
and clo: "closedin (subtopology euclidean U) S" and K: "disjnt K S" "K \<subseteq> U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1149 
obtains g where "continuous_on (U  L) g" "g ` (U  L) \<subseteq> T" "\<And>x. x \<in> S \<Longrightarrow> g x = f x" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1150 
proof (cases "K = {}") 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1151 
case True 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1152 
then show ?thesis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1153 
by (metis Diff_empty Diff_subset contf fim continuous_on_subset image_subsetI rev_image_eqI subset_iff that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1154 
next 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1155 
case False 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1156 
have "S \<subseteq> U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1157 
using clo closedin_limpt by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1158 
then have "(U  S) \<inter> K \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1159 
by (metis Diff_triv False Int_Diff K disjnt_def inf.absorb_iff2 inf_commute) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1160 
then have "\<Union>(components (U  S)) \<inter> K \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1161 
using Union_components by simp 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1162 
then obtain C0 where C0: "C0 \<in> components (U  S)" "C0 \<inter> K \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1163 
by blast 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1164 
have "convex U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1165 
by (simp add: affine_imp_convex \<open>affine U\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1166 
then have "locally connected U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1167 
by (rule convex_imp_locally_connected) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1168 
have "\<exists>a g. a \<in> C \<and> a \<in> L \<and> continuous_on (S \<union> (C  {a})) g \<and> 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1169 
g ` (S \<union> (C  {a})) \<subseteq> T \<and> (\<forall>x \<in> S. g x = f x)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1170 
if C: "C \<in> components (U  S)" and CK: "C \<inter> K \<noteq> {}" for C 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1171 
proof  
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1172 
have "C \<subseteq> US" "C \<inter> L \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1173 
by (simp_all add: in_components_subset comps that) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1174 
then obtain a where a: "a \<in> C" "a \<in> L" by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1175 
have opeUC: "openin (subtopology euclidean U) C" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1176 
proof (rule openin_trans) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1177 
show "openin (subtopology euclidean (US)) C" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1178 
by (simp add: \<open>locally connected U\<close> clo locally_diff_closed openin_components_locally_connected [OF _ C]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1179 
show "openin (subtopology euclidean U) (U  S)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1180 
by (simp add: clo openin_diff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1181 
qed 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1182 
then obtain d where "C \<subseteq> U" "0 < d" and d: "cball a d \<inter> U \<subseteq> C" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1183 
using openin_contains_cball by (metis \<open>a \<in> C\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1184 
then have "ball a d \<inter> U \<subseteq> C" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1185 
by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1186 
obtain h k where homhk: "homeomorphism (S \<union> C) (S \<union> C) h k" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1187 
and subC: "{x. (~ (h x = x \<and> k x = x))} \<subseteq> C" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1188 
and bou: "bounded {x. (~ (h x = x \<and> k x = x))}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1189 
and hin: "\<And>x. x \<in> C \<inter> K \<Longrightarrow> h x \<in> ball a d \<inter> U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1190 
proof (rule homeomorphism_grouping_points_exists_gen [of C "ball a d \<inter> U" "C \<inter> K" "S \<union> C"]) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1191 
show "openin (subtopology euclidean C) (ball a d \<inter> U)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1192 
by (metis Topology_Euclidean_Space.open_ball \<open>C \<subseteq> U\<close> \<open>ball a d \<inter> U \<subseteq> C\<close> inf.absorb_iff2 inf.orderE inf_assoc open_openin openin_subtopology) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1193 
show "openin (subtopology euclidean (affine hull C)) C" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1194 
by (metis \<open>a \<in> C\<close> \<open>openin (subtopology euclidean U) C\<close> affine_hull_eq affine_hull_openin all_not_in_conv \<open>affine U\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1195 
show "ball a d \<inter> U \<noteq> {}" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1196 
using \<open>0 < d\<close> \<open>C \<subseteq> U\<close> \<open>a \<in> C\<close> by force 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1197 
show "finite (C \<inter> K)" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1198 
by (simp add: \<open>finite K\<close>) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1199 
show "S \<union> C \<subseteq> affine hull C" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1200 
by (metis \<open>C \<subseteq> U\<close> \<open>S \<subseteq> U\<close> \<open>a \<in> C\<close> opeUC affine_hull_eq affine_hull_openin all_not_in_conv assms(2) sup.bounded_iff) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1201 
show "connected C" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1202 
by (metis C in_components_connected) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1203 
qed auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1204 
have a_BU: "a \<in> ball a d \<inter> U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1205 
using \<open>0 < d\<close> \<open>C \<subseteq> U\<close> \<open>a \<in> C\<close> by auto 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1206 
have "rel_frontier (cball a d \<inter> U) retract_of (affine hull (cball a d \<inter> U)  {a})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1207 
apply (rule rel_frontier_retract_of_punctured_affine_hull) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1208 
apply (auto simp: \<open>convex U\<close> convex_Int) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1209 
by (metis \<open>affine U\<close> convex_cball empty_iff interior_cball a_BU rel_interior_convex_Int_affine) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1210 
moreover have "rel_frontier (cball a d \<inter> U) = frontier (cball a d) \<inter> U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1211 
apply (rule convex_affine_rel_frontier_Int) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1212 
using a_BU by (force simp: \<open>affine U\<close>)+ 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1213 
moreover have "affine hull (cball a d \<inter> U) = U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1214 
by (metis \<open>convex U\<close> a_BU affine_hull_convex_Int_nonempty_interior affine_hull_eq \<open>affine U\<close> equals0D inf.commute interior_cball) 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1215 
ultimately have "frontier (cball a d) \<inter> U retract_of (U  {a})" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1216 
by metis 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1217 
then obtain r where contr: "continuous_on (U  {a}) r" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1218 
and rim: "r ` (U  {a}) \<subseteq> sphere a d" "r ` (U  {a}) \<subseteq> U" 
0de4736dad8b
new theorems including the theory FurtherTopology
paulson <lp15@cam.ac.uk>
parents:
diff
changeset

1219 
and req: "\<And>x. x \<in> sphere a d \<inter> U \<Longrightarrow> r x = x" 
