From dedd3b1e5ff9881a744987d63664fa41bd28f73b Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 5 Mar 2026 18:36:43 +0900
Subject: [PATCH] add lt_nbhs{r,l} variants

- fixes #1879
---
 CHANGELOG_UNRELEASED.md                 |  3 +++
 theories/topology_theory/num_topology.v | 10 +++++++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 1a0d322e8..fe82a9443 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -94,6 +94,7 @@
 
 - in `measurable_function.v`:
   + lemma `preimage_set_system_compS`
+  + lemmas `lt_le_nbhsr`, `lt_le_nbhsl`
 
 ### Changed
 
@@ -313,6 +314,8 @@
   + lemma `derivable_powR`
 - in `convex.v`:
   + definition `convex_function` (from a realType as domain to a convex_lmodType as domain)
+- in `num_topology.v`:
+  + lemma `lt_nbhsl`
 
 ### Deprecated
 
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 8be5ed022..3772ff353 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -399,7 +399,7 @@ exists x => // z /=; rewrite sub0r normrN.
 by apply: le_lt_trans; rewrite ler_norm.
 Qed.
 
-Lemma lt_nbhsl {R : realType} (x a : R) : x < a ->
+Lemma lt_nbhsl {R : realFieldType} (x a : R) : x < a ->
   \forall y \near nbhs x, y < a.
 Proof.
 move=> xb; exists ((a - x) / 2) => /=; first by rewrite divr_gt0// subr_gt0.
@@ -407,6 +407,10 @@ move=> r/=; rewrite ltr_pdivlMr// ltrBrDr; apply: le_lt_trans.
 by rewrite -lerBlDr -normrN opprB (le_trans (ler_norm _))// ler_peMr// ler1n.
 Qed.
 
+Lemma lt_le_nbhsl {R : realFieldType} (t x : R) :
+  x < t -> \forall y \near nbhs x, y <= t.
+Proof. by move/lt_nbhsl; apply: filterS => y /ltW. Qed.
+
 Lemma Nlt_nbhsl {R : realType} (x a : R) :
   - x < a -> \forall y \near nbhs x, - y < a.
 Proof.
@@ -451,6 +455,10 @@ have [uz|uz] := leP u z.
 by rewrite ltr0_norm ?subr_lt0// opprB addrAC -lerBlDr opprK lerD// ?ltW.
 Qed.
 
+Lemma lt_le_nbhsr {R : realFieldType} (t x : R) :
+  t < x -> \forall y \near nbhs x, t <= y.
+Proof. by move/lt_nbhsr; apply: filterS => y /ltW. Qed.
+
 Global Instance Proper_dnbhs_regular_numFieldType (R : numFieldType) (x : R^o) :
   ProperFilter x^'.
 Proof.