proposition: Lemma dynkin_monotone G : dynkin G <-> monotone_class setT G.
proof: Proof. split => [[GT setCG trG]|[_ GT setDG ndG]]; split => //. - move=> A B BA GA GB; rewrite setDE -(setCK (_ `&` _)) setCI; apply: (setCG). rewrite setCK -bigcup2E; apply trG. + by rewrite -trivIset_bigcup2 setIC; apply subsets_disjoint. + by move=> [|[//|n]]; [exact: setCG|rewrite /bigcup2 -setCT; apply: setCG]. - move=> F ndF GF; rewrite eq_bigcup_seqD; apply: (trG). exact: trivIset_seqD. move=> [/=|n]; first exact: GF. rewrite /seqD setDE -(setCK (_ `&` _)) setCI; apply: (setCG). rewrite setCK -bigcup2E; apply: trG. + rewrite -trivIset_bigcup2 setIC; apply subsets_disjoint. exact/subsetPset/ndF/ltnW. + move=> [|[|]]; rewrite /bigcup2 /=; [exact/setCG/GF|exact/GF|]. by move=> _; rewrite -setCT; apply: setCG. - by move=> A B; rewrite -setTD; apply: setDG. - move=> F tF GF; pose A i := \big[setU/set0]_(k < i.+1) F k. rewrite (_ : bigcup _ _ = \bigcup_i A i); last first. rewrite predeqE => t; split => [[n _ Fn]|[n _]]. by exists n => //; rewrite /A -bigcup_mkord; exists n=> //=; rewrite ltnS. by rewrite /A -bigcup_mkord => -[m /=]; rewrite ltnS => mn Fmt; exists m. apply: ndG; first by move=> a b ab; exact/subsetPset/subset_bigsetU. elim=> /= => [|n ih]. by rewrite /A big_ord_recr /= big_ord0 set0U; exact: GF. rewrite /A /= big_ord_recr /= -/(A n). rewrite (_ : _ `|` _ = ~` (~` A n `\` F n.+1)); last first. by rewrite setDE setCI !setCK. rewrite -setTD; apply: (setDG) => //; apply: (setDG) => //; last first. by rewrite -setTD; apply: setDG. apply/disjoints_subset; rewrite setIC. by apply: (@trivIset_bigsetUI _ predT) => //; rewrite /predT /= trueE. 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)