author nipkow Fri, 29 Nov 2019 17:43:00 +0100 changeset 71375 a1e94be66bd6 parent 71374 7fac205dd737 child 71376 6c208c2dca53
reduced imports; deleted unusewd minor lemmas for that purpose
```--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Nov 29 15:06:04 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Nov 29 17:43:00 2019 +0100
@@ -5,7 +5,7 @@
section \<open>Finite Cartesian Products of Euclidean Spaces\<close>

theory Cartesian_Euclidean_Space
-imports Convex_Euclidean_Space Derivative
+imports Derivative
begin

lemma subspace_special_hyperplane: "subspace {x. x \$ k = 0}"
@@ -450,6 +450,7 @@
shows "convex {x. \<forall>i. P i (x\$i)}"
using assms unfolding convex_def by auto

+(* Unused
lemma convex_positive_orthant_cart: "convex {x::real^'n. (\<forall>i. 0 \<le> x\$i)}"
by (rule convex_box_cart) (simp add: atLeast_def[symmetric])

@@ -464,12 +465,12 @@
where "finite s" "cbox (x - (\<chi> i. d)) (x + (\<chi> i. d)) = convex hull s"
proof -
from assms obtain s where "finite s"
-    and "cbox (x - sum ((*\<^sub>R) d) Basis) (x + sum ((*\<^sub>R) d) Basis) = convex hull s"
+    and "cbox (x - sum (( *\<^sub>R) d) Basis) (x + sum (( *\<^sub>R) d) Basis) = convex hull s"
by (rule cube_convex_hull)
with that[of s] show thesis