1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 17 17:57:37 2010 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Feb 17 18:33:45 2010 +0100
     1.3 @@ -3179,6 +3179,23 @@
     1.4          (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall> x'\<in>s. dist x' x < d
     1.5                             --> dist (f x') (f x) < e)"
     1.6  
     1.7 +
     1.8 +text{* Lifting and dropping *}
     1.9 +
    1.10 +lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
    1.11 +  assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
    1.12 +  using assms unfolding continuous_on_def apply safe
    1.13 +  apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
    1.14 +  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
    1.15 +  apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
    1.16 +
    1.17 +lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
    1.18 +  assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
    1.19 +  using assms unfolding continuous_on_def apply safe
    1.20 +  apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
    1.21 +  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
    1.22 +  apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
    1.23 +
    1.24  text{* Some simple consequential lemmas. *}
    1.25  
    1.26  lemma uniformly_continuous_imp_continuous:
    1.27 @@ -3708,6 +3725,17 @@
    1.28    shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
    1.29    unfolding vimage_def by (rule continuous_closed_preimage_univ)
    1.30  
    1.31 +lemma interior_image_subset: fixes f::"_::metric_space \<Rightarrow> _::metric_space"
    1.32 +  assumes "\<forall>x. continuous (at x) f" "inj f"
    1.33 +  shows "interior (f ` s) \<subseteq> f ` (interior s)"
    1.34 +  apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
    1.35 +proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s" 
    1.36 +  hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this
    1.37 +  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
    1.38 +    apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ)
    1.39 +  proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
    1.40 +    thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
    1.41 +
    1.42  text{* Equality of continuous functions on closure and related results.          *}
    1.43  
    1.44  lemma continuous_closed_in_preimage_constant: