chore(*): introduce notation for left/right/punctured nhds (#10694)

New notation:

* `𝓝[≤] x`: the filter `nhds_within x (set.Iic x)` of left-neighborhoods of `x`;
* `𝓝[≥] x`: the filter `nhds_within x (set.Ici x)` of right-neighborhoods of `x`;
* `𝓝[<] x`: the filter `nhds_within x (set.Iio x)` of punctured left-neighborhoods of `x`;
* `𝓝[>] x`: the filter `nhds_within x (set.Ioi x)` of punctured right-neighborhoods of `x`;
* `𝓝[≠] x`: the filter `nhds_within x {x}ᶜ` of punctured neighborhoods of `x`.

Author: urkud

src/analysis/ODE/gronwall.lean

@@ -106,7 +106,7 @@ See also `norm_le_gronwall_bound_of_norm_deriv_right_le` for a version bounding
 theorem le_gronwall_bound_of_liminf_deriv_right_le {f f' : ℝ → ℝ} {δ K ε : ℝ} {a b : ℝ}
   (hf : continuous_on f (Icc a b))
   (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r →
-    ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r)
+    ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r)
   (ha : f a ≤ δ) (bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε) :
   ∀ x ∈ Icc a b, f x ≤ gronwall_bound δ K ε (x - a) :=
 begin

src/analysis/analytic/basic.lean

@@ -358,7 +358,7 @@ lemma has_fpower_series_on_ball.mono
 ⟨le_trans hr hf.1, r'_pos, λ y hy, hf.has_sum (emetric.ball_subset_ball hr hy)⟩
 
 protected lemma has_fpower_series_at.eventually (hf : has_fpower_series_at f p x) :
-  ∀ᶠ r : ℝ≥0∞ in 𝓝[Ioi 0] 0, has_fpower_series_on_ball f p x r :=
+  ∀ᶠ r : ℝ≥0∞ in 𝓝[>] 0, has_fpower_series_on_ball f p x r :=
 let ⟨r, hr⟩ := hf in
 mem_of_superset (Ioo_mem_nhds_within_Ioi (left_mem_Ico.2 hr.r_pos)) $
   λ r' hr', hr.mono hr'.1 hr'.2.le

src/analysis/analytic/inverse.lean

@@ -477,7 +477,7 @@ begin
       (𝓝 (r * (I + 1) * 0)) := tendsto_const_nhds.mul tendsto_id,
     have B : ∀ᶠ a in 𝓝 0, r * (I + 1) * a < 1/2,
       by { apply (tendsto_order.1 this).2, simp [zero_lt_one] },
-    have C : ∀ᶠ a in 𝓝[set.Ioi (0 : ℝ)] (0 : ℝ), (0 : ℝ) < a,
+    have C : ∀ᶠ a in 𝓝[>] (0 : ℝ), (0 : ℝ) < a,
       by { filter_upwards [self_mem_nhds_within], exact λ a ha, ha },
     rcases (C.and ((A.and B).filter_mono inf_le_left)).exists with ⟨a, ha⟩,
     exact ⟨a, ha.1, ha.2.1.le, ha.2.2.le⟩ },

src/analysis/asymptotics/asymptotics.lean

@@ -755,7 +755,7 @@ begin
   refine ⟨_, λ h, (is_o_zero g' ⊤).congr (λ x, (h x).symm) (λ x, rfl)⟩,
   simp only [is_o_iff, eventually_top],
   refine λ h x, norm_le_zero_iff.1 _,
-  have : tendsto (λ c : ℝ, c * ∥g' x∥) (𝓝[Ioi 0] 0) (𝓝 0) :=
+  have : tendsto (λ c : ℝ, c * ∥g' x∥) (𝓝[>] 0) (𝓝 0) :=
     ((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left inf_le_left,
   exact le_of_tendsto_of_tendsto tendsto_const_nhds this
     (eventually_nhds_within_iff.2 $ eventually_of_forall $ λ c hc, h hc x)

src/analysis/box_integral/divergence_theorem.lean

@@ -170,7 +170,7 @@ begin
     `volume J ≤ (2 * δ) ^ (n + 1)` is small, and the difference of the integrals is small
     because each of the integrals is close to `volume (J.face i) • f x`.
     TODO: there should be a shorter and more readable way to formalize this simple proof. -/
-    have : ∀ᶠ δ in 𝓝[Ioi 0] (0 : ℝ), δ ∈ Ioc (0 : ℝ) (1 / 2) ∧
+    have : ∀ᶠ δ in 𝓝[>] (0 : ℝ), δ ∈ Ioc (0 : ℝ) (1 / 2) ∧
       (∀ y₁ y₂ ∈ closed_ball x δ ∩ I.Icc, ∥f y₁ - f y₂∥ ≤ ε / 2) ∧
       ((2 * δ) ^ (n + 1) * ∥f' x (pi.single i 1)∥ ≤ ε / 2),
     { refine eventually.and _ (eventually.and _ _),

src/analysis/calculus/deriv.lean

@@ -275,7 +275,7 @@ end
 
 lemma has_deriv_at_iff_tendsto_slope :
   has_deriv_at f f' x ↔
-    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[{x}ᶜ] x) (𝓝 f') :=
+    tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[≠] x) (𝓝 f') :=
 has_deriv_at_filter_iff_tendsto_slope
 
 theorem has_deriv_within_at_congr_set {s t u : set 𝕜}
@@ -1724,7 +1724,7 @@ lemma local_homeomorph.has_deriv_at_symm (f : local_homeomorph 𝕜 𝕜) {a f'
 htff'.of_local_left_inverse (f.symm.continuous_at ha) hf' (f.eventually_right_inverse ha)
 
 lemma has_deriv_at.eventually_ne (h : has_deriv_at f f' x) (hf' : f' ≠ 0) :
-  ∀ᶠ z in 𝓝[{x}ᶜ] x, f z ≠ f x :=
+  ∀ᶠ z in 𝓝[≠] x, f z ≠ f x :=
 (has_deriv_at_iff_has_fderiv_at.1 h).eventually_ne
   ⟨∥f'∥⁻¹, λ z, by field_simp [norm_smul, mt norm_eq_zero.1 hf']⟩
 
@@ -2015,7 +2015,7 @@ lemma has_deriv_within_at.limsup_slope_le' (hf : has_deriv_within_at f f' s x)
 
 lemma has_deriv_within_at.liminf_right_slope_le
   (hf : has_deriv_within_at f f' (Ici x) x) (hr : f' < r) :
-  ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r :=
+  ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r :=
 (hf.Ioi_of_Ici.limsup_slope_le' (lt_irrefl x) hr).frequently
 
 end real
@@ -2072,7 +2072,7 @@ is less than or equal to `∥f'∥`. See also `has_deriv_within_at.limsup_norm_s
 for a stronger version using limit superior and any set `s`. -/
 lemma has_deriv_within_at.liminf_right_norm_slope_le
   (hf : has_deriv_within_at f f' (Ici x) x) (hr : ∥f'∥ < r) :
-  ∃ᶠ z in 𝓝[Ioi x] x, ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
+  ∃ᶠ z in 𝓝[>] x, ∥z - x∥⁻¹ * ∥f z - f x∥ < r :=
 (hf.Ioi_of_Ici.limsup_norm_slope_le hr).frequently
 
 /-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ∥f'∥` the ratio
@@ -2088,7 +2088,7 @@ See also
   `∥f z - f x∥` instead of `∥f z∥ - ∥f x∥`. -/
 lemma has_deriv_within_at.liminf_right_slope_norm_le
   (hf : has_deriv_within_at f f' (Ici x) x) (hr : ∥f'∥ < r) :
-  ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r :=
+  ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r :=
 begin
   have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently,
   refine this.mp (eventually.mono self_mem_nhds_within _),

src/analysis/calculus/extend_deriv.lean

@@ -99,8 +99,8 @@ end
 its derivative also converges at `a`, then `f` is differentiable on the right at `a`. -/
 lemma has_deriv_at_interval_left_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
   (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
-  (hs : s ∈ 𝓝[Ioi a] a)
-  (f_lim' : tendsto (λx, deriv f x) (𝓝[Ioi a] a) (𝓝 e)) :
+  (hs : s ∈ 𝓝[>] a)
+  (f_lim' : tendsto (λx, deriv f x) (𝓝[>] a) (𝓝 e)) :
   has_deriv_within_at f e (Ici a) a :=
 begin
   /- This is a specialization of `has_fderiv_at_boundary_of_tendsto_fderiv`. To be in the setting of
@@ -136,8 +136,8 @@ end
 its derivative also converges at `a`, then `f` is differentiable on the left at `a`. -/
 lemma has_deriv_at_interval_right_endpoint_of_tendsto_deriv {s : set ℝ} {e : E} {a : ℝ} {f : ℝ → E}
   (f_diff : differentiable_on ℝ f s) (f_lim : continuous_within_at f s a)
-  (hs : s ∈ 𝓝[Iio a] a)
-  (f_lim' : tendsto (λx, deriv f x) (𝓝[Iio a] a) (𝓝 e)) :
+  (hs : s ∈ 𝓝[<] a)
+  (f_lim' : tendsto (λx, deriv f x) (𝓝[<] a) (𝓝 e)) :
   has_deriv_within_at f e (Iic a) a :=
 begin
   /- This is a specialization of `has_fderiv_at_boundary_of_differentiable`. To be in the setting of
@@ -183,7 +183,7 @@ begin
     -- extension results.
     apply has_deriv_at_interval_left_endpoint_of_tendsto_deriv diff hf.continuous_within_at
       self_mem_nhds_within,
-    have : tendsto g (𝓝[Ioi x] x) (𝓝 (g x)) := tendsto_inf_left hg,
+    have : tendsto g (𝓝[>] x) (𝓝 (g x)) := tendsto_inf_left hg,
     apply this.congr' _,
     apply mem_of_superset self_mem_nhds_within (λy hy, _),
     exact (f_diff y (ne_of_gt hy)).deriv.symm },
@@ -194,7 +194,7 @@ begin
     -- extension results.
     apply has_deriv_at_interval_right_endpoint_of_tendsto_deriv diff hf.continuous_within_at
       self_mem_nhds_within,
-    have : tendsto g (𝓝[Iio x] x) (𝓝 (g x)) := tendsto_inf_left hg,
+    have : tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg,
     apply this.congr' _,
     apply mem_of_superset self_mem_nhds_within (λy hy, _),
     exact (f_diff y (ne_of_lt hy)).deriv.symm },

src/analysis/calculus/fderiv.lean

@@ -2780,7 +2780,7 @@ begin
 end
 
 lemma has_fderiv_at.eventually_ne (h : has_fderiv_at f f' x) (hf' : ∃ C, ∀ z, ∥z∥ ≤ C * ∥f' z∥) :
-  ∀ᶠ z in 𝓝[{x}ᶜ] x, f z ≠ f x :=
+  ∀ᶠ z in 𝓝[≠] x, f z ≠ f x :=
 by simpa only [compl_eq_univ_diff] using (has_fderiv_within_at_univ.2 h).eventually_ne hf'
 
 end

src/analysis/calculus/fderiv_symmetric.lean

@@ -70,7 +70,7 @@ This is a technical statement used to show that the second derivative is symmetr
 lemma convex.taylor_approx_two_segment
   {v w : E} (hv : x + v ∈ interior s) (hw : x + v + w ∈ interior s) :
   is_o (λ (h : ℝ), f (x + h • v + h • w) - f (x + h • v) - h • f' x w
-    - h^2 • f'' v w - (h^2/2) • f'' w w) (λ h, h^2) (𝓝[Ioi (0 : ℝ)] 0) :=
+    - h^2 • f'' v w - (h^2/2) • f'' w w) (λ h, h^2) (𝓝[>] (0 : ℝ)) :=
 begin
   -- it suffices to check that the expression is bounded by `ε * ((∥v∥ + ∥w∥) * ∥w∥) * h^2` for
   -- small enough `h`, for any positive `ε`.
@@ -79,12 +79,12 @@ begin
   -- good up to `δ`.
   rw [has_fderiv_within_at, has_fderiv_at_filter, is_o_iff] at hx,
   rcases metric.mem_nhds_within_iff.1 (hx εpos) with ⟨δ, δpos, sδ⟩,
-  have E1 : ∀ᶠ h in 𝓝[Ioi (0:ℝ)] 0, h * (∥v∥ + ∥w∥) < δ,
-  { have : filter.tendsto (λ h, h * (∥v∥ + ∥w∥)) (𝓝[Ioi (0:ℝ)] 0) (𝓝 (0 * (∥v∥ + ∥w∥))) :=
+  have E1 : ∀ᶠ h in 𝓝[>] (0:ℝ), h * (∥v∥ + ∥w∥) < δ,
+  { have : filter.tendsto (λ h, h * (∥v∥ + ∥w∥)) (𝓝[>] (0:ℝ)) (𝓝 (0 * (∥v∥ + ∥w∥))) :=
       (continuous_id.mul continuous_const).continuous_within_at,
     apply (tendsto_order.1 this).2 δ,
     simpa only [zero_mul] using δpos },
-  have E2 : ∀ᶠ h in 𝓝[Ioi (0:ℝ)] 0, (h : ℝ) < 1 :=
+  have E2 : ∀ᶠ h in 𝓝[>] (0:ℝ), (h : ℝ) < 1 :=
     mem_nhds_within_Ioi_iff_exists_Ioo_subset.2
       ⟨(1 : ℝ), by simp only [mem_Ioi, zero_lt_one], λ x hx, hx.2⟩,
   filter_upwards [E1, E2, self_mem_nhds_within],
@@ -194,7 +194,7 @@ lemma convex.is_o_alternate_sum_square
   {v w : E} (h4v : x + (4 : ℝ) • v ∈ interior s) (h4w : x + (4 : ℝ) • w ∈ interior s) :
   is_o (λ (h : ℝ), f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w))
     - f (x + h • (2 • v + w)) - f (x + h • (v + 2 • w)) - h^2 • f'' v w)
-    (λ h, h^2) (𝓝[Ioi (0 : ℝ)] 0) :=
+    (λ h, h^2) (𝓝[>] (0 : ℝ)) :=
 begin
   have A : (1 : ℝ)/2 ∈ Ioc (0 : ℝ) 1 := ⟨by norm_num, by norm_num⟩,
   have B : (1 : ℝ)/2 ∈ Icc (0 : ℝ) 1 := ⟨by norm_num, by norm_num⟩,
@@ -252,14 +252,14 @@ lemma convex.second_derivative_within_at_symmetric_of_mem_interior
   {v w : E} (h4v : x + (4 : ℝ) • v ∈ interior s) (h4w : x + (4 : ℝ) • w ∈ interior s) :
   f'' w v = f'' v w :=
 begin
-  have A : is_o (λ (h : ℝ), h^2 • (f'' w v- f'' v w)) (λ h, h^2) (𝓝[Ioi (0 : ℝ)] 0),
+  have A : is_o (λ (h : ℝ), h^2 • (f'' w v- f'' v w)) (λ h, h^2) (𝓝[>] (0 : ℝ)),
   { convert (s_conv.is_o_alternate_sum_square hf xs hx h4v h4w).sub
             (s_conv.is_o_alternate_sum_square hf xs hx h4w h4v),
     ext h,
     simp only [add_comm, smul_add, smul_sub],
     abel },
-  have B : is_o (λ (h : ℝ), f'' w v - f'' v w) (λ h, (1 : ℝ)) (𝓝[Ioi (0 : ℝ)] 0),
-  { have : is_O (λ (h : ℝ), 1/h^2) (λ h, 1/h^2) (𝓝[Ioi (0 : ℝ)] 0) := is_O_refl _ _,
+  have B : is_o (λ (h : ℝ), f'' w v - f'' v w) (λ h, (1 : ℝ)) (𝓝[>] (0 : ℝ)),
+  { have : is_O (λ (h : ℝ), 1/h^2) (λ h, 1/h^2) (𝓝[>] (0 : ℝ)) := is_O_refl _ _,
     have C := this.smul_is_o A,
     apply C.congr' _ _,
     { filter_upwards [self_mem_nhds_within],
@@ -298,7 +298,7 @@ begin
     refine tendsto_const_nhds.smul _,
     refine tendsto_const_nhds.add _,
     exact continuous_at_id.smul continuous_at_const },
-  have B : ∀ (m : E), ∀ᶠ t in 𝓝[Ioi (0 : ℝ)] (0 : ℝ), x + (4 : ℝ) • (z + t • m) ∈ interior s,
+  have B : ∀ (m : E), ∀ᶠ t in 𝓝[>] (0 : ℝ), x + (4 : ℝ) • (z + t • m) ∈ interior s,
   { assume m,
     apply nhds_within_le_nhds,
     apply A m,

src/analysis/calculus/lhopital.lean

@@ -47,14 +47,14 @@ include hab
 theorem lhopital_zero_right_on_Ioo
   (hff' : ∀ x ∈ Ioo a b, has_deriv_at f (f' x) x) (hgg' : ∀ x ∈ Ioo a b, has_deriv_at g (g' x) x)
   (hg' : ∀ x ∈ Ioo a b, g' x ≠ 0)
-  (hfa : tendsto f (𝓝[Ioi a] a) (𝓝 0)) (hga : tendsto g (𝓝[Ioi a] a) (𝓝 0))
-  (hdiv : tendsto (λ x, (f' x) / (g' x)) (𝓝[Ioi a] a) l) :
-  tendsto (λ x, (f x) / (g x)) (𝓝[Ioi a] a) l :=
+  (hfa : tendsto f (𝓝[>] a) (𝓝 0)) (hga : tendsto g (𝓝[>] a) (𝓝 0))
+  (hdiv : tendsto (λ x, (f' x) / (g' x)) (𝓝[>] a) l) :
+  tendsto (λ x, (f x) / (g x)) (𝓝[>] a) l :=
 begin
   have sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b := λ x hx, Ioo_subset_Ioo (le_refl a) (le_of_lt hx.2),
   have hg : ∀ x ∈ (Ioo a b), g x ≠ 0,
   { intros x hx h,
-    have : tendsto g (𝓝[Iio x] x) (𝓝 0),
+    have : tendsto g (𝓝[<] x) (𝓝 0),
     { rw [← h, ← nhds_within_Ioo_eq_nhds_within_Iio hx.1],
       exact ((hgg' x hx).continuous_at.continuous_within_at.mono $ sub x hx).tendsto },
     obtain ⟨y, hyx, hy⟩ : ∃ c ∈ Ioo a x, g' c = 0,
@@ -220,9 +220,9 @@ include hab
 
 theorem lhopital_zero_right_on_Ioo
   (hdf : differentiable_on ℝ f (Ioo a b)) (hg' : ∀ x ∈ Ioo a b, deriv g x ≠ 0)
-  (hfa : tendsto f (𝓝[Ioi a] a) (𝓝 0)) (hga : tendsto g (𝓝[Ioi a] a) (𝓝 0))
-  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (𝓝[Ioi a] a) l) :
-  tendsto (λ x, (f x) / (g x)) (𝓝[Ioi a] a) l :=
+  (hfa : tendsto f (𝓝[>] a) (𝓝 0)) (hga : tendsto g (𝓝[>] a) (𝓝 0))
+  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (𝓝[>] a) l) :
+  tendsto (λ x, (f x) / (g x)) (𝓝[>] a) l :=
 begin
   have hdf : ∀ x ∈ Ioo a b, differentiable_at ℝ f x,
     from λ x hx, (hdf x hx).differentiable_at (Ioo_mem_nhds hx.1 hx.2),
@@ -307,19 +307,19 @@ namespace has_deriv_at
 
 /-- L'Hôpital's rule for approaching a real from the right, `has_deriv_at` version -/
 theorem lhopital_zero_nhds_right
-  (hff' : ∀ᶠ x in 𝓝[Ioi a] a, has_deriv_at f (f' x) x)
-  (hgg' : ∀ᶠ x in 𝓝[Ioi a] a, has_deriv_at g (g' x) x)
-  (hg' : ∀ᶠ x in 𝓝[Ioi a] a, g' x ≠ 0)
-  (hfa : tendsto f (𝓝[Ioi a] a) (𝓝 0)) (hga : tendsto g (𝓝[Ioi a] a) (𝓝 0))
-  (hdiv : tendsto (λ x, (f' x) / (g' x)) (𝓝[Ioi a] a) l) :
-  tendsto (λ x, (f x) / (g x)) (𝓝[Ioi a] a) l :=
+  (hff' : ∀ᶠ x in 𝓝[>] a, has_deriv_at f (f' x) x)
+  (hgg' : ∀ᶠ x in 𝓝[>] a, has_deriv_at g (g' x) x)
+  (hg' : ∀ᶠ x in 𝓝[>] a, g' x ≠ 0)
+  (hfa : tendsto f (𝓝[>] a) (𝓝 0)) (hga : tendsto g (𝓝[>] a) (𝓝 0))
+  (hdiv : tendsto (λ x, (f' x) / (g' x)) (𝓝[>] a) l) :
+  tendsto (λ x, (f x) / (g x)) (𝓝[>] a) l :=
 begin
   rw eventually_iff_exists_mem at *,
   rcases hff' with ⟨s₁, hs₁, hff'⟩,
   rcases hgg' with ⟨s₂, hs₂, hgg'⟩,
   rcases hg' with ⟨s₃, hs₃, hg'⟩,
   let s := s₁ ∩ s₂ ∩ s₃,
-  have hs : s ∈ 𝓝[Ioi a] a := inter_mem (inter_mem hs₁ hs₂) hs₃,
+  have hs : s ∈ 𝓝[>] a := inter_mem (inter_mem hs₁ hs₂) hs₃,
   rw mem_nhds_within_Ioi_iff_exists_Ioo_subset at hs,
   rcases hs with ⟨u, hau, hu⟩,
   refine lhopital_zero_right_on_Ioo hau _ _ _ hfa hga hdiv;
@@ -330,19 +330,19 @@ end
 
 /-- L'Hôpital's rule for approaching a real from the left, `has_deriv_at` version -/
 theorem lhopital_zero_nhds_left
-  (hff' : ∀ᶠ x in 𝓝[Iio a] a, has_deriv_at f (f' x) x)
-  (hgg' : ∀ᶠ x in 𝓝[Iio a] a, has_deriv_at g (g' x) x)
-  (hg' : ∀ᶠ x in 𝓝[Iio a] a, g' x ≠ 0)
-  (hfa : tendsto f (𝓝[Iio a] a) (𝓝 0)) (hga : tendsto g (𝓝[Iio a] a) (𝓝 0))
-  (hdiv : tendsto (λ x, (f' x) / (g' x)) (𝓝[Iio a] a) l) :
-  tendsto (λ x, (f x) / (g x)) (𝓝[Iio a] a) l :=
+  (hff' : ∀ᶠ x in 𝓝[<] a, has_deriv_at f (f' x) x)
+  (hgg' : ∀ᶠ x in 𝓝[<] a, has_deriv_at g (g' x) x)
+  (hg' : ∀ᶠ x in 𝓝[<] a, g' x ≠ 0)
+  (hfa : tendsto f (𝓝[<] a) (𝓝 0)) (hga : tendsto g (𝓝[<] a) (𝓝 0))
+  (hdiv : tendsto (λ x, (f' x) / (g' x)) (𝓝[<] a) l) :
+  tendsto (λ x, (f x) / (g x)) (𝓝[<] a) l :=
 begin
   rw eventually_iff_exists_mem at *,
   rcases hff' with ⟨s₁, hs₁, hff'⟩,
   rcases hgg' with ⟨s₂, hs₂, hgg'⟩,
   rcases hg' with ⟨s₃, hs₃, hg'⟩,
   let s := s₁ ∩ s₂ ∩ s₃,
-  have hs : s ∈ 𝓝[Iio a] a := inter_mem (inter_mem hs₁ hs₂) hs₃,
+  have hs : s ∈ 𝓝[<] a := inter_mem (inter_mem hs₁ hs₂) hs₃,
   rw mem_nhds_within_Iio_iff_exists_Ioo_subset at hs,
   rcases hs with ⟨l, hal, hl⟩,
   refine lhopital_zero_left_on_Ioo hal _ _ _ hfa hga hdiv;
@@ -436,36 +436,36 @@ namespace deriv
 
 /-- **L'Hôpital's rule** for approaching a real from the right, `deriv` version -/
 theorem lhopital_zero_nhds_right
-  (hdf : ∀ᶠ x in 𝓝[Ioi a] a, differentiable_at ℝ f x)
-  (hg' : ∀ᶠ x in 𝓝[Ioi a] a, deriv g x ≠ 0)
-  (hfa : tendsto f (𝓝[Ioi a] a) (𝓝 0)) (hga : tendsto g (𝓝[Ioi a] a) (𝓝 0))
-  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (𝓝[Ioi a] a) l) :
-  tendsto (λ x, (f x) / (g x)) (𝓝[Ioi a] a) l :=
+  (hdf : ∀ᶠ x in 𝓝[>] a, differentiable_at ℝ f x)
+  (hg' : ∀ᶠ x in 𝓝[>] a, deriv g x ≠ 0)
+  (hfa : tendsto f (𝓝[>] a) (𝓝 0)) (hga : tendsto g (𝓝[>] a) (𝓝 0))
+  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (𝓝[>] a) l) :
+  tendsto (λ x, (f x) / (g x)) (𝓝[>] a) l :=
 begin
-  have hdg : ∀ᶠ x in 𝓝[Ioi a] a, differentiable_at ℝ g x,
+  have hdg : ∀ᶠ x in 𝓝[>] a, differentiable_at ℝ g x,
     from hg'.mp (eventually_of_forall $
       λ _ hg', classical.by_contradiction (λ h, hg' (deriv_zero_of_not_differentiable_at h))),
-  have hdf' : ∀ᶠ x in 𝓝[Ioi a] a, has_deriv_at f (deriv f x) x,
+  have hdf' : ∀ᶠ x in 𝓝[>] a, has_deriv_at f (deriv f x) x,
     from hdf.mp (eventually_of_forall $ λ _, differentiable_at.has_deriv_at),
-  have hdg' : ∀ᶠ x in 𝓝[Ioi a] a, has_deriv_at g (deriv g x) x,
+  have hdg' : ∀ᶠ x in 𝓝[>] a, has_deriv_at g (deriv g x) x,
     from hdg.mp (eventually_of_forall $ λ _, differentiable_at.has_deriv_at),
   exact has_deriv_at.lhopital_zero_nhds_right hdf' hdg' hg' hfa hga hdiv
 end
 
 /-- **L'Hôpital's rule** for approaching a real from the left, `deriv` version -/
 theorem lhopital_zero_nhds_left
-  (hdf : ∀ᶠ x in 𝓝[Iio a] a, differentiable_at ℝ f x)
-  (hg' : ∀ᶠ x in 𝓝[Iio a] a, deriv g x ≠ 0)
-  (hfa : tendsto f (𝓝[Iio a] a) (𝓝 0)) (hga : tendsto g (𝓝[Iio a] a) (𝓝 0))
-  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (𝓝[Iio a] a) l) :
-  tendsto (λ x, (f x) / (g x)) (𝓝[Iio a] a) l :=
+  (hdf : ∀ᶠ x in 𝓝[<] a, differentiable_at ℝ f x)
+  (hg' : ∀ᶠ x in 𝓝[<] a, deriv g x ≠ 0)
+  (hfa : tendsto f (𝓝[<] a) (𝓝 0)) (hga : tendsto g (𝓝[<] a) (𝓝 0))
+  (hdiv : tendsto (λ x, ((deriv f) x) / ((deriv g) x)) (𝓝[<] a) l) :
+  tendsto (λ x, (f x) / (g x)) (𝓝[<] a) l :=
 begin
-  have hdg : ∀ᶠ x in 𝓝[Iio a] a, differentiable_at ℝ g x,
+  have hdg : ∀ᶠ x in 𝓝[<] a, differentiable_at ℝ g x,
     from hg'.mp (eventually_of_forall $
       λ _ hg', classical.by_contradiction (λ h, hg' (deriv_zero_of_not_differentiable_at h))),
-  have hdf' : ∀ᶠ x in 𝓝[Iio a] a, has_deriv_at f (deriv f x) x,
+  have hdf' : ∀ᶠ x in 𝓝[<] a, has_deriv_at f (deriv f x) x,
     from hdf.mp (eventually_of_forall $ λ _, differentiable_at.has_deriv_at),
-  have hdg' : ∀ᶠ x in 𝓝[Iio a] a, has_deriv_at g (deriv g x) x,
+  have hdg' : ∀ᶠ x in 𝓝[<] a, has_deriv_at g (deriv g x) x,
     from hdg.mp (eventually_of_forall $ λ _, differentiable_at.has_deriv_at),
   exact has_deriv_at.lhopital_zero_nhds_left hdf' hdg' hg' hfa hga hdiv
 end