isolate the theory of lime_sup

CHANGELOG_UNRELEASED.md

@@ -53,6 +53,34 @@
     `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`,
     `maximal_inequality`
 
+- in `constructive_ereal.v`
+  + lemma `lee_subgt0Pr`
+
+- in `topology.v`:
+  + lemma `nbhs_dnbhs_neq`
+
+- in `normedtype.v`:
+  + lemma `not_near_at_rightP`
+
+- in `realfun.v`:
+  + lemma `cvg_at_right_left_dnbhs`
+  + lemma `cvg_at_rightP`
+  + lemma `cvg_at_leftP`
+  + lemma `cvge_at_rightP`
+  + lemma `lime_sup`
+  + lemma `lime_inf`
+  + lemma `lime_supE`
+  + lemma `lime_infE`
+  + lemma `lime_infN`
+  + lemma `lime_supN`
+  + lemma `lime_sup_ge0`
+  + lemma `lime_inf_ge0`
+  + lemma `lime_supD`
+  + lemma `lime_sup_le`
+  + lemma `lime_inf_sup`
+  + lemma `lim_lime_inf`
+  + lemma `lim_lime_sup`
+
 ### Changed
 
 - in `normedtype.v`:

theories/constructive_ereal.v

@@ -3035,6 +3035,14 @@ apply/(iffP idP) => [|].
   by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy.
 Qed.
 
+Lemma lee_subgt0Pr x y :
+  reflect (forall e, (0 < e)%R -> x - e%:E <= y) (x <= y).
+Proof.
+apply/(iffP idP) => [xy e|xy].
+  by rewrite lee_subl_addr//; move: e; exact/lee_addgt0Pr.
+by apply/lee_addgt0Pr => e e0; rewrite -lee_subl_addr// xy.
+Qed.
+
 Lemma lee_mul01Pr x y : 0 <= x ->
   reflect (forall r, (0 < r < 1)%R -> r%:E * x <= y) (x <= y).
 Proof.

theories/normedtype.v

@@ -2077,6 +2077,16 @@ Lemma nbhs_left_ge x z : z < x -> \forall y \near x^'-, z <= y.
 Proof. by move=> xz; near do apply/ltW; apply: nbhs_left_gt.
 Unshelve. all: by end_near. Qed.
 
+Lemma not_near_at_rightP T (f : R -> T) (p : R) (P : pred T) :
+  ~ (\forall x \near p^'+, P (f x)) ->
+  forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P (f x).
+Proof.
+move=> pPf e; apply: contrapT => /forallPNP pePf; apply: pPf; near=> t.
+apply: contrapT; apply: pePf; apply/andP; split.
+- by near: t; exact: nbhs_right_gt.
+- by near: t; apply: nbhs_right_lt; rewrite ltr_addl.
+Unshelve. all: by end_near. Qed.
+
 End at_left_right.
 #[global] Typeclasses Opaque at_left at_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.