summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 04 Dec 2019 14:12:59 +0100 | |

changeset 71228 | dc767054de47 |

parent 71225 | 1249859d23dd |

child 71229 | be2c2bfa54a0 |

moved lemmas

src/HOL/Analysis/Elementary_Topology.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Analysis/Starlike.thy | file | annotate | diff | comparison | revisions |

--- 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

--- 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> {}"