minor fix

math-comp · Feb 23, 2023 · daf0fad · daf0fad
1 parent ee484f4
commit daf0fad
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -3754,8 +3754,7 @@ 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.
+move: (sa); rewrite /summable -fun_true -nneseries_esum//; apply: le_lt_trans.
 by apply lee_nneseries => // n _ /=; case: (a n) => //; rewrite leey.
 Qed.
 

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)