proposition: Lemma smallest_monotone_classE : (forall X, <<s D, G >> X -> X `<=` D) -> (forall E, monotone_class D E -> G `<=` E -> H `<=` E) -> H = <<s D, G >>.
proof: Proof. move=> sDGD smallestH; rewrite eqEsubset; split. apply: (smallestH _ _ (@sub_sigma_algebra _ D G)). exact: monotone_class_g_salgebra. suff: setI_closed H. move=> IH; apply: smallest_sub => //. by apply/sigma_algebraP; by case: monoH. pose H_ A := [set X | H X /\ H (X `&` A)]. have setDH_ A : setD_closed (H_ A). move=> X Y XY [HX HXA] [HY HYA]; case: monoH => h _ setDH _; split. exact: setDH. rewrite (_ : _ `&` _ = (X `&` A) `\` (Y `&` A)); last first. rewrite predeqE => x; split=> [[[? ?] ?]|]; first by split => // -[]. by move=> [[? ?] YAx]; split => //; split => //; apply: contra_not YAx. by apply: setDH => //; exact: setSI. have ndH_ A : ndseq_closed (H_ A). move=> F ndF H_AF; split. by case: monoH => h _ _; apply => // => n; have [] := H_AF n. rewrite setI_bigcupl; case: monoH => h _ _; apply => //. by move=> m n mn; apply/subsetPset; apply: setSI; apply/subsetPset/ndF. by move=> n; have [] := H_AF n. have GGH_ X : G X -> G `<=` H_ X. by move=> *; split; [exact: GH | apply: GH; exact: setIG]. have GHH_ X : G X -> H `<=` H_ X. move=> CX; apply: smallestH; [split => //; last exact: GGH_|exact: GGH_]. by move=> ? [? ?]; case: monoH => + _ _ _; exact. have HGH_ X : H X -> G `<=` H_ X. by move=> *; split; [exact: GH|rewrite setIC; apply GHH_]. have HHH_ X : H X -> H `<=` H_ X. move=> HX; apply: (smallestH _ _ (HGH_ _ HX)); split=> //. - by move=> ? [? ?]; case: monoH => + _ _ _; exact. - exact: HGH_. by move=> *; apply HHH_. 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)