--- a/src/HOL/Analysis/Abstract_Topology.thy Mon May 15 17:12:18 2023 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu May 18 11:44:42 2023 +0100
@@ -1098,7 +1098,6 @@
"X frontier_of S = X closure_of S \<inter> X closure_of (topspace X - S)"
by (metis Diff_Diff_Int closure_of_complement closure_of_subset_topspace double_diff frontier_of_def interior_of_subset_closure_of)
-
lemma interior_of_union_frontier_of [simp]:
"X interior_of S \<union> X frontier_of S = X closure_of S"
by (simp add: frontier_of_def interior_of_subset_closure_of subset_antisym)
@@ -1265,6 +1264,37 @@
"(discrete_topology U) frontier_of S = {}"
by (simp add: Diff_eq discrete_topology_closure_of frontier_of_closures)
+lemma openin_subset_topspace_eq:
+ assumes "disjnt S (X frontier_of U)"
+ shows "openin (subtopology X U) S \<longleftrightarrow> openin X S \<and> S \<subseteq> U"
+proof
+ assume S: "openin (subtopology X U) S"
+ show "openin X S \<and> S \<subseteq> U"
+ proof
+ show "S \<subseteq> U"
+ using S openin_imp_subset by blast
+ have "disjnt S (X frontier_of (topspace X \<inter> U))"
+ by (metis assms frontier_of_restrict)
+ moreover
+ have "openin (subtopology X (topspace X \<inter> U)) S"
+ by (simp add: S subtopology_restrict)
+ moreover
+ have "openin X S"
+ if dis: "disjnt S (X frontier_of U)" and ope: "openin (subtopology X U) S" and "U \<subseteq> topspace X"
+ for S U
+ proof -
+ obtain T where T: "openin X T" "S = T \<inter> U"
+ using ope by (auto simp: openin_subtopology)
+ have "T \<inter> U = T \<inter> X interior_of U"
+ using that T interior_of_subset in_closure_of by (fastforce simp: disjnt_iff frontier_of_def)
+ then show ?thesis
+ using \<open>S = T \<inter> U\<close> \<open>openin X T\<close> by auto
+ qed
+ ultimately show "openin X S"
+ by blast
+ qed
+qed (metis inf.absorb_iff1 openin_subtopology_Int)
+
subsection\<open>Locally finite collections\<close>