proposition: Lemma lebesgue_stieltjes_measure_unique (f : cumulative R) (mu : {measure set gitvs -> \bar R}) : (forall X, ocitv X -> lebesgue_stieltjes_measure f X = mu X) -> forall X, measurable X -> lebesgue_stieltjes_measure f X = mu X.
proof: Proof. move=> muE X mX; apply: measure_extension_unique => //=. exact: wlength_sigma_finite. by move=> A mA; rewrite -muE// -measurable_mu_extE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) HB(structures) mathcomp.classical(mathcomp_extra boolp classical_sets) mathcomp.classical(functions fsbigop cardinality) reals ereal signed topology numfun normedtype sequences esum real_interval measure realfun