proposition: Lemma funID (N : set T) (mN : measurable N) (f : T -> \bar R) : let oneCN := [the {nnsfun T >-> R} of mindic R (measurableC mN)] in let oneN := [the {nnsfun T >-> R} of mindic R mN] in f = (fun x => f x * (oneCN x)%:E) \+ (fun x => f x * (oneN x)%:E).
proof: Proof. move=> oneCN oneN; rewrite funeqE => x. rewrite /oneCN /oneN/= /mindic !indicE. have [xN|xN] := boolP (x \in N). by rewrite mule1 in_setC xN mule0 add0e. by rewrite in_setC xN mule0 adde0 mule1. 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