# HG changeset patch
# User paulson
# Date 1575463487 0
# Node ID e9a4bd0a836e5ee142e73c39cdb27708cf68cad1
# Parent  1249859d23dd76f6ae47aa6bd16568ff9b127fcb# Parent  9adb1e16b2a65d10ce8f9bc63404bbed5850b0eb
merged

diff -r 9adb1e16b2a6 -r e9a4bd0a836e src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Dec 04 12:44:38 2019 +0000
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Dec 04 12:44:47 2019 +0000
@@ -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"
diff -r 9adb1e16b2a6 -r e9a4bd0a836e src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Wed Dec 04 12:44:38 2019 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Wed Dec 04 12:44:47 2019 +0000
@@ -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"