proposition: Lemma bigcupT_emeasurable (F : (set \bar R)^nat) : (forall i, emeasurable (F i)) -> emeasurable (\bigcup_i (F i)).
proof: Proof. move=> mF; pose P := fun i j => measurableR j.1 /\ ps_infty j.2 /\ F i = [set x%:E | x in j.1] `|` j.2. have [f fi] : {f : nat -> (set R) * (set \bar R) & forall i, P i (f i) }. by apply: choice => i; have [x mx [y PSoo'y] xy] := mF i; exists (x, y). exists (\bigcup_i (f i).1). by apply: bigcupT_measurable => i; exact: (fi i).1. exists (\bigcup_i (f i).2). apply/ps_inftyP => x [n _] fn2x. have /ps_inftyP : ps_infty(f n).2 by have [_ []] := fi n. exact. rewrite [RHS](@eq_bigcupr _ _ _ _ (fun i => [set x%:E | x in (f i).1] `|` (f i).2)); last first. by move=> i; have [_ []] := fi i. rewrite bigcupU; congr (_ `|` _). rewrite predeqE => i /=; split=> [[r [n _ fn1r <-{i}]]|[n _ [r fn1r <-{i}]]]; by [exists n => //; exists r | exists r => //; exists n]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure