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
```