proposition: Lemma measurable_comp F (f : T2 -> T3) E (g : T1 -> T2) : measurable F -> g @` E `<=` F -> measurable_fun F f -> measurable_fun E g -> measurable_fun E (f \o g).
proof: Proof. move=> mF FgE mf mg /= mE A mA. rewrite comp_preimage. rewrite (_ : _ `&` _ = E `&` g @^-1` (F `&` f @^-1` A)); last first. apply/seteqP; split=> [|? [?] []//]. by move=> x/= [Ex Afgx]; split => //; split => //; exact: FgE. by apply/mg => //; exact: mf. 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)