--- a/src/HOL/Analysis/Set_Integral.thy Tue Mar 05 20:13:20 2024 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy Tue Mar 05 20:20:34 2024 +0100
@@ -1746,7 +1746,7 @@
text \<open>We aim to lift results from the real case to arbitrary Banach spaces.
Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \cite{Lang_1993}.
- The theorem allows us to make statements about a function’s value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
+ The theorem allows us to make statements about a function's value almost everywhere, depending on the value its integral takes on various sets of the measure space.\<close>
text \<open>Before we introduce and prove the averaging theorem, we will first show the following lemma which is crucial for our proof.
While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \cite{engelking_1989}.