From c72cd759d05fa8d77d6a46078e5806dc19a0cf4b Mon Sep 17 00:00:00 2001
From: Francois Clement <Francois.Clement@inria.fr>
Date: Tue, 8 Feb 2022 18:57:39 +0100
Subject: [PATCH] incr_fun_seq hyp goes first.
---
Lebesgue/Tonelli.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/Lebesgue/Tonelli.v b/Lebesgue/Tonelli.v
index f4b16803..d2bf23fb 100644
--- a/Lebesgue/Tonelli.v
+++ b/Lebesgue/Tonelli.v
@@ -871,20 +871,20 @@ now apply Mplus_plus.
Qed.
Lemma LInt_p_section_fun_Sup_seq :
- forall f x1, Mplus_seq genX1xX2 f -> incr_fun_seq f ->
+ forall f x1, incr_fun_seq f -> Mplus_seq genX1xX2 f ->
LInt_p_section_fun (fun x => Sup_seq (fun n => f n x)) x1 =
Sup_seq (fun n => LInt_p_section_fun (f n) x1).
Proof.
intros f x1 Hf1 Hf2.
apply Beppo_Levi; try easy.
-intros n; apply (section_fun_Mplus _ _ (Hf1 n)).
+intros n; apply (section_fun_Mplus _ _ (Hf2 n)).
Qed.
Lemma LInt_p_section_fun_Mplus_Sup_seq :
- forall f, Mplus_seq genX1xX2 f -> incr_fun_seq f ->
+ forall f, incr_fun_seq f -> Mplus_seq genX1xX2 f ->
(forall n, P0 (f n)) -> P0 (fun x => Sup_seq (fun n => f n x)).
Proof.
-intros f Hf1 Hf2 H; intros.
+intros f; intros.
apply Mplus_ext with (fun x1 => Sup_seq (fun n => LInt_p_section_fun (f n) x1)).
intros; now rewrite LInt_p_section_fun_Sup_seq.
now apply Mplus_Sup_seq.
--
GitLab