rm near_in_itvyy, deprecation, renaming

CHANGELOG_UNRELEASED.md

@@ -56,7 +56,7 @@
     `nbhs_one_point_compactification_weakE`,
     `locally_compact_completely_regular`, and
     `completely_regular_regular`.
-  + new lemmas `near_in_itvoy`, `near_in_itvyo`, `near_in_itvyy`
+  + new lemmas `near_in_itvoy`, `near_in_itvNyo`
 
 ### Changed
 
@@ -77,6 +77,9 @@
 
 ### Renamed
 
+- in `normedtype.v`:
+  + `near_in_itv` -> `near_in_itvoo`
+
 ### Generalized
 
 ### Deprecated

theories/ftc.v

@@ -979,7 +979,7 @@ rewrite (@integration_by_substitution_decreasing (- F)%R); first last.
   rewrite -derive1E.
   have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg.
   rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//.
-  by case: Fab => + _ _; apply; near: y; exact: near_in_itv.
+  by case: Fab => + _ _; apply; near: y; exact: near_in_itvoo.
 - by move=> x y xab yab yx; rewrite ltrN2 incrF.
 - by [].
 have mGF : measurable_fun `]a, b[ (G \o F).

theories/normedtype.v

@@ -5339,7 +5339,7 @@ Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed.
 Section near_in_itv.
 Context {R : realFieldType} (a b : R).
 
-Lemma near_in_itv :
+Lemma near_in_itvoo :
   {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}.
 Proof. exact: interval_open. Qed.
 
@@ -5352,10 +5352,10 @@ suff : z \in `]a, +oo[%classic by rewrite inE.
 near: z.
 rewrite near_nbhs.
 apply: (@open_in_nearW _ _ `]a, +oo[%classic) => //.
-by rewrite inE/=.
+by rewrite inE.
 Unshelve. end_near. Qed.
 
-Lemma near_in_itvyo :
+Lemma near_in_itvNyo :
   {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}.
 Proof.
 move=> x xb.
@@ -5367,15 +5367,10 @@ apply: (@open_in_nearW _ _ `]-oo, b[%classic) => //.
 by rewrite inE/=.
 Unshelve. end_near. Qed.
 
-Lemma near_in_itvyy :
-  {in `]-oo, +oo[, forall y : R, \forall z \near y, z \in `]-oo, +oo[}.
-Proof.
-move=> x _.
-rewrite -near_nbhs.
-exact: nearW => //.
-Qed.
-
 End near_in_itv.
+#[deprecated(since="mathcomp-analysis 1.7.0",
+  note="use `near_in_itvoo` instead")]
+Notation near_in_itv := near_in_itvoo (only parsing).
 
 Lemma cvg_patch {R : realType} (f : R -> R^o) (a b : R) (x : R) : (a < b)%R ->
   x \in `]a, b[ ->
@@ -5387,15 +5382,15 @@ move/cvgrPdist_lt : xf => /(_ e e0) xf.
 near=> z.
 rewrite patchE ifT//; last first.
   rewrite inE; apply: subset_itv_oo_cc.
-  by near: z; exact: near_in_itv.
+  by near: z; exact: near_in_itvoo.
 near: z.
 rewrite /prop_near1 /nbhs/= /nbhs_subspace ifT// in xf; last first.
   by rewrite inE/=; exact: subset_itv_oo_cc xab.
 case: xf => x0 /= x00 xf.
 near=> z.
 apply: xf => //=.
 rewrite inE; apply: subset_itv_oo_cc.
-by near: z; exact: near_in_itv.
+by near: z; exact: near_in_itvoo.
 Unshelve. all: by end_near. Qed.
 
 Notation "f @`[ a , b ]" :=

theories/realfun.v

@@ -1421,10 +1421,10 @@ have := xb; rewrite le_eqVlt => /orP[/eqP {}xb {ax}|{}xb].
 have xoab : x \in `]a, b[ by rewrite in_itv /=; apply/andP; split.
 near=> y; suff: l <= f y <= u.
   by rewrite ge_max le_min -!andbA => /and4P[-> _ ->].
-have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; apply: near_in_itv.
+have ? : y \in `[a, b] by apply: subset_itv_oo_cc; near: y; exact: near_in_itvoo.
 have fyab : f y \in `[f a, f b] by rewrite in_itv/= !fle// ?ltW.
 rewrite -[l <= _]gle -?[_ <= u]gle// ?fK //.
-apply: subset_itv_oo_cc; near: y; apply: near_in_itv; rewrite in_itv /=.
+apply: subset_itv_oo_cc; near: y; apply: near_in_itvoo; rewrite in_itv /=.
 rewrite -[x]fK // !glt//= lt_min gt_max ?andbT ltrBlDr ltr_pwDr //.
 by apply/and3P; split; rewrite // flt.
 Unshelve. all: by end_near. Qed.

theories/trigo.v

@@ -1003,7 +1003,7 @@ move=> /andP[x_gtN1 x_lt1]; rewrite -[x]acosK; first last.
   by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB.
 apply: nbhs_singleton (near_can_continuous _ _); last first.
    by near=> z; apply: continuous_cos.
-have /near_in_itv aI : acos x \in `]0, pi[.
+have /near_in_itvoo aI : acos x \in `]0, pi[.
   suff : 0 < acos x < pi by [].
   by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT.
 near=> z; apply: cosK.
@@ -1016,7 +1016,7 @@ Lemma is_derive1_acos x :
 Proof.
 move=> /andP[x_gtN1 x_lt1]; rewrite -sin_acos ?ltW // -invrN.
 rewrite -{1}[x]acosK; last by have : -1 <= x <= 1 by rewrite ltW // ltW.
-have /near_in_itv aI : acos x \in `]0, pi[.
+have /near_in_itvoo aI : acos x \in `]0, pi[.
   suff : 0 < acos x < pi by [].
   by rewrite acos_gt0 ?ltW //= acos_ltpi // ltW ?andbT.
 apply: (@is_derive_inverse R cos).
@@ -1103,7 +1103,7 @@ move=> /andP[x_gtN1 x_lt1]; rewrite -[x]asinK; first last.
   by have : -1 <= x <= 1 by rewrite !ltW //; case/andP: xB.
 apply: nbhs_singleton (near_can_continuous _ _); last first.
   by near=> z; apply: continuous_sin.
-have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[.
+have /near_in_itvoo aI : asin x \in `](-(pi/2)), (pi/2)[.
   suff : - (pi / 2) < asin x < pi / 2 by [].
   by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW.
 near=> z; apply: sinK.
@@ -1117,7 +1117,7 @@ Lemma is_derive1_asin x :
 Proof.
 move=> /andP[x_gtN1 x_lt1]; rewrite -cos_asin ?ltW //.
 rewrite -{1}[x]asinK; last by have : -1 <= x <= 1 by rewrite ltW // ltW.
-have /near_in_itv aI : asin x \in `](-(pi/2)), (pi/2)[.
+have /near_in_itvoo aI : asin x \in `](-(pi/2)), (pi/2)[.
   suff : -(pi/2) < asin x < pi/2 by [].
   by rewrite asin_gtNpi2 ?ltW ?andbT //= asin_ltpi2 // ltW.
 apply: (@is_derive_inverse R sin).
@@ -1219,7 +1219,7 @@ Qed.
 Lemma continuous_atan x : {for x, continuous (@atan R)}.
 Proof.
 rewrite -[x]atanK.
-have /near_in_itv aI : atan x \in `](-(pi / 2)), (pi / 2)[.
+have /near_in_itvoo aI : atan x \in `](-(pi / 2)), (pi / 2)[.
   suff : - (pi / 2) < atan x < pi / 2 by [].
   by rewrite atan_gtNpi2 atan_ltpi2.
 apply: nbhs_singleton (near_can_continuous _ _); last first.
@@ -1244,7 +1244,7 @@ Proof.
 rewrite -{1}[x]atanK.
 have cosD0 : cos (atan x) != 0.
   by apply/lt0r_neq0/cos_gt0_pihalf; rewrite atan_gtNpi2 atan_ltpi2.
-have /near_in_itv aI : atan x \in `](-(pi/2)), (pi/2)[.
+have /near_in_itvoo aI : atan x \in `](-(pi/2)), (pi/2)[.
   suff : - (pi / 2) < atan x < pi / 2 by [].
   by rewrite atan_gtNpi2 atan_ltpi2.
 apply: (@is_derive_inverse R tan).