src/HOL/Topological_Spaces.thy
changeset 62049 b0f941e207cf
parent 61976 3a27957ac658
child 62083 7582b39f51ed
     1.1 --- a/src/HOL/Topological_Spaces.thy	Sun Jan 03 21:45:34 2016 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Jan 04 17:45:36 2016 +0100
     1.3 @@ -1621,6 +1621,23 @@
     1.4  
     1.5  lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
     1.6    unfolding isCont_def by (rule tendsto_compose)
     1.7 +  
     1.8 +lemma continuous_on_tendsto_compose:
     1.9 +  assumes f_cont: "continuous_on s f"
    1.10 +  assumes g: "(g \<longlongrightarrow> l) F"
    1.11 +  assumes l: "l \<in> s"
    1.12 +  assumes ev: "\<forall>\<^sub>F x in F. g x \<in> s"
    1.13 +  shows "((\<lambda>x. f (g x)) \<longlongrightarrow> f l) F"
    1.14 +proof -
    1.15 +  from f_cont l have f: "(f \<longlongrightarrow> f l) (at l within s)"
    1.16 +    by (simp add: continuous_on_def)
    1.17 +  have i: "((\<lambda>x. if g x = l then f l else f (g x)) \<longlongrightarrow> f l) F"
    1.18 +    by (rule filterlim_If)
    1.19 +       (auto intro!: filterlim_compose[OF f] eventually_conj tendsto_mono[OF _ g]
    1.20 +             simp: filterlim_at eventually_inf_principal eventually_mono[OF ev])
    1.21 +  show ?thesis
    1.22 +    by (rule filterlim_cong[THEN iffD1[OF _ i]]) auto
    1.23 +qed
    1.24  
    1.25  lemma continuous_within_compose3:
    1.26    "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"