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/Urysohn.thy
changeset 82664 e9f3b94eb6a0
parent 82323 b022c013b04b 
--- a/src/HOL/Analysis/Urysohn.thy	Sat May 24 09:06:26 2025 +0200
+++ b/src/HOL/Analysis/Urysohn.thy	Wed May 28 17:49:22 2025 +0200
@@ -5516,9 +5516,8 @@
             moreover have "\<Union>\<V> = topspace X"
               using ABC UU \<V>_def by auto
             moreover have "pairwise (separatedin X) \<V>"
-              using pwU sep ABC unfolding  \<V>_def
-              apply (simp add: separatedin_sym pairwise_def)
-              by (metis member_remove remove_def separatedin_Un(1))
+              using pwU sep ABC separatedin_Un(1) [of X _ A B]
+              by (simp add: separatedin_sym pairwise_def \<V>_def) (metis DiffD1 DiffD2 singleton_iff)
             ultimately show ?thesis
               by blast
           qed
isabelle