proposition: Lemma mfun_prod I r (P : {pred I}) (f : I -> {mfun aT >-> rT}) (x : aT) : (\sum_(i <- r | P i) f i) x = \sum_(i <- r | P i) f i x.
proof: Proof. by elim/big_rec2: _ => //= i y ? Pi <-. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun