--- 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
--- 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>