proposition: Lemma ring_finite_set (A : set rT) : measurable A -> exists B : set (set T), [/\ finite_set B, (forall X, B X -> X !=set0), trivIset B id, (forall X : set T, X \in B -> measurable X) & A = \bigcup_(X in B) X].
proof: Proof. rewrite ring_measurableE => -[B [-> Bm Bfin Btriv]]. exists (B `&` [set X | X != set0]); split. - by apply: sub_finite_set Bfin; exact: subIsetl. - by move=> ?/= [_ /set0P]. - by move=> X Y/= [XB _] [YB _]; exact: Btriv. - by move=> X/= /[!inE] -[] /Bm. rewrite bigcup_mkcondr; apply: eq_bigcupr => X Bx; case: ifPn => //. by rewrite notin_set/= => /negP/negPn/eqP. 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)