moved lemmas
authornipkow
Wed Dec 04 14:12:59 2019 +0100 (2 days ago ago)
changeset 71429dc767054de47
parent 71428 1249859d23dd
child 71432 be2c2bfa54a0
moved lemmas
src/HOL/Analysis/Elementary_Topology.thy
src/HOL/Analysis/Starlike.thy
     1.1 --- a/src/HOL/Analysis/Elementary_Topology.thy	Wed Dec 04 12:00:07 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed Dec 04 14:12:59 2019 +0100
     1.3 @@ -1057,6 +1057,39 @@
     1.4      done
     1.5  qed
     1.6  
     1.7 +lemma closure_open_Int_superset:
     1.8 +  assumes "open S" "S \<subseteq> closure T"
     1.9 +  shows "closure(S \<inter> T) = closure S"
    1.10 +proof -
    1.11 +  have "closure S \<subseteq> closure(S \<inter> T)"
    1.12 +    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
    1.13 +  then show ?thesis
    1.14 +    by (simp add: closure_mono dual_order.antisym)
    1.15 +qed
    1.16 +
    1.17 +lemma closure_Int: "closure (\<Inter>I) \<le> \<Inter>{closure S |S. S \<in> I}"
    1.18 +proof -
    1.19 +  {
    1.20 +    fix y
    1.21 +    assume "y \<in> \<Inter>I"
    1.22 +    then have y: "\<forall>S \<in> I. y \<in> S" by auto
    1.23 +    {
    1.24 +      fix S
    1.25 +      assume "S \<in> I"
    1.26 +      then have "y \<in> closure S"
    1.27 +        using closure_subset y by auto
    1.28 +    }
    1.29 +    then have "y \<in> \<Inter>{closure S |S. S \<in> I}"
    1.30 +      by auto
    1.31 +  }
    1.32 +  then have "\<Inter>I \<subseteq> \<Inter>{closure S |S. S \<in> I}"
    1.33 +    by auto
    1.34 +  moreover have "closed (\<Inter>{closure S |S. S \<in> I})"
    1.35 +    unfolding closed_Inter closed_closure by auto
    1.36 +  ultimately show ?thesis using closure_hull[of "\<Inter>I"]
    1.37 +    hull_minimal[of "\<Inter>I" "\<Inter>{closure S |S. S \<in> I}" "closed"] by auto
    1.38 +qed
    1.39 +
    1.40  lemma islimpt_in_closure: "(x islimpt S) = (x\<in>closure(S-{x}))"
    1.41    unfolding closure_def using islimpt_punctured by blast
    1.42  
     2.1 --- a/src/HOL/Analysis/Starlike.thy	Wed Dec 04 12:00:07 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Starlike.thy	Wed Dec 04 14:12:59 2019 +0100
     2.3 @@ -420,16 +420,6 @@
     2.4    finally show "(1 - u) *\<^sub>R a + u *\<^sub>R b \<in> interior S" .
     2.5  qed
     2.6  
     2.7 -lemma closure_open_Int_superset:
     2.8 -  assumes "open S" "S \<subseteq> closure T"
     2.9 -  shows "closure(S \<inter> T) = closure S"
    2.10 -proof -
    2.11 -  have "closure S \<subseteq> closure(S \<inter> T)"
    2.12 -    by (metis assms closed_closure closure_minimal inf.orderE open_Int_closure_subset)
    2.13 -  then show ?thesis
    2.14 -    by (simp add: closure_mono dual_order.antisym)
    2.15 -qed
    2.16 -
    2.17  lemma convex_closure_interior:
    2.18    fixes S :: "'a::euclidean_space set"
    2.19    assumes "convex S" and int: "interior S \<noteq> {}"
    2.20 @@ -1645,29 +1635,6 @@
    2.21    then show ?thesis by auto
    2.22  qed
    2.23  
    2.24 -lemma closure_Int: "closure (\<Inter>I) \<le> \<Inter>{closure S |S. S \<in> I}"
    2.25 -proof -
    2.26 -  {
    2.27 -    fix y
    2.28 -    assume "y \<in> \<Inter>I"
    2.29 -    then have y: "\<forall>S \<in> I. y \<in> S" by auto
    2.30 -    {
    2.31 -      fix S
    2.32 -      assume "S \<in> I"
    2.33 -      then have "y \<in> closure S"
    2.34 -        using closure_subset y by auto
    2.35 -    }
    2.36 -    then have "y \<in> \<Inter>{closure S |S. S \<in> I}"
    2.37 -      by auto
    2.38 -  }
    2.39 -  then have "\<Inter>I \<subseteq> \<Inter>{closure S |S. S \<in> I}"
    2.40 -    by auto
    2.41 -  moreover have "closed (\<Inter>{closure S |S. S \<in> I})"
    2.42 -    unfolding closed_Inter closed_closure by auto
    2.43 -  ultimately show ?thesis using closure_hull[of "\<Inter>I"]
    2.44 -    hull_minimal[of "\<Inter>I" "\<Inter>{closure S |S. S \<in> I}" "closed"] by auto
    2.45 -qed
    2.46 -
    2.47  lemma convex_closure_rel_interior_inter:
    2.48    assumes "\<forall>S\<in>I. convex (S :: 'n::euclidean_space set)"
    2.49      and "\<Inter>{rel_interior S |S. S \<in> I} \<noteq> {}"