src/HOL/Topological_Spaces.thy
changeset 60762 bf0c76ccee8d
parent 60758 d8d85a8172b5
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Topological_Spaces.thy	Mon Jul 20 11:40:43 2015 +0200
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Jul 20 23:12:50 2015 +0100
     1.3 @@ -1526,7 +1526,7 @@
     1.4  lemma isCont_def: "isCont f a \<longleftrightarrow> f -- a --> f a"
     1.5    by (rule continuous_at)
     1.6  
     1.7 -lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
     1.8 +lemma continuous_at_imp_continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
     1.9    by (auto intro: tendsto_mono at_le simp: continuous_at continuous_within)
    1.10  
    1.11  lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
    1.12 @@ -1536,7 +1536,7 @@
    1.13    unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
    1.14  
    1.15  lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
    1.16 -  by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
    1.17 +  by (auto intro: continuous_at_imp_continuous_at_within simp: continuous_on_eq_continuous_within)
    1.18  
    1.19  lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
    1.20    unfolding isCont_def by (rule tendsto_compose)
    1.21 @@ -1549,7 +1549,7 @@
    1.22  
    1.23  lemma continuous_within_compose3:
    1.24    "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
    1.25 -  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within)
    1.26 +  using continuous_within_compose2[of x s f g] by (simp add: continuous_at_imp_continuous_at_within)
    1.27  
    1.28  lemma filtermap_nhds_open_map:
    1.29    assumes cont: "isCont f a" and open_map: "\<And>S. open S \<Longrightarrow> open (f`S)"