minor fix

math-comp · Feb 24, 2023 · a9b7c16 · a9b7c16
1 parent 8f43a83
commit a9b7c16
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 4 deletions.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -3754,9 +3754,8 @@ apply: (@le_lt_trans _ _ (\sum_(i <oo) `|fine (a i)|%:E)).
   apply: lee_nneseries => // n _; rewrite integral_dirac//.
   move: (@summable_pinfty _ _ _ _ sa n Logic.I).
   by case: (a n) => //= r _; rewrite indicE/= mem_set// mul1r.
-move: (sa); rewrite /summable (_ : [set: nat] = xpredT)//; last exact/seteqP.
-rewrite -nneseries_esum//; apply: le_lt_trans.
-by apply: lee_nneseries => // n _ /=; case: (a n) => //; rewrite leey.
+move: (sa); rewrite /summable -fun_true -nneseries_esum//; apply: le_lt_trans.
+by apply lee_nneseries => // n _ /=; case: (a n) => //; rewrite leey.
 Qed.
 
 Lemma integral_count (a : nat -> \bar R) : summable setT a ->

diff --git a/theories/measure.v b/theories/measure.v
@@ -2543,7 +2543,7 @@ Definition fin_num_fun d (T : semiRingOfSetsType d) (R : numDomainType)
   (mu : set T -> \bar R) := forall U, measurable U -> mu U \is a fin_num.
 
 Lemma fin_num_fun_lty d (T : algebraOfSetsType d) (R : realFieldType)
-    (mu : set T -> \bar R) : fin_num_fun mu -> mu setT < +oo.
+  (mu : set T -> \bar R) : fin_num_fun mu -> mu setT < +oo.
 Proof. by move=> h; rewrite ltey_eq h. Qed.
 
 Lemma lty_fin_num_fun d (T : algebraOfSetsType d)