proposition: Lemma integrable_locally D f : open D -> mu.-integrable D (EFin \o f) -> locally_integrable D f.
proof: Proof. move=> oD /integrableP[mf foo]; split => //; first exact/EFin_measurable_fun. move=> K KD cK; rewrite (le_lt_trans _ foo)// subset_integral//=. - exact: compact_measurable. - exact: open_measurable. - apply/EFin_measurable_fun; apply: measurableT_comp => //. exact/EFin_measurable_fun. 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