src/HOL/Topological_Spaces.thy
changeset 60150 bd773c47ad0b
parent 60040 1fa1023b13b9
child 60172 423273355b55
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue Apr 28 16:23:05 2015 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Apr 28 16:23:38 2015 +0100
     1.3 @@ -1479,14 +1479,6 @@
     1.4  lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
     1.5    by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
     1.6  
     1.7 -lemma isContI_continuous: "continuous (at x within UNIV) f \<Longrightarrow> isCont f x"
     1.8 -  by simp
     1.9 -
    1.10 -lemma isCont_ident[continuous_intros, simp]: "isCont (\<lambda>x. x) a"
    1.11 -  using continuous_ident by (rule isContI_continuous)
    1.12 -
    1.13 -lemmas isCont_const = continuous_const
    1.14 -
    1.15  lemma isCont_o2: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (\<lambda>x. g (f x)) a"
    1.16    unfolding isCont_def by (rule tendsto_compose)
    1.17