tentative definition of lebesgue stieltjes measure

math-comp · Oct 21, 2022 · dfe97b1 · dfe97b1
1 parent 95da6ec
commit dfe97b1
Show file tree

Hide file tree

Showing 3 changed files with 204 additions and 1,504 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -31,6 +31,7 @@ theories/nsatz_realtype.v
 theories/esum.v
 theories/set_interval.v
 theories/lebesgue_measure.v
+theories/lebesgue_stieltjes_measure.v
 theories/forms.v
 theories/derive.v
 theories/measure.v

diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -554,7 +554,7 @@ Qed.
 End puncture_ereal_itv.
 
 Lemma set1_bigcap_oc (R : realType) (r : R) :
-   [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic.
+  [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic.
 Proof.
 apply/seteqP; split=> [x ->|].
   by move=> i _/=; rewrite in_itv/= lexx ltr_subl_addr ltr_addl invr_gt0 ltr0n.