# HG changeset patch
# User hoelzl
# Date 1515086337 -3600
# Node ID d91b9d22305b1df07569f9eff25cb2e4cc17cbcd
# Parent  b164fdbb423db6c911f6e84867026d8a24946991
HOL-Analysis: add set_integrable_restrict_space

diff -r b164fdbb423d -r d91b9d22305b src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Wed Jan 03 23:18:46 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Jan 04 18:18:57 2018 +0100
@@ -99,6 +99,19 @@
     by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
 qed
 
+lemma set_integrable_restrict_space:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes f: "set_integrable M S f" and T: "T \<in> sets (restrict_space M S)"
+  shows "set_integrable M T f"
+proof -
+  obtain T' where T_eq: "T = S \<inter> T'" and "T' \<in> sets M" using T by (auto simp: sets_restrict_space)
+
+  have \<open>integrable M (\<lambda>x. indicator T' x *\<^sub>R (indicator S x *\<^sub>R f x))\<close>
+    by (rule integrable_mult_indicator; fact)
+  then show ?thesis
+    unfolding T_eq indicator_inter_arith by (simp add: ac_simps)
+qed
+
 (* TODO: integral_cmul_indicator should be named set_integral_const *)
 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)