add setU_itvob1 and setU_1itvob

CHANGELOG_UNRELEASED.md

@@ -3,6 +3,8 @@
 ## [Unreleased]
 
 ### Added
+- in `set_interval.v`:
+  + lemmas `setU_itvob1`, `setU_1itvob`
 
 - in `realfun.v`:
   + lemma `derivable_sqrt`

classical/set_interval.v

@@ -36,6 +36,13 @@ From mathcomp Require Import functions.
 (*          open_itv_cover A == the set A can be covered by open intervals    *)
 (* ```                                                                        *)
 (*                                                                            *)
+(*  Naming convention for lemmas: itv??    | ? can be:                        *)
+(*                                   ||    |       o = open                   *)
+(*                   left boundary --+|    |       c = closed                 *)
+(*                  right boundary ---+    |       y = +oo%O                  *)
+(*                                         |      Ny = -oo%O                  *)
+(*                                         |  b, bnd = any of the above       *)
+(*                                                                            *)
 (******************************************************************************)
 
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
@@ -183,22 +190,32 @@ Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
 Lemma set_itvxx a : [set` Interval a a] = set0.
 Proof. by move: a => [[|] a |[|]]; rewrite !set_itvE. Qed.
 
+Lemma setU_itvob1 a x : (a <= BLeft x)%O ->
+  [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].
+Proof.
+move=> ax; apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
+by rewrite (rwP eqP) (rwP orP) orbC.
+Qed.
+
+Lemma setU_1itvob a x : (BRight x <= a)%O ->
+  x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].
+Proof.
+move=> ax; apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
+by rewrite (rwP eqP) (rwP orP) orbC.
+Qed.
+
 Lemma setUitv1 a x b : (a <= BLeft x)%O ->
   [set` Interval a (BSide b x)] `|` [set x] = [set` Interval a (BRight x)].
 Proof.
-move=> ax; case: b; last first.
-  by apply: setUidl => ? /= ->; rewrite itv_boundlr ax lexx.
-apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
-by rewrite (rwP eqP) (rwP orP) orbC.
+move=> ax; case: b; [exact: setU_itvob1|].
+by apply: setUidl => ? /= ->; rewrite itv_boundlr ax lexx.
 Qed.
 
 Lemma setU1itv a x b : (BRight x <= a)%O ->
   x |` [set` Interval (BSide b x) a] = [set` Interval (BLeft x) a].
 Proof.
-move=> ax; case: b.
-  by apply: setUidr => ? /= ->; rewrite itv_boundlr ax lexx.
-apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
-by rewrite (rwP eqP) (rwP orP) orbC.
+move=> ax; case: b; [|exact: setU_1itvob].
+by apply: setUidr => ? /= ->; rewrite itv_boundlr ax lexx.
 Qed.
 
 Lemma setUitv_set2 x y b1 b2 :

theories/lebesgue_measure.v

@@ -657,8 +657,8 @@ suff : (lebesgue_measure (`]a - 1, a]%classic%R : set R) =
   rewrite wlength_itv lte_fin ltrBlDr ltrDl ltr01.
   rewrite [in X in X == _]/= EFinN EFinB fin_num_oppeB// addeA subee// add0e.
   by rewrite addeC -sube_eq ?fin_num_adde_defl// subee// => /eqP.
-rewrite -(setUitv1 true) ?bnd_simp; first by rewrite ltrBlDr ltrDl.
-by rewrite measureU// -(setDitv1r _ a true) setDKI.
+rewrite -setU_itvob1; first by rewrite bnd_simp ltrBlDr ltrDl.
+by rewrite measureU// -setDidPl setDitv1r.
 Qed.
 
 Lemma countable_lebesgue_measure0 (A : set R) :
@@ -686,7 +686,7 @@ Let lebesgue_measure_itvoo (a b : R) :
 Proof.
 have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoc a b.
-rewrite 2!wlength_itv => <-; rewrite -(setUitv1 true)// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -setU_itvob1// measureU//.
 - by apply/seteqP; split => // x [/= + xb]; rewrite in_itv/= xb ltxx andbF.
 - by have /= -> := lebesgue_measure_set1 b; rewrite adde0.
 Qed.
@@ -696,7 +696,7 @@ Let lebesgue_measure_itvcc (a b : R) :
 Proof.
 have [ab|ba] := leP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoc a b.
-rewrite 2!wlength_itv => <-; rewrite -(setU1itv false)// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -setU_1itvob// measureU//.
 - by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
 - by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
 Qed.
@@ -706,7 +706,7 @@ Let lebesgue_measure_itvco (a b : R) :
 Proof.
 have [ab|ba] := ltP a b; last by rewrite set_itv_ge ?measure0// -leNgt.
 have := lebesgue_measure_itvoo a b.
-rewrite 2!wlength_itv => <-; rewrite -(setU1itv false)// measureU//.
+rewrite 2!wlength_itv => <-; rewrite -setU_1itvob// measureU//.
 - by apply/seteqP; split => // x [/= ->]; rewrite in_itv/= ltxx.
 - by have /= -> := lebesgue_measure_set1 a; rewrite add0e.
 Qed.

theories/lebesgue_stieltjes_measure.v

@@ -582,14 +582,14 @@ have moo (a b : R) : measurable `]a, b[.
   by rewrite ooE; exact: measurableD.
 have mcc (a b : R) : measurable `[a, b].
   case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
-  by rewrite -(setU1itv false)//; apply/measurableU.
+  by rewrite -setU_1itvob//; apply/measurableU.
 have mco (a b : R) : measurable `[a, b[.
   case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
-  by rewrite -(setU1itv false)//; apply/measurableU.
+  by rewrite -setU_1itvob//; apply/measurableU.
 have oooE (b : R) : `]-oo, b[%classic = `]-oo, b] `\ b.
   by rewrite setDitv1r.
 case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
-- by rewrite -(setU1itv false)//; exact/measurableU.
+- by rewrite -setU_1itvob//; exact/measurableU.
 - by rewrite oooE; exact/measurableD.
 - by rewrite set_itvNyy.
 Qed.

theories/measurable_realfun.v

@@ -1419,7 +1419,7 @@ Lemma emeasurable_fun_itv_obnd_cbndP (a : R) (b : itv_bound R) (f : R -> \bar R)
 Proof.
 have [ab|ba] := leP (BRight a) b; last first.
   by rewrite !set_itv_ge// -leNgt ?(ltW ba)// -ltBRight_leBLeft.
-rewrite -(setU1itv false)// measurable_funU// (propT (measurable_fun_set1 _)).
+rewrite -setU_1itvob// measurable_funU// (propT (measurable_fun_set1 _)).
 by split => // -[].
 Qed.
 
@@ -1436,7 +1436,7 @@ Lemma emeasurable_fun_itv_bndo_bndcP (a : itv_bound R) (b : R) (f : R -> \bar R)
 Proof.
 have [ab|ba] := leP a (BLeft b); last first.
   by rewrite !set_itv_ge// -leNgt// ltW.
-rewrite -(setUitv1 true)// measurable_funU// (propT (measurable_fun_set1 _)).
+rewrite -setU_itvob1// measurable_funU// (propT (measurable_fun_set1 _)).
 by split => // -[].
 Qed.