making lemma non-local

math-comp · Aug 31, 2023 · 5582231 · 5582231
1 parent fe955b5
commit 5582231
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -4877,7 +4877,7 @@ move=> cptA ctsfA; apply: measurable_bounded_integrable.
   by exists M; split; rewrite ?num_real // => ? ? ? ?; exact: mrt.
 Qed.
 
-Local Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o):
+Lemma approximation_continuous_integrable (E : set R) (f : R -> R^o):
   measurable E -> mu E < +oo -> mu.-integrable E (EFin \o f) ->
   exists g_ : (rT -> rT)^nat,
     [/\ forall n, continuous (g_ n),