Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Abstract_Topology_2.thy
changeset 71174 7fac205dd737
parent 71172 575b3a818de5
child 71842 db120661dded 
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -706,7 +706,7 @@
   unfolding continuous_map_openin_preimage_eq
 proof (intro conjI allI impI)
   show "g ` topspace X \<subseteq> topspace Y"
-    using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
+    using g cont continuous_map_image_subset_topspace by fastforce
 next
   fix U
   assume Y: "openin Y U"
@@ -747,7 +747,7 @@
   unfolding continuous_map_closedin_preimage_eq
 proof (intro conjI allI impI)
   show "g ` topspace X \<subseteq> topspace Y"
-    using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
+    using g cont continuous_map_image_subset_topspace by fastforce
 next
   fix U
   assume Y: "closedin Y U"
isabelle