proposition: Lemma measurable_almost_continuous (f : R -> R) (eps : rT) : (0 < eps)%R -> measurable_fun A f -> exists K, [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E & {within K, continuous f}].
proof: Proof. move: eps=> _/posnumP[eps] mf; have e2pos : (0 < eps%:num/2)%R by []. have [K [mK KA ? ?]] := measurable_almost_continuous' e2pos mf. have Kfin : mu K < +oo by rewrite (le_lt_trans _ finA)// le_measure ?inE. have [D /= [cD DK KDe]] := lebesgue_regularity_inner mK Kfin e2pos. exists D; split => //; last exact: (continuous_subspaceW DK). exact: (subset_trans DK). have -> : A `\` D = (A `\` K) `|` (K `\` D). rewrite eqEsubset; split => z. by case: (pselect (K z)) => // ? [? ?]; [right | left]. case; case=> az nz; split => //; [by move: z nz {az}; apply/subsetC|]. exact: KA. apply: le_lt_trans. apply: measureU2; apply: measurableD => //; apply: closed_measurable. by apply: compact_closed; first exact: Rhausdorff. by rewrite [_ eps]splitr EFinD lteD. 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