fixes #1390

math-comp · Dec 2, 2024 · 391501a · 391501a
1 parent 2425737
commit 391501a
Show file tree

Hide file tree

Showing 5 changed files with 44 additions and 30 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -11,6 +11,12 @@
 - in `measure.v`:
   + `dynkin_setI_bigsetI` -> `setT_setI_bigsetI`
 
+- 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`
+
 ### Generalized
 
 ### Deprecated

diff --git a/classical/classical_sets.v b/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].

diff --git a/theories/kernel.v b/theories/kernel.v
@@ -639,7 +639,7 @@ Let measurable_fun_kprobability U : measurable U ->
 Proof.
 move=> mU.
 apply: (measurability (ErealGenInftyO.measurableE R)) => _ /= -[_ [r ->] <-].
-rewrite setTI preimage_itv_infty_o -/(P @^-1` mset U r).
+rewrite setTI preimage_itvNyo -/(P @^-1` mset U r).
 have [r0|r0] := leP 0%R r; last by rewrite lt0_mset// preimage_set0.
 have [r1|r1] := leP r 1%R; last by rewrite gt1_mset// preimage_setT.
 move: mP => /(_ measurableT (mset U r)); rewrite setTI; apply.

diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
@@ -434,16 +434,16 @@ Hypotheses (mD : measurable D) (mf : measurable_fun D f).
 Implicit Types y : \bar R.
 
 Lemma emeasurable_fun_c_infty y : measurable (D `&` [set x | y <= f x]).
-Proof. by rewrite -preimage_itv_c_infty; exact/mf/emeasurable_itv. Qed.
+Proof. by rewrite -preimage_itvcy; exact/mf/emeasurable_itv. Qed.
 
 Lemma emeasurable_fun_o_infty y :  measurable (D `&` [set x | y < f x]).
-Proof. by rewrite -preimage_itv_o_infty; exact/mf/emeasurable_itv. Qed.
+Proof. by rewrite -preimage_itvoy; exact/mf/emeasurable_itv. Qed.
 
 Lemma emeasurable_fun_infty_o y : measurable (D `&` [set x | f x < y]).
-Proof. by rewrite -preimage_itv_infty_o; exact/mf/emeasurable_itv. Qed.
+Proof. by rewrite -preimage_itvNyo; exact/mf/emeasurable_itv. Qed.
 
 Lemma emeasurable_fun_infty_c y : measurable (D `&` [set x | f x <= y]).
-Proof. by rewrite -preimage_itv_infty_c; exact/mf/emeasurable_itv. Qed.
+Proof. by rewrite -preimage_itvNyc; exact/mf/emeasurable_itv. Qed.
 
 Lemma emeasurable_fin_num : measurable (D `&` [set x | f x \is a fin_num]).
 Proof.
@@ -908,7 +908,7 @@ Lemma lower_semicontinuous_measurable {R : realType} (f : R -> \bar R) :
 Proof.
 move=> scif; apply: (measurability (ErealGenOInfty.measurableE R)).
 move=> /= _ [_ [a ->]] <-; apply: measurableI => //; apply: open_measurable.
-by rewrite preimage_itv_o_infty; move/lower_semicontinuousP : scif; exact.
+by rewrite preimage_itvoy; move/lower_semicontinuousP : scif; exact.
 Qed.
 
 Section standard_measurable_fun.
@@ -986,12 +986,12 @@ Lemma measurable_funD D f g :
   measurable_fun D f -> measurable_fun D g -> measurable_fun D (f \+ g).
 Proof.
 move=> mf mg mD; apply: (measurability (RGenOInfty.measurableE R)) => //.
-move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_o_infty.
+move=> /= _ [_ [a ->] <-]; rewrite preimage_itvoy.
 rewrite [X in measurable X](_ : _ = \bigcup_(q : rat)
   ((D `&` [set x | ratr q < f x]) `&` (D `&` [set x | a - ratr q < g x]))).
   apply: bigcupT_measurable_rat => q; apply: measurableI.
-  - by rewrite -preimage_itv_o_infty; apply: mf => //; apply: measurable_itv.
-  - by rewrite -preimage_itv_o_infty; apply: mg => //; apply: measurable_itv.
+  - by rewrite -preimage_itvoy; apply: mf => //; exact: measurable_itv.
+  - by rewrite -preimage_itvoy; apply: mg => //; exact: measurable_itv.
 rewrite predeqE => x; split => [|[r _] []/= [Dx rfx]] /= => [[Dx]|[_]].
   rewrite -ltrBlDr => /rat_in_itvoo[r]; rewrite inE /= => /itvP h.
   exists r => //; rewrite setIACA setIid; split => //; split => /=.
@@ -1026,15 +1026,15 @@ Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g ->
 Proof.
 move=> mf mg mD; apply: (measurable_fun_bool true) => //.
 under eq_fun do rewrite -subr_gt0.
-by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_funB.
+by rewrite preimage_true -preimage_itvoy; exact: measurable_funB.
 Qed.
 
 Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => f x <= g x).
 Proof.
 move=> mf mg mD; apply: (measurable_fun_bool true) => //.
 under eq_fun do rewrite -subr_ge0.
-by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB.
+by rewrite preimage_true -preimage_itvcy; exact: measurable_funB.
 Qed.
 
 Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g ->
@@ -1247,12 +1247,12 @@ Lemma measurable_fun_addn D f g : measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => f x + g x)%N.
 Proof.
 move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
-move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_c_infty.
+move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy.
 rewrite [X in measurable X](_ : _ = \bigcup_q
   ((D `&` [set x | q <= f x]%O) `&` (D `&` [set x | (a - q)%N <= g x]%O))).
   apply: bigcupT_measurable => q; apply: measurableI.
-  - by rewrite -preimage_itv_c_infty; exact: mf.
-  - by rewrite -preimage_itv_c_infty; exact: mg.
+  - by rewrite -preimage_itvcy; exact: mf.
+  - by rewrite -preimage_itvcy; exact: mg.
 rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[?]].
 - move=> afxgx; exists (a - g x)%N => //=; split; split => //.
     by rewrite leEnat leq_subLR// addnC -leEnat.
@@ -1269,8 +1269,8 @@ move=> mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
 move=> /= _ [_ [a ->] <-]; rewrite [X in measurable X](_ : _ =
   ((D `&` [set x | a <= f x]%O) `|` (D `&` [set x | a <= g x]%O))).
   apply: measurableU.
-  - by rewrite -preimage_itv_c_infty; exact: mf.
-  - by rewrite -preimage_itv_c_infty; exact: mg.
+  - by rewrite -preimage_itvcy; exact: mf.
+  - by rewrite -preimage_itvcy; exact: mg.
 rewrite predeqE => x; split => [[Dx /=]|].
 - by rewrite in_itv/= andbT; have [fg agx|gf afx] := leqP (f x) (g x); tauto.
 - move=> [[Dx /= afx]|[Dx /= agx]].
@@ -1285,13 +1285,13 @@ Let measurable_fun_subn' D f g : (forall t, g t <= f t)%N ->
   measurable_fun D (fun x => f x - g x)%N.
 Proof.
 move=> gf mf mg mD; apply: (measurability NGenCInfty.measurableE) => //.
-move=> /= _ [_ [a ->] <-]; rewrite preimage_itv_c_infty.
+move=> /= _ [_ [a ->] <-]; rewrite preimage_itvcy.
 rewrite [X in measurable X](_ : _ = \bigcup_q
   ((D `&` [set x | maxn a q <= f x]%O) `&`
    (D `&` [set x | g x <= (q - a)%N]%O))).
   apply: bigcupT_measurable => q; apply: measurableI.
-  - by rewrite -preimage_itv_c_infty; exact: mf.
-  - by rewrite -preimage_itv_infty_c; exact: mg.
+  - by rewrite -preimage_itvcy; exact: mf.
+  - by rewrite -preimage_itvNyc; exact: mg.
 rewrite predeqE => x; split => [|[r ?] []/= [Dx rfx]] /= => [[Dx]|[_]].
 - move=> afxgx; exists (g x + a)%N => //; split; split => //=.
     rewrite leEnat; have /maxn_idPr -> := leq_addl (g x) a.
@@ -1325,15 +1325,15 @@ move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
     apply/funext => n; apply/idP/idP.
       by rewrite !ltEnat /ltn/= => fg; rewrite subn_gt0.
     by rewrite !ltEnat /ltn/= => fg; rewrite -subn_gt0.
-  by rewrite preimage_true -preimage_itv_o_infty; exact: measurable_fun_subn.
+  by rewrite preimage_true -preimage_itvoy; exact: measurable_fun_subn.
 - under eq_fun do rewrite ltnNge.
   rewrite preimage_false set_predC setCK.
   rewrite [X in _ `&` X](_ : _ = \bigcup_(i in range f)
       ([set y | g y <= i]%O `&` [set t | i <= f t]%O)).
     rewrite setI_bigcupr; apply: bigcup_measurable => k fk.
     rewrite setIIr; apply: measurableI => //.
-    + by rewrite -preimage_itv_infty_c; exact: mg.
-    + by rewrite -preimage_itv_c_infty; exact: mf.
+    + by rewrite -preimage_itvNyc; exact: mg.
+    + by rewrite -preimage_itvcy; exact: mf.
   apply/funext => n/=.
   suff : (g n <= f n)%N <->
       (\bigcup_(i in range f) ([set y | g y <= i]%O `&` [set t | i <= f t]%O)) n.
@@ -1353,8 +1353,8 @@ move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
       \bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)).
     rewrite setI_bigcupr; apply: bigcup_measurable => k fk.
     rewrite setIIr; apply: measurableI => //.
-    + by rewrite -preimage_itv_infty_c; exact: mf.
-    + by rewrite -preimage_itv_c_infty; exact: mg.
+    + by rewrite -preimage_itvNyc; exact: mf.
+    + by rewrite -preimage_itvcy; exact: mg.
   apply/funext => n/=.
   suff : (f n <= g n)%N <->
     (\bigcup_(i in range g) ([set y | f y <= i]%O `&` [set t | i <= g t]%O)) n.
@@ -1386,7 +1386,7 @@ Lemma EFin_measurable (D : set R) : measurable_fun D EFin.
 Proof.
 move=> mD; apply: (measurability (ErealGenOInfty.measurableE R)) => //.
 move=> /= _ [_ [x ->]] <-; apply: measurableI => //.
-by rewrite preimage_itv_o_infty EFin_itv; exact: measurable_itv.
+by rewrite preimage_itvoy EFin_itv; exact: measurable_itv.
 Qed.
 
 Lemma abse_measurable (D : set (\bar R)) : measurable_fun D abse.

diff --git a/theories/realfun.v b/theories/realfun.v
@@ -1516,7 +1516,7 @@ have fwcte : {within `[x - e, x + e], continuous f}.
 have fKe : {in `[x - e, x + e], cancel f g}
   by near: e; apply/at_right_in_segment.
 have nearfx : \forall y \near f x, y \in f @`](x - e), (x + e)[.
-  apply: near_in_itv; apply: mono_mem_image_itvoo; last first.
+  apply: near_in_itvoo; apply: mono_mem_image_itvoo; last first.
     by rewrite in_itv/= -ltr_distlC subrr normr0.
   apply: itv_continuous_inj_mono => //.
   by apply: (@can_in_inj _ _ _ _ g); near: e; apply/at_right_in_segment.