From daf0fad16eb13ed51fa77b3e7307ef3db2cd8a63 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 23 Feb 2023 22:36:36 +0900 Subject: [PATCH] minor fix --- theories/lebesgue_integral.v | 3 +-- theories/measure.v | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index afaf0b3110..10ecda078a 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -3754,8 +3754,7 @@ apply: (@le_lt_trans _ _ (\sum_(i // 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 index d03605b71c..02e5bbbf60 100644 --- 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)