src/HOL/Probability/Tree_Space.thy

     using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
   finally show "value -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in>
       sets (restrict_space (tree_sigma M) (- {Leaf}))"
     by (auto simp: sets_restrict_space_iff space_restrict_space)
 qed
-
-lemma measurable_restrict_mono:
-  assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A"
-  shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N"
-by (rule measurable_compose[OF measurable_restrict_space3 f])
-   (insert \<open>B \<subseteq> A\<close>, auto)
-
 
 lemma measurable_value[measurable (raw)]:
   assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M"
     and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf"
   shows "(\<lambda>\<omega>. value (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"