author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51481 ef949192e5d6 parent 51480 3793c3a11378 child 51482 80efd8c49f52
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
 src/HOL/Deriv.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Path_Connected.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/RealVector.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
1.2 +++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
1.3 @@ -831,16 +831,7 @@
1.4
1.5  lemma lemma_MVT:
1.6       "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)"
1.7 -proof cases
1.8 -  assume "a=b" thus ?thesis by simp
1.9 -next
1.10 -  assume "a\<noteq>b"
1.11 -  hence ba: "b-a \<noteq> 0" by arith
1.12 -  show ?thesis
1.13 -    by (rule real_mult_left_cancel [OF ba, THEN iffD1],
1.16 -qed
1.17 +  by (cases "a = b") (simp_all add: field_simps)
1.18
1.19  theorem MVT:
1.20    assumes lt:  "a < b"
1.21 @@ -1090,152 +1081,47 @@
1.22      by simp
1.23  qed
1.24
1.25 -subsection {* Continuous injective functions *}
1.26 -
1.27 -text{*Dull lemma: an continuous injection on an interval must have a
1.28 -strict maximum at an end point, not in the middle.*}
1.29 -
1.30 -lemma lemma_isCont_inj:
1.31 -  fixes f :: "real \<Rightarrow> real"
1.32 -  assumes d: "0 < d"
1.33 -      and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
1.34 -      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
1.35 -  shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
1.36 -proof (rule ccontr)
1.37 -  assume  "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
1.38 -  hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto
1.39 -  show False
1.40 -  proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
1.41 -    case le
1.42 -    from d cont all [of "x+d"]
1.43 -    have flef: "f(x+d) \<le> f x"
1.44 -     and xlex: "x - d \<le> x"
1.45 -     and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z"
1.46 -       by (auto simp add: abs_if)
1.47 -    from IVT [OF le flef xlex cont']
1.48 -    obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
1.49 -    moreover
1.50 -    hence "g(f x') = g (f(x+d))" by simp
1.51 -    ultimately show False using d inj [of x'] inj [of "x+d"]
1.52 -      by (simp add: abs_le_iff)
1.53 -  next
1.54 -    case ge
1.55 -    from d cont all [of "x-d"]
1.56 -    have flef: "f(x-d) \<le> f x"
1.57 -     and xlex: "x \<le> x+d"
1.58 -     and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z"
1.59 -       by (auto simp add: abs_if)
1.60 -    from IVT2 [OF ge flef xlex cont']
1.61 -    obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
1.62 -    moreover
1.63 -    hence "g(f x') = g (f(x-d))" by simp
1.64 -    ultimately show False using d inj [of x'] inj [of "x-d"]
1.65 -      by (simp add: abs_le_iff)
1.66 -  qed
1.67 -qed
1.68 -
1.69 -
1.70 -text{*Similar version for lower bound.*}
1.71 -
1.72 -lemma lemma_isCont_inj2:
1.73 -  fixes f g :: "real \<Rightarrow> real"
1.74 -  shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
1.75 -        \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
1.76 -      ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
1.77 -apply (insert lemma_isCont_inj
1.78 -          [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
1.80 -done
1.81 -
1.82 -text{*Show there's an interval surrounding @{term "f(x)"} in
1.83 -@{text "f[[x - d, x + d]]"} .*}
1.84 -
1.85 -lemma isCont_inj_range:
1.86 -  fixes f :: "real \<Rightarrow> real"
1.87 -  assumes d: "0 < d"
1.88 -      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
1.89 -      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
1.90 -  shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
1.91 -proof -
1.92 -  have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
1.93 -    by (auto simp add: abs_le_iff)
1.94 -  from isCont_Lb_Ub [OF this]
1.95 -  obtain L M
1.96 -  where all1 [rule_format]: "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> L \<le> f z \<and> f z \<le> M"
1.97 -    and all2 [rule_format]:
1.98 -           "\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>z. x-d \<le> z \<and> z \<le> x+d \<and> f z = y)"
1.99 -    by auto
1.100 -  with d have "L \<le> f x & f x \<le> M" by simp
1.101 -  moreover have "L \<noteq> f x"
1.102 -  proof -
1.103 -    from lemma_isCont_inj2 [OF d inj cont]
1.104 -    obtain u where "\<bar>u - x\<bar> \<le> d" "f u < f x"  by auto
1.105 -    thus ?thesis using all1 [of u] by arith
1.106 -  qed
1.107 -  moreover have "f x \<noteq> M"
1.108 -  proof -
1.109 -    from lemma_isCont_inj [OF d inj cont]
1.110 -    obtain u where "\<bar>u - x\<bar> \<le> d" "f x < f u"  by auto
1.111 -    thus ?thesis using all1 [of u] by arith
1.112 -  qed
1.113 -  ultimately have "L < f x & f x < M" by arith
1.114 -  hence "0 < f x - L" "0 < M - f x" by arith+
1.115 -  from real_lbound_gt_zero [OF this]
1.116 -  obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
1.117 -  thus ?thesis
1.118 -  proof (intro exI conjI)
1.119 -    show "0<e" using e(1) .
1.120 -    show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
1.121 -    proof (intro strip)
1.122 -      fix y::real
1.123 -      assume "\<bar>y - f x\<bar> \<le> e"
1.124 -      with e have "L \<le> y \<and> y \<le> M" by arith
1.125 -      from all2 [OF this]
1.126 -      obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
1.127 -      thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
1.128 -        by (force simp add: abs_le_iff)
1.129 -    qed
1.130 -  qed
1.131 -qed
1.132 -
1.133 -
1.134  text{*Continuity of inverse function*}
1.135
1.136  lemma isCont_inverse_function:
1.137    fixes f g :: "real \<Rightarrow> real"
1.138    assumes d: "0 < d"
1.139 -      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
1.140 -      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
1.141 +      and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z"
1.142 +      and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z"
1.143    shows "isCont g (f x)"
1.144 -proof (simp add: isCont_iff LIM_eq)
1.145 -  show "\<forall>r. 0 < r \<longrightarrow>
1.146 -         (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
1.147 -  proof (intro strip)
1.148 -    fix r::real
1.149 -    assume r: "0<r"
1.150 -    from real_lbound_gt_zero [OF r d]
1.151 -    obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
1.152 -    with inj cont
1.153 -    have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z"
1.154 -                  "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z"   by auto
1.155 -    from isCont_inj_range [OF e this]
1.156 -    obtain e' where e': "0 < e'"
1.157 -        and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
1.158 -          by blast
1.159 -    show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
1.160 -    proof (intro exI conjI)
1.161 -      show "0<e'" using e' .
1.162 -      show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
1.163 -      proof (intro strip)
1.164 -        fix z::real
1.165 -        assume z: "z \<noteq> 0 \<and> \<bar>z\<bar> < e'"
1.166 -        with e e_lt e_simps all [rule_format, of "f x + z"]
1.167 -        show "\<bar>g (f x + z) - g (f x)\<bar> < r" by force
1.168 -      qed
1.169 -    qed
1.170 -  qed
1.171 +proof -
1.172 +  let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}"
1.173 +
1.174 +  have f: "continuous_on ?D f"
1.175 +    using cont by (intro continuous_at_imp_continuous_on ballI) auto
1.176 +  then have g: "continuous_on (f`?D) g"
1.177 +    using inj by (intro continuous_on_inv) auto
1.178 +
1.179 +  from d f have "{min ?A ?B <..< max ?A ?B} \<subseteq> f ` ?D"
1.180 +    by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max)
1.181 +  with g have "continuous_on {min ?A ?B <..< max ?A ?B} g"
1.182 +    by (rule continuous_on_subset)
1.183 +  moreover
1.184 +  have "(?A < f x \<and> f x < ?B) \<or> (?B < f x \<and> f x < ?A)"
1.185 +    using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto
1.186 +  then have "f x \<in> {min ?A ?B <..< max ?A ?B}"
1.187 +    by auto
1.188 +  ultimately
1.189 +  show ?thesis
1.190 +    by (simp add: continuous_on_eq_continuous_at)
1.191  qed
1.192
1.193 +lemma isCont_inverse_function2:
1.194 +  fixes f g :: "real \<Rightarrow> real" shows
1.195 +  "\<lbrakk>a < x; x < b;
1.196 +    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
1.197 +    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
1.198 +   \<Longrightarrow> isCont g (f x)"
1.199 +apply (rule isCont_inverse_function
1.200 +       [where f=f and d="min (x - a) (b - x)"])
1.202 +done
1.203 +
1.204  text {* Derivative of inverse function *}
1.205
1.206  lemma DERIV_inverse_function:
1.207 @@ -1285,7 +1171,6 @@
1.208      using neq by (rule tendsto_inverse)
1.209  qed
1.210
1.211 -
1.212  subsection {* Generalized Mean Value Theorem *}
1.213
1.214  theorem GMVT:
1.215 @@ -1355,21 +1240,6 @@
1.216        ==> isCont g (f x)"
1.217  by (rule isCont_inverse_function)
1.218
1.219 -lemma isCont_inv_fun_inv:
1.220 -  fixes f g :: "real \<Rightarrow> real"
1.221 -  shows "[| 0 < d;
1.222 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;
1.223 -         \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]
1.224 -       ==> \<exists>e. 0 < e &
1.225 -             (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
1.226 -apply (drule isCont_inj_range)
1.227 -prefer 2 apply (assumption, assumption, auto)
1.228 -apply (rule_tac x = e in exI, auto)
1.229 -apply (rotate_tac 2)
1.230 -apply (drule_tac x = y in spec, auto)
1.231 -done
1.232 -
1.233 -
1.234  text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
1.235  lemma LIM_fun_gt_zero:
1.236       "[| f -- c --> (l::real); 0 < l |]
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Mar 22 10:41:43 2013 +0100
2.3 @@ -470,7 +470,7 @@
2.4    fixes f :: "'a::t2_space => real"
2.5    fixes A assumes "open A"
2.6    shows "continuous_on A f <-> continuous_on A (ereal o f)"
2.7 -  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)
2.8 +  using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
2.9
2.10
2.11  lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
3.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
3.3 @@ -8,14 +8,6 @@
3.4  imports Convex_Euclidean_Space
3.5  begin
3.6
3.7 -lemma continuous_on_cong: (* MOVE to Topological_Spaces *)
3.8 -  "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
3.9 -  unfolding continuous_on_def by (intro ball_cong Lim_cong_within) auto
3.10 -
3.11 -lemma continuous_on_compose2:
3.12 -  shows "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
3.13 -  using continuous_on_compose[of s f g] by (simp add: comp_def)
3.14 -
3.15  subsection {* Paths. *}
3.16
3.17  definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
3.18 @@ -126,7 +118,8 @@
3.19    have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))"
3.20      using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
3.21    show "continuous_on {0..1} g1" "continuous_on {0..1} g2"
3.22 -    unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont])
3.23 +    unfolding g1 g2
3.24 +    by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply)
3.25  next
3.26    assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
3.27    have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
3.28 @@ -689,8 +682,8 @@
3.29      unfolding xy
3.30      apply (rule_tac x="f \<circ> g" in exI)
3.31      unfolding path_defs
3.32 -    using assms(1)
3.33 -    apply (auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"])
3.34 +    apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)])
3.35 +    apply auto
3.36      done
3.37  qed
3.38
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
4.3 @@ -34,6 +34,24 @@
4.4    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
4.5    by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
4.6
4.7 +lemma Lim_within_open:
4.8 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
4.9 +  shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
4.10 +  by (fact tendsto_within_open)
4.11 +
4.12 +lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
4.13 +  by (fact tendsto_within_subset)
4.14 +
4.15 +lemma continuous_on_union:
4.16 +  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
4.17 +  by (fact continuous_on_closed_Un)
4.18 +
4.19 +lemma continuous_on_cases:
4.20 +  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
4.21 +    \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
4.22 +    continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
4.23 +  by (rule continuous_on_If) auto
4.24 +
4.25  subsection {* Topological Basis *}
4.26
4.27  context topological_space
4.28 @@ -1301,10 +1319,6 @@
4.29  lemma Lim_within_empty: "(f ---> l) (net within {})"
4.30    unfolding tendsto_def Limits.eventually_within by simp
4.31
4.32 -lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
4.33 -  unfolding tendsto_def Topological_Spaces.eventually_within
4.34 -  by (auto elim!: eventually_elim1)
4.35 -
4.36  lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
4.37    shows "(f ---> l) (net within (S \<union> T))"
4.38    using assms unfolding tendsto_def Limits.eventually_within
4.39 @@ -1352,16 +1366,6 @@
4.40    "x \<in> interior S \<Longrightarrow> at x within S = at x"
4.41    by (simp add: filter_eq_iff eventually_within_interior)
4.42
4.43 -lemma at_within_open:
4.44 -  "\<lbrakk>x \<in> S; open S\<rbrakk> \<Longrightarrow> at x within S = at x"
4.45 -  by (simp only: at_within_interior interior_open)
4.46 -
4.47 -lemma Lim_within_open:
4.48 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
4.49 -  assumes"a \<in> S" "open S"
4.50 -  shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
4.51 -  using assms by (simp only: at_within_open)
4.52 -
4.53  lemma Lim_within_LIMSEQ:
4.54    fixes a :: "'a::metric_space"
4.55    assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
4.56 @@ -2552,35 +2556,6 @@
4.57    thus ?thesis unfolding closed_sequential_limits by fast
4.58  qed
4.59
4.60 -lemma compact_imp_closed:
4.61 -  fixes s :: "'a::t2_space set"
4.62 -  assumes "compact s" shows "closed s"
4.63 -unfolding closed_def
4.64 -proof (rule openI)
4.65 -  fix y assume "y \<in> - s"
4.66 -  let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
4.67 -  note `compact s`
4.68 -  moreover have "\<forall>u\<in>?C. open u" by simp
4.69 -  moreover have "s \<subseteq> \<Union>?C"
4.70 -  proof
4.71 -    fix x assume "x \<in> s"
4.72 -    with `y \<in> - s` have "x \<noteq> y" by clarsimp
4.73 -    hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
4.74 -      by (rule hausdorff)
4.75 -    with `x \<in> s` show "x \<in> \<Union>?C"
4.76 -      unfolding eventually_nhds by auto
4.77 -  qed
4.78 -  ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
4.79 -    by (rule compactE)
4.80 -  from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
4.81 -  with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
4.82 -    by (simp add: eventually_Ball_finite)
4.83 -  with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
4.84 -    by (auto elim!: eventually_mono [rotated])
4.85 -  thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
4.86 -    by (simp add: eventually_nhds subset_eq)
4.87 -qed
4.88 -
4.89  lemma compact_imp_bounded:
4.90    assumes "compact U" shows "bounded U"
4.91  proof -
4.92 @@ -2614,20 +2589,6 @@
4.93    "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
4.94    unfolding SUP_def by (rule compact_Union) auto
4.95
4.96 -lemma compact_inter_closed [intro]:
4.97 -  assumes "compact s" and "closed t"
4.98 -  shows "compact (s \<inter> t)"
4.99 -proof (rule compactI)
4.100 -  fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
4.101 -  from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
4.102 -  moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
4.103 -  ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
4.104 -    using `compact s` unfolding compact_eq_heine_borel by auto
4.105 -  then guess D ..
4.106 -  then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
4.107 -    by (intro exI[of _ "D - {-t}"]) auto
4.108 -qed
4.109 -
4.110  lemma closed_inter_compact [intro]:
4.111    assumes "closed s" and "compact t"
4.112    shows "compact (s \<inter> t)"
4.113 @@ -3802,19 +3763,11 @@
4.114
4.115  lemmas continuous_on = continuous_on_def -- "legacy theorem name"
4.116
4.117 -lemma continuous_on_eq_continuous_at:
4.118 -  shows "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
4.119 -  by (auto simp add: continuous_on continuous_at Lim_within_open)
4.120 -
4.121  lemma continuous_within_subset:
4.122   "continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
4.123               ==> continuous (at x within t) f"
4.124    unfolding continuous_within by(metis Lim_within_subset)
4.125
4.126 -lemma continuous_on_subset:
4.127 -  shows "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
4.128 -  unfolding continuous_on by (metis subset_eq Lim_within_subset)
4.129 -
4.130  lemma continuous_on_interior:
4.131    shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
4.132    by (erule interiorE, drule (1) continuous_on_subset,
4.133 @@ -4087,70 +4040,18 @@
4.134  qed
4.135
4.136  lemma continuous_on_open:
4.137 -  shows "continuous_on s f \<longleftrightarrow>
4.138 +  "continuous_on s f \<longleftrightarrow>
4.139          (\<forall>t. openin (subtopology euclidean (f ` s)) t
4.140              --> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
4.141 -proof (safe)
4.142 -  fix t :: "'b set"
4.143 -  assume 1: "continuous_on s f"
4.144 -  assume 2: "openin (subtopology euclidean (f ` s)) t"
4.145 -  from 2 obtain B where B: "open B" and t: "t = f ` s \<inter> B"
4.146 -    unfolding openin_open by auto
4.147 -  def U == "\<Union>{A. open A \<and> (\<forall>x\<in>s. x \<in> A \<longrightarrow> f x \<in> B)}"
4.148 -  have "open U" unfolding U_def by (simp add: open_Union)
4.149 -  moreover have "\<forall>x\<in>s. x \<in> U \<longleftrightarrow> f x \<in> t"
4.150 -  proof (intro ballI iffI)
4.151 -    fix x assume "x \<in> s" and "x \<in> U" thus "f x \<in> t"
4.152 -      unfolding U_def t by auto
4.153 -  next
4.154 -    fix x assume "x \<in> s" and "f x \<in> t"
4.155 -    hence "x \<in> s" and "f x \<in> B"
4.156 -      unfolding t by auto
4.157 -    with 1 B obtain A where "open A" "x \<in> A" "\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B"
4.158 -      unfolding t continuous_on_topological by metis
4.159 -    then show "x \<in> U"
4.160 -      unfolding U_def by auto
4.161 -  qed
4.162 -  ultimately have "open U \<and> {x \<in> s. f x \<in> t} = s \<inter> U" by auto
4.163 -  then show "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
4.164 -    unfolding openin_open by fast
4.165 -next
4.166 -  assume "?rhs" show "continuous_on s f"
4.167 -  unfolding continuous_on_topological
4.168 -  proof (clarify)
4.169 -    fix x and B assume "x \<in> s" and "open B" and "f x \<in> B"
4.170 -    have "openin (subtopology euclidean (f ` s)) (f ` s \<inter> B)"
4.171 -      unfolding openin_open using `open B` by auto
4.172 -    then have "openin (subtopology euclidean s) {x \<in> s. f x \<in> f ` s \<inter> B}"
4.173 -      using `?rhs` by fast
4.174 -    then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
4.175 -      unfolding openin_open using `x \<in> s` and `f x \<in> B` by auto
4.176 -  qed
4.177 -qed
4.178 +  unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
4.179 +  by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
4.180
4.181  text {* Similarly in terms of closed sets. *}
4.182
4.183  lemma continuous_on_closed:
4.184    shows "continuous_on s f \<longleftrightarrow>  (\<forall>t. closedin (subtopology euclidean (f ` s)) t  --> closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
4.185 -proof
4.186 -  assume ?lhs
4.187 -  { fix t
4.188 -    have *:"s - {x \<in> s. f x \<in> f ` s - t} = {x \<in> s. f x \<in> t}" by auto
4.189 -    have **:"f ` s - (f ` s - (f ` s - t)) = f ` s - t" by auto
4.190 -    assume as:"closedin (subtopology euclidean (f ` s)) t"
4.191 -    hence "closedin (subtopology euclidean (f ` s)) (f ` s - (f ` s - t))" unfolding closedin_def topspace_euclidean_subtopology unfolding ** by auto
4.192 -    hence "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}" using `?lhs`[unfolded continuous_on_open, THEN spec[where x="(f ` s) - t"]]
4.193 -      unfolding openin_closedin_eq topspace_euclidean_subtopology unfolding * by auto  }
4.194 -  thus ?rhs by auto
4.195 -next
4.196 -  assume ?rhs
4.197 -  { fix t
4.198 -    have *:"s - {x \<in> s. f x \<in> f ` s - t} = {x \<in> s. f x \<in> t}" by auto
4.199 -    assume as:"openin (subtopology euclidean (f ` s)) t"
4.200 -    hence "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" using `?rhs`[THEN spec[where x="(f ` s) - t"]]
4.201 -      unfolding openin_closedin_eq topspace_euclidean_subtopology *[THEN sym] closedin_subtopology by auto }
4.202 -  thus ?lhs unfolding continuous_on_open by auto
4.203 -qed
4.204 +  unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
4.205 +  by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
4.206
4.207  text {* Half-global and completely global cases. *}
4.208
4.209 @@ -4544,38 +4445,6 @@
4.210    qed (insert D, auto)
4.211  qed auto
4.212
4.213 -text{* Continuity of inverse function on compact domain. *}
4.214 -
4.215 -lemma continuous_on_inv:
4.216 -  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
4.217 -  assumes "continuous_on s f"  "compact s"  "\<forall>x \<in> s. g (f x) = x"
4.218 -  shows "continuous_on (f ` s) g"
4.219 -unfolding continuous_on_topological
4.220 -proof (clarsimp simp add: assms(3))
4.221 -  fix x :: 'a and B :: "'a set"
4.222 -  assume "x \<in> s" and "open B" and "x \<in> B"
4.223 -  have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
4.224 -    using assms(3) by (auto, metis)
4.225 -  have "continuous_on (s - B) f"
4.226 -    using `continuous_on s f` Diff_subset
4.227 -    by (rule continuous_on_subset)
4.228 -  moreover have "compact (s - B)"
4.229 -    using `open B` and `compact s`
4.230 -    unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
4.231 -  ultimately have "compact (f ` (s - B))"
4.232 -    by (rule compact_continuous_image)
4.233 -  hence "closed (f ` (s - B))"
4.234 -    by (rule compact_imp_closed)
4.235 -  hence "open (- f ` (s - B))"
4.236 -    by (rule open_Compl)
4.237 -  moreover have "f x \<in> - f ` (s - B)"
4.238 -    using `x \<in> s` and `x \<in> B` by (simp add: 1)
4.239 -  moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
4.240 -    by (simp add: 1)
4.241 -  ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
4.242 -    by fast
4.243 -qed
4.244 -
4.245  text {* A uniformly convergent limit of continuous functions is continuous. *}
4.246
4.247  lemma continuous_uniform_limit:
4.248 @@ -5664,27 +5533,6 @@
4.249          (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
4.250    unfolding tendsto_def trivial_limit_eq by auto
4.251
4.252 -lemma continuous_on_union:
4.253 -  assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
4.254 -  shows "continuous_on (s \<union> t) f"
4.255 -  using assms unfolding continuous_on Lim_within_union
4.256 -  unfolding Lim_topological trivial_limit_within closed_limpt by auto
4.257 -
4.258 -lemma continuous_on_cases:
4.259 -  assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
4.260 -          "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
4.261 -  shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
4.262 -proof-
4.263 -  let ?h = "(\<lambda>x. if P x then f x else g x)"
4.264 -  have "\<forall>x\<in>s. f x = (if P x then f x else g x)" using assms(5) by auto
4.265 -  hence "continuous_on s ?h" using continuous_on_eq[of s f ?h] using assms(3) by auto
4.266 -  moreover
4.267 -  have "\<forall>x\<in>t. g x = (if P x then f x else g x)" using assms(5) by auto
4.268 -  hence "continuous_on t ?h" using continuous_on_eq[of t g ?h] using assms(4) by auto
4.269 -  ultimately show ?thesis using continuous_on_union[OF assms(1,2), of ?h] by auto
4.270 -qed
4.271 -
4.272 -
4.273  text{* Some more convenient intermediate-value theorem formulations.             *}
4.274
4.275  lemma connected_ivt_hyperplane:
```
```     5.1 --- a/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
5.2 +++ b/src/HOL/RealVector.thy	Fri Mar 22 10:41:43 2013 +0100
5.3 @@ -950,6 +950,8 @@
5.4
5.5  end
5.6
5.7 +instance real :: linear_continuum_topology ..
5.8 +
5.9  lemma connectedI_interval:
5.10    fixes U :: "'a :: linear_continuum_topology set"
5.11    assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
5.12 @@ -1068,6 +1070,27 @@
5.13    shows "f b \<le> y \<Longrightarrow> y \<le> f a \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
5.14    by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
5.15
5.16 -instance real :: linear_continuum_topology ..
5.17 +lemma continuous_inj_imp_mono:
5.18 +  fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
5.19 +  assumes x: "a < x" "x < b"
5.20 +  assumes cont: "continuous_on {a..b} f"
5.21 +  assumes inj: "inj_on f {a..b}"
5.22 +  shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
5.23 +proof -
5.24 +  note I = inj_on_iff[OF inj]
5.25 +  { assume "f x < f a" "f x < f b"
5.26 +    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
5.27 +      using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
5.28 +      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
5.29 +    with x I have False by auto }
5.30 +  moreover
5.31 +  { assume "f a < f x" "f b < f x"
5.32 +    then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f s < f x"
5.33 +      using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
5.34 +      by (auto simp: continuous_on_subset[OF cont] less_imp_le)
5.35 +    with x I have False by auto }
5.36 +  ultimately show ?thesis
5.37 +    using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
5.38 +qed
5.39
5.40  end
```
```     6.1 --- a/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
6.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
6.3 @@ -724,6 +724,9 @@
6.4    "eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
6.5  unfolding at_def eventually_within eventually_nhds by simp
6.6
6.7 +lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
6.8 +  unfolding filter_eq_iff eventually_within eventually_at_topological by (metis open_Int Int_iff)
6.9 +
6.10  lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
6.11    unfolding trivial_limit_def eventually_at_topological
6.12    by (safe, case_tac "S = {a}", simp, fast, fast)
6.13 @@ -869,6 +872,9 @@
6.14      by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
6.15  qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
6.16
6.17 +lemma tendsto_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
6.18 +  by (auto simp: tendsto_def eventually_within elim!: eventually_elim1)
6.19 +
6.20  lemma filterlim_at:
6.21    "(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
6.22    by (simp add: at_def filterlim_within)
6.23 @@ -1540,6 +1546,9 @@
6.24          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
6.25    "f -- a --> L \<equiv> (f ---> L) (at a)"
6.26
6.27 +lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
6.28 +  unfolding tendsto_def by (simp add: at_within_open)
6.29 +
6.30  lemma LIM_const_not_eq[tendsto_intros]:
6.31    fixes a :: "'a::perfect_space"
6.32    fixes k L :: "'b::t2_space"
6.33 @@ -1629,6 +1638,10 @@
6.34  definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
6.35    "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
6.36
6.37 +lemma continuous_on_cong [cong]:
6.38 +  "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
6.39 +  unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_within)
6.40 +
6.41  lemma continuous_on_topological:
6.42    "continuous_on s f \<longleftrightarrow>
6.43      (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
6.44 @@ -1655,6 +1668,11 @@
6.45    qed
6.46  qed
6.47
6.48 +lemma continuous_on_open_vimage:
6.49 +  "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> open (f -` B \<inter> s))"
6.50 +  unfolding continuous_on_open_invariant
6.51 +  by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
6.52 +
6.53  lemma continuous_on_closed_invariant:
6.54    "continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
6.55  proof -
6.56 @@ -1664,6 +1682,36 @@
6.57      unfolding continuous_on_open_invariant by (intro *) (auto simp: open_closed[symmetric])
6.58  qed
6.59
6.60 +lemma continuous_on_closed_vimage:
6.61 +  "closed s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> closed (f -` B \<inter> s))"
6.62 +  unfolding continuous_on_closed_invariant
6.63 +  by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
6.64 +
6.65 +lemma continuous_on_open_Union:
6.66 +  "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
6.67 +  unfolding continuous_on_def by (simp add: tendsto_within_open open_Union)
6.68 +
6.69 +lemma continuous_on_open_UN:
6.70 +  "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
6.71 +  unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
6.72 +
6.73 +lemma continuous_on_closed_Un:
6.74 +  "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
6.75 +  by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)
6.76 +
6.77 +lemma continuous_on_If:
6.78 +  assumes closed: "closed s" "closed t" and cont: "continuous_on s f" "continuous_on t g"
6.79 +    and P: "\<And>x. x \<in> s \<Longrightarrow> \<not> P x \<Longrightarrow> f x = g x" "\<And>x. x \<in> t \<Longrightarrow> P x \<Longrightarrow> f x = g x"
6.80 +  shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" (is "continuous_on _ ?h")
6.81 +proof-
6.82 +  from P have "\<forall>x\<in>s. f x = ?h x" "\<forall>x\<in>t. g x = ?h x"
6.83 +    by auto
6.84 +  with cont have "continuous_on s ?h" "continuous_on t ?h"
6.85 +    by simp_all
6.86 +  with closed show ?thesis
6.87 +    by (rule continuous_on_closed_Un)
6.88 +qed
6.89 +
6.90  ML {*
6.91
6.92  structure Continuous_On_Intros = Named_Thms
6.93 @@ -1686,6 +1734,10 @@
6.94    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
6.95    unfolding continuous_on_topological by simp metis
6.96
6.97 +lemma continuous_on_compose2:
6.98 +  "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
6.99 +  using continuous_on_compose[of s f g] by (simp add: comp_def)
6.100 +
6.101  subsubsection {* Continuity at a point *}
6.102
6.103  definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
6.104 @@ -1749,6 +1801,12 @@
6.105  lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
6.106    by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
6.107
6.108 +lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
6.109 +  by (simp add: continuous_on_def continuous_at tendsto_within_open)
6.110 +
6.111 +lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
6.112 +  unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
6.113 +
6.114  lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
6.115    by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
6.116
6.117 @@ -1801,8 +1859,101 @@
6.118    using assms unfolding ball_simps[symmetric] SUP_def
6.119    by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
6.120
6.121 +lemma compact_inter_closed [intro]:
6.122 +  assumes "compact s" and "closed t"
6.123 +  shows "compact (s \<inter> t)"
6.124 +proof (rule compactI)
6.125 +  fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
6.126 +  from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
6.127 +  moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
6.128 +  ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
6.129 +    using `compact s` unfolding compact_eq_heine_borel by auto
6.130 +  then guess D ..
6.131 +  then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
6.132 +    by (intro exI[of _ "D - {-t}"]) auto
6.133 +qed
6.134 +
6.135  end
6.136
6.137 +lemma (in t2_space) compact_imp_closed:
6.138 +  assumes "compact s" shows "closed s"
6.139 +unfolding closed_def
6.140 +proof (rule openI)
6.141 +  fix y assume "y \<in> - s"
6.142 +  let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
6.143 +  note `compact s`
6.144 +  moreover have "\<forall>u\<in>?C. open u" by simp
6.145 +  moreover have "s \<subseteq> \<Union>?C"
6.146 +  proof
6.147 +    fix x assume "x \<in> s"
6.148 +    with `y \<in> - s` have "x \<noteq> y" by clarsimp
6.149 +    hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
6.150 +      by (rule hausdorff)
6.151 +    with `x \<in> s` show "x \<in> \<Union>?C"
6.152 +      unfolding eventually_nhds by auto
6.153 +  qed
6.154 +  ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
6.155 +    by (rule compactE)
6.156 +  from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
6.157 +  with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
6.158 +    by (simp add: eventually_Ball_finite)
6.159 +  with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
6.160 +    by (auto elim!: eventually_mono [rotated])
6.161 +  thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
6.162 +    by (simp add: eventually_nhds subset_eq)
6.163 +qed
6.164 +
6.165 +lemma compact_continuous_image:
6.166 +  assumes f: "continuous_on s f" and s: "compact s"
6.167 +  shows "compact (f ` s)"
6.168 +proof (rule compactI)
6.169 +  fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
6.170 +  with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
6.171 +    unfolding continuous_on_open_invariant by blast
6.172 +  then guess A unfolding bchoice_iff .. note A = this
6.173 +  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
6.174 +    by (fastforce simp add: subset_eq set_eq_iff)+
6.175 +  from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
6.176 +  with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
6.177 +    by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
6.178 +qed
6.179 +
6.180 +lemma continuous_on_inv:
6.181 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
6.182 +  assumes "continuous_on s f"  "compact s"  "\<forall>x\<in>s. g (f x) = x"
6.183 +  shows "continuous_on (f ` s) g"
6.184 +unfolding continuous_on_topological
6.185 +proof (clarsimp simp add: assms(3))
6.186 +  fix x :: 'a and B :: "'a set"
6.187 +  assume "x \<in> s" and "open B" and "x \<in> B"
6.188 +  have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
6.189 +    using assms(3) by (auto, metis)
6.190 +  have "continuous_on (s - B) f"
6.191 +    using `continuous_on s f` Diff_subset
6.192 +    by (rule continuous_on_subset)
6.193 +  moreover have "compact (s - B)"
6.194 +    using `open B` and `compact s`
6.195 +    unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
6.196 +  ultimately have "compact (f ` (s - B))"
6.197 +    by (rule compact_continuous_image)
6.198 +  hence "closed (f ` (s - B))"
6.199 +    by (rule compact_imp_closed)
6.200 +  hence "open (- f ` (s - B))"
6.201 +    by (rule open_Compl)
6.202 +  moreover have "f x \<in> - f ` (s - B)"
6.203 +    using `x \<in> s` and `x \<in> B` by (simp add: 1)
6.204 +  moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
6.205 +    by (simp add: 1)
6.206 +  ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
6.207 +    by fast
6.208 +qed
6.209 +
6.210 +lemma continuous_on_inv_into:
6.211 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
6.212 +  assumes s: "continuous_on s f" "compact s" and f: "inj_on f s"
6.213 +  shows "continuous_on (f ` s) (the_inv_into s f)"
6.214 +  by (rule continuous_on_inv[OF s]) (auto simp: the_inv_into_f_f[OF f])
6.215 +
6.216  lemma (in linorder_topology) compact_attains_sup:
6.217    assumes "compact S" "S \<noteq> {}"
6.218    shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
6.219 @@ -1841,21 +1992,6 @@
6.220      by fastforce
6.221  qed
6.222
6.223 -lemma compact_continuous_image:
6.224 -  assumes f: "continuous_on s f" and s: "compact s"
6.225 -  shows "compact (f ` s)"
6.226 -proof (rule compactI)
6.227 -  fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
6.228 -  with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
6.229 -    unfolding continuous_on_open_invariant by blast
6.230 -  then guess A unfolding bchoice_iff .. note A = this
6.231 -  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
6.232 -    by (fastforce simp add: subset_eq set_eq_iff)+
6.233 -  from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
6.234 -  with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
6.235 -    by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
6.236 -qed
6.237 -
6.238  lemma continuous_attains_sup:
6.239    fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
6.240    shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s.  f y \<le> f x)"
```
```     7.1 --- a/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
7.2 +++ b/src/HOL/Transcendental.thy	Fri Mar 22 10:41:43 2013 +0100
7.3 @@ -2457,17 +2457,6 @@
7.4  lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
7.5    using arctan_eq_iff [of x 0] by simp
7.6
7.7 -lemma isCont_inverse_function2: (* generalize with continuous_on *)
7.8 -  fixes f g :: "real \<Rightarrow> real" shows
7.9 -  "\<lbrakk>a < x; x < b;
7.10 -    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
7.11 -    \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
7.12 -   \<Longrightarrow> isCont g (f x)"
7.13 -apply (rule isCont_inverse_function
7.14 -       [where f=f and d="min (x - a) (b - x)"])