various fixes (#1409)

* fix technical lemma

* fixes #1417

* fixes #1390

* fixes #1389

CHANGELOG_UNRELEASED.md

@@ -38,6 +38,18 @@
   + `emeasurable_fun_fsum` -> `emeasurable_fsum`
   + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
 
+- in `classical_sets.v`:
+  + `preimage_itv_o_infty` -> `preimage_itvoy`
+  + `preimage_itv_c_infty` -> `preimage_itvcy`
+  + `preimage_itv_infty_o` -> `preimage_itvNyo`
+  + `preimage_itv_infty_c` -> `preimage_itvNyc`
+
+- in `constructive_ereal.v`:
+  + `maxeMr` -> `maxe_pMr`
+  + `maxeMl` -> `maxe_pMl`
+  + `mineMr` -> `mine_pMr`
+  + `mineMl` -> `mine_pMl`
+
 ### Generalized
 
 ### Deprecated
@@ -50,6 +62,11 @@
 - in `lebesgue_integral.v`:
   + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
   + notation `measurable_fun_indic` (deprecation since 0.6.3)
+- in `constructive_ereal.v`
+  + notation `lee_opp` (deprecated since 0.6.5)
+  + notation `lte_opp` (deprecated since 0.6.5)
+- in `measure.v`:
+  + `dynkin_setI_bigsetI` (use `big_ind` instead)
 
 ### Infrastructure
 

classical/classical_sets.v

@@ -469,25 +469,33 @@ Lemma preimage_itv T d (rT : porderType d) (f : T -> rT) (i : interval rT) (x :
   ((f @^-1` [set` i]) x) = (f x \in i).
 Proof. by rewrite inE. Qed.
 
-Lemma preimage_itv_o_infty T d (rT : porderType d) (f : T -> rT) y :
+Lemma preimage_itvoy T d (rT : porderType d) (f : T -> rT) y :
   f @^-1` `]y, +oo[%classic = [set x | (y < f x)%O].
 Proof.
 by rewrite predeqE => t; split => [|?]; rewrite /= in_itv/= andbT.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to preimage_itvoy")]
+Notation preimage_itv_o_infty := preimage_itvoy (only parsing).
 
-Lemma preimage_itv_c_infty T d (rT : porderType d) (f : T -> rT) y :
+Lemma preimage_itvcy T d (rT : porderType d) (f : T -> rT) y :
   f @^-1` `[y, +oo[%classic = [set x | (y <= f x)%O].
 Proof.
 by rewrite predeqE => t; split => [|?]; rewrite /= in_itv/= andbT.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to preimage_itvcy")]
+Notation preimage_itv_c_infty := preimage_itvcy (only parsing).
 
-Lemma preimage_itv_infty_o T d (rT : orderType d) (f : T -> rT) y :
+Lemma preimage_itvNyo T d (rT : orderType d) (f : T -> rT) y :
   f @^-1` `]-oo, y[%classic = [set x | (f x < y)%O].
 Proof. by rewrite predeqE => t; split => [|?]; rewrite /= in_itv. Qed.
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to preimage_itvNyo")]
+Notation preimage_itv_infty_o := preimage_itvNyo (only parsing).
 
-Lemma preimage_itv_infty_c T d (rT : orderType d) (f : T -> rT) y :
+Lemma preimage_itvNyc T d (rT : orderType d) (f : T -> rT) y :
   f @^-1` `]-oo, y]%classic = [set x | (f x <= y)%O].
 Proof. by rewrite predeqE => t; split => [|?]; rewrite /= in_itv. Qed.
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to preimage_itvNyc")]
+Notation preimage_itv_infty_c := preimage_itvNyc (only parsing).
 
 Lemma eq_set T (P Q : T -> Prop) : (forall x : T, P x = Q x) ->
   [set x | P x] = [set x | Q x].

reals/constructive_ereal.v

@@ -2468,7 +2468,7 @@ Qed.
 Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.
 Proof. by move=> x y; rewrite -[RHS]oppeK oppe_max !oppeK. Qed.
 
-Lemma maxeMr z x y : z \is a fin_num -> 0 <= z ->
+Lemma maxe_pMr z x y : z \is a fin_num -> 0 <= z ->
   z * maxe x y = maxe (z * x) (z * y).
 Proof.
 move=> /[swap]; rewrite le_eqVlt => /predU1P[<- _|z0].
@@ -2478,20 +2478,20 @@ have [xy|yx|->] := ltgtP x y; last by rewrite maxxx.
 - by move=> zfin; rewrite maxC /maxe lte_pmul2l// yx.
 Qed.
 
-Lemma maxeMl z x y : z \is a fin_num -> 0 <= z ->
+Lemma maxe_pMl z x y : z \is a fin_num -> 0 <= z ->
   maxe x y * z = maxe (x * z) (y * z).
-Proof. by move=> zfin z0; rewrite muleC maxeMr// !(muleC z). Qed.
+Proof. by move=> zfin z0; rewrite muleC maxe_pMr// !(muleC z). Qed.
 
-Lemma mineMr z x y : z \is a fin_num -> 0 <= z ->
+Lemma mine_pMr z x y : z \is a fin_num -> 0 <= z ->
   z * mine x y = mine (z * x) (z * y).
 Proof.
 move=> fz zge0.
-by rewrite -eqe_oppP -muleN [in LHS]oppe_min maxeMr// !muleN -oppe_min.
+by rewrite -eqe_oppP -muleN [in LHS]oppe_min maxe_pMr// !muleN -oppe_min.
 Qed.
 
-Lemma mineMl z x y : z \is a fin_num -> 0 <= z ->
+Lemma mine_pMl z x y : z \is a fin_num -> 0 <= z ->
   mine x y * z = mine (x * z) (y * z).
-Proof. by move=> zfin z0; rewrite muleC mineMr// !(muleC z). Qed.
+Proof. by move=> zfin z0; rewrite muleC mine_pMr// !(muleC z). Qed.
 
 Lemma bigmaxe_fin_num (s : seq R) r : r \in s ->
   \big[maxe/-oo%E]_(i <- s) i%:E \is a fin_num.
@@ -2660,10 +2660,6 @@ Arguments lee_sum_nneg_natl {R}.
 Arguments lee_sum_npos_natl {R}.
 #[global] Hint Extern 0 (is_true (0 <= `| _ |)%E) => solve [apply: abse_ge0] : core.
 
-#[deprecated(since="mathcomp-analysis 0.6.5", note="Use leeN2 instead.")]
-Notation lee_opp := leeN2 (only parsing).
-#[deprecated(since="mathcomp-analysis 0.6.5", note="Use lteN2 instead.")]
-Notation lte_opp := lteN2 (only parsing).
 #[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeDl instead.")]
 Notation lee_addl := leeDl (only parsing).
 #[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeDr instead.")]
@@ -2730,6 +2726,14 @@ Notation lte_le_sub := lte_leB (only parsing).
 Notation lee_opp2 := leeN2 (only parsing).
 #[deprecated(since="mathcomp-analysis 1.3.0", note="Use lteN2 instead.")]
 Notation lte_opp2 := lteN2 (only parsing).
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to maxe_pMr")]
+Notation maxeMr := maxe_pMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to maxe_pMl")]
+Notation maxeMl := maxe_pMl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to mine_pMr")]
+Notation mineMr := mine_pMr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to mine_pMl")]
+Notation mineMl := mine_pMl (only parsing).
 
 Module DualAddTheoryRealDomain.