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 +
    1.30  lemma frontier_straddle:
    1.31    fixes a :: "'a::metric_space"
    1.32    shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
    1.33 @@ -2528,6 +2551,9 @@
    1.34  lemma frontier_complement [simp]: "frontier (- S) = frontier S"
    1.35    by (auto simp: frontier_def closure_complement interior_complement)
    1.36  
    1.37 +lemma frontier_Un_subset: "frontier(S \<union> T) \<subseteq> frontier S \<union> frontier T"
    1.38 +  by (metis compl_sup frontier_Int_subset frontier_complement)
    1.39 +
    1.40  lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
    1.41    using frontier_complement frontier_subset_eq[of "- S"]
    1.42    unfolding open_closed by auto