From 545186ca49a574ea01df6b65892c76b4c3142ad5 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 5 Aug 2020 09:09:06 +0000 Subject: [PATCH] refactor(*): add a notation for `nhds_within` (#3683) The definition is still there and can be used too. --- src/analysis/ODE/gronwall.lean | 4 +- src/analysis/calculus/deriv.lean | 41 ++-- src/analysis/calculus/extend_deriv.lean | 20 +- src/analysis/calculus/fderiv.lean | 30 +-- src/analysis/calculus/local_extr.lean | 2 +- src/analysis/calculus/mean_value.lean | 16 +- src/analysis/calculus/specific_functions.lean | 6 +- src/analysis/calculus/tangent_cone.lean | 16 +- src/analysis/calculus/times_cont_diff.lean | 28 +-- src/analysis/normed_space/basic.lean | 4 +- src/analysis/specific_limits.lean | 8 +- .../manifold/basic_smooth_bundle.lean | 6 +- .../manifold/local_invariant_properties.lean | 6 +- src/geometry/manifold/mfderiv.lean | 24 +-- .../smooth_manifold_with_corners.lean | 18 +- src/geometry/manifold/times_cont_mdiff.lean | 18 +- src/measure_theory/borel_space.lean | 4 +- src/measure_theory/measure_space.lean | 6 +- src/order/filter/basic.lean | 2 + src/topology/algebra/module.lean | 4 +- src/topology/algebra/ordered.lean | 176 ++++++++--------- src/topology/basic.lean | 5 + src/topology/continuous_on.lean | 186 +++++++++--------- src/topology/dense_embedding.lean | 4 +- src/topology/local_extr.lean | 22 +-- src/topology/local_homeomorph.lean | 4 +- src/topology/metric_space/basic.lean | 19 +- src/topology/metric_space/emetric_space.lean | 7 +- src/topology/separation.lean | 12 +- src/topology/subset_properties.lean | 32 ++- src/topology/uniform_space/basic.lean | 8 +- .../uniform_space/complete_separated.lean | 2 +- .../uniform_space/uniform_convergence.lean | 22 +-- .../uniform_space/uniform_embedding.lean | 10 +- 34 files changed, 389 insertions(+), 383 deletions(-) diff --git a/src/analysis/ODE/gronwall.lean b/src/analysis/ODE/gronwall.lean index f3efe9490a343..afd35b79489be 100644 --- a/src/analysis/ODE/gronwall.lean +++ b/src/analysis/ODE/gronwall.lean @@ -32,7 +32,7 @@ variables {E : Type*} [normed_group E] [normed_space ℝ E] {F : Type*} [normed_group F] [normed_space ℝ F] open metric set asymptotics filter real -open_locale classical +open_locale classical topological_space /-! ### Technical lemmas about `gronwall_bound` -/ @@ -107,7 +107,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 nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r) + ∃ᶠ z in 𝓝[Ioi x] 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 diff --git a/src/analysis/calculus/deriv.lean b/src/analysis/calculus/deriv.lean index 29b0f24de1c7a..507f57d417160 100644 --- a/src/analysis/calculus/deriv.lean +++ b/src/analysis/calculus/deriv.lean @@ -107,7 +107,7 @@ has_fderiv_at_filter f (smul_right 1 f' : 𝕜 →L[𝕜] F) x L That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x` inside `s`. -/ def has_deriv_within_at (f : 𝕜 → F) (f' : F) (s : set 𝕜) (x : 𝕜) := -has_deriv_at_filter f f' x (nhds_within x s) +has_deriv_at_filter f f' x (𝓝[s] x) /-- `f` has the derivative `f'` at the point `x`. @@ -215,7 +215,7 @@ theorem has_deriv_at_filter_iff_tendsto : has_fderiv_at_filter_iff_tendsto theorem has_deriv_within_at_iff_tendsto : has_deriv_within_at f f' s x ↔ - tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (nhds_within x s) (𝓝 0) := + tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - (x' - x) • f'∥) (𝓝[s] x) (𝓝 0) := has_fderiv_at_filter_iff_tendsto theorem has_deriv_at_iff_tendsto : has_deriv_at f f' x ↔ @@ -244,7 +244,7 @@ end lemma has_deriv_within_at_iff_tendsto_slope {x : 𝕜} {s : set 𝕜} : has_deriv_within_at f f' s x ↔ - tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x (s \ {x})) (𝓝 f') := + tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[s \ {x}] x) (𝓝 f') := begin simp only [has_deriv_within_at, nhds_within, diff_eq, inf_assoc.symm, inf_principal.symm], exact has_deriv_at_filter_iff_tendsto_slope @@ -252,7 +252,7 @@ end lemma has_deriv_within_at_iff_tendsto_slope' {x : 𝕜} {s : set 𝕜} (hs : x ∉ s) : has_deriv_within_at f f' s x ↔ - tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x s) (𝓝 f') := + tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[s] x) (𝓝 f') := begin convert ← has_deriv_within_at_iff_tendsto_slope, exact diff_singleton_eq_self hs @@ -260,7 +260,7 @@ end lemma has_deriv_at_iff_tendsto_slope {x : 𝕜} : has_deriv_at f f' x ↔ - tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (nhds_within x {x}ᶜ) (𝓝 f') := + tendsto (λ y, (y - x)⁻¹ • (f y - f x)) (𝓝[{x}ᶜ] x) (𝓝 f') := has_deriv_at_filter_iff_tendsto_slope theorem has_deriv_at_iff_is_o_nhds_zero : has_deriv_at f f' x ↔ @@ -297,7 +297,7 @@ theorem has_deriv_at_unique (h₀ : has_deriv_at f f₀' x) (h₁ : has_deriv_at f f₁' x) : f₀' = f₁' := smul_right_one_eq_iff.mp $ has_fderiv_at_unique h₀ h₁ -lemma has_deriv_within_at_inter' (h : t ∈ nhds_within x s) : +lemma has_deriv_within_at_inter' (h : t ∈ 𝓝[s] x) : has_deriv_within_at f f' (s ∩ t) x ↔ has_deriv_within_at f f' s x := has_fderiv_within_at_inter' h @@ -313,7 +313,7 @@ begin end lemma has_deriv_within_at.nhds_within (h : has_deriv_within_at f f' s x) - (ht : s ∈ nhds_within x t) : has_deriv_within_at f f' t x := + (ht : s ∈ 𝓝[t] x) : has_deriv_within_at f f' t x := (has_deriv_within_at_inter' ht).1 (h.mono (inter_subset_right _ _)) lemma has_deriv_within_at.has_deriv_at (h : has_deriv_within_at f f' s x) (hs : s ∈ 𝓝 x) : @@ -386,7 +386,7 @@ lemma has_deriv_within_at.congr (h : has_deriv_within_at f f' s x) (hs : ∀x h.congr_mono hs hx (subset.refl _) lemma has_deriv_within_at.congr_of_eventually_eq (h : has_deriv_within_at f f' s x) - (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : has_deriv_within_at f₁ f' s x := + (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : has_deriv_within_at f₁ f' s x := has_deriv_at_filter.congr_of_eventually_eq h h₁ hx lemma has_deriv_at.congr_of_eventually_eq (h : has_deriv_at f f' x) @@ -394,7 +394,7 @@ lemma has_deriv_at.congr_of_eventually_eq (h : has_deriv_at f f' x) has_deriv_at_filter.congr_of_eventually_eq h h₁ (mem_of_nhds h₁ : _) lemma filter.eventually_eq.deriv_within_eq (hs : unique_diff_within_at 𝕜 s x) - (hL : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : + (hL : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : deriv_within f₁ s x = deriv_within f s x := by { unfold deriv_within, rw hL.fderiv_within_eq hs hx } @@ -941,9 +941,8 @@ theorem has_deriv_within_at.scomp {t : set 𝕜} has_deriv_within_at (g ∘ h) (h' • g') s x := begin apply has_deriv_at_filter.scomp _ (has_deriv_at_filter.mono hg _) hh, - calc map h (nhds_within x s) - ≤ nhds_within (h x) (h '' s) : hh.continuous_within_at.tendsto_nhds_within_image - ... ≤ nhds_within (h x) t : nhds_within_mono _ (image_subset_iff.mpr hst) + calc map h (𝓝[s] x) ≤ 𝓝[h '' s] (h x) : hh.continuous_within_at.tendsto_nhds_within_image + ... ≤ 𝓝[t] (h x) : nhds_within_mono _ (image_subset_iff.mpr hst) end /-- The chain rule. -/ @@ -1685,17 +1684,17 @@ section real 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 nhds_within x (s \ {x}), (z - x)⁻¹ * (f z - f x) < 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) 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 nhds_within x s, (z - x)⁻¹ * (f z - f x) < 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) lemma has_deriv_within_at.liminf_right_slope_le (hf : has_deriv_within_at f f' (Ioi x) x) (hr : f' < r) : - ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r := + ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r := (hf.limsup_slope_le' (lt_irrefl x) hr).frequently end real @@ -1713,12 +1712,12 @@ In other words, the limit superior of this ratio as `z` tends to `x` along `s` is less than or equal to `∥f'∥`. -/ lemma has_deriv_within_at.limsup_norm_slope_le (hf : has_deriv_within_at f f' s x) (hr : ∥f'∥ < r) : - ∀ᶠ z in nhds_within x s, ∥z - x∥⁻¹ * ∥f z - f x∥ < r := + ∀ᶠ z in 𝓝[s] x, ∥z - x∥⁻¹ * ∥f z - f x∥ < r := begin have hr₀ : 0 < r, from lt_of_le_of_lt (norm_nonneg f') hr, - have A : ∀ᶠ z in nhds_within x (s \ {x}), ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r, + 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), - have B : ∀ᶠ z in nhds_within x {x}, ∥(z - x)⁻¹ • (f z - f x)∥ ∈ Iio r, + 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₀]), have C := mem_sup_sets.2 ⟨A, B⟩, @@ -1737,7 +1736,7 @@ This lemma is a weaker version of `has_deriv_within_at.limsup_norm_slope_le` where `∥f z∥ - ∥f x∥` is replaced by `∥f z - f x∥`. -/ lemma has_deriv_within_at.limsup_slope_norm_le (hf : has_deriv_within_at f f' s x) (hr : ∥f'∥ < r) : - ∀ᶠ z in nhds_within x s, ∥z - x∥⁻¹ * (∥f z∥ - ∥f x∥) < r := + ∀ᶠ z in 𝓝[s] x, ∥z - x∥⁻¹ * (∥f z∥ - ∥f x∥) < r := begin apply (hf.limsup_norm_slope_le hr).mono, assume z hz, @@ -1752,7 +1751,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' (Ioi x) x) (hr : ∥f'∥ < r) : - ∃ᶠ z in nhds_within x (Ioi x), ∥z - x∥⁻¹ * ∥f z - f x∥ < r := + ∃ᶠ z in 𝓝[Ioi x] x, ∥z - x∥⁻¹ * ∥f z - f x∥ < r := (hf.limsup_norm_slope_le hr).frequently /-- If `f` has derivative `f'` within `(x, +∞)` at `x`, then for any `r > ∥f'∥` the ratio @@ -1768,7 +1767,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' (Ioi x) x) (hr : ∥f'∥ < r) : - ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r := + ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r := begin have := (hf.limsup_slope_norm_le hr).frequently, refine this.mp (eventually.mono self_mem_nhds_within _), diff --git a/src/analysis/calculus/extend_deriv.lean b/src/analysis/calculus/extend_deriv.lean index 9d8addd48936c..437ead513a0d9 100644 --- a/src/analysis/calculus/extend_deriv.lean +++ b/src/analysis/calculus/extend_deriv.lean @@ -34,7 +34,7 @@ with derivative `f'`. -/ theorem has_fderiv_at_boundary_of_tendsto_fderiv {f : E → F} {s : set E} {x : E} {f' : E →L[ℝ] F} (f_diff : differentiable_on ℝ f s) (s_conv : convex s) (s_open : is_open s) (f_cont : ∀y ∈ closure s, continuous_within_at f s y) - (h : tendsto (λy, fderiv ℝ f y) (nhds_within x s) (𝓝 f')) : + (h : tendsto (λy, fderiv ℝ f y) (𝓝[s] x) (𝓝 f')) : has_fderiv_within_at f f' (closure s) x := begin classical, @@ -83,7 +83,7 @@ begin obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s, by simpa [closure_prod_eq] using closure_mono this uv_in, apply continuous_within_at.mono _ this, - simp only [continuous_within_at, nhds_prod_eq] }, + simp only [continuous_within_at] }, rw nhds_within_prod_eq, { have : f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by abel, rw this, @@ -100,8 +100,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 ∈ nhds_within a (Ioi a)) - (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Ioi a)) (𝓝 e)) : + (hs : s ∈ 𝓝[Ioi a] a) + (f_lim' : tendsto (λx, deriv f x) (𝓝[Ioi a] 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 @@ -122,7 +122,7 @@ begin { rw h, exact f_lim.mono ts }, { have : y ∈ s := sab ⟨lt_of_le_of_ne hy.1 (ne.symm h), hy.2⟩, exact (f_diff.continuous_on y this).mono ts } }, - have t_diff' : tendsto (λx, fderiv ℝ f x) (nhds_within a t) (𝓝 (smul_right 1 e)), + have t_diff' : tendsto (λx, fderiv ℝ f x) (𝓝[t] a) (𝓝 (smul_right 1 e)), { simp [deriv_fderiv.symm], refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _, exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Ioi_self) f_lim' }, @@ -137,8 +137,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 ∈ nhds_within a (Iio a)) - (f_lim' : tendsto (λx, deriv f x) (nhds_within a (Iio a)) (𝓝 e)) : + (hs : s ∈ 𝓝[Iio a] a) + (f_lim' : tendsto (λx, deriv f x) (𝓝[Iio a] 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 @@ -159,7 +159,7 @@ begin { rw h, exact f_lim.mono ts }, { have : y ∈ s := sab ⟨hy.1, lt_of_le_of_ne hy.2 h⟩, exact (f_diff.continuous_on y this).mono ts } }, - have t_diff' : tendsto (λx, fderiv ℝ f x) (nhds_within a t) (𝓝 (smul_right 1 e)), + have t_diff' : tendsto (λx, fderiv ℝ f x) (𝓝[t] a) (𝓝 (smul_right 1 e)), { simp [deriv_fderiv.symm], refine tendsto.comp is_bounded_bilinear_map_smul_right.continuous_right.continuous_at _, exact tendsto_le_left (nhds_within_mono _ Ioo_subset_Iio_self) f_lim' }, @@ -184,7 +184,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 (nhds_within x (Ioi x)) (𝓝 (g x)) := tendsto_inf_left hg, + have : tendsto g (𝓝[Ioi x] x) (𝓝 (g x)) := tendsto_inf_left hg, apply this.congr' _, apply mem_sets_of_superset self_mem_nhds_within (λy hy, _), exact (f_diff y (ne_of_gt hy)).deriv.symm }, @@ -195,7 +195,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 (nhds_within x (Iio x)) (𝓝 (g x)) := tendsto_inf_left hg, + have : tendsto g (𝓝[Iio x] x) (𝓝 (g x)) := tendsto_inf_left hg, apply this.congr' _, apply mem_sets_of_superset self_mem_nhds_within (λy hy, _), exact (f_diff y (ne_of_lt hy)).deriv.symm }, diff --git a/src/analysis/calculus/fderiv.lean b/src/analysis/calculus/fderiv.lean index 2e955ee0c6c5a..4fee06d10f9d6 100644 --- a/src/analysis/calculus/fderiv.lean +++ b/src/analysis/calculus/fderiv.lean @@ -128,7 +128,7 @@ variables {G' : Type*} [normed_group G'] [normed_space 𝕜 G'] /-- A function `f` has the continuous linear map `f'` as derivative along the filter `L` if `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` converges along the filter `L`. This definition is designed to be specialized for `L = 𝓝 x` (in `has_fderiv_at`), giving rise to the usual notion -of Fréchet derivative, and for `L = nhds_within x s` (in `has_fderiv_within_at`), giving rise to +of Fréchet derivative, and for `L = 𝓝[s] x` (in `has_fderiv_within_at`), giving rise to the notion of Fréchet derivative along the set `s`. -/ def has_fderiv_at_filter (f : E → F) (f' : E →L[𝕜] F) (x : E) (L : filter E) := is_o (λ x', f x' - f x - f' (x' - x)) (λ x', x' - x) L @@ -136,7 +136,7 @@ is_o (λ x', f x' - f x - f' (x' - x)) (λ x', x' - x) L /-- A function `f` has the continuous linear map `f'` as derivative at `x` within a set `s` if `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` tends to `x` inside `s`. -/ def has_fderiv_within_at (f : E → F) (f' : E →L[𝕜] F) (s : set E) (x : E) := -has_fderiv_at_filter f f' x (nhds_within x s) +has_fderiv_at_filter f f' x (𝓝[s] x) /-- A function `f` has the continuous linear map `f'` as derivative at `x` if `f x' = f x + f' (x' - x) + o (x' - x)` when `x'` tends to `x`. -/ @@ -213,13 +213,13 @@ theorem has_fderiv_within_at.lim (h : has_fderiv_within_at f f' s x) {α : Type* (cdlim : tendsto (λ n, c n • d n) l (𝓝 v)) : tendsto (λn, c n • (f (x + d n) - f x)) l (𝓝 (f' v)) := begin - have tendsto_arg : tendsto (λ n, x + d n) l (nhds_within x s), - { conv in (nhds_within x s) { rw ← add_zero x }, + have tendsto_arg : tendsto (λ n, x + d n) l (𝓝[s] x), + { conv in (𝓝[s] x) { rw ← add_zero x }, rw [nhds_within, tendsto_inf], split, { apply tendsto_const_nhds.add (tangent_cone_at.lim_zero l clim cdlim) }, { rwa tendsto_principal } }, - have : is_o (λ y, f y - f x - f' (y - x)) (λ y, y - x) (nhds_within x s) := h, + have : is_o (λ y, f y - f x - f' (y - x)) (λ y, y - x) (𝓝[s] x) := h, have : is_o (λ n, f (x + d n) - f x - f' ((x + d n) - x)) (λ n, (x + d n) - x) l := this.comp_tendsto tendsto_arg, have : is_o (λ n, f (x + d n) - f x - f' (d n)) d l := by simpa only [add_sub_cancel'], @@ -288,7 +288,7 @@ begin end theorem has_fderiv_within_at_iff_tendsto : has_fderiv_within_at f f' s x ↔ - tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) (nhds_within x s) (𝓝 0) := + tendsto (λ x', ∥x' - x∥⁻¹ * ∥f x' - f x - f' (x' - x)∥) (𝓝[s] x) (𝓝 0) := has_fderiv_at_filter_iff_tendsto theorem has_fderiv_at_iff_tendsto : has_fderiv_at f f' x ↔ @@ -379,7 +379,7 @@ begin exact unique_diff_within_at_univ.eq h₀ h₁ end -lemma has_fderiv_within_at_inter' (h : t ∈ nhds_within x s) : +lemma has_fderiv_within_at_inter' (h : t ∈ 𝓝[s] x) : has_fderiv_within_at f f' (s ∩ t) x ↔ has_fderiv_within_at f f' s x := by simp [has_fderiv_within_at, nhds_within_restrict'' s h] @@ -395,7 +395,7 @@ begin end lemma has_fderiv_within_at.nhds_within (h : has_fderiv_within_at f f' s x) - (ht : s ∈ nhds_within x t) : has_fderiv_within_at f f' t x := + (ht : s ∈ 𝓝[t] x) : has_fderiv_within_at f f' t x := (has_fderiv_within_at_inter' ht).1 (h.mono (inter_subset_right _ _)) lemma has_fderiv_within_at.has_fderiv_at (h : has_fderiv_within_at f f' s x) (hs : s ∈ 𝓝 x) : @@ -453,7 +453,7 @@ lemma differentiable_within_at_inter (ht : t ∈ 𝓝 x) : by simp only [differentiable_within_at, has_fderiv_within_at, has_fderiv_at_filter, nhds_within_restrict' s ht] -lemma differentiable_within_at_inter' (ht : t ∈ nhds_within x s) : +lemma differentiable_within_at_inter' (ht : t ∈ 𝓝[s] x) : differentiable_within_at 𝕜 f (s ∩ t) x ↔ differentiable_within_at 𝕜 f s x := by simp only [differentiable_within_at, has_fderiv_within_at, has_fderiv_at_filter, nhds_within_restrict'' s ht] @@ -617,7 +617,7 @@ lemma has_fderiv_within_at.congr (h : has_fderiv_within_at f f' s x) (hs : ∀x h.congr_mono hs hx (subset.refl _) lemma has_fderiv_within_at.congr_of_eventually_eq (h : has_fderiv_within_at f f' s x) - (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : has_fderiv_within_at f₁ f' s x := + (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : has_fderiv_within_at f₁ f' s x := 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) @@ -633,7 +633,7 @@ lemma differentiable_within_at.congr (h : differentiable_within_at 𝕜 f s x) differentiable_within_at.congr_mono h ht hx (subset.refl _) lemma differentiable_within_at.congr_of_eventually_eq - (h : differentiable_within_at 𝕜 f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) + (h : differentiable_within_at 𝕜 f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : differentiable_within_at 𝕜 f₁ s x := (h.has_fderiv_within_at.congr_of_eventually_eq h₁ hx).differentiable_within_at @@ -661,7 +661,7 @@ lemma differentiable_within_at.fderiv_within_congr_mono (h : differentiable_with (has_fderiv_within_at.congr_mono h.has_fderiv_within_at hs hx h₁).fderiv_within hxt lemma filter.eventually_eq.fderiv_within_eq (hs : unique_diff_within_at 𝕜 s x) - (hL : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : + (hL : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : fderiv_within 𝕜 f₁ s x = fderiv_within 𝕜 f s x := if h : differentiable_within_at 𝕜 f s x then has_fderiv_within_at.fderiv_within (h.has_fderiv_within_at.congr_of_eventually_eq hL hx) hs @@ -924,9 +924,9 @@ theorem has_fderiv_within_at.comp {g : F → G} {g' : F →L[𝕜] G} {t : set F has_fderiv_within_at (g ∘ f) (g'.comp f') s x := begin apply has_fderiv_at_filter.comp _ (has_fderiv_at_filter.mono hg _) hf, - calc map f (nhds_within x s) - ≤ nhds_within (f x) (f '' s) : hf.continuous_within_at.tendsto_nhds_within_image - ... ≤ nhds_within (f x) t : nhds_within_mono _ (image_subset_iff.mpr hst) + calc map f (𝓝[s] x) + ≤ 𝓝[f '' s] (f x) : hf.continuous_within_at.tendsto_nhds_within_image + ... ≤ 𝓝[t] (f x) : nhds_within_mono _ (image_subset_iff.mpr hst) end /-- The chain rule. -/ diff --git a/src/analysis/calculus/local_extr.lean b/src/analysis/calculus/local_extr.lean index 8eaf28507c275..9d6fdddaa591d 100644 --- a/src/analysis/calculus/local_extr.lean +++ b/src/analysis/calculus/local_extr.lean @@ -123,7 +123,7 @@ begin have hc' : tendsto (λ n, ∥c n∥) at_top at_top, from tendsto_at_top_mono (λ n, le_abs_self _) hc, refine le_of_tendsto (hf.lim at_top hd hc' hcd) _, - replace hd : tendsto (λ n, a + d n) at_top (nhds_within (a + 0) s), + replace hd : tendsto (λ n, a + d n) at_top (𝓝[s] (a + 0)), from tendsto_inf.2 ⟨tendsto_const_nhds.add (tangent_cone_at.lim_zero _ hc' hcd), by rwa tendsto_principal⟩, rw [add_zero] at hd, diff --git a/src/analysis/calculus/mean_value.lean b/src/analysis/calculus/mean_value.lean index 6740434c71a4a..d9ce653c3cb9d 100644 --- a/src/analysis/calculus/mean_value.lean +++ b/src/analysis/calculus/mean_value.lean @@ -83,7 +83,7 @@ lemma image_le_of_liminf_slope_right_lt_deriv_boundary' {f f' : ℝ → ℝ} {a (hf : continuous_on f (Icc a b)) -- `hf'` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ f' x` (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r → - ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r) + ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : continuous_on B (Icc a b)) (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x) (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) : @@ -100,17 +100,17 @@ begin change f x ≤ B x at hxB, cases lt_or_eq_of_le hxB with hxB hxB, { -- If `f x < B x`, then all we need is continuity of both sides - apply @nonempty_of_mem_sets _ (nhds_within x (Ioi x)), + apply @nonempty_of_mem_sets _ (𝓝[Ioi x] x), refine inter_mem_sets _ (Ioc_mem_nhds_within_Ioi ⟨le_refl x, hy⟩), - have : ∀ᶠ x in nhds_within x (Icc a b), f x < B x, + 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), - have : ∀ᶠ x in nhds_within x (Ioi x), f x < B x, + have : ∀ᶠ x in 𝓝[Ioi x] x, f x < B x, from nhds_within_le_of_mem (Icc_mem_nhds_within_Ioi xab) this, refine mem_sets_of_superset this (set_of_subset_set_of.2 $ λ y, le_of_lt) }, { rcases dense (bound x xab hxB) with ⟨r, hfr, hrB⟩, specialize hf' x xab r hfr, - have HB : ∀ᶠ z in nhds_within x (Ioi x), r < (z - x)⁻¹ * (B z - B x), + have HB : ∀ᶠ z in 𝓝[Ioi x] x, r < (z - x)⁻¹ * (B z - B x), from (has_deriv_within_at_iff_tendsto_slope' $ lt_irrefl x).1 (hB' x xab) (mem_nhds_sets is_open_Ioi hrB), obtain ⟨z, ⟨hfz, hzB⟩, hz⟩ : @@ -137,7 +137,7 @@ lemma image_le_of_liminf_slope_right_lt_deriv_boundary {f f' : ℝ → ℝ} {a b (hf : continuous_on f (Icc a b)) -- `hf'` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ f' x` (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r → - ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r) + ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r) {B B' : ℝ → ℝ} (ha : f a ≤ B a) (hB : ∀ x, has_deriv_at B (B' x) x) (bound : ∀ x ∈ Ico a b, f x = B x → f' x < B' x) : ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x := @@ -160,7 +160,7 @@ lemma image_le_of_liminf_slope_right_le_deriv_boundary {f : ℝ → ℝ} {a b : (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x) -- `bound` actually says `liminf (z - x)⁻¹ * (f z - f x) ≤ B' x` (bound : ∀ x ∈ Ico a b, ∀ r, B' x < r → - ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (f z - f x) < r) : + ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r) : ∀ ⦃x⦄, x ∈ Icc a b → f x ≤ B x := begin have Hr : ∀ x ∈ Icc a b, ∀ r ∈ Ioi (0:ℝ), f x ≤ B x + r * (x - a), @@ -258,7 +258,7 @@ lemma image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary {E : Type*} [no {f : ℝ → E} {f' : ℝ → ℝ} (hf : continuous_on f (Icc a b)) -- `hf'` actually says `liminf ∥z - x∥⁻¹ * (∥f z∥ - ∥f x∥) ≤ f' x` (hf' : ∀ x ∈ Ico a b, ∀ r, f' x < r → - ∃ᶠ z in nhds_within x (Ioi x), (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r) + ∃ᶠ z in 𝓝[Ioi x] x, (z - x)⁻¹ * (∥f z∥ - ∥f x∥) < r) {B B' : ℝ → ℝ} (ha : ∥f a∥ ≤ B a) (hB : continuous_on B (Icc a b)) (hB' : ∀ x ∈ Ico a b, has_deriv_within_at B (B' x) (Ioi x) x) (bound : ∀ x ∈ Ico a b, ∥f x∥ = B x → f' x < B' x) : diff --git a/src/analysis/calculus/specific_functions.lean b/src/analysis/calculus/specific_functions.lean index 28646e84d6dc0..5c15034e56853 100644 --- a/src/analysis/calculus/specific_functions.lean +++ b/src/analysis/calculus/specific_functions.lean @@ -81,11 +81,11 @@ end is `0`, to be able to apply general differentiability extension theorems. This limit is checked in this lemma. -/ lemma f_aux_limit (n : ℕ) : - tendsto (λx, (P_aux n).eval x * exp (-x⁻¹) / x^(2 * n)) (nhds_within 0 (Ioi 0)) (𝓝 0) := + tendsto (λx, (P_aux n).eval x * exp (-x⁻¹) / x^(2 * n)) (𝓝[Ioi 0] 0) (𝓝 0) := begin - have A : tendsto (λx, (P_aux n).eval x) (nhds_within 0 (Ioi 0)) (𝓝 ((P_aux n).eval 0)) := + have A : tendsto (λx, (P_aux n).eval x) (𝓝[Ioi 0] 0) (𝓝 ((P_aux n).eval 0)) := (P_aux n).continuous_within_at, - have B : tendsto (λx, exp (-x⁻¹) / x^(2 * n)) (nhds_within 0 (Ioi 0)) (𝓝 0), + have B : tendsto (λx, exp (-x⁻¹) / x^(2 * n)) (𝓝[Ioi 0] 0) (𝓝 0), { convert (tendsto_pow_mul_exp_neg_at_top_nhds_0 (2 * n)).comp tendsto_inv_zero_at_top, ext x, field_simp }, diff --git a/src/analysis/calculus/tangent_cone.lean b/src/analysis/calculus/tangent_cone.lean index 54592889c52d3..87a4b9fe75581 100644 --- a/src/analysis/calculus/tangent_cone.lean +++ b/src/analysis/calculus/tangent_cone.lean @@ -110,20 +110,20 @@ begin exact D end -lemma tangent_cone_mono_nhds (h : nhds_within x s ≤ nhds_within x t) : +lemma tangent_cone_mono_nhds (h : 𝓝[s] x ≤ 𝓝[t] x) : tangent_cone_at 𝕜 s x ⊆ tangent_cone_at 𝕜 t x := begin rintros y ⟨c, d, ds, ctop, clim⟩, refine ⟨c, d, _, ctop, clim⟩, - suffices : tendsto (λ n, x + d n) at_top (nhds_within x t), + suffices : tendsto (λ n, x + d n) at_top (𝓝[t] x), from tendsto_principal.1 (tendsto_inf.1 this).2, apply tendsto_le_right h, refine tendsto_inf.2 ⟨_, tendsto_principal.2 ds⟩, simpa only [add_zero] using tendsto_const_nhds.add (tangent_cone_at.lim_zero at_top ctop clim) end -/-- Tangent cone of `s` at `x` depends only on `nhds_within x s`. -/ -lemma tangent_cone_congr (h : nhds_within x s = nhds_within x t) : +/-- Tangent cone of `s` at `x` depends only on `𝓝[s] x`. -/ +lemma tangent_cone_congr (h : 𝓝[s] x = 𝓝[t] x) : tangent_cone_at 𝕜 s x = tangent_cone_at 𝕜 t x := subset.antisymm (tangent_cone_mono_nhds $ le_of_eq h) @@ -259,7 +259,7 @@ lemma unique_diff_on_empty : unique_diff_on 𝕜 (∅ : set E) := λ x hx, hx.elim lemma unique_diff_within_at.mono_nhds (h : unique_diff_within_at 𝕜 s x) - (st : nhds_within x s ≤ nhds_within x t) : + (st : 𝓝[s] x ≤ 𝓝[t] x) : unique_diff_within_at 𝕜 t x := begin unfold unique_diff_within_at at *, @@ -273,7 +273,7 @@ lemma unique_diff_within_at.mono (h : unique_diff_within_at 𝕜 s x) (st : s unique_diff_within_at 𝕜 t x := h.mono_nhds $ nhds_within_mono _ st -lemma unique_diff_within_at_congr (st : nhds_within x s = nhds_within x t) : +lemma unique_diff_within_at_congr (st : 𝓝[s] x = 𝓝[t] x) : unique_diff_within_at 𝕜 s x ↔ unique_diff_within_at 𝕜 t x := ⟨λ h, h.mono_nhds $ le_of_eq st, λ h, h.mono_nhds $ le_of_eq st.symm⟩ @@ -285,11 +285,11 @@ lemma unique_diff_within_at.inter (hs : unique_diff_within_at 𝕜 s x) (ht : t unique_diff_within_at 𝕜 (s ∩ t) x := (unique_diff_within_at_inter ht).2 hs -lemma unique_diff_within_at_inter' (ht : t ∈ nhds_within x s) : +lemma unique_diff_within_at_inter' (ht : t ∈ 𝓝[s] x) : unique_diff_within_at 𝕜 (s ∩ t) x ↔ unique_diff_within_at 𝕜 s x := unique_diff_within_at_congr $ (nhds_within_restrict'' _ ht).symm -lemma unique_diff_within_at.inter' (hs : unique_diff_within_at 𝕜 s x) (ht : t ∈ nhds_within x s) : +lemma unique_diff_within_at.inter' (hs : unique_diff_within_at 𝕜 s x) (ht : t ∈ 𝓝[s] x) : unique_diff_within_at 𝕜 (s ∩ t) x := (unique_diff_within_at_inter' ht).2 hs diff --git a/src/analysis/calculus/times_cont_diff.lean b/src/analysis/calculus/times_cont_diff.lean index 9d6dde730ef7b..5e2695035c883 100644 --- a/src/analysis/calculus/times_cont_diff.lean +++ b/src/analysis/calculus/times_cont_diff.lean @@ -447,14 +447,14 @@ better, is `C^∞` at `0` within `univ`. -/ def times_cont_diff_within_at (n : with_top ℕ) (f : E → F) (s : set E) (x : E) := ∀ (m : ℕ), (m : with_top ℕ) ≤ n → - ∃ u ∈ nhds_within x (insert x s), ∃ p : E → formal_multilinear_series 𝕜 E F, + ∃ u ∈ 𝓝[insert x s] x, ∃ p : E → formal_multilinear_series 𝕜 E F, has_ftaylor_series_up_to_on m f p u variable {𝕜} lemma times_cont_diff_within_at_nat {n : ℕ} : times_cont_diff_within_at 𝕜 n f s x ↔ - ∃ u ∈ nhds_within x (insert x s), ∃ p : E → formal_multilinear_series 𝕜 E F, + ∃ u ∈ 𝓝[insert x s] x, ∃ p : E → formal_multilinear_series 𝕜 E F, has_ftaylor_series_up_to_on n f p u := ⟨λ H, H n (le_refl _), λ ⟨u, hu, p, hp⟩ m hm, ⟨u, hu, p, hp.of_le hm⟩⟩ @@ -486,7 +486,7 @@ lemma times_cont_diff_within_at.continuous_within_at {n : with_top ℕ} (h.continuous_within_at').mono (subset_insert x s) lemma times_cont_diff_within_at.congr_of_eventually_eq {n : with_top ℕ} - (h : times_cont_diff_within_at 𝕜 n f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : + (h : times_cont_diff_within_at 𝕜 n f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : times_cont_diff_within_at 𝕜 n f₁ s x := begin assume m hm, @@ -503,7 +503,7 @@ begin end lemma times_cont_diff_within_at.congr_of_eventually_eq' {n : with_top ℕ} - (h : times_cont_diff_within_at 𝕜 n f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : x ∈ s) : + (h : times_cont_diff_within_at 𝕜 n f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : x ∈ s) : times_cont_diff_within_at 𝕜 n f₁ s x := begin apply h.congr_of_eventually_eq h₁, @@ -512,7 +512,7 @@ begin end lemma filter.eventually_eq.times_cont_diff_within_at_iff {n : with_top ℕ} - (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : + (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : times_cont_diff_within_at 𝕜 n f₁ s x ↔ times_cont_diff_within_at 𝕜 n f s x := ⟨λ H, times_cont_diff_within_at.congr_of_eventually_eq H h₁.symm hx.symm, λ H, H.congr_of_eventually_eq h₁ hx⟩ @@ -536,7 +536,7 @@ lemma times_cont_diff_within_at.of_le {m n : with_top ℕ} times_cont_diff_within_at 𝕜 m f s x := λ k hk, h k (le_trans hk hmn) -lemma times_cont_diff_within_at_inter' {n : with_top ℕ} (h : t ∈ nhds_within x s) : +lemma times_cont_diff_within_at_inter' {n : with_top ℕ} (h : t ∈ 𝓝[s] x) : times_cont_diff_within_at 𝕜 n f (s ∩ t) x ↔ times_cont_diff_within_at 𝕜 n f s x := begin refine ⟨λ H m hm, _, λ H, H.mono (inter_subset_left _ _)⟩, @@ -572,7 +572,7 @@ lemma times_cont_diff_within_at.differentiable_within_at {n : with_top ℕ} /-- A function is `C^(n + 1)` on a domain iff locally, it has a derivative which is `C^n`. -/ theorem times_cont_diff_within_at_succ_iff_has_fderiv_within_at {n : ℕ} : times_cont_diff_within_at 𝕜 ((n + 1) : ℕ) f s x - ↔ ∃ u ∈ nhds_within x (insert x s), ∃ f' : E → (E →L[𝕜] F), + ↔ ∃ u ∈ 𝓝[insert x s] x, ∃ f' : E → (E →L[𝕜] F), (∀ x ∈ u, has_fderiv_within_at f (f' x) u x) ∧ (times_cont_diff_within_at 𝕜 n f' u x) := begin split, @@ -638,7 +638,7 @@ h x hx lemma times_cont_diff_within_at.times_cont_diff_on {n : with_top ℕ} {m : ℕ} (hm : (m : with_top ℕ) ≤ n) (h : times_cont_diff_within_at 𝕜 n f s x) : - ∃ u ∈ nhds_within x (insert x s), u ⊆ insert x s ∧ times_cont_diff_on 𝕜 m f u := + ∃ u ∈ 𝓝[insert x s] x, u ⊆ insert x s ∧ times_cont_diff_on 𝕜 m f u := begin rcases h m hm with ⟨u, u_nhd, p, hp⟩, refine ⟨u ∩ insert x s, filter.inter_mem_sets u_nhd self_mem_nhds_within, inter_subset_right _ _, _⟩, @@ -699,7 +699,7 @@ end /-- A function is `C^(n + 1)` on a domain iff locally, it has a derivative which is `C^n`. -/ theorem times_cont_diff_on_succ_iff_has_fderiv_within_at {n : ℕ} : times_cont_diff_on 𝕜 ((n + 1) : ℕ) f s - ↔ ∀ x ∈ s, ∃ u ∈ nhds_within x (insert x s), ∃ f' : E → (E →L[𝕜] F), + ↔ ∀ x ∈ s, ∃ u ∈ 𝓝[insert x s] x, ∃ f' : E → (E →L[𝕜] F), (∀ x ∈ u, has_fderiv_within_at f (f' x) u x) ∧ (times_cont_diff_on 𝕜 n f' u) := begin split, @@ -838,7 +838,7 @@ end /-- The iterated differential within a set `s` at a point `x` is not modified if one intersects `s` with a neighborhood of `x` within `s`. -/ lemma iterated_fderiv_within_inter' {n : ℕ} - (hu : u ∈ nhds_within x s) (hs : unique_diff_on 𝕜 s) (xs : x ∈ s) : + (hu : u ∈ 𝓝[s] x) (hs : unique_diff_on 𝕜 s) (xs : x ∈ s) : iterated_fderiv_within 𝕜 n f (s ∩ u) x = iterated_fderiv_within 𝕜 n f s x := begin obtain ⟨v, v_open, xv, vu⟩ : ∃ v, is_open v ∧ x ∈ v ∧ v ∩ s ⊆ u := mem_nhds_within.1 hu, @@ -1011,7 +1011,7 @@ begin rw times_cont_diff_within_at_inter' (mem_nhds_within_of_mem_nhds (mem_nhds_sets o_open xo)) at this, apply this.congr_of_eventually_eq' _ hx, - have : o ∩ s ∈ nhds_within x s := mem_nhds_within.2 ⟨o, o_open, xo, subset.refl _⟩, + have : o ∩ s ∈ 𝓝[s] x := mem_nhds_within.2 ⟨o, o_open, xo, subset.refl _⟩, rw inter_comm at this, apply filter.eventually_eq_of_mem this (λ y hy, _), have A : fderiv_within 𝕜 f (s ∩ o) y = f' y := @@ -1838,7 +1838,7 @@ begin have wu : w ⊆ u := λ y hy, hy.2.1, have ws : w ⊆ s := λ y hy, hy.1, refine ⟨w, _, λ y, (g' (f y)).comp (f' y), _, _⟩, - show w ∈ nhds_within x s, + show w ∈ 𝓝[s] x, { apply filter.inter_mem_sets self_mem_nhds_within, apply filter.inter_mem_sets hu, apply continuous_within_at.preimage_mem_nhds_within', @@ -1941,14 +1941,14 @@ begin have xmem : x ∈ f ⁻¹' u ∩ v := ⟨(mem_of_mem_nhds_within (mem_insert (f x) _) u_nhd : _), mem_of_mem_nhds_within (mem_insert x s) v_nhd⟩, - have : f ⁻¹' u ∈ nhds_within x (insert x s), + have : f ⁻¹' u ∈ 𝓝[insert x s] x, { apply hf.continuous_within_at'.preimage_mem_nhds_within', apply nhds_within_mono _ _ u_nhd, rw image_insert_eq, exact insert_subset_insert (image_subset_iff.mpr st) }, have Z := ((hu.comp (hv.mono (inter_subset_right (f ⁻¹' u) v)) (inter_subset_left _ _)) .times_cont_diff_within_at) xmem m (le_refl _), - have : nhds_within x (f ⁻¹' u ∩ v) = nhds_within x (insert x s), + have : 𝓝[f ⁻¹' u ∩ v] x = 𝓝[insert x s] x, { have A : f ⁻¹' u ∩ v = (insert x s) ∩ (f ⁻¹' u ∩ v), { apply subset.antisymm _ (inter_subset_right _ _), rintros y ⟨hy1, hy2⟩, diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean index 1fcae5f044b22..0f9e1c5e7227c 100644 --- a/src/analysis/normed_space/basic.lean +++ b/src/analysis/normed_space/basic.lean @@ -611,7 +611,7 @@ by rwa norm_fpow⟩ @[instance] lemma punctured_nhds_ne_bot {α : Type*} [nondiscrete_normed_field α] (x : α) : - ne_bot (nhds_within x {x}ᶜ) := + ne_bot (𝓝[{x}ᶜ] x) := begin rw [← mem_closure_iff_nhds_within_ne_bot, metric.mem_closure_iff], rintros ε ε0, @@ -622,7 +622,7 @@ end @[instance] lemma nhds_within_is_unit_ne_bot {α : Type*} [nondiscrete_normed_field α] : - ne_bot (nhds_within (0:α) {x : α | is_unit x}) := + ne_bot (𝓝[{x : α | is_unit x}] 0) := by simpa only [is_unit_iff_ne_zero] using punctured_nhds_ne_bot (0:α) lemma tendsto_inv [normed_field α] {r : α} (r0 : r ≠ 0) : tendsto (λq, q⁻¹) (𝓝 r) (𝓝 r⁻¹) := diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean index c11983d1d587d..0f69e53f3f81b 100644 --- a/src/analysis/specific_limits.lean +++ b/src/analysis/specific_limits.lean @@ -90,7 +90,7 @@ tendsto_at_top_mul_right' (inv_pos.2 hr) hf /-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/ lemma tendsto_inv_zero_at_top [discrete_linear_ordered_field α] [topological_space α] - [order_topology α] : tendsto (λx:α, x⁻¹) (nhds_within (0 : α) (set.Ioi 0)) at_top := + [order_topology α] : tendsto (λx:α, x⁻¹) (𝓝[set.Ioi (0:α)] 0) at_top := begin apply (tendsto_at_top _ _).2 (λb, _), refine mem_nhds_within_Ioi_iff_exists_Ioo_subset.2 ⟨(max b 1)⁻¹, by simp [zero_lt_one], λx hx, _⟩, @@ -103,7 +103,7 @@ end /-- The function `r ↦ r⁻¹` tends to `0` on the right as `r → +∞`. -/ lemma tendsto_inv_at_top_zero' [discrete_linear_ordered_field α] [topological_space α] - [order_topology α] : tendsto (λr:α, r⁻¹) at_top (nhds_within (0 : α) (set.Ioi 0)) := + [order_topology α] : tendsto (λr:α, r⁻¹) at_top (𝓝[set.Ioi (0:α)] 0) := begin assume s hs, rw mem_nhds_within_Ioi_iff_exists_Ioc_subset at hs, @@ -167,11 +167,11 @@ begin end lemma lim_norm_zero' {𝕜 : Type*} [normed_group 𝕜] : - tendsto (norm : 𝕜 → ℝ) (nhds_within 0 {x | x ≠ 0}) (nhds_within 0 (set.Ioi 0)) := + tendsto (norm : 𝕜 → ℝ) (𝓝[{x | x ≠ 0}] 0) (𝓝[set.Ioi 0] 0) := lim_norm_zero.inf $ tendsto_principal_principal.2 $ λ x hx, norm_pos_iff.2 hx lemma normed_field.tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type*} [normed_field 𝕜] : - tendsto (λ x:𝕜, ∥x⁻¹∥) (nhds_within 0 {x | x ≠ 0}) at_top := + tendsto (λ x:𝕜, ∥x⁻¹∥) (𝓝[{x | x ≠ 0}] 0) at_top := (tendsto_inv_zero_at_top.comp lim_norm_zero').congr $ λ x, (normed_field.norm_inv x).symm lemma tendsto_pow_at_top_nhds_0_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) : diff --git a/src/geometry/manifold/basic_smooth_bundle.lean b/src/geometry/manifold/basic_smooth_bundle.lean index e5f88b8fcec64..e58be4301d3d4 100644 --- a/src/geometry/manifold/basic_smooth_bundle.lean +++ b/src/geometry/manifold/basic_smooth_bundle.lean @@ -83,7 +83,7 @@ noncomputable theory universe u open topological_space set -open_locale manifold +open_locale manifold topological_space /-- Core structure used to create a smooth bundle above `M` (a manifold over the model with corner `I`) with fiber the normed vector space `F` over `𝕜`, which is trivial in the chart domains @@ -337,13 +337,13 @@ def tangent_bundle_core : basic_smooth_bundle_core I M E := identity. One just needs to write this carefully, paying attention to the sets where the functions are defined. -/ have A : I.symm ⁻¹' (i.1.symm.trans i.1).source ∩ range I ∈ - nhds_within (I x) (range I), + 𝓝[range I] (I x), { rw inter_comm, apply inter_mem_nhds_within, apply I.continuous_symm.continuous_at.preimage_mem_nhds (mem_nhds_sets (local_homeomorph.open_source _) _), simp only [hx, i.1.map_target] with mfld_simps }, - have B : ∀ᶠ y in nhds_within (I x) (range I), + have B : ∀ᶠ y in 𝓝[range I] (I x), (I ∘ i.1 ∘ i.1.symm ∘ I.symm) y = (id : E → E) y, { apply filter.mem_sets_of_superset A, assume y hy, diff --git a/src/geometry/manifold/local_invariant_properties.lean b/src/geometry/manifold/local_invariant_properties.lean index b24e5b6fbb171..47bb9fe6003b2 100644 --- a/src/geometry/manifold/local_invariant_properties.lean +++ b/src/geometry/manifold/local_invariant_properties.lean @@ -228,7 +228,7 @@ begin repeat { simp only [hy] with mfld_simps }, end -lemma lift_prop_within_at_inter' (ht : t ∈ nhds_within x s) : +lemma lift_prop_within_at_inter' (ht : t ∈ 𝓝[s] x) : lift_prop_within_at P g (s ∩ t) x ↔ lift_prop_within_at P g s x := begin by_cases hcont : ¬ (continuous_within_at g s x), @@ -328,7 +328,7 @@ lemma lift_prop_within_at_congr_iff (h₁ : ∀ y ∈ s, g' y = g y) (hx : g' x λ h, hG.lift_prop_within_at_congr h h₁ hx⟩ lemma lift_prop_within_at_congr_of_eventually_eq - (h : lift_prop_within_at P g s x) (h₁ : g' =ᶠ[nhds_within x s] g) (hx : g' x = g x) : + (h : lift_prop_within_at P g s x) (h₁ : g' =ᶠ[𝓝[s] x] g) (hx : g' x = g x) : lift_prop_within_at P g' s x := begin rcases h₁.exists_mem with ⟨t, t_nhd, ht⟩, @@ -337,7 +337,7 @@ begin end lemma lift_prop_within_at_congr_iff_of_eventually_eq - (h₁ : g' =ᶠ[nhds_within x s] g) (hx : g' x = g x) : + (h₁ : g' =ᶠ[𝓝[s] x] g) (hx : g' x = g x) : lift_prop_within_at P g' s x ↔ lift_prop_within_at P g s x := ⟨λ h, hG.lift_prop_within_at_congr_of_eventually_eq h h₁.symm hx.symm, λ h, hG.lift_prop_within_at_congr_of_eventually_eq h h₁ hx⟩ diff --git a/src/geometry/manifold/mfderiv.lean b/src/geometry/manifold/mfderiv.lean index 0d712fa48280a..9d3e19dd33e94 100644 --- a/src/geometry/manifold/mfderiv.lean +++ b/src/geometry/manifold/mfderiv.lean @@ -274,7 +274,7 @@ lemma unique_mdiff_within_at.mono (h : unique_mdiff_within_at I s x) (st : s ⊆ unique_mdiff_within_at I t x := unique_diff_within_at.mono h $ inter_subset_inter (preimage_mono st) (subset.refl _) -lemma unique_mdiff_within_at.inter' (hs : unique_mdiff_within_at I s x) (ht : t ∈ nhds_within x s) : +lemma unique_mdiff_within_at.inter' (hs : unique_mdiff_within_at I s x) (ht : t ∈ 𝓝[s] x) : unique_mdiff_within_at I (s ∩ t) x := begin rw [unique_mdiff_within_at, ext_chart_preimage_inter_eq], @@ -376,7 +376,7 @@ begin exact (unique_mdiff_within_at_univ I).eq h₀ h₁ end -lemma has_mfderiv_within_at_inter' (h : t ∈ nhds_within x s) : +lemma has_mfderiv_within_at_inter' (h : t ∈ 𝓝[s] x) : has_mfderiv_within_at I I' f (s ∩ t) x f' ↔ has_mfderiv_within_at I I' f s x f' := begin rw [has_mfderiv_within_at, has_mfderiv_within_at, ext_chart_preimage_inter_eq, @@ -403,7 +403,7 @@ begin end lemma has_mfderiv_within_at.nhds_within (h : has_mfderiv_within_at I I' f s x f') - (ht : s ∈ nhds_within x t) : has_mfderiv_within_at I I' f t x f' := + (ht : s ∈ 𝓝[t] x) : has_mfderiv_within_at I I' f t x f' := (has_mfderiv_within_at_inter' ht).1 (h.mono (inter_subset_right _ _)) lemma has_mfderiv_within_at.has_mfderiv_at (h : has_mfderiv_within_at I I' f s x f') (hs : s ∈ 𝓝 x) : @@ -479,7 +479,7 @@ begin exact ext_chart_preimage_mem_nhds I x ht end -lemma mdifferentiable_within_at_inter' (ht : t ∈ nhds_within x s) : +lemma mdifferentiable_within_at_inter' (ht : t ∈ 𝓝[s] x) : mdifferentiable_within_at I I' f (s ∩ t) x ↔ mdifferentiable_within_at I I' f s x := begin rw [mdifferentiable_within_at, mdifferentiable_within_at, ext_chart_preimage_inter_eq, @@ -592,12 +592,12 @@ omit Is I's /-! ### Congruence lemmas for derivatives on manifolds -/ lemma has_mfderiv_within_at.congr_of_eventually_eq (h : has_mfderiv_within_at I I' f s x f') - (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : has_mfderiv_within_at I I' f₁ s x f' := + (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : has_mfderiv_within_at I I' f₁ s x f' := begin refine ⟨continuous_within_at.congr_of_eventually_eq h.1 h₁ hx, _⟩, apply has_fderiv_within_at.congr_of_eventually_eq h.2, { have : (ext_chart_at I x).symm ⁻¹' {y | f₁ y = f y} ∈ - nhds_within ((ext_chart_at I x) x) ((ext_chart_at I x).symm ⁻¹' s ∩ range I) := + 𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x) := ext_chart_preimage_mem_nhds_within I x h₁, apply filter.mem_sets_of_superset this (λy, _), simp only [hx] with mfld_simps {contextual := tt} }, @@ -620,13 +620,13 @@ end include Is I's lemma mdifferentiable_within_at.congr_of_eventually_eq - (h : mdifferentiable_within_at I I' f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) + (h : mdifferentiable_within_at I I' f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : mdifferentiable_within_at I I' f₁ s x := (h.has_mfderiv_within_at.congr_of_eventually_eq h₁ hx).mdifferentiable_within_at variables (I I') lemma filter.eventually_eq.mdifferentiable_within_at_iff - (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : + (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : mdifferentiable_within_at I I' f s x ↔ mdifferentiable_within_at I I' f₁ s x := begin split, @@ -662,7 +662,7 @@ lemma mdifferentiable_within_at.mfderiv_within_congr_mono (h : mdifferentiable_w (has_mfderiv_within_at.congr_mono h.has_mfderiv_within_at hs hx h₁).mfderiv_within hxt lemma filter.eventually_eq.mfderiv_within_eq (hs : unique_mdiff_within_at I s x) - (hL : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : + (hL : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : mfderiv_within I I' f₁ s x = (mfderiv_within I I' f s x : _) := begin by_cases h : mdifferentiable_within_at I I' f s x, @@ -702,7 +702,7 @@ omit Is I's lemma written_in_ext_chart_comp (h : continuous_within_at f s x) : {y | written_in_ext_chart_at I I'' x (g ∘ f) y = ((written_in_ext_chart_at I' I'' (f x) g) ∘ (written_in_ext_chart_at I I' x f)) y} - ∈ nhds_within ((ext_chart_at I x) x) ((ext_chart_at I x).symm ⁻¹' s ∩ range I) := + ∈ 𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x) := begin apply @filter.mem_sets_of_superset _ _ ((f ∘ (ext_chart_at I x).symm)⁻¹' (ext_chart_at I' (f x)).source) _ @@ -725,7 +725,7 @@ begin ((ext_chart_at I x).symm ⁻¹' s ∩ range (I)) ((ext_chart_at I x) x), { have : (ext_chart_at I x).symm ⁻¹' (f ⁻¹' (ext_chart_at I' (f x)).source) - ∈ nhds_within ((ext_chart_at I x) x) ((ext_chart_at I x).symm ⁻¹' s ∩ range I) := + ∈ 𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x) := (ext_chart_preimage_mem_nhds_within I x (hf.1.preimage_mem_nhds_within (ext_chart_at_source_mem_nhds _ _))), unfold has_mfderiv_within_at at *, @@ -845,7 +845,7 @@ lemma has_mfderiv_at_id (x : M) : has_mfderiv_at I I (@_root_.id M) x (continuous_linear_map.id 𝕜 (tangent_space I x)) := begin refine ⟨continuous_id.continuous_at, _⟩, - have : ∀ᶠ y in nhds_within ((ext_chart_at I x) x) (range (I)), + have : ∀ᶠ y in 𝓝[range I] ((ext_chart_at I x) x), ((ext_chart_at I x) ∘ (ext_chart_at I x).symm) y = id y, { apply filter.mem_sets_of_superset (ext_chart_at_target_mem_nhds_within I x), mfld_set_tac }, diff --git a/src/geometry/manifold/smooth_manifold_with_corners.lean b/src/geometry/manifold/smooth_manifold_with_corners.lean index b13cd7e811490..365b9662fc57c 100644 --- a/src/geometry/manifold/smooth_manifold_with_corners.lean +++ b/src/geometry/manifold/smooth_manifold_with_corners.lean @@ -620,7 +620,7 @@ begin end lemma ext_chart_at_target_mem_nhds_within : - (ext_chart_at I x).target ∈ nhds_within ((ext_chart_at I x) x) (range I) := + (ext_chart_at I x).target ∈ 𝓝[range I] ((ext_chart_at I x) x) := begin rw [ext_chart_at, local_equiv.trans_target], simp only [function.comp_app, local_equiv.coe_trans, model_with_corners.target], @@ -635,8 +635,8 @@ lemma ext_chart_at_coe_symm (p : E) : (ext_chart_at I x).symm p = ((chart_at H x).symm : H → M) (I.symm p) := rfl lemma nhds_within_ext_chart_target_eq : - nhds_within ((ext_chart_at I x) x) (ext_chart_at I x).target = - nhds_within ((ext_chart_at I x) x) (range I) := + 𝓝[(ext_chart_at I x).target] ((ext_chart_at I x) x) = + 𝓝[range I] ((ext_chart_at I x) x) := begin apply le_antisymm, { apply nhds_within_mono, @@ -664,9 +664,9 @@ ext_chart_continuous_at_symm' I x (mem_ext_chart_source I x) /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point in the source is a neighborhood of the preimage, within a set. -/ lemma ext_chart_preimage_mem_nhds_within' {x' : M} (h : x' ∈ (ext_chart_at I x).source) - (ht : t ∈ nhds_within x' s) : - (ext_chart_at I x).symm ⁻¹' t ∈ nhds_within ((ext_chart_at I x) x') - ((ext_chart_at I x).symm ⁻¹' s ∩ range I) := + (ht : t ∈ 𝓝[s] x') : + (ext_chart_at I x).symm ⁻¹' t ∈ + 𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x') := begin apply (ext_chart_continuous_at_symm' I x h).continuous_within_at.tendsto_nhds_within_image, rw (ext_chart_at I x).left_inv h, @@ -678,9 +678,9 @@ end /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of the base point is a neighborhood of the preimage, within a set. -/ -lemma ext_chart_preimage_mem_nhds_within (ht : t ∈ nhds_within x s) : - (ext_chart_at I x).symm ⁻¹' t ∈ nhds_within ((ext_chart_at I x) x) - ((ext_chart_at I x).symm ⁻¹' s ∩ range I) := +lemma ext_chart_preimage_mem_nhds_within (ht : t ∈ 𝓝[s] x) : + (ext_chart_at I x).symm ⁻¹' t ∈ + 𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x) := ext_chart_preimage_mem_nhds_within' I x (mem_ext_chart_source I x) ht /-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point diff --git a/src/geometry/manifold/times_cont_mdiff.lean b/src/geometry/manifold/times_cont_mdiff.lean index a7e632ca02d49..57ffb09a34f23 100644 --- a/src/geometry/manifold/times_cont_mdiff.lean +++ b/src/geometry/manifold/times_cont_mdiff.lean @@ -445,7 +445,7 @@ lemma smooth.smooth_on (hf : smooth I I' f) : smooth_on I I' f s := times_cont_mdiff.times_cont_mdiff_on hf -lemma times_cont_mdiff_within_at_inter' (ht : t ∈ nhds_within x s) : +lemma times_cont_mdiff_within_at_inter' (ht : t ∈ 𝓝[s] x) : times_cont_mdiff_within_at I I' n f (s ∩ t) x ↔ times_cont_mdiff_within_at I I' n f s x := (times_cont_diff_within_at_local_invariant_prop I I' n).lift_prop_within_at_inter' ht @@ -469,7 +469,7 @@ include Is I's a neighborhood of this point. -/ lemma times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds {n : ℕ} : times_cont_mdiff_within_at I I' n f s x ↔ - ∃ u ∈ nhds_within x (insert x s), times_cont_mdiff_on I I' n f u := + ∃ u ∈ 𝓝[insert x s] x, times_cont_mdiff_on I I' n f u := begin split, { assume h, @@ -498,10 +498,10 @@ begin { simp only with mfld_simps }, { apply h'o ⟨hy.1.2, h'⟩ } }, refine ⟨v, _, _⟩, - show v ∈ nhds_within x (insert x s), + show v ∈ 𝓝[insert x s] x, { rw nhds_within_restrict _ xo o_open, refine filter.inter_mem_sets self_mem_nhds_within _, - suffices : u ∈ nhds_within (ext_chart_at I x x) ((ext_chart_at I x) '' (insert x s ∩ o)), + suffices : u ∈ 𝓝[(ext_chart_at I x) '' (insert x s ∩ o)] (ext_chart_at I x x), from (ext_chart_at_continuous_at I x).continuous_within_at.preimage_mem_nhds_within' this, apply nhds_within_mono _ _ u_nhds, rw image_subset_iff, @@ -561,13 +561,13 @@ lemma times_cont_mdiff_within_at_congr (h₁ : ∀ y ∈ s, f₁ y = f y) (hx : (times_cont_diff_within_at_local_invariant_prop I I' n).lift_prop_within_at_congr_iff h₁ hx lemma times_cont_mdiff_within_at.congr_of_eventually_eq - (h : times_cont_mdiff_within_at I I' n f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) + (h : times_cont_mdiff_within_at I I' n f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : times_cont_mdiff_within_at I I' n f₁ s x := (times_cont_diff_within_at_local_invariant_prop I I' n).lift_prop_within_at_congr_of_eventually_eq h h₁ hx lemma filter.eventually_eq.times_cont_mdiff_within_at_iff - (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : + (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : times_cont_mdiff_within_at I I' n f₁ s x ↔ times_cont_mdiff_within_at I I' n f s x := (times_cont_diff_within_at_local_invariant_prop I I' n) .lift_prop_within_at_congr_iff_of_eventually_eq h₁ hx @@ -630,11 +630,11 @@ begin (ext_chart_at I x).symm ⁻¹' (f ⁻¹' (ext_chart_at I' (f x')).source), { have x'z : (ext_chart_at I x) x' = z, by simp only [x', hz.1, -ext_chart_at] with mfld_simps, have : continuous_within_at f s x' := hf.1 _ hz.2.1, - have : f ⁻¹' (ext_chart_at I' (f x')).source ∈ nhds_within x' s := + have : f ⁻¹' (ext_chart_at I' (f x')).source ∈ 𝓝[s] x' := this.preimage_mem_nhds_within (mem_nhds_sets (ext_chart_at_open_source I' (f x')) (mem_ext_chart_source I' (f x'))), have : (ext_chart_at I x).symm ⁻¹' (f ⁻¹' (ext_chart_at I' (f x')).source) ∈ - nhds_within ((ext_chart_at I x) x') ((ext_chart_at I x).symm ⁻¹' s ∩ range I) := + 𝓝[(ext_chart_at I x).symm ⁻¹' s ∩ range I] ((ext_chart_at I x) x') := ext_chart_preimage_mem_nhds_within' _ _ x'_source this, rw x'z at this, exact mem_nhds_within.1 this }, @@ -684,7 +684,7 @@ begin rcases times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds.1 (hf.of_le hm) with ⟨u, u_nhds, hu⟩, apply times_cont_mdiff_within_at_iff_times_cont_mdiff_on_nhds.2 ⟨_, _, hv.comp' hu⟩, apply filter.inter_mem_sets u_nhds, - suffices h : v ∈ nhds_within (f x) (f '' s), + suffices h : v ∈ 𝓝[f '' s] (f x), { convert mem_nhds_within_insert (hf.continuous_within_at.preimage_mem_nhds_within' h), rw insert_eq_of_mem, apply mem_of_mem_nhds_within (mem_insert (f x) t) v_nhds }, diff --git a/src/measure_theory/borel_space.lean b/src/measure_theory/borel_space.lean index 12b7a02fb4919..a713c4ce0b317 100644 --- a/src/measure_theory/borel_space.lean +++ b/src/measure_theory/borel_space.lean @@ -186,11 +186,11 @@ begin exact i.2.2.is_measurable.principal_is_measurably_generated end -/-- If `s` is a measurable set, then `nhds_within a s` is a measurably generated filter for +/-- If `s` is a measurable set, then `𝓝[s] a` is a measurably generated filter for each `a`. This cannot be an `instance` because it depends on a non-instance `hs : is_measurable s`. -/ lemma is_measurable.nhds_within_is_measurably_generated {s : set α} (hs : is_measurable s) (a : α) : - (nhds_within a s).is_measurably_generated := + (𝓝[s] a).is_measurably_generated := by haveI := hs.principal_is_measurably_generated; exact filter.inf_is_measurably_generated _ _ @[priority 100] -- see Note [lower instance priority] diff --git a/src/measure_theory/measure_space.lean b/src/measure_theory/measure_space.lean index 8837834ee265c..10fc30eaf7d1a 100644 --- a/src/measure_theory/measure_space.lean +++ b/src/measure_theory/measure_space.lean @@ -1115,7 +1115,7 @@ end finite_at_filter lemma finite_at_nhds_within [topological_space α] (μ : measure α) [locally_finite_measure μ] (x : α) (s : set α) : - μ.finite_at_filter (nhds_within x s) := + μ.finite_at_filter (𝓝[s] x) := (finite_at_nhds μ x).inf_of_left @[simp] lemma finite_at_principal {s : set α} : μ.finite_at_filter (𝓟 s) ↔ μ s < ⊤ := @@ -1310,7 +1310,7 @@ namespace is_compact variables {α : Type*} [topological_space α] [measurable_space α] {μ : measure α} {s : set α} lemma finite_measure_of_nhds_within (hs : is_compact s) : - (∀ a ∈ s, μ.finite_at_filter (nhds_within a s)) → μ s < ⊤ := + (∀ a ∈ s, μ.finite_at_filter (𝓝[s] a)) → μ s < ⊤ := by simpa only [← measure.compl_mem_cofinite, measure.finite_at_filter] using hs.compl_mem_sets_of_nhds_within @@ -1318,7 +1318,7 @@ lemma finite_measure [locally_finite_measure μ] (hs : is_compact s) : μ s < hs.finite_measure_of_nhds_within $ λ a ha, μ.finite_at_nhds_within _ _ lemma measure_zero_of_nhds_within (hs : is_compact s) : - (∀ a ∈ s, ∃ t ∈ nhds_within a s, μ t = 0) → μ s = 0 := + (∀ a ∈ s, ∃ t ∈ 𝓝[s] a, μ t = 0) → μ s = 0 := by simpa only [← compl_mem_ae_iff] using hs.compl_mem_sets_of_nhds_within end is_compact diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean index f1e05652968c0..0aa4c7108fe0a 100644 --- a/src/order/filter/basic.lean +++ b/src/order/filter/basic.lean @@ -2003,6 +2003,8 @@ lemma tendsto_iff_comap {f : α → β} {l₁ : filter α} {l₂ : filter β} : tendsto f l₁ l₂ ↔ l₁ ≤ l₂.comap f := map_le_iff_le_comap +alias tendsto_iff_comap ↔ filter.tendsto.le_comap _ + lemma tendsto_congr' {f₁ f₂ : α → β} {l₁ : filter α} {l₂ : filter β} (hl : f₁ =ᶠ[l₁] f₂) : tendsto f₁ l₁ l₂ ↔ tendsto f₂ l₁ l₂ := by rw [tendsto, tendsto, map_congr hl] diff --git a/src/topology/algebra/module.lean b/src/topology/algebra/module.lean index ff685784237f8..f14b8675ee5d0 100644 --- a/src/topology/algebra/module.lean +++ b/src/topology/algebra/module.lean @@ -117,14 +117,14 @@ lemma is_closed_map_smul_of_unit (a : units R) : is_closed_map (λ (x : M), (a : `⊤` is the only submodule of `M` with a nonempty interior. This is the case, e.g., if `R` is a nondiscrete normed field. -/ lemma submodule.eq_top_of_nonempty_interior' [has_continuous_add M] - [ne_bot (nhds_within (0:R) {x | is_unit x})] + [ne_bot (𝓝[{x : R | is_unit x}] 0)] (s : submodule R M) (hs : (interior (s:set M)).nonempty) : s = ⊤ := begin rcases hs with ⟨y, hy⟩, refine (submodule.eq_top_iff'.2 $ λ x, _), rw [mem_interior_iff_mem_nhds] at hy, - have : tendsto (λ c:R, y + c • x) (nhds_within 0 {x | is_unit x}) (𝓝 (y + (0:R) • x)), + have : tendsto (λ c:R, y + c • x) (𝓝[{x : R | is_unit x}] 0) (𝓝 (y + (0:R) • x)), from tendsto_const_nhds.add ((tendsto_nhds_within_of_tendsto_nhds tendsto_id).smul tendsto_const_nhds), rw [zero_smul, add_zero] at this, diff --git a/src/topology/algebra/ordered.lean b/src/topology/algebra/ordered.lean index 2fe4e54ccf768..6110b2f5d6940 100644 --- a/src/topology/algebra/ordered.lean +++ b/src/topology/algebra/ordered.lean @@ -202,19 +202,19 @@ lemma is_closed.is_closed_le [topological_space β] {f g : β → α} {s : set omit t lemma nhds_within_Ici_ne_bot {a b : α} (H₂ : a ≤ b) : - nhds_within b (Ici a) ≠ ⊥ := + 𝓝[Ici a] b ≠ ⊥ := nhds_within_ne_bot_of_mem H₂ lemma nhds_within_Ici_self_ne_bot (a : α) : - nhds_within a (Ici a) ≠ ⊥ := + 𝓝[Ici a] a ≠ ⊥ := nhds_within_Ici_ne_bot (le_refl a) lemma nhds_within_Iic_ne_bot {a b : α} (H : a ≤ b) : - nhds_within a (Iic b) ≠ ⊥ := + 𝓝[Iic b] a ≠ ⊥ := nhds_within_ne_bot_of_mem H lemma nhds_within_Iic_self_ne_bot (a : α) : - nhds_within a (Iic a) ≠ ⊥ := + 𝓝[Iic a] a ≠ ⊥ := nhds_within_Iic_ne_bot (le_refl a) end preorder @@ -333,8 +333,8 @@ end ### Neighborhoods to the left and to the right on an `order_closed_topology` Limits to the left and to the right of real functions are defined in terms of neighborhoods to -the left and to the right, either open or closed, i.e., members of `nhds_within a (Ioi a)` and -`nhds_within a (Ici a)` on the right, and similarly on the left. Here we simply prove that all +the left and to the right, either open or closed, i.e., members of `𝓝[Ioi a] a` and +`𝓝[Ici a] a` on the right, and similarly on the left. Here we simply prove that all right-neighborhoods of a point are equal, and we'll prove later other useful characterizations which require the stronger hypothesis `order_topology α` -/ @@ -343,29 +343,29 @@ require the stronger hypothesis `order_topology α` -/ -/ lemma Ioo_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) : - Ioo a c ∈ nhds_within b (Ioi b) := + Ioo a c ∈ 𝓝[Ioi b] b := mem_nhds_within.2 ⟨Iio c, is_open_Iio, H.2, by rw [inter_comm, Ioi_inter_Iio]; exact Ioo_subset_Ioo_left H.1⟩ lemma Ioc_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) : - Ioc a c ∈ nhds_within b (Ioi b) := + Ioc a c ∈ 𝓝[Ioi b] b := mem_sets_of_superset (Ioo_mem_nhds_within_Ioi H) Ioo_subset_Ioc_self lemma Ico_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) : - Ico a c ∈ nhds_within b (Ioi b) := + Ico a c ∈ 𝓝[Ioi b] b := mem_sets_of_superset (Ioo_mem_nhds_within_Ioi H) Ioo_subset_Ico_self lemma Icc_mem_nhds_within_Ioi {a b c : α} (H : b ∈ Ico a c) : - Icc a c ∈ nhds_within b (Ioi b) := + Icc a c ∈ 𝓝[Ioi b] b := mem_sets_of_superset (Ioo_mem_nhds_within_Ioi H) Ioo_subset_Icc_self @[simp] lemma nhds_within_Ioc_eq_nhds_within_Ioi {a b : α} (h : a < b) : - nhds_within a (Ioc a b) = nhds_within a (Ioi a) := + 𝓝[Ioc a b] a = 𝓝[Ioi a] a := le_antisymm (nhds_within_mono _ Ioc_subset_Ioi_self) $ nhds_within_le_of_mem $ Ioc_mem_nhds_within_Ioi $ left_mem_Ico.2 h @[simp] lemma nhds_within_Ioo_eq_nhds_within_Ioi {a b : α} (h : a < b) : - nhds_within a (Ioo a b) = nhds_within a (Ioi a) := + 𝓝[Ioo a b] a = 𝓝[Ioi a] a := le_antisymm (nhds_within_mono _ Ioo_subset_Ioi_self) $ nhds_within_le_of_mem $ Ioo_mem_nhds_within_Ioi $ left_mem_Ico.2 h @@ -384,27 +384,27 @@ by simp only [continuous_within_at, nhds_within_Ioo_eq_nhds_within_Ioi h] -/ lemma Ioo_mem_nhds_within_Iio {a b c : α} (H : b ∈ Ioc a c) : - Ioo a c ∈ nhds_within b (Iio b) := + Ioo a c ∈ 𝓝[Iio b] b := by simpa only [dual_Ioo] using @Ioo_mem_nhds_within_Ioi (order_dual α) _ _ _ _ _ _ ⟨H.2, H.1⟩ lemma Ico_mem_nhds_within_Iio {a b c : α} (H : b ∈ Ioc a c) : - Ico a c ∈ nhds_within b (Iio b) := + Ico a c ∈ 𝓝[Iio b] b := mem_sets_of_superset (Ioo_mem_nhds_within_Iio H) Ioo_subset_Ico_self lemma Ioc_mem_nhds_within_Iio {a b c : α} (H : b ∈ Ioc a c) : - Ioc a c ∈ nhds_within b (Iio b) := + Ioc a c ∈ 𝓝[Iio b] b := mem_sets_of_superset (Ioo_mem_nhds_within_Iio H) Ioo_subset_Ioc_self lemma Icc_mem_nhds_within_Iio {a b c : α} (H : b ∈ Ioc a c) : - Icc a c ∈ nhds_within b (Iio b) := + Icc a c ∈ 𝓝[Iio b] b := mem_sets_of_superset (Ioo_mem_nhds_within_Iio H) Ioo_subset_Icc_self @[simp] lemma nhds_within_Ico_eq_nhds_within_Iio {a b : α} (h : a < b) : - nhds_within b (Ico a b) = nhds_within b (Iio b) := + 𝓝[Ico a b] b = 𝓝[Iio b] b := by simpa only [dual_Ioc] using @nhds_within_Ioc_eq_nhds_within_Ioi (order_dual α) _ _ _ _ _ h @[simp] lemma nhds_within_Ioo_eq_nhds_within_Iio {a b : α} (h : a < b) : - nhds_within b (Ioo a b) = nhds_within b (Iio b) := + 𝓝[Ioo a b] b = 𝓝[Iio b] b := by simpa only [dual_Ioo] using @nhds_within_Ioo_eq_nhds_within_Ioi (order_dual α) _ _ _ _ _ h @[simp] lemma continuous_within_at_Ico_iff_Iio [topological_space β] {a b : α} {f : α → β} (h : a < b) : @@ -420,29 +420,29 @@ by simp only [continuous_within_at, nhds_within_Ioo_eq_nhds_within_Iio h] -/ lemma Ioo_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ioo a c) : - Ioo a c ∈ nhds_within b (Ici b) := + Ioo a c ∈ 𝓝[Ici b] b := mem_nhds_within_of_mem_nhds $ mem_nhds_sets is_open_Ioo H lemma Ioc_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ioo a c) : - Ioc a c ∈ nhds_within b (Ici b) := + Ioc a c ∈ 𝓝[Ici b] b := mem_sets_of_superset (Ioo_mem_nhds_within_Ici H) Ioo_subset_Ioc_self lemma Ico_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ico a c) : - Ico a c ∈ nhds_within b (Ici b) := + Ico a c ∈ 𝓝[Ici b] b := mem_nhds_within.2 ⟨Iio c, is_open_Iio, H.2, by simp only [inter_comm, Ici_inter_Iio, Ico_subset_Ico_left H.1]⟩ lemma Icc_mem_nhds_within_Ici {a b c : α} (H : b ∈ Ico a c) : - Icc a c ∈ nhds_within b (Ici b) := + Icc a c ∈ 𝓝[Ici b] b := mem_sets_of_superset (Ico_mem_nhds_within_Ici H) Ico_subset_Icc_self @[simp] lemma nhds_within_Icc_eq_nhds_within_Ici {a b : α} (h : a < b) : - nhds_within a (Icc a b) = nhds_within a (Ici a) := + 𝓝[Icc a b] a = 𝓝[Ici a] a := le_antisymm (nhds_within_mono _ Icc_subset_Ici_self) $ nhds_within_le_of_mem $ Icc_mem_nhds_within_Ici $ left_mem_Ico.2 h @[simp] lemma nhds_within_Ico_eq_nhds_within_Ici {a b : α} (h : a < b) : - nhds_within a (Ico a b) = nhds_within a (Ici a) := + 𝓝[Ico a b] a = 𝓝[Ici a] a := le_antisymm (nhds_within_mono _ (λ x, and.left)) $ nhds_within_le_of_mem $ Ico_mem_nhds_within_Ici $ left_mem_Ico.2 h @@ -461,27 +461,27 @@ by simp only [continuous_within_at, nhds_within_Ico_eq_nhds_within_Ici h] -/ lemma Ioo_mem_nhds_within_Iic {a b c : α} (H : b ∈ Ioo a c) : - Ioo a c ∈ nhds_within b (Iic b) := + Ioo a c ∈ 𝓝[Iic b] b := mem_nhds_within_of_mem_nhds $ mem_nhds_sets is_open_Ioo H lemma Ico_mem_nhds_within_Iic {a b c : α} (H : b ∈ Ioo a c) : - Ico a c ∈ nhds_within b (Iic b) := + Ico a c ∈ 𝓝[Iic b] b := mem_sets_of_superset (Ioo_mem_nhds_within_Iic H) Ioo_subset_Ico_self lemma Ioc_mem_nhds_within_Iic {a b c : α} (H : b ∈ Ioc a c) : - Ioc a c ∈ nhds_within b (Iic b) := + Ioc a c ∈ 𝓝[Iic b] b := by simpa only [dual_Ico] using @Ico_mem_nhds_within_Ici (order_dual α) _ _ _ _ _ _ ⟨H.2, H.1⟩ lemma Icc_mem_nhds_within_Iic {a b c : α} (H : b ∈ Ioc a c) : - Icc a c ∈ nhds_within b (Iic b) := + Icc a c ∈ 𝓝[Iic b] b := mem_sets_of_superset (Ioc_mem_nhds_within_Iic H) Ioc_subset_Icc_self @[simp] lemma nhds_within_Icc_eq_nhds_within_Iic {a b : α} (h : a < b) : - nhds_within b (Icc a b) = nhds_within b (Iic b) := + 𝓝[Icc a b] b = 𝓝[Iic b] b := by simpa only [dual_Icc] using @nhds_within_Icc_eq_nhds_within_Ici (order_dual α) _ _ _ _ _ h @[simp] lemma nhds_within_Ioc_eq_nhds_within_Iic {a b : α} (h : a < b) : - nhds_within b (Ioc a b) = nhds_within b (Iic b) := + 𝓝[Ioc a b] b = 𝓝[Iic b] b := by simpa only [dual_Ico] using @nhds_within_Ico_eq_nhds_within_Ici (order_dual α) _ _ _ _ _ h @[simp] @@ -837,7 +837,7 @@ lemma order_topology.t2_space : t2_space α := by apply_instance instance order_topology.regular_space : regular_space α := { regular := assume s a hs ha, have hs' : sᶜ ∈ 𝓝 a, from mem_nhds_sets hs ha, - have ∃t:set α, is_open t ∧ (∀l∈ s, l < a → l ∈ t) ∧ 𝓝 a ⊓ 𝓟 t = ⊥, + have ∃t:set α, is_open t ∧ (∀l∈ s, l < a → l ∈ t) ∧ 𝓝[t] a = ⊥, from by_cases (assume h : ∃l, l < a, let ⟨l, hl, h⟩ := exists_Ioc_subset_of_mem_nhds hs' h in @@ -852,9 +852,9 @@ instance order_topology.regular_space : regular_space α := assume x (hx : l < x), show ¬ x < a, from not_lt.2 $ h₁ _ hx⟩ end) (assume : ¬ ∃l, l < a, ⟨∅, is_open_empty, assume l _ hl, (this ⟨l, hl⟩).elim, - by rw [principal_empty, inf_bot_eq]⟩), + nhds_within_empty _⟩), let ⟨t₁, ht₁o, ht₁s, ht₁a⟩ := this in - have ∃t:set α, is_open t ∧ (∀u∈ s, u>a → u ∈ t) ∧ 𝓝 a ⊓ 𝓟 t = ⊥, + have ∃t:set α, is_open t ∧ (∀u∈ s, u>a → u ∈ t) ∧ 𝓝[t] a = ⊥, from by_cases (assume h : ∃u, u > a, let ⟨u, hu, h⟩ := exists_Ico_subset_of_mem_nhds hs' h in @@ -869,13 +869,13 @@ instance order_topology.regular_space : regular_space α := assume x (hx : u > x), show ¬ x > a, from not_lt.2 $ h₂ _ hx⟩ end) (assume : ¬ ∃u, u > a, ⟨∅, is_open_empty, assume l _ hl, (this ⟨l, hl⟩).elim, - by rw [principal_empty, inf_bot_eq]⟩), + nhds_within_empty _⟩), let ⟨t₂, ht₂o, ht₂s, ht₂a⟩ := this in ⟨t₁ ∪ t₂, is_open_union ht₁o ht₂o, assume x hx, have x ≠ a, from assume eq, ha $ eq ▸ hx, (ne_iff_lt_or_gt.mp this).imp (ht₁s _ hx) (ht₂s _ hx), - by rw [←sup_principal, inf_sup_left, ht₁a, ht₂a, bot_sup_eq]⟩, + by rw [nhds_within_union, ht₁a, ht₂a, bot_sup_eq]⟩, ..order_topology.t2_space } /-- A set is a neighborhood of `a` if and only if it contains an interval `(l, u)` containing `a`, @@ -967,9 +967,9 @@ intervals to the right or to the left of `a`. We give now these characterization 3. `s` includes `(a, u)` for some `u ∈ (a, b]` 4. `s` includes `(a, u)` for some `u > a` -/ lemma tfae_mem_nhds_within_Ioi {a b : α} (hab : a < b) (s : set α) : - tfae [s ∈ nhds_within a (Ioi a), -- 0 : `s` is a neighborhood of `a` within `(a, +∞)` - s ∈ nhds_within a (Ioc a b), -- 1 : `s` is a neighborhood of `a` within `(a, b]` - s ∈ nhds_within a (Ioo a b), -- 2 : `s` is a neighborhood of `a` within `(a, b)` + tfae [s ∈ 𝓝[Ioi a] a, -- 0 : `s` is a neighborhood of `a` within `(a, +∞)` + s ∈ 𝓝[Ioc a b] a, -- 1 : `s` is a neighborhood of `a` within `(a, b]` + s ∈ 𝓝[Ioo a b] a, -- 2 : `s` is a neighborhood of `a` within `(a, b)` ∃ u ∈ Ioc a b, Ioo a u ⊆ s, -- 3 : `s` includes `(a, u)` for some `u ∈ (a, b]` ∃ u ∈ Ioi a, Ioo a u ⊆ s] := -- 4 : `s` includes `(a, u)` for some `u > a` begin @@ -990,25 +990,25 @@ begin end lemma mem_nhds_within_Ioi_iff_exists_mem_Ioc_Ioo_subset {a u' : α} {s : set α} (hu' : a < u') : - s ∈ nhds_within a (Ioi a) ↔ ∃u ∈ Ioc a u', Ioo a u ⊆ s := + s ∈ 𝓝[Ioi a] a ↔ ∃u ∈ Ioc a u', Ioo a u ⊆ s := (tfae_mem_nhds_within_Ioi hu' s).out 0 3 /-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)` with `a < u < u'`, provided `a` is not a top element. -/ lemma mem_nhds_within_Ioi_iff_exists_Ioo_subset' {a u' : α} {s : set α} (hu' : a < u') : - s ∈ nhds_within a (Ioi a) ↔ ∃u ∈ Ioi a, Ioo a u ⊆ s := + s ∈ 𝓝[Ioi a] a ↔ ∃u ∈ Ioi a, Ioo a u ⊆ s := (tfae_mem_nhds_within_Ioi hu' s).out 0 4 /-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)` with `a < u`. -/ lemma mem_nhds_within_Ioi_iff_exists_Ioo_subset [no_top_order α] {a : α} {s : set α} : - s ∈ nhds_within a (Ioi a) ↔ ∃u ∈ Ioi a, Ioo a u ⊆ s := + s ∈ 𝓝[Ioi a] a ↔ ∃u ∈ Ioi a, Ioo a u ⊆ s := let ⟨u', hu'⟩ := no_top a in mem_nhds_within_Ioi_iff_exists_Ioo_subset' hu' /-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u]` with `a < u`. -/ lemma mem_nhds_within_Ioi_iff_exists_Ioc_subset [no_top_order α] [densely_ordered α] - {a : α} {s : set α} : s ∈ nhds_within a (Ioi a) ↔ ∃u ∈ Ioi a, Ioc a u ⊆ s := + {a : α} {s : set α} : s ∈ 𝓝[Ioi a] a ↔ ∃u ∈ Ioi a, Ioc a u ⊆ s := begin rw mem_nhds_within_Ioi_iff_exists_Ioo_subset, split, @@ -1027,9 +1027,9 @@ end 3. `s` includes `(l, b)` for some `l ∈ [a, b)` 4. `s` includes `(l, b)` for some `l < b` -/ lemma tfae_mem_nhds_within_Iio {a b : α} (h : a < b) (s : set α) : - tfae [s ∈ nhds_within b (Iio b), -- 0 : `s` is a neighborhood of `b` within `(-∞, b)` - s ∈ nhds_within b (Ico a b), -- 1 : `s` is a neighborhood of `b` within `[a, b)` - s ∈ nhds_within b (Ioo a b), -- 2 : `s` is a neighborhood of `b` within `(a, b)` + tfae [s ∈ 𝓝[Iio b] b, -- 0 : `s` is a neighborhood of `b` within `(-∞, b)` + s ∈ 𝓝[Ico a b] b, -- 1 : `s` is a neighborhood of `b` within `[a, b)` + s ∈ 𝓝[Ioo a b] b, -- 2 : `s` is a neighborhood of `b` within `(a, b)` ∃ l ∈ Ico a b, Ioo l b ⊆ s, -- 3 : `s` includes `(l, b)` for some `l ∈ [a, b)` ∃ l ∈ Iio b, Ioo l b ⊆ s] := -- 4 : `s` includes `(l, b)` for some `l < b` begin @@ -1041,25 +1041,25 @@ begin end lemma mem_nhds_within_Iio_iff_exists_mem_Ico_Ioo_subset {a l' : α} {s : set α} (hl' : l' < a) : - s ∈ nhds_within a (Iio a) ↔ ∃l ∈ Ico l' a, Ioo l a ⊆ s := + s ∈ 𝓝[Iio a] a ↔ ∃l ∈ Ico l' a, Ioo l a ⊆ s := (tfae_mem_nhds_within_Iio hl' s).out 0 3 /-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)` with `l < a`, provided `a` is not a bottom element. -/ lemma mem_nhds_within_Iio_iff_exists_Ioo_subset' {a l' : α} {s : set α} (hl' : l' < a) : - s ∈ nhds_within a (Iio a) ↔ ∃l ∈ Iio a, Ioo l a ⊆ s := + s ∈ 𝓝[Iio a] a ↔ ∃l ∈ Iio a, Ioo l a ⊆ s := (tfae_mem_nhds_within_Iio hl' s).out 0 4 /-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `(l, a)` with `l < a`. -/ lemma mem_nhds_within_Iio_iff_exists_Ioo_subset [no_bot_order α] {a : α} {s : set α} : - s ∈ nhds_within a (Iio a) ↔ ∃l ∈ Iio a, Ioo l a ⊆ s := + s ∈ 𝓝[Iio a] a ↔ ∃l ∈ Iio a, Ioo l a ⊆ s := let ⟨l', hl'⟩ := no_bot a in mem_nhds_within_Iio_iff_exists_Ioo_subset' hl' /-- A set is a neighborhood of `a` within `(-∞, a)` if and only if it contains an interval `[l, a)` with `l < a`. -/ lemma mem_nhds_within_Iio_iff_exists_Ico_subset [no_bot_order α] [densely_ordered α] - {a : α} {s : set α} : s ∈ nhds_within a (Iio a) ↔ ∃l ∈ Iio a, Ico l a ⊆ s := + {a : α} {s : set α} : s ∈ 𝓝[Iio a] a ↔ ∃l ∈ Iio a, Ico l a ⊆ s := begin convert @mem_nhds_within_Ioi_iff_exists_Ioc_subset (order_dual α) _ _ _ _ _ _ _, simp only [dual_Ioc], refl @@ -1073,9 +1073,9 @@ end 3. `s` includes `[a, u)` for some `u ∈ (a, b]` 4. `s` includes `[a, u)` for some `u > a` -/ lemma tfae_mem_nhds_within_Ici {a b : α} (hab : a < b) (s : set α) : - tfae [s ∈ nhds_within a (Ici a), -- 0 : `s` is a neighborhood of `a` within `[a, +∞)` - s ∈ nhds_within a (Icc a b), -- 1 : `s` is a neighborhood of `a` within `[a, b]` - s ∈ nhds_within a (Ico a b), -- 2 : `s` is a neighborhood of `a` within `[a, b)` + tfae [s ∈ 𝓝[Ici a] a, -- 0 : `s` is a neighborhood of `a` within `[a, +∞)` + s ∈ 𝓝[Icc a b] a, -- 1 : `s` is a neighborhood of `a` within `[a, b]` + s ∈ 𝓝[Ico a b] a, -- 2 : `s` is a neighborhood of `a` within `[a, b)` ∃ u ∈ Ioc a b, Ico a u ⊆ s, -- 3 : `s` includes `[a, u)` for some `u ∈ (a, b]` ∃ u ∈ Ioi a, Ico a u ⊆ s] := -- 4 : `s` includes `[a, u)` for some `u > a` begin @@ -1096,25 +1096,25 @@ begin end lemma mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset {a u' : α} {s : set α} (hu' : a < u') : - s ∈ nhds_within a (Ici a) ↔ ∃u ∈ Ioc a u', Ico a u ⊆ s := + s ∈ 𝓝[Ici a] a ↔ ∃u ∈ Ioc a u', Ico a u ⊆ s := (tfae_mem_nhds_within_Ici hu' s).out 0 3 (by norm_num) (by norm_num) /-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)` with `a < u < u'`, provided `a` is not a top element. -/ lemma mem_nhds_within_Ici_iff_exists_Ico_subset' {a u' : α} {s : set α} (hu' : a < u') : - s ∈ nhds_within a (Ici a) ↔ ∃u ∈ Ioi a, Ico a u ⊆ s := + s ∈ 𝓝[Ici a] a ↔ ∃u ∈ Ioi a, Ico a u ⊆ s := (tfae_mem_nhds_within_Ici hu' s).out 0 4 (by norm_num) (by norm_num) /-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u)` with `a < u`. -/ lemma mem_nhds_within_Ici_iff_exists_Ico_subset [no_top_order α] {a : α} {s : set α} : - s ∈ nhds_within a (Ici a) ↔ ∃u ∈ Ioi a, Ico a u ⊆ s := + s ∈ 𝓝[Ici a] a ↔ ∃u ∈ Ioi a, Ico a u ⊆ s := let ⟨u', hu'⟩ := no_top a in mem_nhds_within_Ici_iff_exists_Ico_subset' hu' /-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u]` with `a < u`. -/ lemma mem_nhds_within_Ici_iff_exists_Icc_subset' [no_top_order α] [densely_ordered α] - {a : α} {s : set α} : s ∈ nhds_within a (Ici a) ↔ ∃u ∈ Ioi a, Icc a u ⊆ s := + {a : α} {s : set α} : s ∈ 𝓝[Ici a] a ↔ ∃u ∈ Ioi a, Icc a u ⊆ s := begin rw mem_nhds_within_Ici_iff_exists_Ico_subset, split, @@ -1133,9 +1133,9 @@ end 3. `s` includes `(l, b]` for some `l ∈ [a, b)` 4. `s` includes `(l, b]` for some `l < b` -/ lemma tfae_mem_nhds_within_Iic {a b : α} (h : a < b) (s : set α) : - tfae [s ∈ nhds_within b (Iic b), -- 0 : `s` is a neighborhood of `b` within `(-∞, b]` - s ∈ nhds_within b (Icc a b), -- 1 : `s` is a neighborhood of `b` within `[a, b]` - s ∈ nhds_within b (Ioc a b), -- 2 : `s` is a neighborhood of `b` within `(a, b]` + tfae [s ∈ 𝓝[Iic b] b, -- 0 : `s` is a neighborhood of `b` within `(-∞, b]` + s ∈ 𝓝[Icc a b] b, -- 1 : `s` is a neighborhood of `b` within `[a, b]` + s ∈ 𝓝[Ioc a b] b, -- 2 : `s` is a neighborhood of `b` within `(a, b]` ∃ l ∈ Ico a b, Ioc l b ⊆ s, -- 3 : `s` includes `(l, b]` for some `l ∈ [a, b)` ∃ l ∈ Iio b, Ioc l b ⊆ s] := -- 4 : `s` includes `(l, b]` for some `l < b` begin @@ -1147,25 +1147,25 @@ begin end lemma mem_nhds_within_Iic_iff_exists_mem_Ico_Ioc_subset {a l' : α} {s : set α} (hl' : l' < a) : - s ∈ nhds_within a (Iic a) ↔ ∃l ∈ Ico l' a, Ioc l a ⊆ s := + s ∈ 𝓝[Iic a] a ↔ ∃l ∈ Ico l' a, Ioc l a ⊆ s := (tfae_mem_nhds_within_Iic hl' s).out 0 3 (by norm_num) (by norm_num) /-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]` with `l < a`, provided `a` is not a bottom element. -/ lemma mem_nhds_within_Iic_iff_exists_Ioc_subset' {a l' : α} {s : set α} (hl' : l' < a) : - s ∈ nhds_within a (Iic a) ↔ ∃l ∈ Iio a, Ioc l a ⊆ s := + s ∈ 𝓝[Iic a] a ↔ ∃l ∈ Iio a, Ioc l a ⊆ s := (tfae_mem_nhds_within_Iic hl' s).out 0 4 (by norm_num) (by norm_num) /-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `(l, a]` with `l < a`. -/ lemma mem_nhds_within_Iic_iff_exists_Ioc_subset [no_bot_order α] {a : α} {s : set α} : - s ∈ nhds_within a (Iic a) ↔ ∃l ∈ Iio a, Ioc l a ⊆ s := + s ∈ 𝓝[Iic a] a ↔ ∃l ∈ Iio a, Ioc l a ⊆ s := let ⟨l', hl'⟩ := no_bot a in mem_nhds_within_Iic_iff_exists_Ioc_subset' hl' /-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `[l, a]` with `l < a`. -/ lemma mem_nhds_within_Iic_iff_exists_Icc_subset' [no_bot_order α] [densely_ordered α] - {a : α} {s : set α} : s ∈ nhds_within a (Iic a) ↔ ∃l ∈ Iio a, Icc l a ⊆ s := + {a : α} {s : set α} : s ∈ 𝓝[Iic a] a ↔ ∃l ∈ Iio a, Icc l a ⊆ s := begin convert @mem_nhds_within_Ici_iff_exists_Icc_subset' (order_dual α) _ _ _ _ _ _ _, simp_rw (show ∀ u : order_dual α, @Icc (order_dual α) _ a u = @Icc α _ u a, from λ u, dual_Icc), @@ -1175,7 +1175,7 @@ end /-- A set is a neighborhood of `a` within `[a, +∞)` if and only if it contains an interval `[a, u]` with `a < u`. -/ lemma mem_nhds_within_Ici_iff_exists_Icc_subset [no_top_order α] [densely_ordered α] - {a : α} {s : set α} : s ∈ nhds_within a (Ici a) ↔ ∃u, a < u ∧ Icc a u ⊆ s := + {a : α} {s : set α} : s ∈ 𝓝[Ici a] a ↔ ∃u, a < u ∧ Icc a u ⊆ s := begin rw mem_nhds_within_Ici_iff_exists_Ico_subset, split, @@ -1189,7 +1189,7 @@ end /-- A set is a neighborhood of `a` within `(-∞, a]` if and only if it contains an interval `[l, a]` with `l < a`. -/ lemma mem_nhds_within_Iic_iff_exists_Icc_subset [no_bot_order α] [densely_ordered α] - {a : α} {s : set α} : s ∈ nhds_within a (Iic a) ↔ ∃l, l < a ∧ Icc l a ⊆ s := + {a : α} {s : set α} : s ∈ 𝓝[Iic a] a ↔ ∃l, l < a ∧ Icc l a ⊆ s := begin rw mem_nhds_within_Iic_iff_exists_Ioc_subset, split, @@ -1230,7 +1230,7 @@ variables [topological_space α] [topological_space β] [linear_order α] [linear_order β] [order_topology α] [order_topology β] lemma is_lub.nhds_within_ne_bot {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) : - ne_bot (nhds_within a s) := + ne_bot (𝓝[s] a) := let ⟨a', ha'⟩ := hs in forall_sets_nonempty_iff_ne_bot.mp $ assume t ht, let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := mem_inf_sets.mp ht in @@ -1252,7 +1252,7 @@ forall_sets_nonempty_iff_ne_bot.mp $ assume t ht, ⟨a', ht ⟨‹a' ∈ t₁›, ht₂ ‹a' ∈ s›⟩⟩) lemma is_glb.nhds_within_ne_bot : ∀ {a : α} {s : set α}, is_glb s a → s.nonempty → - ne_bot (nhds_within a s) := + ne_bot (𝓝[s] a) := @is_lub.nhds_within_ne_bot (order_dual α) _ _ _ lemma is_lub_of_mem_nhds {s : set α} {a : α} {f : filter α} @@ -1271,8 +1271,8 @@ lemma is_glb_of_mem_nhds : ∀ {s : set α} {a : α} {f : filter α}, lemma is_lub_of_is_lub_of_tendsto {f : α → β} {s : set α} {a : α} {b : β} (hf : ∀x∈s, ∀y∈s, x ≤ y → f x ≤ f y) (ha : is_lub s a) (hs : s.nonempty) - (hb : tendsto f (nhds_within a s) (𝓝 b)) : is_lub (f '' s) b := -have hnbot : ne_bot (nhds_within a s), from ha.nhds_within_ne_bot hs, + (hb : tendsto f (𝓝[s] a) (𝓝 b)) : is_lub (f '' s) b := +have hnbot : ne_bot (𝓝[s] a), from ha.nhds_within_ne_bot hs, have ∀a'∈s, ¬ b < f a', from assume a' ha' h, have ∀ᶠ x in 𝓝 b, x < f a', from mem_nhds_sets (is_open_gt' _) h, @@ -1286,7 +1286,7 @@ have ∀a'∈s, ¬ b < f a', have a' < a, from lt_of_le_of_ne (ha.left ha') h.symm, have {x | a' < x} ∈ 𝓝 a, from mem_nhds_sets (is_open_lt' _) this, have {x | a' < x} ∩ t₁ ∈ 𝓝 a, from inter_mem_sets this ht₁, - have ({x | a' < x} ∩ t₁) ∩ s ∈ 𝓝 a ⊓ 𝓟 s, + have ({x | a' < x} ∩ t₁) ∩ s ∈ 𝓝[s] a, from inter_mem_inf_sets this (subset.refl s), let ⟨x, ⟨hx₁, hx₂⟩, hx₃⟩ := hnbot.nonempty_of_mem this in have hxa' : f x < f a', from hs ⟨hx₂, ht₂ hx₃⟩, @@ -1299,18 +1299,18 @@ and.intro lemma is_glb_of_is_glb_of_tendsto {f : α → β} {s : set α} {a : α} {b : β} (hf : ∀x∈s, ∀y∈s, x ≤ y → f x ≤ f y) : is_glb s a → s.nonempty → - tendsto f (nhds_within a s) (𝓝 b) → is_glb (f '' s) b := + tendsto f (𝓝[s] a) (𝓝 b) → is_glb (f '' s) b := @is_lub_of_is_lub_of_tendsto (order_dual α) (order_dual β) _ _ _ _ _ _ f s a b (λ x hx y hy, hf y hy x hx) lemma is_glb_of_is_lub_of_tendsto : ∀ {f : α → β} {s : set α} {a : α} {b : β}, (∀x∈s, ∀y∈s, x ≤ y → f y ≤ f x) → is_lub s a → s.nonempty → - tendsto f (𝓝 a ⊓ 𝓟 s) (𝓝 b) → is_glb (f '' s) b := + tendsto f (𝓝[s] a) (𝓝 b) → is_glb (f '' s) b := @is_lub_of_is_lub_of_tendsto α (order_dual β) _ _ _ _ _ _ lemma is_lub_of_is_glb_of_tendsto : ∀ {f : α → β} {s : set α} {a : α} {b : β}, (∀x∈s, ∀y∈s, x ≤ y → f y ≤ f x) → is_glb s a → s.nonempty → - tendsto f (𝓝 a ⊓ 𝓟 s) (𝓝 b) → is_lub (f '' s) b := + tendsto f (𝓝[s] a) (𝓝 b) → is_lub (f '' s) b := @is_glb_of_is_glb_of_tendsto α (order_dual β) _ _ _ _ _ _ lemma mem_closure_of_is_lub {a : α} {s : set α} (ha : is_lub s a) (hs : s.nonempty) : @@ -1468,37 +1468,37 @@ by simp [frontier, h, le_of_lt h, Icc_diff_Ioo_same] by simp [frontier, h, le_of_lt h, Icc_diff_Ioo_same] lemma nhds_within_Ioi_ne_bot' {a b c : α} (H₁ : a < c) (H₂ : a ≤ b) : - ne_bot (nhds_within b (Ioi a)) := + ne_bot (𝓝[Ioi a] b) := mem_closure_iff_nhds_within_ne_bot.1 $ by { rw [closure_Ioi' H₁], exact H₂ } lemma nhds_within_Ioi_ne_bot [no_top_order α] {a b : α} (H : a ≤ b) : - ne_bot (nhds_within b (Ioi a)) := + ne_bot (𝓝[Ioi a] b) := let ⟨c, hc⟩ := no_top a in nhds_within_Ioi_ne_bot' hc H lemma nhds_within_Ioi_self_ne_bot' {a b : α} (H : a < b) : - ne_bot (nhds_within a (Ioi a)) := + ne_bot (𝓝[Ioi a] a) := nhds_within_Ioi_ne_bot' H (le_refl a) @[instance] lemma nhds_within_Ioi_self_ne_bot [no_top_order α] (a : α) : - ne_bot (nhds_within a (Ioi a)) := + ne_bot (𝓝[Ioi a] a) := nhds_within_Ioi_ne_bot (le_refl a) lemma nhds_within_Iio_ne_bot' {a b c : α} (H₁ : a < c) (H₂ : b ≤ c) : - ne_bot (nhds_within b (Iio c)) := + ne_bot (𝓝[Iio c] b) := mem_closure_iff_nhds_within_ne_bot.1 $ by { rw [closure_Iio' H₁], exact H₂ } lemma nhds_within_Iio_ne_bot [no_bot_order α] {a b : α} (H : a ≤ b) : - ne_bot (nhds_within a (Iio b)) := + ne_bot (𝓝[Iio b] a) := let ⟨c, hc⟩ := no_bot b in nhds_within_Iio_ne_bot' hc H lemma nhds_within_Iio_self_ne_bot' {a b : α} (H : a < b) : - ne_bot (nhds_within b (Iio b)) := + ne_bot (𝓝[Iio b] b) := nhds_within_Iio_ne_bot' H (le_refl b) @[instance] lemma nhds_within_Iio_self_ne_bot [no_bot_order α] (a : α) : - ne_bot (nhds_within a (Iio a)) := + ne_bot (𝓝[Iio a] a) := nhds_within_Iio_ne_bot (le_refl a) end linear_order @@ -1782,12 +1782,12 @@ on a closed subset, contains `a`, and for any `x ∈ s ∩ [a, b)` the set `s` i neighborhood of `x` within `(x, +∞)`, then `[a, b] ⊆ s`. -/ lemma is_closed.Icc_subset_of_forall_mem_nhds_within {a b : α} {s : set α} (hs : is_closed (s ∩ Icc a b)) (ha : a ∈ s) - (hgt : ∀ x ∈ s ∩ Ico a b, s ∈ nhds_within x (Ioi x)) : + (hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[Ioi x] x) : Icc a b ⊆ s := begin apply hs.Icc_subset_of_forall_exists_gt ha, rintros x ⟨hxs, hxab⟩ y hyxb, - have : s ∩ Ioc x y ∈ nhds_within x (Ioi x), + have : s ∩ Ioc x y ∈ 𝓝[Ioi x] x, from inter_mem_sets (hgt x ⟨hxs, hxab⟩) (Ioc_mem_nhds_within_Ioi ⟨le_refl _, hyxb⟩), exact (nhds_within_Ioi_self_ne_bot' hxab.2).nonempty_of_mem this end @@ -1805,7 +1805,7 @@ begin apply (is_closed_inter hs is_closed_Icc).Icc_subset_of_forall_mem_nhds_within hx.2, rintros z ⟨zs, hz⟩, have zt : z ∈ tᶜ, from λ zt, hst ⟨z, xyab $ Ico_subset_Icc_self hz, zs, zt⟩, - have : tᶜ ∩ Ioc z y ∈ nhds_within z (Ioi z), + have : tᶜ ∩ Ioc z y ∈ 𝓝[Ioi z] z, { rw [← nhds_within_Ioc_eq_nhds_within_Ioi hz.2], exact mem_nhds_within.2 ⟨tᶜ, ht, zt, subset.refl _⟩}, apply mem_sets_of_superset this, @@ -2212,20 +2212,20 @@ else or.inl $ tendsto_at_top_at_top_of_monotone' h_mono H @[to_additive] lemma tendsto_inv_nhds_within_Ioi {α : Type*} [ordered_comm_group α] [topological_space α] [topological_group α] {a : α} : - tendsto has_inv.inv (nhds_within a (Ioi a)) (nhds_within (a⁻¹) (Iio (a⁻¹))) := + tendsto has_inv.inv (𝓝[Ioi a] a) (𝓝[Iio (a⁻¹)] (a⁻¹)) := (continuous_inv.tendsto a).inf $ by simp [tendsto_principal_principal] @[to_additive] lemma tendsto_inv_nhds_within_Iio {α : Type*} [ordered_comm_group α] [topological_space α] [topological_group α] {a : α} : - tendsto has_inv.inv (nhds_within a (Iio a)) (nhds_within (a⁻¹) (Ioi (a⁻¹))) := + tendsto has_inv.inv (𝓝[Iio a] a) (𝓝[Ioi (a⁻¹)] (a⁻¹)) := (continuous_inv.tendsto a).inf $ by simp [tendsto_principal_principal] @[to_additive] lemma tendsto_inv_nhds_within_Ioi_inv {α : Type*} [ordered_comm_group α] [topological_space α] [topological_group α] {a : α} : - tendsto has_inv.inv (nhds_within (a⁻¹) (Ioi (a⁻¹))) (nhds_within a (Iio a)) := + tendsto has_inv.inv (𝓝[Ioi (a⁻¹)] (a⁻¹)) (𝓝[Iio a] a) := by simpa only [inv_inv] using @tendsto_inv_nhds_within_Ioi _ _ _ _ (a⁻¹) @[to_additive] lemma tendsto_inv_nhds_within_Iio_inv {α : Type*} [ordered_comm_group α] [topological_space α] [topological_group α] {a : α} : - tendsto has_inv.inv (nhds_within (a⁻¹) (Iio (a⁻¹))) (nhds_within a (Ioi a)) := + tendsto has_inv.inv (𝓝[Iio (a⁻¹)] (a⁻¹)) (𝓝[Ioi a] a) := by simpa only [inv_inv] using @tendsto_inv_nhds_within_Iio _ _ _ _ (a⁻¹) diff --git a/src/topology/basic.lean b/src/topology/basic.lean index b39c4369b3b24..676f2867c0f22 100644 --- a/src/topology/basic.lean +++ b/src/topology/basic.lean @@ -24,6 +24,11 @@ For topological spaces `α` and `β`, a function `f : α → β` and a point `a `continuous f`. There is also a version of continuity `pcontinuous` for partially defined functions. +## Notation + +* `𝓝 x`: the filter of neighborhoods of a point `x`; +* `𝓟 s`: the principal filter of a set `s`; + ## Implementation notes Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in diff --git a/src/topology/continuous_on.lean b/src/topology/continuous_on.lean index 45bea7803aa96..45653a9230408 100644 --- a/src/topology/continuous_on.lean +++ b/src/topology/continuous_on.lean @@ -10,14 +10,20 @@ import topology.constructions This file defines relative versions -`nhds_within` of `nhds` -`continuous_on` of `continuous` -`continuous_within_at` of `continuous_at` +* `nhds_within` of `nhds` +* `continuous_on` of `continuous` +* `continuous_within_at` of `continuous_at` and proves their basic properties, including the relationships between these restricted notions and the corresponding notions for the subtype equipped with the subspace topology. +## Notation + +* `𝓝 x`: the filter of neighborhoods of a point `x`; +* `𝓟 s`: the principal filter of a set `s`; +* `𝓝[s] x`: the filter `nhds_within x s` of neighborhoods of a point `x` within a set `s`. + -/ open set filter @@ -26,24 +32,26 @@ open_locale topological_space filter variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} variables [topological_space α] -/-- The "neighborhood within" filter. Elements of `nhds_within a s` are sets containing the +/-- The "neighborhood within" filter. Elements of `𝓝[s] a` are sets containing the intersection of `s` and a neighborhood of `a`. -/ def nhds_within (a : α) (s : set α) : filter α := 𝓝 a ⊓ 𝓟 s +localized "notation `𝓝[` s `] ` x:100 := nhds_within x s" in topological_space + @[simp] lemma nhds_bind_nhds_within {a : α} {s : set α} : - (𝓝 a).bind (λ x, nhds_within x s) = nhds_within a s := + (𝓝 a).bind (λ x, 𝓝[s] x) = 𝓝[s] a := bind_inf_principal.trans $ congr_arg2 _ nhds_bind_nhds rfl @[simp] lemma eventually_nhds_nhds_within {a : α} {s : set α} {p : α → Prop} : - (∀ᶠ y in 𝓝 a, ∀ᶠ x in nhds_within y s, p x) ↔ ∀ᶠ x in nhds_within a s, p x := + (∀ᶠ y in 𝓝 a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x := filter.ext_iff.1 nhds_bind_nhds_within {x | p x} lemma eventually_nhds_within_iff {a : α} {s : set α} {p : α → Prop} : - (∀ᶠ x in nhds_within a s, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x := + (∀ᶠ x in 𝓝[s] a, p x) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → p x := eventually_inf_principal @[simp] lemma eventually_nhds_within_nhds_within {a : α} {s : set α} {p : α → Prop} : - (∀ᶠ y in nhds_within a s, ∀ᶠ x in nhds_within y s, p x) ↔ ∀ᶠ x in nhds_within a s, p x := + (∀ᶠ y in 𝓝[s] a, ∀ᶠ x in 𝓝[s] y, p x) ↔ ∀ᶠ x in 𝓝[s] a, p x := begin refine ⟨λ h, _, λ h, (eventually_nhds_nhds_within.2 h).filter_mono inf_le_left⟩, simp only [eventually_nhds_within_iff] at h ⊢, @@ -51,113 +59,107 @@ begin end theorem nhds_within_eq (a : α) (s : set α) : - nhds_within a s = ⨅ t ∈ {t : set α | a ∈ t ∧ is_open t}, 𝓟 (t ∩ s) := -begin - rw [nhds_within, nhds, binfi_inf], - simp only [inf_principal], - exact ⟨univ, mem_univ _, is_open_univ⟩ -end + 𝓝[s] a = ⨅ t ∈ {t : set α | a ∈ t ∧ is_open t}, 𝓟 (t ∩ s) := +((nhds_basis_opens a).inf_principal s).eq_binfi -theorem nhds_within_univ (a : α) : nhds_within a set.univ = 𝓝 a := +theorem nhds_within_univ (a : α) : 𝓝[set.univ] a = 𝓝 a := by rw [nhds_within, principal_univ, inf_top_eq] lemma nhds_within_has_basis {p : β → Prop} {s : β → set α} {a : α} (h : (𝓝 a).has_basis p s) (t : set α) : - (nhds_within a t).has_basis p (λ i, s i ∩ t) := + (𝓝[t] a).has_basis p (λ i, s i ∩ t) := h.inf_principal t lemma nhds_within_basis_open (a : α) (t : set α) : - (nhds_within a t).has_basis (λ u, a ∈ u ∧ is_open u) (λ u, u ∩ t) := + (𝓝[t] a).has_basis (λ u, a ∈ u ∧ is_open u) (λ u, u ∩ t) := nhds_within_has_basis (nhds_basis_opens a) t theorem mem_nhds_within {t : set α} {a : α} {s : set α} : - t ∈ nhds_within a s ↔ ∃ u, is_open u ∧ a ∈ u ∧ u ∩ s ⊆ t := + t ∈ 𝓝[s] a ↔ ∃ u, is_open u ∧ a ∈ u ∧ u ∩ s ⊆ t := by simpa only [exists_prop, and_assoc, and_comm] using (nhds_within_basis_open a s).mem_iff lemma mem_nhds_within_iff_exists_mem_nhds_inter {t : set α} {a : α} {s : set α} : - t ∈ nhds_within a s ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t := + t ∈ 𝓝[s] a ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t := (nhds_within_has_basis (𝓝 a).basis_sets s).mem_iff lemma nhds_of_nhds_within_of_nhds - {s t : set α} {a : α} (h1 : s ∈ 𝓝 a) (h2 : t ∈ nhds_within a s) : (t ∈ 𝓝 a) := + {s t : set α} {a : α} (h1 : s ∈ 𝓝 a) (h2 : t ∈ 𝓝[s] a) : (t ∈ 𝓝 a) := begin rcases mem_nhds_within_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩, exact (nhds a).sets_of_superset ((nhds a).inter_sets Hw h1) hw, end lemma mem_nhds_within_of_mem_nhds {s t : set α} {a : α} (h : s ∈ 𝓝 a) : - s ∈ nhds_within a t := + s ∈ 𝓝[t] a := mem_inf_sets_of_left h -theorem self_mem_nhds_within {a : α} {s : set α} : s ∈ nhds_within a s := +theorem self_mem_nhds_within {a : α} {s : set α} : s ∈ 𝓝[s] a := mem_inf_sets_of_right (mem_principal_self s) theorem inter_mem_nhds_within (s : set α) {t : set α} {a : α} (h : t ∈ 𝓝 a) : - s ∩ t ∈ nhds_within a s := + s ∩ t ∈ 𝓝[s] a := inter_mem_sets (mem_inf_sets_of_right (mem_principal_self s)) (mem_inf_sets_of_left h) -theorem nhds_within_mono (a : α) {s t : set α} (h : s ⊆ t) : nhds_within a s ≤ nhds_within a t := +theorem nhds_within_mono (a : α) {s t : set α} (h : s ⊆ t) : 𝓝[s] a ≤ 𝓝[t] a := inf_le_inf_left _ (principal_mono.mpr h) -lemma mem_of_mem_nhds_within {a : α} {s t : set α} (ha : a ∈ s) (ht : t ∈ nhds_within a s) : +lemma mem_of_mem_nhds_within {a : α} {s t : set α} (ha : a ∈ s) (ht : t ∈ 𝓝[s] a) : a ∈ t := let ⟨u, hu, H⟩ := mem_nhds_within.1 ht in H.2 ⟨H.1, ha⟩ lemma filter.eventually.self_of_nhds_within {p : α → Prop} {s : set α} {x : α} - (h : ∀ᶠ y in nhds_within x s, p y) (hx : x ∈ s) : p x := + (h : ∀ᶠ y in 𝓝[s] x, p y) (hx : x ∈ s) : p x := mem_of_mem_nhds_within hx h -theorem nhds_within_restrict'' {a : α} (s : set α) {t : set α} (h : t ∈ nhds_within a s) : - nhds_within a s = nhds_within a (s ∩ t) := +theorem nhds_within_restrict'' {a : α} (s : set α) {t : set α} (h : t ∈ 𝓝[s] a) : + 𝓝[s] a = 𝓝[s ∩ t] a := le_antisymm (le_inf inf_le_left (le_principal_iff.mpr (inter_mem_sets self_mem_nhds_within h))) (inf_le_inf_left _ (principal_mono.mpr (set.inter_subset_left _ _))) theorem nhds_within_restrict' {a : α} (s : set α) {t : set α} (h : t ∈ 𝓝 a) : - nhds_within a s = nhds_within a (s ∩ t) := + 𝓝[s] a = 𝓝[s ∩ t] a := nhds_within_restrict'' s $ mem_inf_sets_of_left h theorem nhds_within_restrict {a : α} (s : set α) {t : set α} (h₀ : a ∈ t) (h₁ : is_open t) : - nhds_within a s = nhds_within a (s ∩ t) := + 𝓝[s] a = 𝓝[s ∩ t] a := nhds_within_restrict' s (mem_nhds_sets h₁ h₀) -theorem nhds_within_le_of_mem {a : α} {s t : set α} (h : s ∈ nhds_within a t) : - nhds_within a t ≤ nhds_within a s := +theorem nhds_within_le_of_mem {a : α} {s t : set α} (h : s ∈ 𝓝[t] a) : + 𝓝[t] a ≤ 𝓝[s] a := begin rcases mem_nhds_within.1 h with ⟨u, u_open, au, uts⟩, - have : nhds_within a t = nhds_within a (t ∩ u) := nhds_within_restrict _ au u_open, + have : 𝓝[t] a = 𝓝[t ∩ u] a := nhds_within_restrict _ au u_open, rw [this, inter_comm], exact nhds_within_mono _ uts end theorem nhds_within_eq_nhds_within {a : α} {s t u : set α} (h₀ : a ∈ s) (h₁ : is_open s) (h₂ : t ∩ s = u ∩ s) : - nhds_within a t = nhds_within a u := + 𝓝[t] a = 𝓝[u] a := by rw [nhds_within_restrict t h₀ h₁, nhds_within_restrict u h₀ h₁, h₂] theorem nhds_within_eq_of_open {a : α} {s : set α} (h₀ : a ∈ s) (h₁ : is_open s) : - nhds_within a s = 𝓝 a := -by rw [←nhds_within_univ]; apply nhds_within_eq_nhds_within h₀ h₁; - rw [set.univ_inter, set.inter_self] + 𝓝[s] a = 𝓝 a := +inf_eq_left.2 $ le_principal_iff.2 $ mem_nhds_sets h₁ h₀ -@[simp] theorem nhds_within_empty (a : α) : nhds_within a {} = ⊥ := +@[simp] theorem nhds_within_empty (a : α) : 𝓝[∅] a = ⊥ := by rw [nhds_within, principal_empty, inf_bot_eq] theorem nhds_within_union (a : α) (s t : set α) : - nhds_within a (s ∪ t) = nhds_within a s ⊔ nhds_within a t := -by unfold nhds_within; rw [←inf_sup_left, sup_principal] + 𝓝[s ∪ t] a = 𝓝[s] a ⊔ 𝓝[t] a := +by { delta nhds_within, rw [←inf_sup_left, sup_principal] } theorem nhds_within_inter (a : α) (s t : set α) : - nhds_within a (s ∩ t) = nhds_within a s ⊓ nhds_within a t := -by unfold nhds_within; rw [inf_left_comm, inf_assoc, inf_principal, - ←inf_assoc, inf_idem] + 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓝[t] a := +by { delta nhds_within, rw [inf_left_comm, inf_assoc, inf_principal, ←inf_assoc, inf_idem] } theorem nhds_within_inter' (a : α) (s t : set α) : - nhds_within a (s ∩ t) = (nhds_within a s) ⊓ 𝓟 t := -by { unfold nhds_within, rw [←inf_principal, inf_assoc] } + 𝓝[s ∩ t] a = (𝓝[s] a) ⊓ 𝓟 t := +by { delta nhds_within, rw [←inf_principal, inf_assoc] } -lemma mem_nhds_within_insert {a : α} {s t : set α} (h : t ∈ nhds_within a s) : - insert a t ∈ nhds_within a (insert a s) := +lemma mem_nhds_within_insert {a : α} {s t : set α} (h : t ∈ 𝓝[s] a) : + insert a t ∈ 𝓝[insert a s] a := begin rcases mem_nhds_within.1 h with ⟨o, o_open, ao, ho⟩, apply mem_nhds_within.2 ⟨o, o_open, ao, _⟩, @@ -170,40 +172,40 @@ end lemma nhds_within_prod_eq {α : Type*} [topological_space α] {β : Type*} [topological_space β] (a : α) (b : β) (s : set α) (t : set β) : - nhds_within (a, b) (s.prod t) = (nhds_within a s).prod (nhds_within b t) := -by { unfold nhds_within, rw [nhds_prod_eq, ←filter.prod_inf_prod, filter.prod_principal_principal] } + 𝓝[s.prod t] (a, b) = (𝓝[s] a).prod (𝓝[t] b) := +by { delta nhds_within, rw [nhds_prod_eq, ←filter.prod_inf_prod, filter.prod_principal_principal] } lemma nhds_within_prod {α : Type*} [topological_space α] {β : Type*} [topological_space β] {s u : set α} {t v : set β} {a : α} {b : β} - (hu : u ∈ nhds_within a s) (hv : v ∈ nhds_within b t) : - (u.prod v) ∈ nhds_within (a, b) (s.prod t) := + (hu : u ∈ 𝓝[s] a) (hv : v ∈ 𝓝[t] b) : + (u.prod v) ∈ 𝓝[s.prod t] (a, b) := by { rw nhds_within_prod_eq, exact prod_mem_prod hu hv, } theorem tendsto_if_nhds_within {f g : α → β} {p : α → Prop} [decidable_pred p] {a : α} {s : set α} {l : filter β} - (h₀ : tendsto f (nhds_within a (s ∩ p)) l) - (h₁ : tendsto g (nhds_within a (s ∩ {x | ¬ p x})) l) : - tendsto (λ x, if p x then f x else g x) (nhds_within a s) l := + (h₀ : tendsto f (𝓝[s ∩ p] a) l) + (h₁ : tendsto g (𝓝[s ∩ {x | ¬ p x}] a) l) : + tendsto (λ x, if p x then f x else g x) (𝓝[s] a) l := by apply tendsto_if; rw [←nhds_within_inter']; assumption lemma map_nhds_within (f : α → β) (a : α) (s : set α) : - map f (nhds_within a s) = + map f (𝓝[s] a) = ⨅ t ∈ {t : set α | a ∈ t ∧ is_open t}, 𝓟 (set.image f (t ∩ s)) := ((nhds_within_basis_open a s).map f).eq_binfi theorem tendsto_nhds_within_mono_left {f : α → β} {a : α} - {s t : set α} {l : filter β} (hst : s ⊆ t) (h : tendsto f (nhds_within a t) l) : - tendsto f (nhds_within a s) l := + {s t : set α} {l : filter β} (hst : s ⊆ t) (h : tendsto f (𝓝[t] a) l) : + tendsto f (𝓝[s] a) l := tendsto_le_left (nhds_within_mono a hst) h theorem tendsto_nhds_within_mono_right {f : β → α} {l : filter β} - {a : α} {s t : set α} (hst : s ⊆ t) (h : tendsto f l (nhds_within a s)) : - tendsto f l (nhds_within a t) := + {a : α} {s t : set α} (hst : s ⊆ t) (h : tendsto f l (𝓝[s] a)) : + tendsto f l (𝓝[t] a) := tendsto_le_right (nhds_within_mono a hst) h theorem tendsto_nhds_within_of_tendsto_nhds {f : α → β} {a : α} {s : set α} {l : filter β} (h : tendsto f (𝓝 a) l) : - tendsto f (nhds_within a s) l := + tendsto f (𝓝[s] a) l := tendsto_le_left inf_le_left h theorem principal_subtype {α : Type*} (s : set α) (t : set {x // x ∈ s}) : @@ -211,72 +213,71 @@ theorem principal_subtype {α : Type*} (s : set α) (t : set {x // x ∈ s}) : by rw [comap_principal, set.preimage_image_eq _ subtype.coe_injective] lemma mem_closure_iff_nhds_within_ne_bot {s : set α} {x : α} : - x ∈ closure s ↔ ne_bot (nhds_within x s) := + x ∈ closure s ↔ ne_bot (𝓝[s] x) := mem_closure_iff_cluster_pt lemma nhds_within_ne_bot_of_mem {s : set α} {x : α} (hx : x ∈ s) : - ne_bot (nhds_within x s) := + ne_bot (𝓝[s] x) := mem_closure_iff_nhds_within_ne_bot.1 $ subset_closure hx lemma is_closed.mem_of_nhds_within_ne_bot {s : set α} (hs : is_closed s) - {x : α} (hx : ne_bot $ nhds_within x s) : x ∈ s := + {x : α} (hx : ne_bot $ 𝓝[s] x) : x ∈ s := by simpa only [hs.closure_eq] using mem_closure_iff_nhds_within_ne_bot.2 hx lemma eventually_eq_nhds_within_iff {f g : α → β} {s : set α} {a : α} : - (f =ᶠ[nhds_within a s] g) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x := + (f =ᶠ[𝓝[s] a] g) ↔ ∀ᶠ x in 𝓝 a, x ∈ s → f x = g x := mem_inf_principal lemma eventually_eq_nhds_within_of_eq_on {f g : α → β} {s : set α} {a : α} (h : eq_on f g s) : - f =ᶠ[nhds_within a s] g := + f =ᶠ[𝓝[s] a] g := mem_inf_sets_of_right h lemma set.eq_on.eventually_eq_nhds_within {f g : α → β} {s : set α} {a : α} (h : eq_on f g s) : - f =ᶠ[nhds_within a s] g := + f =ᶠ[𝓝[s] a] g := eventually_eq_nhds_within_of_eq_on h lemma tendsto_nhds_within_congr {f g : α → β} {s : set α} {a : α} {l : filter β} - (hfg : ∀ x ∈ s, f x = g x) (hf : tendsto f (nhds_within a s) l) : tendsto g (nhds_within a s) l := + (hfg : ∀ x ∈ s, f x = g x) (hf : tendsto f (𝓝[s] a) l) : tendsto g (𝓝[s] a) l := (tendsto_congr' $ eventually_eq_nhds_within_of_eq_on hfg).1 hf lemma eventually_nhds_with_of_forall {s : set α} {a : α} {p : α → Prop} (h : ∀ x ∈ s, p x) : - ∀ᶠ x in nhds_within a s, p x := + ∀ᶠ x in 𝓝[s] a, p x := mem_inf_sets_of_right h lemma tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {β : Type*} {a : α} {l : filter β} {s : set α} (f : β → α) (h1 : tendsto f l (nhds a)) (h2 : ∀ᶠ x in l, f x ∈ s) : - tendsto f l (nhds_within a s) := + tendsto f l (𝓝[s] a) := tendsto_inf.2 ⟨h1, tendsto_principal.2 h2⟩ lemma filter.eventually_eq.eq_of_nhds_within {s : set α} {f g : α → β} {a : α} - (h : f =ᶠ[nhds_within a s] g) (hmem : a ∈ s) : f a = g a := + (h : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : f a = g a := h.self_of_nhds_within hmem /- nhds_within and subtypes -/ -theorem mem_nhds_within_subtype (s : set α) (a : {x // x ∈ s}) (t u : set {x // x ∈ s}) : - t ∈ nhds_within a u ↔ - t ∈ comap (coe : s → α) (nhds_within a (coe '' u)) := +theorem mem_nhds_within_subtype {s : set α} {a : {x // x ∈ s}} {t u : set {x // x ∈ s}} : + t ∈ 𝓝[u] a ↔ t ∈ comap (coe : s → α) (𝓝[coe '' u] a) := by rw [nhds_within, nhds_subtype, principal_subtype, ←comap_inf, ←nhds_within] theorem nhds_within_subtype (s : set α) (a : {x // x ∈ s}) (t : set {x // x ∈ s}) : - nhds_within a t = comap (coe : s → α) (nhds_within a (coe '' t)) := -filter_eq $ by ext u; rw mem_nhds_within_subtype + 𝓝[t] a = comap (coe : s → α) (𝓝[coe '' t] a) := +filter.ext $ λ u, mem_nhds_within_subtype theorem nhds_within_eq_map_subtype_coe {s : set α} {a : α} (h : a ∈ s) : - nhds_within a s = map (coe : s → α) (𝓝 ⟨a, h⟩) := -have h₀ : s ∈ nhds_within a s, + 𝓝[s] a = map (coe : s → α) (𝓝 ⟨a, h⟩) := +have h₀ : s ∈ 𝓝[s] a, by { rw [mem_nhds_within], existsi set.univ, simp [set.diff_eq] }, have h₁ : ∀ y ∈ s, ∃ x : s, ↑x = y, from λ y h, ⟨⟨y, h⟩, rfl⟩, begin - rw [←nhds_within_univ, nhds_within_subtype, subtype.coe_image_univ], + conv_rhs { rw [← nhds_within_univ, nhds_within_subtype, subtype.coe_image_univ] }, exact (map_comap_of_surjective' h₀ h₁).symm, end theorem tendsto_nhds_within_iff_subtype {s : set α} {a : α} (h : a ∈ s) (f : α → β) (l : filter β) : - tendsto f (nhds_within a s) l ↔ tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l := + tendsto f (𝓝[s] a) l ↔ tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l := by simp only [tendsto, nhds_within_eq_map_subtype_coe h, filter.map_map, restrict] variables [topological_space β] [topological_space γ] [topological_space δ] @@ -284,13 +285,13 @@ variables [topological_space β] [topological_space γ] [topological_space δ] /-- A function between topological spaces is continuous at a point `x₀` within a subset `s` if `f x` tends to `f x₀` when `x` tends to `x₀` while staying within `s`. -/ def continuous_within_at (f : α → β) (s : set α) (x : α) : Prop := -tendsto f (nhds_within x s) (𝓝 (f x)) +tendsto f (𝓝[s] x) (𝓝 (f x)) /-- If a function is continuous within `s` at `x`, then it tends to `f x` within `s` by definition. We register this fact for use with the dot notation, especially to use `tendsto.comp` as `continuous_within_at.comp` will have a different meaning. -/ lemma continuous_within_at.tendsto {f : α → β} {s : set α} {x : α} (h : continuous_within_at f s x) : - tendsto f (nhds_within x s) (𝓝 (f x)) := h + tendsto f (𝓝[s] x) (𝓝 (f x)) := h /-- A function between topological spaces is continuous on a subset `s` when it's continuous at every point of `s` within `s`. -/ @@ -310,7 +311,7 @@ tendsto_nhds_within_iff_subtype h f _ theorem continuous_within_at.tendsto_nhds_within_image {f : α → β} {x : α} {s : set α} (h : continuous_within_at f s x) : - tendsto f (nhds_within x s) (nhds_within (f x) (f '' s)) := + tendsto f (𝓝[s] x) (𝓝[f '' s] (f x)) := tendsto_inf.2 ⟨h, tendsto_principal.2 $ mem_inf_sets_of_right $ mem_principal_sets.2 $ λ x, mem_image_of_mem _⟩ @@ -370,7 +371,7 @@ lemma continuous_on_empty (f : α → β) : continuous_on f ∅ := λ x, false.elim theorem nhds_within_le_comap {x : α} {s : set α} {f : α → β} (ctsf : continuous_within_at f s x) : - nhds_within x s ≤ comap f (nhds_within (f x) (f '' s)) := + 𝓝[s] x ≤ comap f (𝓝[f '' s] (f x)) := map_le_iff_le_comap.1 ctsf.tendsto_nhds_within_image theorem continuous_within_at_iff_ptendsto_res (f : α → β) {x : α} {s : set α} : @@ -385,7 +386,7 @@ lemma continuous_within_at.mono {f : α → β} {s t : set α} {x : α} (h : con (hs : s ⊆ t) : continuous_within_at f s x := tendsto_le_left (nhds_within_mono x hs) h -lemma continuous_within_at_inter' {f : α → β} {s t : set α} {x : α} (h : t ∈ nhds_within x s) : +lemma continuous_within_at_inter' {f : α → β} {s t : set α} {x : α} (h : t ∈ 𝓝[s] x) : continuous_within_at f (s ∩ t) x ↔ continuous_within_at f s x := by simp [continuous_within_at, nhds_within_restrict'' s h] @@ -448,8 +449,7 @@ begin have A := (h x (h₁ hx)).mono h₁, unfold continuous_within_at at A, rw ← h' hx at A, - have : (g =ᶠ[nhds_within x s₁] f) := mem_inf_sets_of_right h', - exact A.congr' this.symm + exact A.congr' h'.eventually_eq_nhds_within.symm end lemma continuous_on.congr {f g : α → β} {s : set α} (h : continuous_on f s) (h' : eq_on g f s) : @@ -481,9 +481,9 @@ lemma continuous_within_at.comp {g : β → γ} {f : α → β} {s : set α} {t begin have : tendsto f (𝓟 s) (𝓟 t), by { rw tendsto_principal_principal, exact λx hx, h hx }, - have : tendsto f (nhds_within x s) (𝓟 t) := + have : tendsto f (𝓝[s] x) (𝓟 t) := tendsto_le_left inf_le_right this, - have : tendsto f (nhds_within x s) (nhds_within (f x) t) := + have : tendsto f (𝓝[s] x) (𝓝[t] (f x)) := tendsto_inf.2 ⟨hf, this⟩, exact tendsto.comp hg this end @@ -524,16 +524,16 @@ lemma continuous.comp_continuous_on {g : β → γ} {f : α → β} {s : set α} hg.continuous_on.comp hf subset_preimage_univ lemma continuous_within_at.preimage_mem_nhds_within {f : α → β} {x : α} {s : set α} {t : set β} - (h : continuous_within_at f s x) (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ nhds_within x s := + (h : continuous_within_at f s x) (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝[s] x := h ht lemma continuous_within_at.preimage_mem_nhds_within' {f : α → β} {x : α} {s : set α} {t : set β} - (h : continuous_within_at f s x) (ht : t ∈ nhds_within (f x) (f '' s)) : - f ⁻¹' t ∈ nhds_within x s := + (h : continuous_within_at f s x) (ht : t ∈ 𝓝[f '' s] (f x)) : + f ⁻¹' t ∈ 𝓝[s] x := begin rw mem_nhds_within at ht, rcases ht with ⟨u, u_open, fxu, hu⟩, - have : f ⁻¹' u ∩ s ∈ nhds_within x s := + have : f ⁻¹' u ∩ s ∈ 𝓝[s] x := filter.inter_mem_sets (h (mem_nhds_sets u_open fxu)) self_mem_nhds_within, apply mem_sets_of_superset this, calc f ⁻¹' u ∩ s @@ -543,7 +543,7 @@ begin end lemma continuous_within_at.congr_of_eventually_eq {f f₁ : α → β} {s : set α} {x : α} - (h : continuous_within_at f s x) (h₁ : f₁ =ᶠ[nhds_within x s] f) (hx : f₁ x = f x) : + (h : continuous_within_at f s x) (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : continuous_within_at f₁ s x := by rwa [continuous_within_at, filter.tendsto, hx, filter.map_congr h₁] diff --git a/src/topology/dense_embedding.lean b/src/topology/dense_embedding.lean index 22f27d6a90f94..2dde8fa6bb7bf 100644 --- a/src/topology/dense_embedding.lean +++ b/src/topology/dense_embedding.lean @@ -43,7 +43,7 @@ lemma dense_range.closure_range (h : dense_range f) : closure (range f) = univ : eq_univ_iff_forall.mpr h lemma dense_range.nhds_within_ne_bot (h : dense_range f) (x : β) : - ne_bot (nhds_within x (range f)) := + ne_bot (𝓝[range f] x) := mem_closure_iff_cluster_pt.1 (h x) lemma dense_range.comp (hg : dense_range g) (hf : dense_range f) (cg : continuous g) : @@ -147,7 +147,7 @@ begin end protected lemma nhds_within_ne_bot (di : dense_inducing i) (b : β) : - ne_bot (nhds_within b (range i)) := + ne_bot (𝓝[range i] b) := di.dense.nhds_within_ne_bot b lemma comap_nhds_ne_bot (di : dense_inducing i) (b : β) : ne_bot (comap i (𝓝 b)) := diff --git a/src/topology/local_extr.lean b/src/topology/local_extr.lean index a42aa4eb345b8..54ce976ab71a4 100644 --- a/src/topology/local_extr.lean +++ b/src/topology/local_extr.lean @@ -43,13 +43,13 @@ section preorder variables [preorder β] [preorder γ] (f : α → β) (s : set α) (a : α) /-- `is_local_min_on f s a` means that `f a ≤ f x` for all `x ∈ s` in some neighborhood of `a`. -/ -def is_local_min_on := is_min_filter f (nhds_within a s) a +def is_local_min_on := is_min_filter f (𝓝[s] a) a /-- `is_local_max_on f s a` means that `f x ≤ f a` for all `x ∈ s` in some neighborhood of `a`. -/ -def is_local_max_on := is_max_filter f (nhds_within a s) a +def is_local_max_on := is_max_filter f (𝓝[s] a) a /-- `is_local_extr_on f s a` means `is_local_min_on f s a ∨ is_local_max_on f s a`. -/ -def is_local_extr_on := is_extr_filter f (nhds_within a s) a +def is_local_extr_on := is_extr_filter f (𝓝[s] a) a /-- `is_local_min f a` means that `f a ≤ f x` for all `x` in some neighborhood of `a`. -/ def is_local_min := is_min_filter f (𝓝 a) a @@ -430,35 +430,35 @@ section eventually variables [preorder β] {s : set α} -lemma filter.eventually_le.is_local_max_on {f g : α → β} {a : α} (hle : g ≤ᶠ[nhds_within a s] f) +lemma filter.eventually_le.is_local_max_on {f g : α → β} {a : α} (hle : g ≤ᶠ[𝓝[s] a] f) (hfga : f a = g a) (h : is_local_max_on f s a) : is_local_max_on g s a := hle.is_max_filter hfga h lemma is_local_max_on.congr {f g : α → β} {a : α} (h : is_local_max_on f s a) - (heq : f =ᶠ[nhds_within a s] g) (hmem : a ∈ s) : is_local_max_on g s a := + (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : is_local_max_on g s a := h.congr heq $ heq.eq_of_nhds_within hmem -lemma filter.eventually_eq.is_local_max_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[nhds_within a s] g) +lemma filter.eventually_eq.is_local_max_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : is_local_max_on f s a ↔ is_local_max_on g s a := heq.is_max_filter_iff $ heq.eq_of_nhds_within hmem -lemma filter.eventually_le.is_local_min_on {f g : α → β} {a : α} (hle : f ≤ᶠ[nhds_within a s] g) +lemma filter.eventually_le.is_local_min_on {f g : α → β} {a : α} (hle : f ≤ᶠ[𝓝[s] a] g) (hfga : f a = g a) (h : is_local_min_on f s a) : is_local_min_on g s a := hle.is_min_filter hfga h lemma is_local_min_on.congr {f g : α → β} {a : α} (h : is_local_min_on f s a) - (heq : f =ᶠ[nhds_within a s] g) (hmem : a ∈ s) : is_local_min_on g s a := + (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : is_local_min_on g s a := h.congr heq $ heq.eq_of_nhds_within hmem -lemma filter.eventually_eq.is_local_min_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[nhds_within a s] g) +lemma filter.eventually_eq.is_local_min_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : is_local_min_on f s a ↔ is_local_min_on g s a := heq.is_min_filter_iff $ heq.eq_of_nhds_within hmem lemma is_local_extr_on.congr {f g : α → β} {a : α} (h : is_local_extr_on f s a) - (heq : f =ᶠ[nhds_within a s] g) (hmem : a ∈ s) : is_local_extr_on g s a := + (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : is_local_extr_on g s a := h.congr heq $ heq.eq_of_nhds_within hmem -lemma filter.eventually_eq.is_local_extr_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[nhds_within a s] g) +lemma filter.eventually_eq.is_local_extr_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : is_local_extr_on f s a ↔ is_local_extr_on g s a := heq.is_extr_filter_iff $ heq.eq_of_nhds_within hmem diff --git a/src/topology/local_homeomorph.lean b/src/topology/local_homeomorph.lean index fe16a51b1c6fd..030a7ae950ef5 100644 --- a/src/topology/local_homeomorph.lean +++ b/src/topology/local_homeomorph.lean @@ -596,7 +596,7 @@ end homeomorphism if a neighborhood of the initial point is sent to the source of the local homeomorphism-/ lemma continuous_within_at_iff_continuous_within_at_comp_left - {f : γ → α} {s : set γ} {x : γ} (hx : f x ∈ e.source) (h : f ⁻¹' e.source ∈ nhds_within x s) : + {f : γ → α} {s : set γ} {x : γ} (hx : f x ∈ e.source) (h : f ⁻¹' e.source ∈ 𝓝[s] x) : continuous_within_at f s x ↔ continuous_within_at (e ∘ f) s x := begin rw [← continuous_within_at_inter' h, ← continuous_within_at_inter' h], @@ -619,7 +619,7 @@ lemma continuous_at_iff_continuous_at_comp_left continuous_at f x ↔ continuous_at (e ∘ f) x := begin have hx : f x ∈ e.source := (mem_of_nhds h : _), - have h' : f ⁻¹' e.source ∈ nhds_within x univ, by rwa nhds_within_univ, + have h' : f ⁻¹' e.source ∈ 𝓝[univ] x, by rwa nhds_within_univ, rw [← continuous_within_at_univ, ← continuous_within_at_univ, e.continuous_within_at_iff_continuous_within_at_comp_left hx h'] end diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean index 65becce68297d..d55d060f6acde 100644 --- a/src/topology/metric_space/basic.lean +++ b/src/topology/metric_space/basic.lean @@ -507,7 +507,7 @@ end lemma tendsto_locally_uniformly_on_iff {ι : Type*} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} : tendsto_locally_uniformly_on F f p s ↔ - ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhds_within x s, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε := + ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε := begin refine ⟨λ H ε hε, H _ (dist_mem_uniformity hε), λ H u hu x hx, _⟩, rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩, @@ -532,7 +532,8 @@ lemma tendsto_locally_uniformly_iff {ι : Type*} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} : tendsto_locally_uniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε := -by simp [← nhds_within_univ, ← tendsto_locally_uniformly_on_univ, tendsto_locally_uniformly_on_iff] +by simp only [← tendsto_locally_uniformly_on_univ, tendsto_locally_uniformly_on_iff, + nhds_within_univ, mem_univ, forall_const, exists_prop] /-- Expressing uniform convergence using `dist`. -/ @[nolint ge_or_gt] -- see Note [nolint_ge] @@ -578,25 +579,25 @@ theorem closed_ball_mem_nhds (x : α) {ε : ℝ} (ε0 : 0 < ε) : closed_ball x mem_sets_of_superset (ball_mem_nhds x ε0) ball_subset_closed_ball theorem nhds_within_basis_ball {s : set α} : - (nhds_within x s).has_basis (λ ε:ℝ, 0 < ε) (λ ε, ball x ε ∩ s) := + (𝓝[s] x).has_basis (λ ε:ℝ, 0 < ε) (λ ε, ball x ε ∩ s) := nhds_within_has_basis nhds_basis_ball s @[nolint ge_or_gt] -- see Note [nolint_ge] -theorem mem_nhds_within_iff {t : set α} : s ∈ nhds_within x t ↔ ∃ε>0, ball x ε ∩ t ⊆ s := +theorem mem_nhds_within_iff {t : set α} : s ∈ 𝓝[t] x ↔ ∃ε>0, ball x ε ∩ t ⊆ s := nhds_within_basis_ball.mem_iff @[nolint ge_or_gt] -- see Note [nolint_ge] theorem tendsto_nhds_within_nhds_within [metric_space β] {t : set β} {f : α → β} {a b} : - tendsto f (nhds_within a s) (nhds_within b t) ↔ + tendsto f (𝓝[s] a) (𝓝[t] b) ↔ ∀ ε > 0, ∃ δ > 0, ∀{x:α}, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε := (nhds_within_basis_ball.tendsto_iff nhds_within_basis_ball).trans $ by simp only [inter_comm, mem_inter_iff, and_imp, mem_ball] @[nolint ge_or_gt] -- see Note [nolint_ge] theorem tendsto_nhds_within_nhds [metric_space β] {f : α → β} {a b} : - tendsto f (nhds_within a s) (𝓝 b) ↔ + tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀{x:α}, x ∈ s → dist x a < δ → dist (f x) b < ε := -by { rw [← nhds_within_univ, tendsto_nhds_within_nhds_within], +by { rw [← nhds_within_univ b, tendsto_nhds_within_nhds_within], simp only [mem_univ, true_and] } @[nolint ge_or_gt] -- see Note [nolint_ge] @@ -643,13 +644,13 @@ by rw [continuous_at, tendsto_nhds] @[nolint ge_or_gt] -- see Note [nolint_ge] theorem continuous_within_at_iff' [topological_space β] {f : β → α} {b : β} {s : set β} : continuous_within_at f s b ↔ - ∀ ε > 0, ∀ᶠ x in nhds_within b s, dist (f x) (f b) < ε := + ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε := by rw [continuous_within_at, tendsto_nhds] @[nolint ge_or_gt] -- see Note [nolint_ge] theorem continuous_on_iff' [topological_space β] {f : β → α} {s : set β} : continuous_on f s ↔ - ∀ (b ∈ s) (ε > 0), ∀ᶠ x in nhds_within b s, dist (f x) (f b) < ε := + ∀ (b ∈ s) (ε > 0), ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε := by simp [continuous_on, continuous_within_at_iff'] @[nolint ge_or_gt] -- see Note [nolint_ge] diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean index 5c276c970edc7..ecb495a0ccb70 100644 --- a/src/topology/metric_space/emetric_space.lean +++ b/src/topology/metric_space/emetric_space.lean @@ -336,7 +336,7 @@ uniform_space.complete_of_cauchy_seq_tendsto uniformity_has_countable_basis lemma tendsto_locally_uniformly_on_iff {ι : Type*} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} : tendsto_locally_uniformly_on F f p s ↔ - ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhds_within x s, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε := + ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε := begin refine ⟨λ H ε hε, H _ (edist_mem_uniformity hε), λ H u hu x hx, _⟩, rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩, @@ -361,14 +361,15 @@ lemma tendsto_locally_uniformly_iff {ι : Type*} [topological_space β] {F : ι → β → α} {f : β → α} {p : filter ι} : tendsto_locally_uniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, edist (f y) (F n y) < ε := -by simp [← nhds_within_univ, ← tendsto_locally_uniformly_on_univ, tendsto_locally_uniformly_on_iff] +by simp only [← tendsto_locally_uniformly_on_univ, tendsto_locally_uniformly_on_iff, + mem_univ, forall_const, exists_prop, nhds_within_univ] /-- Expressing uniform convergence using `edist`. -/ @[nolint ge_or_gt] -- see Note [nolint_ge] lemma tendsto_uniformly_iff {ι : Type*} {F : ι → β → α} {f : β → α} {p : filter ι} : tendsto_uniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, edist (f x) (F n x) < ε := -by { rw [← tendsto_uniformly_on_univ, tendsto_uniformly_on_iff], simp } +by simp only [← tendsto_uniformly_on_univ, tendsto_uniformly_on_iff, mem_univ, forall_const] end emetric diff --git a/src/topology/separation.lean b/src/topology/separation.lean index 2f9b6ce82b0e6..0dd1fcd92f90d 100644 --- a/src/topology/separation.lean +++ b/src/topology/separation.lean @@ -200,12 +200,12 @@ Lim_eq (le_refl _) Lim_nhds a @[simp] lemma Lim_nhds_within {a : α} {s : set α} (h : a ∈ closure s) : - @Lim _ _ ⟨a⟩ (nhds_within a s) = a := -by haveI : ne_bot (nhds_within a s) := mem_closure_iff_cluster_pt.1 h; + @Lim _ _ ⟨a⟩ (𝓝[s] a) = a := +by haveI : ne_bot (𝓝[s] a) := mem_closure_iff_cluster_pt.1 h; exact Lim_eq inf_le_left @[simp] lemma lim_nhds_within_id {a : α} {s : set α} (h : a ∈ closure s) : - @lim _ _ _ ⟨a⟩ (nhds_within a s) id = a := + @lim _ _ _ ⟨a⟩ (𝓝[s] a) id = a := Lim_nhds_within h end lim @@ -375,13 +375,13 @@ set_option default_priority 100 -- see Note [default priority] omits T₂), is one in which for every closed `C` and `x ∉ C`, there exist disjoint open sets containing `x` and `C` respectively. -/ class regular_space (α : Type u) [topological_space α] extends t1_space α : Prop := -(regular : ∀{s:set α} {a}, is_closed s → a ∉ s → ∃t, is_open t ∧ s ⊆ t ∧ 𝓝 a ⊓ 𝓟 t = ⊥) +(regular : ∀{s:set α} {a}, is_closed s → a ∉ s → ∃t, is_open t ∧ s ⊆ t ∧ 𝓝[t] a = ⊥) end prio lemma nhds_is_closed [regular_space α] {a : α} {s : set α} (h : s ∈ 𝓝 a) : ∃t∈(𝓝 a), t ⊆ s ∧ is_closed t := let ⟨s', h₁, h₂, h₃⟩ := mem_nhds_sets_iff.mp h in -have ∃t, is_open t ∧ s'ᶜ ⊆ t ∧ 𝓝 a ⊓ 𝓟 t = ⊥, +have ∃t, is_open t ∧ s'ᶜ ⊆ t ∧ 𝓝[t] a = ⊥, from regular_space.regular (is_closed_compl_iff.mpr h₂) (not_not_intro h₃), let ⟨t, ht₁, ht₂, ht₃⟩ := this in ⟨tᶜ, @@ -400,7 +400,7 @@ instance subtype.regular_space [regular_space α] {p : α → Prop} : regular_sp rcases is_closed_induced_iff.1 hs with ⟨s, hs', rfl⟩, rcases regular_space.regular hs' ha with ⟨t, ht, hst, hat⟩, refine ⟨coe ⁻¹' t, is_open_induced ht, preimage_mono hst, _⟩, - rw [nhds_induced, ← comap_principal, ← comap_inf, hat, comap_bot] + rw [nhds_within, nhds_induced, ← comap_principal, ← comap_inf, ← nhds_within, hat, comap_bot] end⟩ variable (α) diff --git a/src/topology/subset_properties.lean b/src/topology/subset_properties.lean index d10c14827de1c..3067d541a41a5 100644 --- a/src/topology/subset_properties.lean +++ b/src/topology/subset_properties.lean @@ -55,7 +55,7 @@ end /-- The complement to a compact set belongs to a filter `f` if each `a ∈ s` has a neighborhood `t` within `s` such that `tᶜ` belongs to `f`. -/ lemma is_compact.compl_mem_sets_of_nhds_within (hs : is_compact s) {f : filter α} - (hf : ∀ a ∈ s, ∃ t ∈ nhds_within a s, tᶜ ∈ f) : + (hf : ∀ a ∈ s, ∃ t ∈ 𝓝[s] a, tᶜ ∈ f) : sᶜ ∈ f := begin refine hs.compl_mem_sets (λ a ha, _), @@ -71,7 +71,7 @@ end @[elab_as_eliminator] lemma is_compact.induction_on {s : set α} (hs : is_compact s) {p : set α → Prop} (he : p ∅) (hmono : ∀ ⦃s t⦄, s ⊆ t → p t → p s) (hunion : ∀ ⦃s t⦄, p s → p t → p (s ∪ t)) - (hnhds : ∀ x ∈ s, ∃ t ∈ nhds_within x s, p t) : + (hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t) : p s := let f : filter α := { sets := {t | p tᶜ}, @@ -115,11 +115,11 @@ classical.by_cases mem_sets_of_eq_bot $ let ⟨a, ha, (hfa : cluster_pt a $ f ⊓ 𝓟 tᶜ)⟩ := @@hs this $ inf_le_left_of_le hf₂ in have a ∈ t, from ht₂ a ha (hfa.of_inf_left), - have tᶜ ∩ t ∈ nhds_within a (tᶜ), + have tᶜ ∩ t ∈ 𝓝[tᶜ] a, from inter_mem_nhds_within _ (mem_nhds_sets ht₁ this), - have A : nhds_within a tᶜ = ⊥, + have A : 𝓝[tᶜ] a = ⊥, from empty_in_sets_eq_bot.1 $ compl_inter_self t ▸ this, - have nhds_within a tᶜ ≠ ⊥, + have 𝓝[tᶜ] a ≠ ⊥, from hfa.of_inf_right, absurd A this @@ -234,9 +234,9 @@ assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, cluster_pt from assume ⟨x, hxs, hx⟩, have ∅ ∈ 𝓝 x ⊓ f, by rw [empty_in_sets_eq_bot, hf x hxs], let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := by rw [mem_inf_sets] at this; exact this in - have ∅ ∈ 𝓝 x ⊓ 𝓟 t₂, - from (𝓝 x ⊓ 𝓟 t₂).sets_of_superset (inter_mem_inf_sets ht₁ (subset.refl t₂)) ht, - have 𝓝 x ⊓ 𝓟 t₂ = ⊥, + have ∅ ∈ 𝓝[t₂] x, + from (𝓝[t₂] x).sets_of_superset (inter_mem_inf_sets ht₁ (subset.refl t₂)) ht, + have 𝓝[t₂] x = ⊥, by rwa [empty_in_sets_eq_bot] at this, by simp only [closure_eq_cluster_pts] at hx; exact hx t₂ ht₂ this, let ⟨t, ht⟩ := h (λ i : f.sets, closure i.1) (λ i, is_closed_closure) @@ -534,15 +534,13 @@ variables {ι : Type*} {π : ι → Type*} [∀i, topological_space (π i)] lemma compact_pi_infinite {s : Πi:ι, set (π i)} : (∀i, is_compact (s i)) → is_compact {x : Πi:ι, π i | ∀i, x i ∈ s i} := begin - simp [compact_iff_ultrafilter_le_nhds, nhds_pi], - exact assume h f hf hfs, - let p : Πi:ι, filter (π i) := λi, map (λx:Πi:ι, π i, x i) f in - have ∀i:ι, ∃a, a∈s i ∧ p i ≤ 𝓝 a, - from assume i, h i (p i) (ultrafilter_map hf) $ - show (λx:Πi:ι, π i, x i) ⁻¹' s i ∈ f.sets, - from mem_sets_of_superset hfs $ assume x (hx : ∀i, x i ∈ s i), hx i, - let ⟨a, ha⟩ := classical.axiom_of_choice this in - ⟨a, assume i, (ha i).left, assume i, map_le_iff_le_comap.mp $ (ha i).right⟩ + simp only [compact_iff_ultrafilter_le_nhds, nhds_pi, exists_prop, mem_set_of_eq, le_infi_iff, le_principal_iff], + intros h f hf hfs, + have : ∀i:ι, ∃a, a∈s i ∧ tendsto (λx:Πi:ι, π i, x i) f (𝓝 a), + { refine λ i, h i _ (ultrafilter_map hf) (mem_map.2 _), + exact mem_sets_of_superset hfs (λ x hx, hx i) }, + choose a ha, + exact ⟨a, assume i, (ha i).left, assume i, (ha i).right.le_comap⟩ end /-- A version of Tychonoff's theorem that uses `set.pi`. -/ diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean index b1dd802279e90..01251d9cae05a 100644 --- a/src/topology/uniform_space/basic.lean +++ b/src/topology/uniform_space/basic.lean @@ -1412,19 +1412,19 @@ theorem continuous_at_iff'_left [topological_space β] {f : β → α} {b : β} by rw [continuous_at, tendsto_nhds_left] theorem continuous_within_at_iff'_right [topological_space β] {f : β → α} {b : β} {s : set β} : - continuous_within_at f s b ↔ tendsto (λ x, (f b, f x)) (nhds_within b s) (𝓤 α) := + continuous_within_at f s b ↔ tendsto (λ x, (f b, f x)) (𝓝[s] b) (𝓤 α) := by rw [continuous_within_at, tendsto_nhds_right] theorem continuous_within_at_iff'_left [topological_space β] {f : β → α} {b : β} {s : set β} : - continuous_within_at f s b ↔ tendsto (λ x, (f x, f b)) (nhds_within b s) (𝓤 α) := + continuous_within_at f s b ↔ tendsto (λ x, (f x, f b)) (𝓝[s] b) (𝓤 α) := by rw [continuous_within_at, tendsto_nhds_left] theorem continuous_on_iff'_right [topological_space β] {f : β → α} {s : set β} : - continuous_on f s ↔ ∀ b ∈ s, tendsto (λ x, (f b, f x)) (nhds_within b s) (𝓤 α) := + continuous_on f s ↔ ∀ b ∈ s, tendsto (λ x, (f b, f x)) (𝓝[s] b) (𝓤 α) := by simp [continuous_on, continuous_within_at_iff'_right] theorem continuous_on_iff'_left [topological_space β] {f : β → α} {s : set β} : - continuous_on f s ↔ ∀ b ∈ s, tendsto (λ x, (f x, f b)) (nhds_within b s) (𝓤 α) := + continuous_on f s ↔ ∀ b ∈ s, tendsto (λ x, (f x, f b)) (𝓝[s] b) (𝓤 α) := by simp [continuous_on, continuous_within_at_iff'_left] theorem continuous_iff'_right [topological_space β] {f : β → α} : diff --git a/src/topology/uniform_space/complete_separated.lean b/src/topology/uniform_space/complete_separated.lean index 13a3844519483..47c05bccd5af3 100644 --- a/src/topology/uniform_space/complete_separated.lean +++ b/src/topology/uniform_space/complete_separated.lean @@ -22,7 +22,7 @@ variables {α : Type*} lemma is_complete.is_closed [uniform_space α] [separated_space α] {s : set α} (h : is_complete s) : is_closed s := is_closed_iff_cluster_pt.2 $ λ a ha, begin - let f := 𝓝 a ⊓ 𝓟 s, + let f := 𝓝[s] a, have : cauchy f := cauchy_nhds.mono' ha inf_le_left, rcases h f this (inf_le_right) with ⟨y, ys, fy⟩, rwa (tendsto_nhds_unique' ha inf_le_left fy : a = y) diff --git a/src/topology/uniform_space/uniform_convergence.lean b/src/topology/uniform_space/uniform_convergence.lean index a6d5ffd0721cc..b6ff3e3d303a7 100644 --- a/src/topology/uniform_space/uniform_convergence.lean +++ b/src/topology/uniform_space/uniform_convergence.lean @@ -112,7 +112,7 @@ variable [topological_space α] `f` with respect to a filter `p` if, for any entourage of the diagonal `u`, for any `x ∈ s`, one has `p`-eventually `(f x, Fₙ x) ∈ u` for all `y` in a neighborhood of `x` in `s`. -/ def tendsto_locally_uniformly_on (F : ι → α → β) (f : α → β) (p : filter ι) (s : set α) := - ∀ u ∈ 𝓤 β, ∀ x ∈ s, ∃ t ∈ nhds_within x s, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u + ∀ u ∈ 𝓤 β, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u /-- A sequence of functions `Fₙ` converges locally uniformly to a limiting function `f` with respect to a filter `p` if, for any entourage of the diagonal `u`, for any `x`, one has `p`-eventually @@ -147,7 +147,7 @@ lemma tendsto_locally_uniformly_on.comp [topological_space γ] {t : set γ} begin assume u hu x hx, rcases h u hu (g x) (hg hx) with ⟨a, ha, H⟩, - have : g⁻¹' a ∈ nhds_within x t := + have : g⁻¹' a ∈ 𝓝[t] x := ((cg x hx).preimage_mem_nhds_within' (nhds_within_mono (g x) hg.image_subset ha)), exact ⟨g ⁻¹' a, this, H.mono (λ n hn y hy, hn _ hy)⟩ end @@ -173,7 +173,7 @@ a point, called `continuous_within_at_of_locally_uniform_approx_of_continuous_wi /-- A function which can be locally uniformly approximated by functions which are continuous within a set at a point is continuous within this set at this point. -/ lemma continuous_within_at_of_locally_uniform_approx_of_continuous_within_at - (hx : x ∈ s) (L : ∀ u ∈ 𝓤 β, ∃ t ∈ nhds_within x s, ∃ n, ∀ y ∈ t, (f y, F n y) ∈ u) + (hx : x ∈ s) (L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ n, ∀ y ∈ t, (f y, F n y) ∈ u) (C : ∀ n, continuous_within_at (F n) s x) : continuous_within_at f s x := begin apply uniform.continuous_within_at_iff'_left.2 (λ u₀ hu₀, _), @@ -182,10 +182,10 @@ begin obtain ⟨u₂, h₂, hsymm, u₂₁⟩ : ∃ (u : set (β × β)) (H : u ∈ 𝓤 β), (∀{a b}, (a, b) ∈ u → (b, a) ∈ u) ∧ comp_rel u u ⊆ u₁ := comp_symm_of_uniformity h₁, rcases L u₂ h₂ with ⟨t, tx, n, ht⟩, - have A : ∀ᶠ y in nhds_within x s, (f y, F n y) ∈ u₂ := eventually.mono tx ht, - have B : ∀ᶠ y in nhds_within x s, (F n y, F n x) ∈ u₂ := + have A : ∀ᶠ y in 𝓝[s] x, (f y, F n y) ∈ u₂ := eventually.mono tx ht, + have B : ∀ᶠ y in 𝓝[s] x, (F n y, F n x) ∈ u₂ := uniform.continuous_within_at_iff'_left.1 (C n) h₂, - have C : ∀ᶠ y in nhds_within x s, (f y, F n x) ∈ u₁ := + have C : ∀ᶠ y in 𝓝[s] x, (f y, F n x) ∈ u₁ := (A.and B).mono (λ y hy, u₂₁ (prod_mk_mem_comp_rel hy.1 hy.2)), have : (F n x, f x) ∈ u₁ := u₂₁ (prod_mk_mem_comp_rel (refl_mem_uniformity h₂) (hsymm (A.self_of_nhds_within hx))), @@ -206,7 +206,7 @@ end /-- A function which can be locally uniformly approximated by functions which are continuous on a set is continuous on this set. -/ lemma continuous_on_of_locally_uniform_approx_of_continuous_on - (L : ∀ (x ∈ s) (u ∈ 𝓤 β), ∃t ∈ nhds_within x s, ∃n, ∀ y ∈ t, (f y, F n y) ∈ u) + (L : ∀ (x ∈ s) (u ∈ 𝓤 β), ∃t ∈ 𝓝[s] x, ∃n, ∀ y ∈ t, (f y, F n y) ∈ u) (C : ∀ n, continuous_on (F n) s) : continuous_on f s := λ x hx, continuous_within_at_of_locally_uniform_approx_of_continuous_within_at hx (L x hx) (λ n, C n x hx) @@ -284,8 +284,8 @@ this paragraph, we prove variations around this statement. which is continuous at `x` within `s `, and `gₙ` tends to `x` within `s`, then `Fₙ (gₙ)` tends to `f x`. -/ lemma tendsto_comp_of_locally_uniform_limit_within - (h : continuous_within_at f s x) (hg : tendsto g p (nhds_within x s)) - (hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ nhds_within x s, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) : + (h : continuous_within_at f s x) (hg : tendsto g p (𝓝[s] x)) + (hunif : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u) : tendsto (λ n, F n (g n)) p (𝓝 (f x)) := begin apply uniform.tendsto_nhds_right.2 (λ u₀ hu₀, _), @@ -313,14 +313,14 @@ end /-- If `Fₙ` tends locally uniformly to `f` on a set `s`, and `gₙ` tends to `x` within `s`, then `Fₙ gₙ` tends to `f x` if `f` is continuous at `x` within `s` and `x ∈ s`. -/ lemma tendsto_locally_uniformly_on.tendsto_comp (h : tendsto_locally_uniformly_on F f p s) - (hf : continuous_within_at f s x) (hx : x ∈ s) (hg : tendsto g p (nhds_within x s)) : + (hf : continuous_within_at f s x) (hx : x ∈ s) (hg : tendsto g p (𝓝[s] x)) : tendsto (λ n, F n (g n)) p (𝓝 (f x)) := tendsto_comp_of_locally_uniform_limit_within hf hg (λ u hu, h u hu x hx) /-- If `Fₙ` tends uniformly to `f` on a set `s`, and `gₙ` tends to `x` within `s`, then `Fₙ gₙ` tends to `f x` if `f` is continuous at `x` within `s`. -/ lemma tendsto_uniformly_on.tendsto_comp (h : tendsto_uniformly_on F f p s) - (hf : continuous_within_at f s x) (hg : tendsto g p (nhds_within x s)) : + (hf : continuous_within_at f s x) (hg : tendsto g p (𝓝[s] x)) : tendsto (λ n, F n (g n)) p (𝓝 (f x)) := tendsto_comp_of_locally_uniform_limit_within hf hg (λ u hu, ⟨s, self_mem_nhds_within, h u hu⟩) diff --git a/src/topology/uniform_space/uniform_embedding.lean b/src/topology/uniform_space/uniform_embedding.lean index dbbf501d9f580..dba1c9ae0814c 100644 --- a/src/topology/uniform_space/uniform_embedding.lean +++ b/src/topology/uniform_space/uniform_embedding.lean @@ -246,14 +246,14 @@ have ne_bot (comap m g), from comap_ne_bot $ assume t ht, let ⟨t', ht', ht_mem⟩ := (mem_lift_sets $ monotone_lift' monotone_const mp₀).mp ht in let ⟨t'', ht'', ht'_sub⟩ := (mem_lift'_sets mp₁).mp ht_mem in let ⟨x, (hx : x ∈ t'')⟩ := hf.left.nonempty_of_mem ht'' in - have h₀ : ne_bot (nhds_within x (range m)), + have h₀ : ne_bot (𝓝[range m] x), from dense.nhds_within_ne_bot x, - have h₁ : {y | (x, y) ∈ t'} ∈ 𝓝 x ⊓ 𝓟 (range m), + have h₁ : {y | (x, y) ∈ t'} ∈ 𝓝[range m] x, from @mem_inf_sets_of_left α (𝓝 x) (𝓟 (range m)) _ $ mem_nhds_left x ht', - have h₂ : range m ∈ 𝓝 x ⊓ 𝓟 (range m), + have h₂ : range m ∈ 𝓝[range m] x, from @mem_inf_sets_of_right α (𝓝 x) (𝓟 (range m)) _ $ subset.refl _, - have {y | (x, y) ∈ t'} ∩ range m ∈ 𝓝 x ⊓ 𝓟 (range m), - from @inter_mem_sets α (𝓝 x ⊓ 𝓟 (range m)) _ _ h₁ h₂, + have {y | (x, y) ∈ t'} ∩ range m ∈ 𝓝[range m] x, + from @inter_mem_sets α (𝓝[range m] x) _ _ h₁ h₂, let ⟨y, xyt', b, b_eq⟩ := h₀.nonempty_of_mem this in ⟨b, b_eq.symm ▸ ht'_sub ⟨x, hx, xyt'⟩⟩,