proposition: Lemma measure_extension_unique : sigma_finite [set: T] mu -> (forall mu' : {measure set I -> \bar R}, (forall X, d.-measurable X -> mu X = mu' X) -> (forall X, (d.-measurable).-sigma.-measurable X -> measure_extension X = mu' X)).
proof: Proof. move=> [F TF /all_and2[Fm muF]] mu' mu'mu X mX. apply: (@measure_unique _ _ [the measurableType _ of I] d.-measurable F) => //. - by move=> A B Am Bm; apply: measurableI. - by move=> A Am; rewrite /= /measure_extension measurable_mu_extE// mu'mu. - by move=> k; rewrite /= /measure_extension measurable_mu_extE. 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)