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/Sigma_Algebra.thy
changeset 69284 3273692de24a
parent 69164 74f1b0f10b2b
child 69313 b021008c5397 
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Sat Nov 10 19:39:38 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Nov 11 13:05:15 2018 +0100
@@ -1333,7 +1333,7 @@
   fix A assume "A \<subseteq> \<Omega> \<and> A \<inter> D \<in> M"
   moreover have "(\<Omega> - A) \<inter> D = (\<Omega> - (A \<inter> D)) - (\<Omega> - D)"
     by auto
-  ultimately show "\<Omega> - A \<subseteq> \<Omega> \<and> (\<Omega> - A) \<inter> D \<in> M"
+  ultimately show "(\<Omega> - A) \<inter> D \<in> M"
     using  \<open>D \<in> M\<close> by (auto intro: diff)
 next
   fix A :: "nat \<Rightarrow> 'a set"
isabelle