proposition: Lemma measurability d d' (aT : measurableType d) (rT : measurableType d') (D : set aT) (f : aT -> rT) (G' : set (set rT)) : @measurable _ rT = <<s G' >> -> preimage_class D f G' `<=` @measurable _ aT -> measurable_fun D f.
proof: Proof. move=> sG_rT fG_aT mD. suff h : preimage_class D f (@measurable _ rT) `<=` @measurable _ aT. by move=> A mA; apply: h; exists A. have -> : preimage_class D f (@measurable _ rT) = <<s D , (preimage_class D f G')>>. by rewrite [in LHS]sG_rT [in RHS]sigma_algebra_preimage_classE. apply: smallest_sub => //; split => //. - by move=> A mA; exact: measurableD. - by move=> F h; exact: bigcupT_measurable. 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)