proposition: Lemma measure_fam_uubP : measure_fam_uub <-> exists r : {posnum R}, forall x, k x [set: Y] < r%:num%:E.
proof: Proof. split => [|] [r kr]; last by exists r%:num. suff r_gt0 : (0 < r)%R by exists (PosNum r_gt0). by rewrite -lte_fin; apply: (le_lt_trans _ (kr point)). 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