3177 "'a::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where |
3177 "'a::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where |
3178 "uniformly_continuous_on s f \<longleftrightarrow> |
3178 "uniformly_continuous_on s f \<longleftrightarrow> |
3179 (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall> x'\<in>s. dist x' x < d |
3179 (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall> x'\<in>s. dist x' x < d |
3180 --> dist (f x') (f x) < e)" |
3180 --> dist (f x') (f x) < e)" |
3181 |
3181 |
|
3182 |
|
3183 text{* Lifting and dropping *} |
|
3184 |
|
3185 lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector" |
|
3186 assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)" |
|
3187 using assms unfolding continuous_on_def apply safe |
|
3188 apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe |
|
3189 apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real |
|
3190 apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def) |
|
3191 |
|
3192 lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector" |
|
3193 assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)" |
|
3194 using assms unfolding continuous_on_def apply safe |
|
3195 apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe |
|
3196 apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real |
|
3197 apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def) |
|
3198 |
3182 text{* Some simple consequential lemmas. *} |
3199 text{* Some simple consequential lemmas. *} |
3183 |
3200 |
3184 lemma uniformly_continuous_imp_continuous: |
3201 lemma uniformly_continuous_imp_continuous: |
3185 " uniformly_continuous_on s f ==> continuous_on s f" |
3202 " uniformly_continuous_on s f ==> continuous_on s f" |
3186 unfolding uniformly_continuous_on_def continuous_on_def by blast |
3203 unfolding uniformly_continuous_on_def continuous_on_def by blast |
3705 |
3722 |
3706 lemma continuous_closed_vimage: |
3723 lemma continuous_closed_vimage: |
3707 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *) |
3724 fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *) |
3708 shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)" |
3725 shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)" |
3709 unfolding vimage_def by (rule continuous_closed_preimage_univ) |
3726 unfolding vimage_def by (rule continuous_closed_preimage_univ) |
|
3727 |
|
3728 lemma interior_image_subset: fixes f::"_::metric_space \<Rightarrow> _::metric_space" |
|
3729 assumes "\<forall>x. continuous (at x) f" "inj f" |
|
3730 shows "interior (f ` s) \<subseteq> f ` (interior s)" |
|
3731 apply rule unfolding interior_def mem_Collect_eq image_iff apply safe |
|
3732 proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s" |
|
3733 hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this |
|
3734 thus "\<exists>xa\<in>{x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> s}. x = f xa" apply(rule_tac x=y in bexI) using assms as |
|
3735 apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ) |
|
3736 proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto |
|
3737 thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed |
3710 |
3738 |
3711 text{* Equality of continuous functions on closure and related results. *} |
3739 text{* Equality of continuous functions on closure and related results. *} |
3712 |
3740 |
3713 lemma continuous_closed_in_preimage_constant: |
3741 lemma continuous_closed_in_preimage_constant: |
3714 "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}" |
3742 "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}" |