proposition: Lemma measurable_fun_bigcup (E : (set T1)^nat) (f : T1 -> T2) : (forall i, measurable (E i)) -> measurable_fun (\bigcup_i E i) f <-> (forall i, measurable_fun (E i) f).
proof: Proof. move=> mE; split => [|mf /= _ A mA]; last first. by rewrite setI_bigcupl; apply: bigcup_measurable => i _; exact: mf. move=> mf i _ A /mf => /(_ (bigcup_measurable (fun k _ => mE k))). move=> /(measurableI (E i))-/(_ (mE i)). by rewrite setICA setIA (@setIidr _ _ (E i))//; exact: bigcup_sup. 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)