proposition: Lemma sigma_algebra_image_class (aT rT : Type) (D : set aT) (f : aT -> rT) (G : set (set aT)) : sigma_algebra D G -> sigma_algebra setT (image_class D f G).
proof: Proof. move=> [G0 GC GU]; split; rewrite /image_class. - by rewrite /= preimage_set0 setI0. - move=> A /= GfAD; rewrite setTD -preimage_setC -setDE. rewrite (_ : _ `\` _ = D `\` (D `&` f @^-1` A)); first exact: GC. rewrite predeqE => x; split=> [[Dx fAx]|[Dx fADx]]. by split => // -[] _ /fAx. by split => //; exact: contra_not fADx. - by move=> F /= mF; rewrite preimage_bigcup setI_bigcupr; exact: GU. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)