From 5582231d135c2dcf005a421b11b47b3ba8173dd3 Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 30 Aug 2023 23:28:34 -0400 Subject: [PATCH] making lemma non-local --- theories/lebesgue_integral.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 7ec0326db..85e19b823 100644 --- 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),