--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Jan 05 16:03:23 2017 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Jan 05 16:37:49 2017 +0000
@@ -876,6 +876,11 @@
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
by (auto simp add: closedin_closed)
+lemma closedin_closed_subset:
+ "\<lbrakk>closedin (subtopology euclidean U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk>
+ \<Longrightarrow> closedin (subtopology euclidean T) S"
+ by (metis (no_types, lifting) Int_assoc Int_commute closedin_closed inf.orderE)
+
lemma finite_imp_closedin:
fixes S :: "'a::t1_space set"
shows "\<lbrakk>finite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> closedin (subtopology euclidean T) S"