chore(Topology/Order): fix name of nhdsLT lemma (#34063)

The dual version of this was renamed over a year and a half ago, and it looks like this one was missed. In particular, all lemmas in mathlib about `𝓝[<]` are named `nhdsLT` with this one as the sole exception, and we choose the new name to match the dual `nhdsGT_neBot_of_exists_gt`. 
Note that the statement itself appears different, but is definitionally equal to the old one, and again matches the dual.

Author: b-mehta

Mathlib/Topology/Instances/ENNReal/Lemmas.lean

@@ -188,7 +188,7 @@ theorem nhdsGT_ofNat_neBot (n : ℕ) [n.AtLeastTwo] : (𝓝[>] (OfNat.ofNat n :
 
 @[instance]
 theorem nhdsLT_neBot [NeZero x] : (𝓝[<] x).NeBot :=
-  nhdsWithin_Iio_self_neBot' ⟨0, NeZero.pos x⟩
+  nhdsLT_neBot_of_exists_lt ⟨0, NeZero.pos x⟩
 
 /-- Closed intervals `Set.Icc (x - ε) (x + ε)`, `ε ≠ 0`, form a basis of neighborhoods of an
 extended nonnegative real number `x ≠ ∞`. We use `Set.Icc` instead of `Set.Ioo` because this way the

Mathlib/Topology/Order/DenselyOrdered.lean

@@ -198,9 +198,11 @@ theorem nhdsWithin_Iio_neBot' {b c : α} (H₁ : (Iio c).Nonempty) (H₂ : b ≤
 theorem nhdsWithin_Iio_neBot [NoMinOrder α] {a b : α} (H : a ≤ b) : NeBot (𝓝[Iio b] a) :=
   nhdsWithin_Iio_neBot' nonempty_Iio H
 
-theorem nhdsWithin_Iio_self_neBot' {b : α} (H : (Iio b).Nonempty) : NeBot (𝓝[<] b) :=
+theorem nhdsLT_neBot_of_exists_lt {b : α} (H : ∃ a, a < b) : NeBot (𝓝[<] b) :=
   nhdsWithin_Iio_neBot' H (le_refl b)
 
+@[deprecated (since := "2026-01-16")] alias nhdsWithin_Iio_self_neBot' := nhdsLT_neBot_of_exists_lt
+
 instance nhdsLT_neBot [NoMinOrder α] (a : α) : NeBot (𝓝[<] a) := nhdsWithin_Iio_neBot (le_refl a)
 
 theorem right_nhdsWithin_Ico_neBot {a b : α} (H : a < b) : NeBot (𝓝[Ico a b] b) :=