proposition: Lemma sigma_algebra_strace G D : sigma_algebra setT G -> sigma_algebra D (strace G D).
proof: Proof. move=> [G0 GC GU]; split; first by exists set0 => //; rewrite set0I. - move=> S [A mA ADS]; have mCA := GC _ mA. have : strace G D (D `&` ~` A). by rewrite setIC; exists (setT `\` A) => //; rewrite setTD. rewrite -setDE => trDA. have DADS : D `\` A = D `\` S by rewrite -ADS !setDE setCI setIUr setICr setU0. by rewrite DADS in trDA. - move=> S mS; have /choice[M GM] : forall n, exists A, G A /\ S n = A `&` D. by move=> n; have [A mA ADSn] := mS n; exists A. exists (\bigcup_i (M i)); first by apply GU => i; exact: (GM i).1. by rewrite setI_bigcupl; apply eq_bigcupr => i _; rewrite (GM i).2. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure