proposition: Lemma eq_measureU d (T : ringOfSetsType d) (R : realFieldType) (A B : set T) (mu mu' : {measure set T -> \bar R}): measurable A -> measurable B -> mu A = mu' A -> mu B = mu' B -> mu (A `&` B) = mu' (A `&` B) -> mu (A `|` B) = mu' (A `|` B).
proof: Proof. move=> mA mB muA muB muAB; have [mu'ANoo|] := ltP (mu' A) +oo. by rewrite !measureUfinl/= ?muA ?muB ?muAB. rewrite leye_eq => /eqP mu'A; transitivity (+oo : \bar R); apply/eqP. by rewrite -leye_eq -mu'A -muA le_measure ?inE//=; apply: measurableU. by rewrite eq_sym -leye_eq -mu'A le_measure ?inE//=; apply: measurableU. 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)