proposition: Lemma nnsfun_mulemu_ge0 d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}) (f : {nnsfun T >-> R}) x : 0 <= x%:E * mu (f @^-1` [set x]).
proof: Proof. by apply: (mulemu_ge0 (fun x => f @^-1` [set x])); exact: preimage_nnfun0. 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