--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Sep 21 17:48:39 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Sep 21 20:47:34 2018 +0100
@@ -11,6 +11,7 @@
"HOL-Library.Indicator_Function"
"HOL-Library.Countable_Set"
"HOL-Library.FuncSet"
+ "HOL-Library.Set_Idioms"
Linear_Algebra
Norm_Arith
begin
@@ -817,6 +818,9 @@
unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
by auto
+lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
+ by (force simp: relative_to_def openin_subtopology)
+
lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
by (auto simp: topspace_def openin_subtopology)