diff -r bb70dc05cd38 -r e5d4bc2016a6 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Jan 09 00:08:18 2017 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Mon Jan 09 14:00:13 2017 +0000
@@ -294,27 +294,6 @@
     unfolding topspace_pullback_topology by blast
 qed
 
-subsubsection {*Miscellaneous*}
-
-text {*The following could belong to \verb+Topology_Euclidean_Spaces.thy+, and will be needed
-below.*}
-lemma openin_INT [intro]:
-  assumes "finite I"
-          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
-  shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
-using assms by (induct, auto simp add: inf_sup_aci(2) openin_Int)
-
-lemma openin_INT2 [intro]:
-  assumes "finite I" "I \<noteq> {}"
-          "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
-  shows "openin T (\<Inter>i \<in> I. U i)"
-proof -
-  have "(\<Inter>i \<in> I. U i) \<subseteq> topspace T"
-    using `I \<noteq> {}` openin_subset[OF assms(3)] by auto
-  then show ?thesis
-    using openin_INT[of _ _ U, OF assms(1) assms(3)] by (simp add: inf.absorb2 inf_commute)
-qed
-
 
 subsection {*The product topology*}