src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 57448 159e45728ceb
parent 57447 87429bdecad5
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 30 15:45:21 2014 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 30 15:45:25 2014 +0200
     1.3 @@ -4616,41 +4616,31 @@
     1.4    using continuous_within_eps_delta [of x UNIV f] by simp
     1.5  
     1.6  lemma continuous_at_right_real_increasing:
     1.7 -  assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
     1.8 -  shows "(continuous (at_right (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f (a + delta) - f a < e)"
     1.9 -  apply (auto simp add: continuous_within_eps_delta dist_real_def greaterThan_def)
    1.10 -  apply (drule_tac x = e in spec, auto)
    1.11 -  apply (drule_tac x = "a + d / 2" in spec)
    1.12 -  apply (subst (asm) abs_of_nonneg)
    1.13 -  apply (auto intro: nondecF simp add: field_simps)
    1.14 -  apply (rule_tac x = "d / 2" in exI)
    1.15 -  apply (auto simp add: field_simps)
    1.16 -  apply (drule_tac x = e in spec, auto)
    1.17 -  apply (rule_tac x = delta in exI, auto)
    1.18 -  apply (subst abs_of_nonneg)
    1.19 -  apply (auto intro: nondecF simp add: field_simps)
    1.20 -  apply (rule le_less_trans)
    1.21 -  prefer 2 apply assumption
    1.22 -by (rule nondecF, auto)
    1.23 +  fixes f :: "real \<Rightarrow> real"
    1.24 +  assumes nondecF: "\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y"
    1.25 +  shows "continuous (at_right a) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f (a + d) - f a < e)"
    1.26 +  apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)
    1.27 +  apply (intro all_cong ex_cong)
    1.28 +  apply safe
    1.29 +  apply (erule_tac x="a + d" in allE)
    1.30 +  apply simp
    1.31 +  apply (simp add: nondecF field_simps)
    1.32 +  apply (drule nondecF)
    1.33 +  apply simp
    1.34 +  done
    1.35  
    1.36  lemma continuous_at_left_real_increasing:
    1.37    assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
    1.38    shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"
    1.39 -  apply (auto simp add: continuous_within_eps_delta dist_real_def lessThan_def)
    1.40 -  apply (drule_tac x = e in spec, auto)
    1.41 -  apply (drule_tac x = "a - d / 2" in spec)
    1.42 -  apply (subst (asm) abs_of_nonpos)
    1.43 -  apply (auto intro: nondecF simp add: field_simps)
    1.44 -  apply (rule_tac x = "d / 2" in exI)
    1.45 -  apply (auto simp add: field_simps)
    1.46 -  apply (drule_tac x = e in spec, auto)
    1.47 -  apply (rule_tac x = delta in exI, auto)
    1.48 -  apply (subst abs_of_nonpos)
    1.49 -  apply (auto intro: nondecF simp add: field_simps)
    1.50 -  apply (rule less_le_trans)
    1.51 -  apply assumption
    1.52 -  apply auto
    1.53 -by (rule nondecF, auto)
    1.54 +  apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)
    1.55 +  apply (intro all_cong ex_cong)
    1.56 +  apply safe
    1.57 +  apply (erule_tac x="a - d" in allE)
    1.58 +  apply simp
    1.59 +  apply (simp add: nondecF field_simps)
    1.60 +  apply (cut_tac x="a - d" and y="x" in nondecF)
    1.61 +  apply simp_all
    1.62 +  done
    1.63  
    1.64  text{* Versions in terms of open balls. *}
    1.65