proposition: Lemma bigcupT_measurable_rat d (T : measurableType d) (F : rat -> set T) : (forall i, measurable (F i)) -> measurable (\bigcup_i F i).
proof: Proof. move=> Fm; have /ppcard_eqP[f] := card_rat. by rewrite (reindex_bigcup f^-1%FUN setT)//=; 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)