proposition: Lemma cvg_nnsfun_approx (f0 : forall x, D x -> (0 <= f x)%E) x : D x -> EFin \o nnsfun_approx^~x @ \oo --> f x.
proof: Proof. by move=> Dx; under eq_fun do rewrite nnsfun_approxE; exact: ecvg_approx. 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