proposition: Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo.
proof: Proof. move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]]. have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R. by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_pwDr// ler_norm. rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=. by rewrite lebesgue_measure_itv/= lte_fin gtrN// EFinD ltry. 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