# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1754667963 -3600
# Node ID dedd9d13c79cb3d078d1aa72a079cafc74f4840f
# Parent  b2b88d5b01b6b227efa12800ee36399535ec9528
Generalised a theorem about Lebesgue integration

diff -r b2b88d5b01b6 -r dedd9d13c79c src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Aug 07 22:42:21 2025 +0200
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Fri Aug 08 16:46:03 2025 +0100
@@ -28,7 +28,7 @@
   from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and
                              Mg': "set_borel_measurable borel {a..b} g'"
-      by (simp_all only: set_measurable_continuous_on_ivl)
+    using atLeastAtMost_borel set_measurable_continuous_on by blast+
   from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
     by (simp only: has_real_derivative_iff_has_vector_derivative)
 
@@ -329,7 +329,7 @@
   from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   with contg' have Mg: "set_borel_measurable borel {a..b} g"
     and Mg': "set_borel_measurable borel {a..b} g'"
-    by (simp_all only: set_measurable_continuous_on_ivl)
+    using atLeastAtMost_borel set_measurable_continuous_on by blast+
   from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
     by (rule deriv_nonneg_imp_mono) simp_all
 
diff -r b2b88d5b01b6 -r dedd9d13c79c src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Thu Aug 07 22:42:21 2025 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Aug 08 16:46:03 2025 +0100
@@ -608,11 +608,11 @@
 translations
   "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
 
-lemma set_measurable_continuous_on_ivl:
-  assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
-  shows "set_borel_measurable borel {a..b} f"
-  unfolding set_borel_measurable_def
-  by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp
+lemma set_measurable_continuous_on:
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  shows "A \<in> sets borel \<Longrightarrow> continuous_on A f \<Longrightarrow> set_borel_measurable borel A f"
+  by (meson borel_measurable_continuous_on_indicator
+      set_borel_measurable_def)
 
 section \<open>NN Set Integrals\<close>