proposition: Lemma continuous_compact_integrable (f : R -> R^o) (A : set R^o) : compact A -> {within A, continuous f} -> mu.-integrable A (EFin \o f).
proof: Proof. move=> cptA ctsfA; apply: measurable_bounded_integrable. - exact: compact_measurable. - exact: compact_finite_measure. - by apply: subspace_continuous_measurable_fun => //; exact: compact_measurable. - have /compact_bounded[M [_ mrt]] := continuous_compact ctsfA cptA. by exists M; split; rewrite ?num_real // => ? ? ? ?; exact: mrt. 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