proposition: Lemma sintegral_indic (A : set T) : sintegral mu \1_A = mu A.
proof: Proof. rewrite sintegralE (fsbig_widen _ [set 0%R; 1%R]) => //; last 2 first. - exact: image_indic_sub. - by move=> t [[] -> /= /preimage10->]; rewrite measure0 mule0. have N01 : (0 <> 1:> R)%R by move=> /esym/eqP; rewrite oner_eq0. rewrite fsbigU//=; last by move=> t [->]//. rewrite !fsbig_set1 mul0e add0e mul1e. by rewrite preimage_indic ifT ?inE// ifN ?notin_set. 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