proposition: Lemma sigma_algebraP T U (C : set (set T)) : (forall X, C X -> X `<=` U) -> sigma_algebra U C <-> [/\ C U, setD_closed C, ndseq_closed C & setI_closed C].
proof: Proof. move=> C_subU; split => [[C0 CD CU]|[DT DC DU DI]]; split. - by rewrite -(setD0 U); apply: CD. - move=> A B BA CA CB; rewrite (_ : A `\` B = U `\` ((U `\` A) `|` B)). by apply CD; rewrite -bigcup2E; apply: CU => -[|[|[|]]] //=; exact: CD. rewrite setDUr setDD [in RHS]setDE setIACA setIid -setDE setIidr//. by rewrite setDE; apply: subIset; left; apply: C_subU. - by move=> F ndF DF; exact: CU. - move=> A B DA DB; rewrite (_ : A `&` B = U `\` ((U `\` A) `|` (U `\` B))). by apply CD; rewrite -bigcup2E; apply: CU => -[|[|[|]]] //; exact: CD. rewrite setDUr !setDD setIACA setIid (@setIidr _ U)//. by apply: subIset; left; exact: C_subU. - by rewrite -(setDv U); exact: DC. - by move=> A CA; apply: DC => //; exact: C_subU. - move=> F DF. rewrite [X in C X](_ : _ = \bigcup_i \big[setU/set0]_(j < i.+1) F j). apply: DU; first by move=> *; exact/subsetPset/subset_bigsetU. elim=> [|n ih]; first by rewrite big_ord_recr /= big_ord0 set0U; exact: DF. have CU : setU_closed C. move=> A B DA DB; rewrite (_ : A `|` B = U `\` ((U `\` A) `&` (U `\` B))). apply DC => //; last by apply: DI; apply: DC => //; exact: C_subU. by apply: subIset; left; apply: subIset; left. by rewrite setDIr// !setDD (setIidr (C_subU _ DA)) (setIidr (C_subU _ _)). by rewrite big_ord_recr; exact: CU. rewrite predeqE => x; split => [[n _ Fnx]|[n _]]. by exists n => //; rewrite big_ord_recr /=; right. by rewrite -bigcup_mkord => -[m /=]; rewrite ltnS => _ Fmx; exists m. 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)