fix

math-comp · Oct 4, 2023 · bcd15c4 · bcd15c4
1 parent 283a3d2
commit bcd15c4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -2049,7 +2049,7 @@ Lemma lebesgue_regularity_inner_sup (D : set R) (eps : R) : measurable D ->
 Proof.
 move=> mD; have [?|] := ltP (mu D) +oo.
   exact: lebesgue_regularity_innerE_bounded.
-have /sigma_finiteP [F RFU [Fsub ffin]] := sigma_finiteT [the {measure set _ -> \bar R} of mu] (*lebesgue_stieltjes_measure.sigmaT_finite_lebesgue_stieltjes_measure [the @cumulative R of idfun] (*TODO: sigma_finiteT mu should be enough but does not seem to work with holder version of mathcomp/coq *) *).
+have /sigma_finiteP [F RFU [Fsub ffin]] := lebesgue_stieltjes_measure.sigmaT_finite_lebesgue_stieltjes_measure [the @cumulative R of idfun] (*TODO: sigma_finiteT mu should be enough but does not seem to work with holder version of mathcomp/coq *).
 rewrite leye_eq => /eqP /[dup] + ->.
 have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI.
 move=> FDp; apply/esym/eq_infty => M.

diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
@@ -493,7 +493,7 @@ HB.instance Definition _ (f : cumulative R) :=
 
 (* TODO: this ought to be turned into a Let but older version of mathcomp/coq
    does not seem to allow, try to change asap *)
-Let sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R) :
+Lemma sigmaT_finite_lebesgue_stieltjes_measure (f : cumulative R) :
   sigma_finite setT (lebesgue_stieltjes_measure f).
 Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed.