proposition: Lemma sfinite_subdef : Kernel_isSFinite_subdef d d' X Y R k.
proof: Proof. split; have [s sE] := sfinite; exists s => //. by move=> n; exact: measure_uub. 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