proposition: Lemma sfinite_kernel_measure d d' (Z : measurableType d) (X : measurableType d') (R : realType) (k : R.-sfker Z ~> X) (z : Z) : sfinite_measure (k z).
proof: Proof. have [s ks] := sfinite_kernel k. exists (s ^~ z). move=> n; have [r snr] := measure_uub (s n). by apply: lty_fin_num_fun; rewrite (lt_le_trans (snr _))// leey. by move=> U mU; rewrite ks. Qed.
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