chore(topology): rename mem_nhds_sets and mem_of_nhds and mem_nhds_sets_iff (#7690)

Rename `mem_nhds_sets` to `is_open.mem_nhds`, and `mem_nhds_sets_iff` to `mem_nhds_iff`, and `mem_of_nhds` to `mem_of_mem_nhds`.

Author: sgouezel

src/algebra/ordered_monoid.lean

@@ -849,7 +849,6 @@ instance [ordered_comm_monoid α] : ordered_comm_monoid (order_dual α) :=
   ..order_dual.partial_order α,
   ..show comm_monoid α, by apply_instance }
 
-
 @[to_additive]
 instance [ordered_cancel_comm_monoid α] : ordered_cancel_comm_monoid (order_dual α) :=
 { le_of_mul_le_mul_left := λ a b c : α, le_of_mul_le_mul_left',

src/analysis/analytic/basic.lean

@@ -588,7 +588,7 @@ begin
   assume u hu x hx,
   rcases ennreal.lt_iff_exists_nnreal_btwn.1 hx with ⟨r', xr', hr'⟩,
   have : emetric.ball (0 : E) r' ∈ 𝓝 x :=
-    mem_nhds_sets emetric.is_open_ball xr',
+    is_open.mem_nhds emetric.is_open_ball xr',
   refine ⟨emetric.ball (0 : E) r', mem_nhds_within_of_mem_nhds this, _⟩,
   simpa [metric.emetric_ball_nnreal] using hf.tendsto_uniformly_on hr' u hu
 end

src/analysis/analytic/composition.lean

@@ -761,7 +761,7 @@ begin
     have B₁ : continuous_at (λ (z : F), g (f x + z)) (f (x + y) - f x),
     { refine continuous_at.comp _ (continuous_const.add continuous_id).continuous_at,
       simp only [add_sub_cancel'_right, id.def],
-      exact Hg.continuous_on.continuous_at (mem_nhds_sets (emetric.is_open_ball) fy_mem) },
+      exact Hg.continuous_on.continuous_at (is_open.mem_nhds (emetric.is_open_ball) fy_mem) },
     have B₂ : f (x + y) - f x ∈ emetric.ball (0 : F) rg,
       by simpa [edist_eq_coe_nnnorm, edist_eq_coe_nnnorm_sub] using fy_mem,
     rw [← nhds_within_eq_of_open B₂ emetric.is_open_ball] at A,

src/analysis/calculus/deriv.lean

@@ -426,7 +426,7 @@ h.congr_of_eventually_eq h₁ (h₁.eq_of_nhds_within hx)
 
 lemma has_deriv_at.congr_of_eventually_eq (h : has_deriv_at f f' x)
   (h₁ : f₁ =ᶠ[𝓝 x] f) : has_deriv_at f₁ f' x :=
-has_deriv_at_filter.congr_of_eventually_eq h h₁ (mem_of_nhds h₁ : _)
+has_deriv_at_filter.congr_of_eventually_eq h h₁ (mem_of_mem_nhds h₁ : _)
 
 lemma filter.eventually_eq.deriv_within_eq (hs : unique_diff_within_at 𝕜 s x)
   (hL : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
@@ -1338,7 +1338,7 @@ begin
   suffices : is_o (λ p : 𝕜 × 𝕜, (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹))
     (λ (p : 𝕜 × 𝕜), (p.1 - p.2) * 1) (𝓝 (x, x)),
   { refine this.congr' _ (eventually_of_forall $ λ _, mul_one _),
-    refine eventually.mono (mem_nhds_sets (is_open_ne.prod is_open_ne) ⟨hx, hx⟩) _,
+    refine eventually.mono (is_open.mem_nhds (is_open_ne.prod is_open_ne) ⟨hx, hx⟩) _,
     rintro ⟨y, z⟩ ⟨hy, hz⟩,
     simp only [mem_set_of_eq] at hy hz, -- hy : y ≠ 0, hz : z ≠ 0
     field_simp [hx, hy, hz], ring, },
@@ -1833,7 +1833,7 @@ begin
       sub_zero, int.cast_one] },
   { rw [function.iterate_succ', finset.prod_range_succ, int.cast_mul, mul_assoc,
       int.coe_nat_succ, ← sub_sub, ← ((has_deriv_at_fpow _ hx).const_mul _).deriv],
-    exact filter.eventually_eq.deriv_eq (eventually.mono (mem_nhds_sets is_open_ne hx) @ihk) }
+    exact filter.eventually_eq.deriv_eq (eventually.mono (is_open.mem_nhds is_open_ne hx) @ihk) }
 end
 
 end fpow
@@ -1846,12 +1846,12 @@ variables {f : ℝ → ℝ} {f' : ℝ} {s : set ℝ} {x : ℝ} {r : ℝ}
 
 lemma has_deriv_within_at.limsup_slope_le (hf : has_deriv_within_at f f' s x) (hr : f' < r) :
   ∀ᶠ z in 𝓝[s \ {x}] x, (z - x)⁻¹ * (f z - f x) < r :=
-has_deriv_within_at_iff_tendsto_slope.1 hf (mem_nhds_sets is_open_Iio hr)
+has_deriv_within_at_iff_tendsto_slope.1 hf (is_open.mem_nhds is_open_Iio hr)
 
 lemma has_deriv_within_at.limsup_slope_le' (hf : has_deriv_within_at f f' s x)
   (hs : x ∉ s) (hr : f' < r) :
   ∀ᶠ z in 𝓝[s] x, (z - x)⁻¹ * (f z - f x) < r :=
-(has_deriv_within_at_iff_tendsto_slope' hs).1 hf (mem_nhds_sets is_open_Iio hr)
+(has_deriv_within_at_iff_tendsto_slope' hs).1 hf (is_open.mem_nhds is_open_Iio hr)
 
 lemma has_deriv_within_at.liminf_right_slope_le
   (hf : has_deriv_within_at f f' (Ici x) x) (hr : f' < r) :
@@ -1877,7 +1877,7 @@ lemma has_deriv_within_at.limsup_norm_slope_le
 begin
   have hr₀ : 0 < r, from lt_of_le_of_lt (norm_nonneg f') hr,
   have A : ∀ᶠ z in 𝓝[s \ {x}] x, ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
-    from (has_deriv_within_at_iff_tendsto_slope.1 hf).norm (mem_nhds_sets is_open_Iio hr),
+    from (has_deriv_within_at_iff_tendsto_slope.1 hf).norm (is_open.mem_nhds is_open_Iio hr),
   have B : ∀ᶠ z in 𝓝[{x}] x, ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r,
     from mem_sets_of_superset self_mem_nhds_within
       (singleton_subset_iff.2 $ by simp [hr₀]),

src/analysis/calculus/extend_deriv.lean

@@ -71,7 +71,7 @@ begin
       convert le_of_lt (hδ _ z_in.2 z_in.1),
       have op : is_open (B ∩ s) := is_open_ball.inter s_open,
       rw differentiable_at.fderiv_within _ (op.unique_diff_on z z_in),
-      exact (diff z z_in).differentiable_at (mem_nhds_sets op z_in) },
+      exact (diff z z_in).differentiable_at (is_open.mem_nhds op z_in) },
     simpa using conv.norm_image_sub_le_of_norm_fderiv_within_le' diff bound u_in v_in },
   rintros ⟨u, v⟩ uv_in,
   refine continuous_within_at.closure_le uv_in _ _ key,

src/analysis/calculus/fderiv.lean

@@ -299,7 +299,7 @@ begin
   exact add_nonneg C.coe_nonneg ε0.le,
   have hs' := hs, rw [← map_add_left_nhds_zero x₀, mem_map] at hs',
   filter_upwards [is_o_iff.1 (has_fderiv_at_iff_is_o_nhds_zero.1 hf) ε0, hs'], intros y hy hys,
-  have := hlip.norm_sub_le hys (mem_of_nhds hs), rw add_sub_cancel' at this,
+  have := hlip.norm_sub_le hys (mem_of_mem_nhds hs), rw add_sub_cancel' at this,
   calc ∥f' y∥ ≤ ∥f (x₀ + y) - f x₀∥ + ∥f (x₀ + y) - f x₀ - f' y∥ : norm_le_insert _ _
           ... ≤ C * ∥y∥ + ε * ∥y∥                                : add_le_add this hy
           ... = (C + ε) * ∥y∥                                    : (add_mul _ _ _).symm
@@ -359,7 +359,7 @@ begin
   refine (has_fderiv_within_at_univ.2 hf).lim _ (univ_mem_sets' (λ _, trivial)) hc _,
   assume U hU,
   refine (eventually_ne_of_tendsto_norm_at_top hc (0:𝕜)).mono (λ y hy, _),
-  convert mem_of_nhds hU,
+  convert mem_of_mem_nhds hU,
   dsimp only,
   rw [← mul_smul, mul_inv_cancel hy, one_smul]
 end
@@ -494,7 +494,7 @@ lemma differentiable_on_of_locally_differentiable_on
 begin
   assume x xs,
   rcases h x xs with ⟨t, t_open, xt, ht⟩,
-  exact (differentiable_within_at_inter (mem_nhds_sets t_open xt)).1 (ht x ⟨xs, xt⟩)
+  exact (differentiable_within_at_inter (is_open.mem_nhds t_open xt)).1 (ht x ⟨xs, xt⟩)
 end
 
 lemma fderiv_within_subset (st : s ⊆ t) (ht : unique_diff_within_at 𝕜 s x)
@@ -537,7 +537,7 @@ end
 
 lemma fderiv_within_of_open (hs : is_open s) (hx : x ∈ s) :
   fderiv_within 𝕜 f s x = fderiv 𝕜 f x :=
-fderiv_within_of_mem_nhds (mem_nhds_sets hs hx)
+fderiv_within_of_mem_nhds (is_open.mem_nhds hs hx)
 
 lemma fderiv_within_eq_fderiv (hs : unique_diff_within_at 𝕜 s x) (h : differentiable_at 𝕜 f x) :
   fderiv_within 𝕜 f s x = fderiv 𝕜 f x :=
@@ -660,7 +660,7 @@ has_fderiv_at_filter.congr_of_eventually_eq h h₁ hx
 
 lemma has_fderiv_at.congr_of_eventually_eq (h : has_fderiv_at f f' x)
   (h₁ : f₁ =ᶠ[𝓝 x] f) : has_fderiv_at f₁ f' x :=
-has_fderiv_at_filter.congr_of_eventually_eq h h₁ (mem_of_nhds h₁ : _)
+has_fderiv_at_filter.congr_of_eventually_eq h h₁ (mem_of_mem_nhds h₁ : _)
 
 lemma differentiable_within_at.congr_mono (h : differentiable_within_at 𝕜 f s x)
   (ht : ∀x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (h₁ : t ⊆ s) : differentiable_within_at 𝕜 f₁ t x :=
@@ -691,7 +691,7 @@ lemma differentiable_on_congr (h' : ∀x ∈ s, f₁ x = f x) :
 lemma differentiable_at.congr_of_eventually_eq (h : differentiable_at 𝕜 f x) (hL : f₁ =ᶠ[𝓝 x] f) :
   differentiable_at 𝕜 f₁ x :=
 has_fderiv_at.differentiable_at
-  (has_fderiv_at_filter.congr_of_eventually_eq h.has_fderiv_at hL (mem_of_nhds hL : _))
+  (has_fderiv_at_filter.congr_of_eventually_eq h.has_fderiv_at hL (mem_of_mem_nhds hL : _))
 
 lemma differentiable_within_at.fderiv_within_congr_mono (h : differentiable_within_at 𝕜 f s x)
   (hs : ∀x ∈ t, f₁ x = f x) (hx : f₁ x = f x) (hxt : unique_diff_within_at 𝕜 t x) (h₁ : t ⊆ s) :
@@ -2118,7 +2118,7 @@ protected lemma is_open [complete_space E] : is_open (range (coe : (E ≃L[𝕜]
 begin
   nontriviality E,
   rw [is_open_iff_mem_nhds, forall_range_iff],
-  refine λ e, mem_nhds_sets _ (mem_range_self _),
+  refine λ e, is_open.mem_nhds _ (mem_range_self _),
   let O : (E →L[𝕜] F) → (E →L[𝕜] E) := λ f, (e.symm : F →L[𝕜] E).comp f,
   have h_O : continuous O := is_bounded_bilinear_map_comp.continuous_left,
   convert units.is_open.preimage h_O using 1,
@@ -2134,7 +2134,7 @@ end
 
 protected lemma nhds [complete_space E] (e : E ≃L[𝕜] F) :
   (range (coe : (E ≃L[𝕜] F) → (E →L[𝕜] F))) ∈ 𝓝 (e : E →L[𝕜] F) :=
-mem_nhds_sets continuous_linear_equiv.is_open (by simp)
+is_open.mem_nhds continuous_linear_equiv.is_open (by simp)
 
 end continuous_linear_equiv
 

src/analysis/calculus/inverse.lean

@@ -314,16 +314,17 @@ lemma image_mem_nhds (hf : approximates_linear_on f f' s c) (f'symm : f'.nonline
   {x : E} (hs : s ∈ 𝓝 x) (hc : subsingleton F ∨ c < f'symm.nnnorm⁻¹) :
   f '' s ∈ 𝓝 (f x) :=
 begin
-  obtain ⟨t, hts, ht, xt⟩ : ∃ t ⊆ s, is_open t ∧ x ∈ t := mem_nhds_sets_iff.1 hs,
-  have := mem_nhds_sets ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt),
+  obtain ⟨t, hts, ht, xt⟩ : ∃ t ⊆ s, is_open t ∧ x ∈ t := _root_.mem_nhds_iff.1 hs,
+  have := is_open.mem_nhds ((hf.mono_set hts).open_image f'symm ht hc) (mem_image_of_mem _ xt),
   exact mem_sets_of_superset this (image_subset _ hts),
 end
 
 lemma map_nhds_eq (hf : approximates_linear_on f f' s c) (f'symm : f'.nonlinear_right_inverse)
   {x : E} (hs : s ∈ 𝓝 x) (hc : subsingleton F ∨ c < f'symm.nnnorm⁻¹) :
   map f (𝓝 x) = 𝓝 (f x) :=
 begin
-  refine le_antisymm ((hf.continuous_on x (mem_of_nhds hs)).continuous_at hs) (le_map (λ t ht, _)),
+  refine le_antisymm ((hf.continuous_on x (mem_of_mem_nhds hs)).continuous_at hs)
+    (le_map (λ t ht, _)),
   have : f '' (s ∩ t) ∈ 𝓝 (f x) := (hf.mono_set (inter_subset_left s t)).image_mem_nhds
     f'symm (inter_mem_sets hs ht) hc,
   exact mem_sets_of_superset this (image_subset _ (inter_subset_right _ _)),
@@ -436,7 +437,7 @@ lemma approximates_deriv_on_nhds {f : E → F} {f' : E →L[𝕜] F} {a : E}
   ∃ s ∈ 𝓝 a, approximates_linear_on f f' s c :=
 begin
   cases hc with hE hc,
-  { refine ⟨univ, mem_nhds_sets is_open_univ trivial, λ x hx y hy, _⟩,
+  { refine ⟨univ, is_open.mem_nhds is_open_univ trivial, λ x hx y hy, _⟩,
     simp [@subsingleton.elim E hE x y] },
   have := hf.def hc,
   rw [nhds_prod_eq, filter.eventually, mem_prod_same_iff] at this,

src/analysis/calculus/mean_value.lean

@@ -104,7 +104,7 @@ begin
     refine nonempty_of_mem_sets (inter_mem_sets _ (Ioc_mem_nhds_within_Ioi ⟨le_rfl, hy⟩)),
     have : ∀ᶠ x in 𝓝[Icc a b] x, f x < B x,
       from A x (Ico_subset_Icc_self xab)
-        (mem_nhds_sets (is_open_lt continuous_fst continuous_snd) hxB),
+        (is_open.mem_nhds (is_open_lt continuous_fst continuous_snd) hxB),
     have : ∀ᶠ x in 𝓝[Ioi x] x, f x < B x,
       from nhds_within_le_of_mem (Icc_mem_nhds_within_Ioi xab) this,
     exact this.mono (λ y, le_of_lt) },
@@ -739,9 +739,9 @@ omit hff'
 lemma exists_ratio_deriv_eq_ratio_slope :
   ∃ c ∈ Ioo a b, (g b - g a) * (deriv f c) = (f b - f a) * (deriv g c) :=
 exists_ratio_has_deriv_at_eq_ratio_slope f (deriv f) hab hfc
-  (λ x hx, ((hfd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
+  (λ x hx, ((hfd x hx).differentiable_at $ is_open.mem_nhds is_open_Ioo hx).has_deriv_at)
   g (deriv g) hgc $
-    λ x hx, ((hgd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at
+    λ x hx, ((hgd x hx).differentiable_at $ is_open.mem_nhds is_open_Ioo hx).has_deriv_at
 
 omit hfc
 
@@ -759,7 +759,7 @@ exists_ratio_has_deriv_at_eq_ratio_slope' _ _ hab _ _
 /-- Lagrange's Mean Value Theorem, `deriv` version. -/
 lemma exists_deriv_eq_slope : ∃ c ∈ Ioo a b, deriv f c = (f b - f a) / (b - a) :=
 exists_has_deriv_at_eq_slope f (deriv f) hab hfc
-  (λ x hx, ((hfd x hx).differentiable_at $ mem_nhds_sets is_open_Ioo hx).has_deriv_at)
+  (λ x hx, ((hfd x hx).differentiable_at $ is_open.mem_nhds is_open_Ioo hx).has_deriv_at)
 
 end interval
 
@@ -1078,7 +1078,7 @@ begin
     { unfold continuous_on,
       exact λ t Ht, (hfg t Ht).continuous_within_at },
     { refine λ t Ht, (hfg t $ hIccIoo Ht).has_deriv_at _,
-      refine mem_nhds_sets_iff.mpr _,
+      refine _root_.mem_nhds_iff.mpr _,
       use (Ioo (0:ℝ) 1),
       refine ⟨hIccIoo, _, Ht⟩,
       simp [real.Ioo_eq_ball, is_open_ball] } },
@@ -1113,7 +1113,7 @@ begin
 -- turn little-o definition of strict_fderiv into an epsilon-delta statement
   refine is_o_iff.mpr (λ c hc, metric.eventually_nhds_iff_ball.mpr _),
 -- the correct ε is the modulus of continuity of f'
-  rcases mem_nhds_iff.mp (inter_mem_sets hder (hcont $ ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩,
+  rcases metric.mem_nhds_iff.mp (inter_mem_sets hder (hcont $ ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩,
   refine ⟨ε, ε0, _⟩,
 -- simplify formulas involving the product E × E
   rintros ⟨a, b⟩ h,

src/analysis/calculus/tangent_cone.lean

@@ -296,10 +296,10 @@ lemma unique_diff_within_at_of_mem_nhds (h : s ∈ 𝓝 x) : unique_diff_within_
 by simpa only [univ_inter] using unique_diff_within_at_univ.inter h
 
 lemma is_open.unique_diff_within_at (hs : is_open s) (xs : x ∈ s) : unique_diff_within_at 𝕜 s x :=
-unique_diff_within_at_of_mem_nhds (mem_nhds_sets hs xs)
+unique_diff_within_at_of_mem_nhds (is_open.mem_nhds hs xs)
 
 lemma unique_diff_on.inter (hs : unique_diff_on 𝕜 s) (ht : is_open t) : unique_diff_on 𝕜 (s ∩ t) :=
-λx hx, (hs x hx.1).inter (mem_nhds_sets ht hx.2)
+λx hx, (hs x hx.1).inter (is_open.mem_nhds ht hx.2)
 
 lemma is_open.unique_diff_on (hs : is_open s) : unique_diff_on 𝕜 s :=
 λx hx, is_open.unique_diff_within_at hs hx