proposition: Lemma integral_abs_eq0 D (N : set T) (f : T -> \bar R) : measurable N -> measurable D -> N `<=` D -> measurable_fun D f -> mu N = 0 -> \int[mu]_(x in N) `|f x| = 0.
proof: Proof. move=> mN mD ND mf muN0; rewrite integralEindic//. rewrite (eq_integral (fun x => `|f x * (\1_N x)%:E|)); last first. by move=> t _; rewrite abseM (@gee0_abs _ (\1_N t)%:E)// lee_fin. apply/ae_eq_integral_abs => //. apply: emeasurable_funM => //; first exact: (measurable_funS mD). exact/EFin_measurable_fun. exists N; split => // t /= /not_implyP[_]; rewrite indicE. by have [|] := boolP (t \in N); rewrite ?inE ?mule0. 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