--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Apr 26 22:21:03 2010 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Apr 27 10:39:52 2010 -0700
@@ -1659,11 +1659,16 @@
text{* Some other lemmas about sequences. *}
+lemma sequentially_offset:
+ assumes "eventually (\<lambda>i. P i) sequentially"
+ shows "eventually (\<lambda>i. P (i + k)) sequentially"
+ using assms unfolding eventually_sequentially by (metis trans_le_add1)
+
lemma seq_offset:
- fixes l :: "'a::metric_space" (* TODO: generalize *)
- shows "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
- apply (auto simp add: Lim_sequentially)
- by (metis trans_le_add1 )
+ assumes "(f ---> l) sequentially"
+ shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
+ using assms unfolding tendsto_def
+ by clarify (rule sequentially_offset, simp)
lemma seq_offset_neg:
"(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
@@ -3355,24 +3360,23 @@
assume ?lhs thus ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto
qed
-lemma uniformly_continuous_on_sequentially:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
- ((\<lambda>n. x n - y n) ---> 0) sequentially
- \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
+lemma uniformly_continuous_on_sequentially':
+ "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+ ((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially
+ \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs")
proof
assume ?lhs
- { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. x n - y n) ---> 0) sequentially"
+ { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially"
{ fix e::real assume "e>0"
then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
- obtain N where N:"\<forall>n\<ge>N. norm (x n - y n - 0) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
+ obtain N where N:"\<forall>n\<ge>N. dist (x n) (y n) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
{ fix n assume "n\<ge>N"
- hence "norm (f (x n) - f (y n) - 0) < e"
+ hence "dist (f (x n)) (f (y n)) < e"
using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y
- unfolding dist_commute and dist_norm by simp }
- hence "\<exists>N. \<forall>n\<ge>N. norm (f (x n) - f (y n) - 0) < e" by auto }
- hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_norm by auto }
+ unfolding dist_commute by simp }
+ hence "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" by auto }
+ hence "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially" unfolding Lim_sequentially and dist_real_def by auto }
thus ?rhs by auto
next
assume ?rhs
@@ -3385,21 +3389,28 @@
def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
have xyn:"\<forall>n. x n \<in> s \<and> y n \<in> s" and xy0:"\<forall>n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\<forall>n. \<not> dist (f (x n)) (f (y n)) < e"
unfolding x_def and y_def using fa by auto
- have 1:"\<And>(x::'a) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
- have 2:"\<And>(x::'b) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
{ fix e::real assume "e>0"
then obtain N::nat where "N \<noteq> 0" and N:"0 < inverse (real N) \<and> inverse (real N) < e" unfolding real_arch_inv[of e] by auto
{ fix n::nat assume "n\<ge>N"
hence "inverse (real n + 1) < inverse (real N)" using real_of_nat_ge_zero and `N\<noteq>0` by auto
also have "\<dots> < e" using N by auto
finally have "inverse (real n + 1) < e" by auto
- hence "dist (x n - y n) 0 < e" unfolding 1 using xy0[THEN spec[where x=n]] by auto }
- hence "\<exists>N. \<forall>n\<ge>N. dist (x n - y n) 0 < e" by auto }
- hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n) - f (y n)) 0 < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially by auto
- hence False unfolding 2 using fxy and `e>0` by auto }
+ hence "dist (x n) (y n) < e" using xy0[THEN spec[where x=n]] by auto }
+ hence "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto }
+ hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially dist_real_def by auto
+ hence False using fxy and `e>0` by auto }
thus ?lhs unfolding uniformly_continuous_on_def by blast
qed
+lemma uniformly_continuous_on_sequentially:
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+ shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+ ((\<lambda>n. x n - y n) ---> 0) sequentially
+ \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
+(* BH: maybe the previous lemma should replace this one? *)
+unfolding uniformly_continuous_on_sequentially'
+unfolding dist_norm Lim_null_norm [symmetric] ..
+
text{* The usual transformation theorems. *}
lemma continuous_transform_within:
@@ -3497,8 +3508,7 @@
unfolding uniformly_continuous_on_def by simp
lemma uniformly_continuous_on_cmul:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- (* FIXME: generalize 'a to metric_space *)
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes "uniformly_continuous_on s f"
shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
proof-
@@ -3507,7 +3517,8 @@
using Lim_cmul[of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
}
- thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
+ thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
+ unfolding dist_norm Lim_null_norm [symmetric] by auto
qed
lemma dist_minus:
@@ -3522,7 +3533,7 @@
unfolding uniformly_continuous_on_def dist_minus .
lemma uniformly_continuous_on_add:
- fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
+ fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
proof-
@@ -3531,11 +3542,12 @@
hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
using Lim_add[of "\<lambda> n. f (x n) - f (y n)" 0 sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto }
- thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
+ thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
+ unfolding dist_norm Lim_null_norm [symmetric] by auto
qed
lemma uniformly_continuous_on_sub:
- fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
==> uniformly_continuous_on s (\<lambda>x. f x - g x)"
unfolding ab_diff_minus
@@ -3562,25 +3574,21 @@
text{* Continuity of all kinds is preserved under composition. *}
+lemma continuous_within_topological:
+ "continuous (at x within s) f \<longleftrightarrow>
+ (\<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)))"
+unfolding continuous_within
+unfolding tendsto_def Limits.eventually_within eventually_at_topological
+by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
+
lemma continuous_within_compose:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
- fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
- assumes "continuous (at x within s) f" "continuous (at (f x) within f ` s) g"
+ assumes "continuous (at x within s) f"
+ assumes "continuous (at (f x) within f ` s) g"
shows "continuous (at x within s) (g o f)"
-proof-
- { fix e::real assume "e>0"
- with assms(2)[unfolded continuous_within Lim_within] obtain d where "d>0" and d:"\<forall>xa\<in>f ` s. 0 < dist xa (f x) \<and> dist xa (f x) < d \<longrightarrow> dist (g xa) (g (f x)) < e" by auto
- from assms(1)[unfolded continuous_within Lim_within] obtain d' where "d'>0" and d':"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < d" using `d>0` by auto
- { fix y assume as:"y\<in>s" "0 < dist y x" "dist y x < d'"
- hence "dist (f y) (f x) < d" using d'[THEN bspec[where x=y]] by (auto simp add:dist_commute)
- hence "dist (g (f y)) (g (f x)) < e" using as(1) d[THEN bspec[where x="f y"]] unfolding dist_nz[THEN sym] using `e>0` by auto }
- hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (g (f xa)) (g (f x)) < e" using `d'>0` by auto }
- thus ?thesis unfolding continuous_within Lim_within by auto
-qed
+using assms unfolding continuous_within_topological by simp metis
lemma continuous_at_compose:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
- fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
assumes "continuous (at x) f" "continuous (at (f x)) g"
shows "continuous (at x) (g o f)"
proof-
@@ -3606,75 +3614,55 @@
text{* Continuity in terms of open preimages. *}
lemma continuous_at_open:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
- shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
-proof
- assume ?lhs
- { fix t assume as: "open t" "f x \<in> t"
- then obtain e where "e>0" and e:"ball (f x) e \<subseteq> t" unfolding open_contains_ball by auto
-
- obtain d where "d>0" and d:"\<forall>y. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e" using `e>0` using `?lhs`[unfolded continuous_at Lim_at open_dist] by auto
-
- have "open (ball x d)" using open_ball by auto
- moreover have "x \<in> ball x d" unfolding centre_in_ball using `d>0` by simp
- moreover
- { fix x' assume "x'\<in>ball x d" hence "f x' \<in> t"
- using e[unfolded subset_eq Ball_def mem_ball, THEN spec[where x="f x'"]] d[THEN spec[where x=x']]
- unfolding mem_ball apply (auto simp add: dist_commute)
- unfolding dist_nz[THEN sym] using as(2) by auto }
- hence "\<forall>x'\<in>ball x d. f x' \<in> t" by auto
- ultimately have "\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x'\<in>s. f x' \<in> t)"
- apply(rule_tac x="ball x d" in exI) by simp }
- thus ?rhs by auto
-next
- assume ?rhs
- { fix e::real assume "e>0"
- then obtain s where s: "open s" "x \<in> s" "\<forall>x'\<in>s. f x' \<in> ball (f x) e" using `?rhs`[unfolded continuous_at Lim_at, THEN spec[where x="ball (f x) e"]]
- unfolding centre_in_ball[of "f x" e, THEN sym] by auto
- then obtain d where "d>0" and d:"ball x d \<subseteq> s" unfolding open_contains_ball by auto
- { fix y assume "0 < dist y x \<and> dist y x < d"
- hence "dist (f y) (f x) < e" using d[unfolded subset_eq Ball_def mem_ball, THEN spec[where x=y]]
- using s(3)[THEN bspec[where x=y], unfolded mem_ball] by (auto simp add: dist_commute) }
- hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `d>0` by auto }
- thus ?lhs unfolding continuous_at Lim_at by auto
-qed
+ shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
+unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
+unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
lemma continuous_on_open:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
- shows "continuous_on s f \<longleftrightarrow>
+ shows "continuous_on s f \<longleftrightarrow>
(\<forall>t. openin (subtopology euclidean (f ` s)) t
--> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
-proof
- assume ?lhs
- { fix t assume as:"openin (subtopology euclidean (f ` s)) t"
- have "{x \<in> s. f x \<in> t} \<subseteq> s" using as[unfolded openin_euclidean_subtopology_iff] by auto
- moreover
- { fix x assume as':"x\<in>{x \<in> s. f x \<in> t}"
- then obtain e where e: "e>0" "\<forall>x'\<in>f ` s. dist x' (f x) < e \<longrightarrow> x' \<in> t" using as[unfolded openin_euclidean_subtopology_iff, THEN conjunct2, THEN bspec[where x="f x"]] by auto
- from this(1) obtain d where d: "d>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `?lhs`[unfolded continuous_on Lim_within, THEN bspec[where x=x]] using as' by auto
- have "\<exists>e>0. \<forall>x'\<in>s. dist x' x < e \<longrightarrow> x' \<in> {x \<in> s. f x \<in> t}" using d e unfolding dist_nz[THEN sym] by (rule_tac x=d in exI, auto) }
- ultimately have "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" unfolding openin_euclidean_subtopology_iff by auto }
- thus ?rhs unfolding continuous_on Lim_within using openin by auto
+proof (safe)
+ fix t :: "'b set"
+ assume 1: "continuous_on s f"
+ assume 2: "openin (subtopology euclidean (f ` s)) t"
+ from 2 obtain B where B: "open B" and t: "t = f ` s \<inter> B"
+ unfolding openin_open by auto
+ def U == "\<Union>{A. open A \<and> (\<forall>x\<in>s. x \<in> A \<longrightarrow> f x \<in> B)}"
+ have "open U" unfolding U_def by (simp add: open_Union)
+ moreover have "\<forall>x\<in>s. x \<in> U \<longleftrightarrow> f x \<in> t"
+ proof (intro ballI iffI)
+ fix x assume "x \<in> s" and "x \<in> U" thus "f x \<in> t"
+ unfolding U_def t by auto
+ next
+ fix x assume "x \<in> s" and "f x \<in> t"
+ hence "x \<in> s" and "f x \<in> B"
+ unfolding t by auto
+ with 1 B obtain A where "open A" "x \<in> A" "\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B"
+ unfolding t continuous_on_topological by metis
+ then show "x \<in> U"
+ unfolding U_def by auto
+ qed
+ ultimately have "open U \<and> {x \<in> s. f x \<in> t} = s \<inter> U" by auto
+ then show "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
+ unfolding openin_open by fast
next
- assume ?rhs
- { fix e::real and x assume "x\<in>s" "e>0"
- { fix xa x' assume "dist (f xa) (f x) < e" "xa \<in> s" "x' \<in> s" "dist (f xa) (f x') < e - dist (f xa) (f x)"
- hence "dist (f x') (f x) < e" using dist_triangle[of "f x'" "f x" "f xa"]
- by (auto simp add: dist_commute) }
- hence "ball (f x) e \<inter> f ` s \<subseteq> f ` s \<and> (\<forall>xa\<in>ball (f x) e \<inter> f ` s. \<exists>ea>0. \<forall>x'\<in>f ` s. dist x' xa < ea \<longrightarrow> x' \<in> ball (f x) e \<inter> f ` s)" apply auto
- apply(rule_tac x="e - dist (f xa) (f x)" in exI) using `e>0` by (auto simp add: dist_commute)
- hence "\<forall>xa\<in>{xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}. \<exists>ea>0. \<forall>x'\<in>s. dist x' xa < ea \<longrightarrow> x' \<in> {xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}"
- using `?rhs`[unfolded openin_euclidean_subtopology_iff, THEN spec[where x="ball (f x) e \<inter> f ` s"]] by auto
- hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" apply(erule_tac x=x in ballE) apply auto using `e>0` `x\<in>s` by (auto simp add: dist_commute) }
- thus ?lhs unfolding continuous_on Lim_within by auto
-qed
-
-(* ------------------------------------------------------------------------- *)
-(* Similarly in terms of closed sets. *)
-(* ------------------------------------------------------------------------- *)
+ assume "?rhs" show "continuous_on s f"
+ unfolding continuous_on_topological
+ proof (clarify)
+ fix x and B assume "x \<in> s" and "open B" and "f x \<in> B"
+ have "openin (subtopology euclidean (f ` s)) (f ` s \<inter> B)"
+ unfolding openin_open using `open B` by auto
+ then have "openin (subtopology euclidean s) {x \<in> s. f x \<in> f ` s \<inter> B}"
+ using `?rhs` by fast
+ then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
+ unfolding openin_open using `x \<in> s` and `f x \<in> B` by auto
+ qed
+qed
+
+text {* Similarly in terms of closed sets. *}
lemma continuous_on_closed:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
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")
proof
assume ?lhs
@@ -3699,7 +3687,6 @@
text{* Half-global and completely global cases. *}
lemma continuous_open_in_preimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "open t"
shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof-
@@ -3710,7 +3697,6 @@
qed
lemma continuous_closed_in_preimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "closed t"
shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof-
@@ -3722,7 +3708,6 @@
qed
lemma continuous_open_preimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "open s" "open t"
shows "open {x \<in> s. f x \<in> t}"
proof-
@@ -3732,7 +3717,6 @@
qed
lemma continuous_closed_preimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "closed s" "closed t"
shows "closed {x \<in> s. f x \<in> t}"
proof-
@@ -3742,26 +3726,22 @@
qed
lemma continuous_open_preimage_univ:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_closed_preimage_univ:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_open_vimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
unfolding vimage_def by (rule continuous_open_preimage_univ)
lemma continuous_closed_vimage:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
unfolding vimage_def by (rule continuous_closed_preimage_univ)
-lemma interior_image_subset: fixes f::"_::metric_space \<Rightarrow> _::metric_space"
+lemma interior_image_subset:
assumes "\<forall>x. continuous (at x) f" "inj f"
shows "interior (f ` s) \<subseteq> f ` (interior s)"
apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
@@ -3775,17 +3755,17 @@
text{* Equality of continuous functions on closure and related results. *}
lemma continuous_closed_in_preimage_constant:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
using continuous_closed_in_preimage[of s f "{a}"] closed_sing by auto
lemma continuous_closed_preimage_constant:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
shows "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
using continuous_closed_preimage[of s f "{a}"] closed_sing by auto
lemma continuous_constant_on_closure:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
assumes "continuous_on (closure s) f"
"\<forall>x \<in> s. f x = a"
shows "\<forall>x \<in> (closure s). f x = a"
@@ -3793,7 +3773,6 @@
assms closure_minimal[of s "{x \<in> closure s. f x = a}"] closure_subset unfolding subset_eq by auto
lemma image_closure_subset:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on (closure s) f" "closed t" "(f ` s) \<subseteq> t"
shows "f ` (closure s) \<subseteq> t"
proof-
@@ -3852,14 +3831,14 @@
text{* Proving a function is constant by proving open-ness of level set. *}
lemma continuous_levelset_open_in_cases:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a}
==> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> s. f x = a)"
unfolding connected_clopen using continuous_closed_in_preimage_constant by auto
lemma continuous_levelset_open_in:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
(\<exists>x \<in> s. f x = a) ==> (\<forall>x \<in> s. f x = a)"
@@ -3867,7 +3846,7 @@
by meson
lemma continuous_levelset_open:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
assumes "connected s" "continuous_on s f" "open {x \<in> s. f x = a}" "\<exists>x \<in> s. f x = a"
shows "\<forall>x \<in> s. f x = a"
using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
@@ -4033,11 +4012,10 @@
unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
lemma bilinear_continuous_on_compose:
- fixes s :: "'a::metric_space set" (* TODO: generalize *)
shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
==> continuous_on s (\<lambda>x. h (f x) (g x))"
- unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
- using bilinear_continuous_within_compose[of _ s f g h] by auto
+ unfolding continuous_on_def
+ by (fast elim: bounded_bilinear.tendsto)
text {* Preservation of compactness and connectedness under continuous function. *}
@@ -4058,7 +4036,6 @@
qed
lemma connected_continuous_image:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "connected s"
shows "connected(f ` s)"
proof-
@@ -4206,10 +4183,8 @@
lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
unfolding continuous_at by (intro tendsto_intros)
-lemma continuous_on_component:
- fixes s :: "('a::metric_space ^ 'n) set" (* TODO: generalize *)
- shows "continuous_on s (\<lambda>x. x $ i)"
-unfolding continuous_on by (intro ballI tendsto_intros)
+lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
+unfolding continuous_on_def by (intro ballI tendsto_intros)
lemma continuous_at_infnorm: "continuous (at x) infnorm"
unfolding continuous_at Lim_at o_def unfolding dist_norm