author huffman Tue Aug 16 09:31:23 2011 -0700 (2011-08-16) changeset 44233 aa74ce315bae parent 44229 7e3a026f014f child 44234 17ae4af434aa
```     1.1 --- a/src/HOL/Deriv.thy	Tue Aug 16 13:07:52 2011 -0700
1.2 +++ b/src/HOL/Deriv.thy	Tue Aug 16 09:31:23 2011 -0700
1.3 @@ -670,7 +670,7 @@
1.4        |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
1.5  apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
1.6  apply (drule IVT [where f = "%x. - f x"], assumption)
1.7 -apply (auto intro: isCont_minus)
1.8 +apply simp_all
1.9  done
1.10
1.11  (*HOL style here: object-level formulations*)
1.12 @@ -750,7 +750,7 @@
1.13        with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
1.14          by (fastsimp simp add: linorder_not_le [symmetric])
1.15        hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
1.16 -        by (auto simp add: isCont_inverse isCont_diff con)
1.17 +        by (auto simp add: con)
1.18        from isCont_bounded [OF le this]
1.19        obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
1.20        have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
1.21 @@ -1059,8 +1059,8 @@
1.22                     (f(b) - f(a) = (b-a) * l)"
1.23  proof -
1.24    let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
1.25 -  have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
1.26 -    by (fast intro: isCont_diff isCont_const isCont_mult isCont_ident)
1.27 +  have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
1.28 +    using con by (fast intro: isCont_intros)
1.29    have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
1.30    proof (clarify)
1.31      fix x::real
1.32 @@ -1353,7 +1353,7 @@
1.33        ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
1.34  apply (insert lemma_isCont_inj
1.35            [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
1.36 -apply (simp add: isCont_minus linorder_not_le)
1.38  done
1.39
1.40  text{*Show there's an interval surrounding @{term "f(x)"} in
1.41 @@ -1509,27 +1509,9 @@
1.42    let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
1.43    from assms have "a < b" by simp
1.44    moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
1.45 -  proof -
1.46 -    have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
1.47 -    with gc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (f b - f a) * g x) x"
1.48 -      by (auto intro: isCont_mult)
1.49 -    moreover
1.50 -    have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. g b - g a) x" by simp
1.51 -    with fc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (g b - g a) * f x) x"
1.52 -      by (auto intro: isCont_mult)
1.53 -    ultimately show ?thesis
1.54 -      by (fastsimp intro: isCont_diff)
1.55 -  qed
1.56 -  moreover
1.57 -  have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
1.58 -  proof -
1.59 -    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by simp
1.60 -    with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by simp
1.61 -    moreover
1.62 -    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by simp
1.63 -    with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by simp
1.64 -    ultimately show ?thesis by simp
1.65 -  qed
1.66 +    using fc gc by simp
1.67 +  moreover have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
1.68 +    using fd gd by simp
1.69    ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
1.70    then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
1.71    then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
```
```     2.1 --- a/src/HOL/Library/Inner_Product.thy	Tue Aug 16 13:07:52 2011 -0700
2.2 +++ b/src/HOL/Library/Inner_Product.thy	Tue Aug 16 09:31:23 2011 -0700
2.3 @@ -175,6 +175,8 @@
2.4    bounded_linear "\<lambda>y::'a::real_inner. inner x y"
2.5    by (rule inner.bounded_linear_right)
2.6
2.7 +declare inner.isCont [simp]
2.8 +
2.9
2.10  subsection {* Class instances *}
2.11
```
```     3.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Aug 16 13:07:52 2011 -0700
3.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 16 09:31:23 2011 -0700
3.3 @@ -359,6 +359,16 @@
3.4         (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
3.5  qed
3.6
3.7 +lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
3.8 +  unfolding isCont_def by (rule tendsto_fst)
3.9 +
3.10 +lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
3.11 +  unfolding isCont_def by (rule tendsto_snd)
3.12 +
3.13 +lemma isCont_Pair [simp]:
3.14 +  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
3.15 +  unfolding isCont_def by (rule tendsto_Pair)
3.16 +
3.17  lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
3.18  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
3.19
3.20 @@ -381,10 +391,6 @@
3.21    then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
3.22  qed
3.23
3.24 -lemma isCont_Pair [simp]:
3.25 -  "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
3.26 -  unfolding isCont_def by (rule tendsto_Pair)
3.27 -
3.28  subsection {* Product is a complete metric space *}
3.29
3.30  instance prod :: (complete_space, complete_space) complete_space
```
```     4.1 --- a/src/HOL/Lim.thy	Tue Aug 16 13:07:52 2011 -0700
4.2 +++ b/src/HOL/Lim.thy	Tue Aug 16 09:31:23 2011 -0700
4.3 @@ -321,9 +321,6 @@
4.4    "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
4.5  by (rule tendsto)
4.6
4.7 -lemma (in bounded_linear) cont: "f -- a --> f a"
4.8 -by (rule LIM [OF LIM_ident])
4.9 -
4.10  lemma (in bounded_linear) LIM_zero:
4.11    "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
4.12    by (rule tendsto_zero)
4.13 @@ -401,39 +398,46 @@
4.14  lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
4.15    unfolding isCont_def by (rule LIM_const)
4.16
4.17 -lemma isCont_norm:
4.18 +lemma isCont_norm [simp]:
4.19    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
4.20    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
4.21    unfolding isCont_def by (rule LIM_norm)
4.22
4.23 -lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a"
4.24 +lemma isCont_rabs [simp]:
4.25 +  fixes f :: "'a::topological_space \<Rightarrow> real"
4.26 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
4.27    unfolding isCont_def by (rule LIM_rabs)
4.28
4.31    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
4.32    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
4.33    unfolding isCont_def by (rule LIM_add)
4.34
4.35 -lemma isCont_minus:
4.36 +lemma isCont_minus [simp]:
4.37    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
4.38    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
4.39    unfolding isCont_def by (rule LIM_minus)
4.40
4.41 -lemma isCont_diff:
4.42 +lemma isCont_diff [simp]:
4.43    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
4.44    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
4.45    unfolding isCont_def by (rule LIM_diff)
4.46
4.47 -lemma isCont_mult:
4.48 +lemma isCont_mult [simp]:
4.49    fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
4.50    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
4.51    unfolding isCont_def by (rule LIM_mult)
4.52
4.53 -lemma isCont_inverse:
4.54 +lemma isCont_inverse [simp]:
4.55    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
4.56    shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
4.57    unfolding isCont_def by (rule LIM_inverse)
4.58
4.59 +lemma isCont_divide [simp]:
4.60 +  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
4.61 +  shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
4.62 +  unfolding isCont_def by (rule tendsto_divide)
4.63 +
4.64  lemma isCont_LIM_compose:
4.65    "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
4.66    unfolding isCont_def by (rule LIM_compose)
4.67 @@ -459,37 +463,40 @@
4.68  lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
4.69    unfolding o_def by (rule isCont_o2)
4.70
4.71 -lemma (in bounded_linear) isCont: "isCont f a"
4.72 -  unfolding isCont_def by (rule cont)
4.73 +lemma (in bounded_linear) isCont:
4.74 +  "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
4.75 +  unfolding isCont_def by (rule LIM)
4.76
4.77  lemma (in bounded_bilinear) isCont:
4.78    "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
4.79    unfolding isCont_def by (rule LIM)
4.80
4.81 -lemmas isCont_scaleR = scaleR.isCont
4.82 +lemmas isCont_scaleR [simp] = scaleR.isCont
4.83
4.84 -lemma isCont_of_real:
4.85 +lemma isCont_of_real [simp]:
4.86    "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
4.87 -  unfolding isCont_def by (rule LIM_of_real)
4.88 +  by (rule of_real.isCont)
4.89
4.90 -lemma isCont_power:
4.91 +lemma isCont_power [simp]:
4.92    fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
4.93    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
4.94    unfolding isCont_def by (rule LIM_power)
4.95
4.96 -lemma isCont_sgn:
4.97 +lemma isCont_sgn [simp]:
4.98    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
4.99    shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
4.100    unfolding isCont_def by (rule LIM_sgn)
4.101
4.102 -lemma isCont_abs [simp]: "isCont abs (a::real)"
4.103 -by (rule isCont_rabs [OF isCont_ident])
4.104 +lemma isCont_setsum [simp]:
4.105 +  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
4.106 +  fixes A :: "'a set"
4.107 +  shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
4.108 +  unfolding isCont_def by (simp add: tendsto_setsum)
4.109
4.110 -lemma isCont_setsum:
4.111 -  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
4.112 -  fixes A :: "'a set" assumes "finite A"
4.113 -  shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
4.114 -  unfolding isCont_def by (simp add: tendsto_setsum)
4.115 +lemmas isCont_intros =
4.116 +  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
4.117 +  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
4.118 +  isCont_of_real isCont_power isCont_sgn isCont_setsum
4.119
4.120  lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
4.121    and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
```
```     5.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 16 13:07:52 2011 -0700
5.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 16 09:31:23 2011 -0700
5.3 @@ -1100,8 +1100,7 @@
5.4  unfolding continuous_on_def by (intro ballI tendsto_intros)
5.5
5.6  lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x\$i}"
5.7 -  unfolding Collect_all_eq
5.8 -  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
5.9 +  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
5.10
5.11  lemma Lim_component_cart:
5.12    fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
5.13 @@ -1287,13 +1286,11 @@
5.14
5.15  lemma closed_interval_left_cart: fixes b::"real^'n"
5.16    shows "closed {x::real^'n. \<forall>i. x\$i \<le> b\$i}"
5.17 -  unfolding Collect_all_eq
5.18 -  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
5.19 +  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
5.20
5.21  lemma closed_interval_right_cart: fixes a::"real^'n"
5.22    shows "closed {x::real^'n. \<forall>i. a\$i \<le> x\$i}"
5.23 -  unfolding Collect_all_eq
5.24 -  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
5.25 +  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
5.26
5.27  lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
5.28    (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a\$i \<le> x\$i \<and> x\$i \<le> b\$i) \<or> (b\$i \<le> x\$i \<and> x\$i \<le> a\$i))) \<longrightarrow> x \<in> s)"
5.29 @@ -1301,19 +1298,19 @@
5.30
5.31  lemma closed_halfspace_component_le_cart:
5.32    shows "closed {x::real^'n. x\$i \<le> a}"
5.33 -  by (intro closed_Collect_le vec_nth.isCont isCont_const)
5.34 +  by (simp add: closed_Collect_le)
5.35
5.36  lemma closed_halfspace_component_ge_cart:
5.37    shows "closed {x::real^'n. x\$i \<ge> a}"
5.38 -  by (intro closed_Collect_le vec_nth.isCont isCont_const)
5.39 +  by (simp add: closed_Collect_le)
5.40
5.41  lemma open_halfspace_component_lt_cart:
5.42    shows "open {x::real^'n. x\$i < a}"
5.43 -  by (intro open_Collect_less vec_nth.isCont isCont_const)
5.44 +  by (simp add: open_Collect_less)
5.45
5.46  lemma open_halfspace_component_gt_cart:
5.47    shows "open {x::real^'n. x\$i  > a}"
5.48 -  by (intro open_Collect_less vec_nth.isCont isCont_const)
5.49 +  by (simp add: open_Collect_less)
5.50
5.51  lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
5.52    assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)\$i \<le> b) net"
5.53 @@ -1352,8 +1349,7 @@
5.54  proof-
5.55    { fix i::'n
5.56      have "closed {x::'a ^ 'n. P i \<longrightarrow> x\$i = 0}"
5.57 -      by (cases "P i", simp_all,
5.58 -        intro closed_Collect_eq vec_nth.isCont isCont_const) }
5.59 +      by (cases "P i", simp_all add: closed_Collect_eq) }
5.60    thus ?thesis
5.61      unfolding Collect_all_eq by (simp add: closed_INT)
5.62  qed
```
```     6.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 16 13:07:52 2011 -0700
6.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 16 09:31:23 2011 -0700
6.3 @@ -124,6 +124,8 @@
6.4    bounded_linear "\<lambda>x. euclidean_component x i"
6.5    by (rule bounded_linear_euclidean_component)
6.6
6.7 +declare euclidean_component.isCont [simp]
6.8 +
6.9  lemma euclidean_eqI:
6.10    fixes x y :: "'a::euclidean_space"
6.11    assumes "\<And>i. i < DIM('a) \<Longrightarrow> x \$\$ i = y \$\$ i" shows "x = y"
```
```     7.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue Aug 16 13:07:52 2011 -0700
7.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue Aug 16 09:31:23 2011 -0700
7.3 @@ -408,6 +408,8 @@
7.4  apply (rule_tac x="1" in exI, simp add: norm_nth_le)
7.5  done
7.6
7.7 +declare vec_nth.isCont [simp]
7.8 +
7.9  instance vec :: (banach, finite) banach ..
7.10
7.11
```
```     8.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 16 13:07:52 2011 -0700
8.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 16 09:31:23 2011 -0700
8.3 @@ -5229,37 +5229,37 @@
8.4    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
8.5
8.6  lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
8.7 -  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
8.8 +  by (simp add: closed_Collect_le)
8.9
8.10  lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
8.11 -  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
8.12 +  by (simp add: closed_Collect_le)
8.13
8.14  lemma closed_hyperplane: "closed {x. inner a x = b}"
8.15 -  by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
8.16 +  by (simp add: closed_Collect_eq)
8.17
8.18  lemma closed_halfspace_component_le:
8.19    shows "closed {x::'a::euclidean_space. x\$\$i \<le> a}"
8.20 -  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
8.21 +  by (simp add: closed_Collect_le)
8.22
8.23  lemma closed_halfspace_component_ge:
8.24    shows "closed {x::'a::euclidean_space. x\$\$i \<ge> a}"
8.25 -  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
8.26 +  by (simp add: closed_Collect_le)
8.27
8.28  text {* Openness of halfspaces. *}
8.29
8.30  lemma open_halfspace_lt: "open {x. inner a x < b}"
8.31 -  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
8.32 +  by (simp add: open_Collect_less)
8.33
8.34  lemma open_halfspace_gt: "open {x. inner a x > b}"
8.35 -  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
8.36 +  by (simp add: open_Collect_less)
8.37
8.38  lemma open_halfspace_component_lt:
8.39    shows "open {x::'a::euclidean_space. x\$\$i < a}"
8.40 -  by (intro open_Collect_less euclidean_component.isCont isCont_const)
8.41 +  by (simp add: open_Collect_less)
8.42
8.43  lemma open_halfspace_component_gt:
8.44    shows "open {x::'a::euclidean_space. x\$\$i > a}"
8.45 -  by (intro open_Collect_less euclidean_component.isCont isCont_const)
8.46 +  by (simp add: open_Collect_less)
8.47
8.48  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
8.49
8.50 @@ -5297,15 +5297,13 @@
8.51    fixes a :: "'a\<Colon>ordered_euclidean_space"
8.52    shows "closed {.. a}"
8.53    unfolding eucl_atMost_eq_halfspaces
8.54 -  by (intro closed_INT ballI closed_Collect_le
8.55 -    euclidean_component.isCont isCont_const)
8.56 +  by (simp add: closed_INT closed_Collect_le)
8.57
8.58  lemma closed_eucl_atLeast[simp, intro]:
8.59    fixes a :: "'a\<Colon>ordered_euclidean_space"
8.60    shows "closed {a ..}"
8.61    unfolding eucl_atLeast_eq_halfspaces
8.62 -  by (intro closed_INT ballI closed_Collect_le
8.63 -    euclidean_component.isCont isCont_const)
8.64 +  by (simp add: closed_INT closed_Collect_le)
8.65
8.66  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x \$\$ i) -` S)"
8.67    by (auto intro!: continuous_open_vimage)
```