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.thy
changeset 69325 4b6ddc5989fc
parent 69313 b021008c5397
child 69508 2a4c8a2a3f8e 
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -2792,7 +2792,7 @@
     show "U ` \<F> \<subseteq> \<U>"
       using \<open>\<F> \<subseteq> \<V>\<close> U by auto
   next
-    show "f ` S \<subseteq> UNION \<F> U"
+    show "f ` S \<subseteq> \<Union> (U ` \<F>)"
       using \<F>(2-3) U UnionE subset_eq U by fastforce
   qed
 qed
isabelle