fact: Variables (k : Y -> \bar R) (k_ : ({nnsfun Y >-> R}) ^nat) (ndk_ : nondecreasing_seq (k_ : (Y -> R)^nat)) (k_k : forall z, [set: Y] z -> (k_ n z)%:E @[n --> \oo] --> k z).
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology normedtype sequences esum measure numfun lebesgue_measure lebesgue_integral