proposition: Lemma sigma_algebra_preimage_classE aT (rT : pointedType) (D : set aT) (f : aT -> rT) (G' : set (set rT)) : <<s D, preimage_class D f G' >> = preimage_class D f (G'.-sigma.-measurable).
proof: Proof. rewrite eqEsubset; split. have mG : sigma_algebra D (preimage_class D f (G'.-sigma.-measurable)). exact/sigma_algebra_preimage_class/sigma_algebra_measurable. have subset_preimage : preimage_class D f G' `<=` preimage_class D f (G'.-sigma.-measurable). by move=> A [B CCB <-{A}]; exists B => //; apply: sub_sigma_algebra. exact: smallest_sub. have G'pre A' : G' A' -> (preimage_class D f G') (D `&` f @^-1` A'). by move=> ?; exists A'. pose I : set (set aT) := <<s D, preimage_class D f G' >>. have G'sfun : G' `<=` image_class D f I. by move=> A' /G'pre[B G'B h]; apply: sub_sigma_algebra; exists B. have sG'sfun : <<s G' >> `<=` image_class D f I. apply: smallest_sub => //; apply: sigma_algebra_image_class. exact: smallest_sigma_algebra. by move=> _ [B mB <-]; exact: sG'sfun. 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)