author nipkow Wed, 04 Dec 2019 12:00:07 +0100 changeset 71225 1249859d23dd parent 71224 54a7ad860a76 child 71227 e9a4bd0a836e child 71228 dc767054de47
moved lemma
```--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Dec 03 16:51:53 2019 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Dec 04 12:00:07 2019 +0100
@@ -455,6 +455,11 @@
shows "closure S \<subseteq> affine hull S"
by (intro closure_minimal hull_subset affine_closed affine_affine_hull)

+lemma closed_affine_hull [iff]:
+  fixes S :: "'n::euclidean_space set"
+  shows "closed (affine hull S)"
+  by (metis affine_affine_hull affine_closed)
+
lemma closure_same_affine_hull [simp]:
fixes S :: "'n::euclidean_space set"
shows "affine hull (closure S) = affine hull S"```
```--- a/src/HOL/Analysis/Starlike.thy	Tue Dec 03 16:51:53 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Wed Dec 04 12:00:07 2019 +0100
@@ -1296,11 +1296,6 @@
shows "rel_frontier((\<lambda>x. a + x) ` S) = (\<lambda>x. a + x) ` (rel_frontier S)"
by (simp add: rel_frontier_def translation_diff rel_interior_translation closure_translation)

-lemma closed_affine_hull [iff]:
-  fixes S :: "'n::euclidean_space set"
-  shows "closed (affine hull S)"
-  by (metis affine_affine_hull affine_closed)
-
lemma rel_frontier_nonempty_interior:
fixes S :: "'n::euclidean_space set"
shows "interior S \<noteq> {} \<Longrightarrow> rel_frontier S = frontier S"```