proposition: Lemma g_salgebra_measure_unique : forall E, <<s G >> E -> m1 E = m2 E.
proof: Proof. pose G_ n := [set X | G X /\ X `<=` g n]. have G_E n : G_ n = [set g n `&` C | C in G]. rewrite eqEsubset; split. by move=> X [GX Xgn] /=; exists X => //; rewrite setIidr. by rewrite /G_ => X [Y GY <-{X}]; split; [exact: setIG|apply: subIset; left]. have gIsGE n : [set g n `&` A | A in <<s G >>] = <<s g n, preimage_class (g n) id G >>. rewrite sigma_algebra_preimage_classE eqEsubset; split. by move=> _ /= [Y sGY <-]; exists Y => //; rewrite preimage_id setIC. by move=> _ [Y mY <-] /=; exists Y => //; rewrite preimage_id setIC. have preimg_gGE n : preimage_class (g n) id G = G_ n. rewrite eqEsubset; split => [_ [Y GY <-]|]. by rewrite preimage_id G_E /=; exists Y => //; rewrite setIC. by move=> X [GX Xgn]; exists X => //; rewrite preimage_id setIidr. apply: g_salgebra_measure_unique_cover => //. move=> n A sGA; apply: (@g_salgebra_measure_unique_trace _ _ _ G (g n)) => //. - exact: Gm. - by move=> ? [? _]; exact/Gm. - by move=> ? ? [? ?] [? ?]; split; [exact: setIG|apply: subIset; tauto]. - by split. - by move=> ? [? ?]; exact: m1m2. - move=> X; rewrite -/(G_ n) -preimg_gGE -gIsGE. by case=> B sGB <-{X}; apply: subIset; left. - by rewrite -/(G_ n) -preimg_gGE -gIsGE; exists A. 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)