proposition: Lemma finite_kernel_measure d d' (X : measurableType d) (Y : measurableType d') (R : realType) (k : R.-fker X ~> Y) (x : X) : fin_num_fun (k x).
proof: Proof. have [r k_r] := measure_uub k. by apply: lty_fin_num_fun; rewrite (@lt_trans _ _ r%:E) ?ltey. 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