src/HOL/Probability/Sigma_Algebra.thy

     by (intro image_cong) (auto dest: sets.sets_into_space)
   ultimately show "sigma_sets (\<Omega> \<inter> space M) (op \<inter> \<Omega> ` sets M) = op \<inter> \<Omega> ` sets M"
     by simp
 qed
 
+lemma sets_restrict_space_count_space :
+  "sets (restrict_space (count_space A) B) = sets (count_space (A \<inter> B))"
+by(auto simp add: sets_restrict_space)
+
 lemma sets_restrict_UNIV[simp]: "sets (restrict_space M UNIV) = sets M"
   by (auto simp add: sets_restrict_space)
 
 lemma sets_restrict_restrict_space:
   "sets (restrict_space (restrict_space M A) B) = sets (restrict_space M (A \<inter> B))"