# HG changeset patch
# User nipkow
# Date 1575465179 -3600
# Node ID dc767054de47a4e7b6f63a0f4fe63dfee840e73e
# Parent  1249859d23dd76f6ae47aa6bd16568ff9b127fcb
moved lemmas

diff -r 1249859d23dd -r dc767054de47 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Wed Dec 04 12:00:07 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed Dec 04 14:12:59 2019 +0100
@@ -1057,6 +1057,39 @@
     done
 qed
 
+lemma closure_open_Int_superset:
+  assumes "open S" "S \<subseteq> closure T"
+  shows "closure(S \<inter> T) = closure S"
+proof -
+  have "closure S \<subseteq> closure(S \<inter> T)"
+    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
+  then show ?thesis
+    by (simp add: closure_mono dual_order.antisym)
+qed
+
+lemma closure_Int: "closure (\<Inter>I) \<le> \<Inter>{closure S |S. S \<in> I}"
+proof -
+  {
+    fix y
+    assume "y \<in> \<Inter>I"
+    then have y: "\<forall>S \<in> I. y \<in> S" by auto
+    {
+      fix S
+      assume "S \<in> I"
+      then have "y \<in> closure S"
+        using closure_subset y by auto
+    }
+    then have "y \<in> \<Inter>{closure S |S. S \<in> I}"
+      by auto
+  }
+  then have "\<Inter>I \<subseteq> \<Inter>{closure S |S. S \<in> I}"
+    by auto
+  moreover have "closed (\<Inter>{closure S |S. S \<in> I})"
+    unfolding closed_Inter closed_closure by auto
+  ultimately show ?thesis using closure_hull[of "\<Inter>I"]
+    hull_minimal[of "\<Inter>I" "\<Inter>{closure S |S. S \<in> I}" "closed"] by auto
+qed
+
 lemma islimpt_in_closure: "(x islimpt S) = (x\<in>closure(S-{x}))"
   unfolding closure_def using islimpt_punctured by blast
 
diff -r 1249859d23dd -r dc767054de47 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Wed Dec 04 12:00:07 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Wed Dec 04 14:12:59 2019 +0100
@@ -420,16 +420,6 @@
   finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
 qed
 
-lemma closure_open_Int_superset:
-  assumes "open S" "S \<subseteq> closure T"
-  shows "closure(S \<inter> T) = closure S"
-proof -
-  have "closure S \<subseteq> closure(S \<inter> T)"
-    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
-  then show ?thesis
-    by (simp add: closure_mono dual_order.antisym)
-qed
-
 lemma convex_closure_interior:
   fixes S :: "'a::euclidean_space set"
   assumes "convex S" and int: "interior S \<noteq> {}"
@@ -1645,29 +1635,6 @@
   then show ?thesis by auto
 qed
 
-lemma closure_Int: "closure (\<Inter>I) \<le> \<Inter>{closure S |S. S \<in> I}"
-proof -
-  {
-    fix y
-    assume "y \<in> \<Inter>I"
-    then have y: "\<forall>S \<in> I. y \<in> S" by auto
-    {
-      fix S
-      assume "S \<in> I"
-      then have "y \<in> closure S"
-        using closure_subset y by auto
-    }
-    then have "y \<in> \<Inter>{closure S |S. S \<in> I}"
-      by auto
-  }
-  then have "\<Inter>I \<subseteq> \<Inter>{closure S |S. S \<in> I}"
-    by auto
-  moreover have "closed (\<Inter>{closure S |S. S \<in> I})"
-    unfolding closed_Inter closed_closure by auto
-  ultimately show ?thesis using closure_hull[of "\<Inter>I"]
-    hull_minimal[of "\<Inter>I" "\<Inter>{closure S |S. S \<in> I}" "closed"] by auto
-qed
-
 lemma convex_closure_rel_interior_inter:
   assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
     and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"