src/HOL/Analysis/Topology_Euclidean_Space.thy
 changeset 66939 04678058308f parent 66884 c2128ab11f61 child 67155 9e5b05d54f9d
```     1.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Oct 29 19:39:03 2017 +0100
1.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Oct 30 16:02:59 2017 +0000
1.3 @@ -2501,6 +2501,29 @@
1.4  lemma frontier_closures: "frontier S = closure S \<inter> closure (- S)"
1.5    by (auto simp: frontier_def interior_closure)
1.6
1.7 +lemma frontier_Int: "frontier(S \<inter> T) = closure(S \<inter> T) \<inter> (frontier S \<union> frontier T)"
1.8 +proof -
1.9 +  have "closure (S \<inter> T) \<subseteq> closure S" "closure (S \<inter> T) \<subseteq> closure T"
1.10 +    by (simp_all add: closure_mono)
1.11 +  then show ?thesis
1.12 +    by (auto simp: frontier_closures)
1.13 +qed
1.14 +
1.15 +lemma frontier_Int_subset: "frontier(S \<inter> T) \<subseteq> frontier S \<union> frontier T"
1.16 +  by (auto simp: frontier_Int)
1.17 +
1.18 +lemma frontier_Int_closed:
1.19 +  assumes "closed S" "closed T"
1.20 +  shows "frontier(S \<inter> T) = (frontier S \<inter> T) \<union> (S \<inter> frontier T)"
1.21 +proof -
1.22 +  have "closure (S \<inter> T) = T \<inter> S"
1.23 +    using assms by (simp add: Int_commute closed_Int)
1.24 +  moreover have "T \<inter> (closure S \<inter> closure (- S)) = frontier S \<inter> T"
1.25 +    by (simp add: Int_commute frontier_closures)
1.26 +  ultimately show ?thesis
1.27 +    by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures)
1.28 +qed
1.29 +