equal
deleted
inserted
replaced
97 lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" |
97 lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)" |
98 using closedin_Inter[of "{S,T}" U] by auto |
98 using closedin_Inter[of "{S,T}" U] by auto |
99 |
99 |
100 lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast |
100 lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast |
101 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)" |
101 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)" |
102 apply (auto simp add: closedin_def) |
102 apply (auto simp add: closedin_def Diff_Diff_Int) |
103 apply (metis openin_subset subset_eq) |
103 apply (metis openin_subset subset_eq) |
104 apply (auto simp add: Diff_Diff_Int) |
104 done |
105 apply (subgoal_tac "topspace U \<inter> S = S") |
|
106 by auto |
|
107 |
105 |
108 lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))" |
106 lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))" |
109 by (simp add: openin_closedin_eq) |
107 by (simp add: openin_closedin_eq) |
110 |
108 |
111 lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)" |
109 lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)" |