near_in_itv_oy/Nyo (#1375)

* near_in_itv_oy/Nyo --------- Co-authored-by: Reynald Affeldt <[email protected]>
math-comp · Nov 13, 2024 · b74a117 · b74a117
1 parent 7e2988d
commit b74a117
Show file tree

Hide file tree

Showing 5 changed files with 48 additions and 12 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -56,6 +56,7 @@
     `nbhs_one_point_compactification_weakE`,
     `locally_compact_completely_regular`, and
     `completely_regular_regular`.
+  + new lemmas `near_in_itvoy`, `near_in_itvNyo`
 
 - in file `mathcomp_extra.v`,
   + new definition `sigT_fun`.
@@ -147,6 +148,9 @@
 
 ### Renamed
 
+- in `normedtype.v`:
+  + `near_in_itv` -> `near_in_itvoo`
+
 ### Generalized
 
 - in `lebesgue_integral.v`:

diff --git a/theories/ftc.v b/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).

diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -5336,10 +5336,42 @@ Lemma bound_itvE (R : numDomainType) (a b : R) :
   (a \in `]-oo, a]).
 Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed.
 
-Lemma near_in_itv {R : realFieldType} (a b : R) :
+Section near_in_itv.
+Context {R : realFieldType} (a b : R).
+
+Lemma near_in_itvoo :
   {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}.
 Proof. exact: interval_open. Qed.
 
+Lemma near_in_itvoy :
+  {in `]a, +oo[, forall y, \forall z \near y, z \in `]a, +oo[}.
+Proof.
+move=> x ax.
+near=> z.
+suff : z \in `]a, +oo[%classic by rewrite inE.
+near: z.
+rewrite near_nbhs.
+apply: (@open_in_nearW _ _ `]a, +oo[%classic) => //.
+by rewrite inE.
+Unshelve. end_near. Qed.
+
+Lemma near_in_itvNyo :
+  {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}.
+Proof.
+move=> x xb.
+near=> z.
+suff : z \in `]-oo, b[%classic by rewrite inE.
+near: z.
+rewrite near_nbhs.
+apply: (@open_in_nearW _ _ `]-oo, b[%classic) => //.
+by rewrite inE/=.
+Unshelve. end_near. 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[ ->
   f @ (x : subspace `[a, b]) --> f x ->
@@ -5350,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 ]" :=

diff --git a/theories/realfun.v b/theories/realfun.v
@@ -1435,10 +1435,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.

diff --git a/theories/trigo.v b/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).