--- a/src/HOL/Analysis/Interval_Integral.thy Sat Aug 16 22:35:44 2025 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Mon Aug 18 22:37:21 2025 +0100
@@ -402,6 +402,14 @@
"a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)"
by (auto simp: interval_lebesgue_integral_def einterval_iff)
+lemma has_bochner_interval_integral_iff:
+ assumes "a\<le>b"
+ shows "has_bochner_integral (restrict_space lborel {a..b}) f x
+ \<longleftrightarrow> set_integrable lborel {a..b} f \<and> (LBINT u=a..b. f u) = x"
+ using assms
+ by (simp add: has_bochner_integral_iff integral_restrict_space interval_integral_Icc
+ set_integrable_eq set_lebesgue_integral_def)
+
lemma interval_integral_discrete_difference:
fixes f :: "real \<Rightarrow> 'b::{banach, second_countable_topology}" and a b :: ereal
assumes "countable X"
--- a/src/HOL/Analysis/Set_Integral.thy Sat Aug 16 22:35:44 2025 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Mon Aug 18 22:37:21 2025 +0100
@@ -33,10 +33,11 @@
section \<open>Basic properties\<close>
-(*
-lemma indicator_abs_eq: "\<And>A x. \<bar>indicator A x\<bar> = ((indicator A x) :: real)"
- by (auto simp add: indicator_def)
-*)
+lemma set_integrable_eq:
+ fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+ assumes "\<Omega> \<inter> space M \<in> sets M"
+ shows "set_integrable M \<Omega> f = integrable (restrict_space M \<Omega>) f"
+ by (meson assms integrable_restrict_space set_integrable_def)
lemma set_integrable_cong:
assumes "M = M'" "A = A'" "\<And>x. x \<in> A \<Longrightarrow> f x = f' x"