[Merged by Bors] - feat(analysis/special_functions/non_integrable): examples of non-integrable functions

src/analysis/calculus/fderiv_measurable.lean

@@ -70,7 +70,7 @@ derivative, measurable function, Borel σ-algebra
 noncomputable theory
 
 open set metric asymptotics filter continuous_linear_map
-open topological_space (second_countable_topology)
+open topological_space (second_countable_topology) measure_theory
 open_locale topological_space
 
 namespace continuous_linear_map
@@ -409,3 +409,7 @@ variable {𝕜}
 lemma measurable_deriv [measurable_space 𝕜] [opens_measurable_space 𝕜] [measurable_space F]
   [borel_space F] (f : 𝕜 → F) : measurable (deriv f) :=
 by simpa only [fderiv_deriv] using measurable_fderiv_apply_const 𝕜 f 1
+
+lemma ae_measurable_deriv [measurable_space 𝕜] [opens_measurable_space 𝕜] [measurable_space F]
+  [borel_space F] (f : 𝕜 → F) (μ : measure 𝕜) : ae_measurable (deriv f) μ :=
+(measurable_deriv f).ae_measurable

src/analysis/special_functions/non_integrable.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import analysis.special_functions.integrals
+import analysis.calculus.fderiv_measurable
+
+/-!
+# Non integrable functions
+
+In this file we prove that the derivative of a function that tends to infinity is not interval
+integrable, see `interval_integral.not_integrable_has_deriv_at_of_tendsto_norm_at_top_filter` and
+`interval_integral.not_integrable_has_deriv_at_of_tendsto_norm_at_top_punctured`.  Then we apply the
+latter lemma to prove that the function `λ x, x⁻¹` is integrable on `a..b` if and only if `a = b` or
+`0 ∉ [a, b]`.
+
+## Main results
+
+* `not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured`: if `f` tends to infinity
+  along `𝓝[≠] c` and `f' = O(g)` along the same filter, then `g` is not interval integrable on any
+  nontrivial integral `a..b`, `c ∈ [a, b]`.
+
+* `not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_filter`: a version of
+  `not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured` that works for one-sided
+  neighborhoods;
+
+* `not_interval_integrable_of_sub_inv_is_O_punctured`: if `1 / (x - c) = O(f)` as `x → c`, `x ≠ c`,
+  then `f` is not interval integrable on any nontrivial interval `a..b`, `c ∈ [a, b]`;
+
+* `interval_integrable_sub_inv_iff`, `interval_integrable_inv_iff`: integrability conditions for
+  `(x - c)⁻¹` and `x⁻¹`.
+
+## Tags
+
+integrable function
+-/
+
+open_locale measure_theory topological_space interval nnreal ennreal
+open measure_theory topological_space set filter asymptotics interval_integral
+
+variables {E F : Type*} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [second_countable_topology E] [complete_space E] [normed_group F]
+  [measurable_space F] [borel_space F]
+
+/-- If `f` is eventually differentiable along a nontrivial filter `l : filter ℝ` that is generated
+by convex sets, the norm of `f` tends to infinity along `l`, and `f' = O(g)` along `l`, where `f'`
+is the derivative of `f`, then `g` is not integrable on any interval `a..b` such that
+`[a, b] ∈ l`. -/
+lemma not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_filter {f : ℝ → E} {g : ℝ → F}
+  {a b : ℝ} (l : filter ℝ) [ne_bot l] [tendsto_Ixx_class Icc l l] (hl : [a, b] ∈ l)
+  (hd : ∀ᶠ x in l, differentiable_at ℝ f x) (hf : tendsto (λ x, ∥f x∥) l at_top)
+  (hfg : is_O (deriv f) g l) :
+  ¬interval_integrable g volume a b :=
+begin
+  intro hgi,
+  obtain ⟨C, hC₀, s, hsl, hsub, hfd, hg⟩ : ∃ (C : ℝ) (hC₀ : 0 ≤ C) (s ∈ l),
+    (∀ (x ∈ s) (y ∈ s), [x, y] ⊆ [a, b]) ∧
+    (∀ (x ∈ s) (y ∈ s) (z ∈ [x, y]), differentiable_at ℝ f z) ∧
+    (∀ (x ∈ s) (y ∈ s) (z ∈ [x, y]), ∥deriv f z∥ ≤ C * ∥g z∥),
+  { rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩,
+    have h : ∀ᶠ x : ℝ × ℝ in l.prod l, ∀ y ∈ [x.1, x.2], (differentiable_at ℝ f y ∧
+      ∥deriv f y∥ ≤ C * ∥g y∥) ∧ y ∈ [a, b],
+      from (tendsto_fst.interval tendsto_snd).eventually ((hd.and hC.bound).and hl).lift'_powerset,
+    rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩,
+    simp only [prod_subset_iff, mem_set_of_eq] at hs,
+    exact ⟨C, C₀, s, hsl, λ x hx y hy z hz, (hs x hx y hy z hz).2,
+      λ x hx y hy z hz, (hs x hx y hy z hz).1.1, λ x hx y hy z hz, (hs x hx y hy z hz).1.2⟩ },
+  replace hgi : interval_integrable (λ x, C * ∥g x∥) volume a b, by convert hgi.norm.smul C,
+  obtain ⟨c, hc, d, hd, hlt⟩ : ∃ (c ∈ s) (d ∈ s), ∥f c∥ + ∫ y in Ι a b, C * ∥g y∥ < ∥f d∥,
+  { rcases filter.nonempty_of_mem hsl with ⟨c, hc⟩,
+    have : ∀ᶠ x in l, ∥f c∥ + ∫ y in Ι a b, C * ∥g y∥ < ∥f x∥,
+      from hf.eventually (eventually_gt_at_top _),
+    exact ⟨c, hc, (this.and hsl).exists.imp (λ d hd, ⟨hd.2, hd.1⟩)⟩ },
+  specialize hsub c hc d hd, specialize hfd c hc d hd,
+  replace hg : ∀ x ∈ Ι c d, ∥deriv f x∥ ≤ C * ∥g x∥, from λ z hz, hg c hc d hd z ⟨hz.1.le, hz.2⟩,
+  have hg_ae : ∀ᵐ x ∂(volume.restrict (Ι c d)), ∥deriv f x∥ ≤ C * ∥g x∥,
+    from (ae_restrict_mem measurable_set_interval_oc).mono hg,
+  have hsub' : Ι c d ⊆ Ι a b,
+    from interval_oc_subset_interval_oc_of_interval_subset_interval hsub,
+  have hfi : interval_integrable (deriv f) volume c d,
+    from (hgi.mono_set hsub).mono_fun' (ae_measurable_deriv _ _) hg_ae,
+  refine hlt.not_le (sub_le_iff_le_add'.1 _),
+  calc ∥f d∥ - ∥f c∥ ≤ ∥f d - f c∥ : norm_sub_norm_le _ _
+  ... = ∥∫ x in c..d, deriv f x∥ : congr_arg _ (integral_deriv_eq_sub hfd hfi).symm
+  ... = ∥∫ x in Ι c d, deriv f x∥ : norm_integral_eq_norm_integral_Ioc _
+  ... ≤ ∫ x in Ι c d, ∥deriv f x∥ : norm_integral_le_integral_norm _
+  ... ≤ ∫ x in Ι c d, C * ∥g x∥ :
+    set_integral_mono_on hfi.norm.def (hgi.def.mono_set hsub') measurable_set_interval_oc hg
+  ... ≤ ∫ x in Ι a b, C * ∥g x∥ :
+    set_integral_mono_set hgi.def (ae_of_all _ $ λ x, mul_nonneg hC₀ (norm_nonneg _))
+      hsub'.eventually_le
+end
+
+/-- If `a ≠ b`, `c ∈ [a, b]`, `f` is differentiable in the neighborhood of `c` within
+`[a, b] \ {c}`, `∥f x∥ → ∞` as `x → c` within `[a, b] \ {c}`, and `f' = O(g)` along
+`𝓝[[a, b] \ {c}] c`, where `f'` is the derivative of `f`, then `g` is not interval integrable on
+`a..b`. -/
+lemma not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_within_diff_singleton
+  {f : ℝ → E} {g : ℝ → F} {a b c : ℝ} (hne : a ≠ b) (hc : c ∈ [a, b])
+  (h_deriv : ∀ᶠ x in 𝓝[[a, b] \ {c}] c, differentiable_at ℝ f x)
+  (h_infty : tendsto (λ x, ∥f x∥) (𝓝[[a, b] \ {c}] c) at_top)
+  (hg : is_O (deriv f) g (𝓝[[a, b] \ {c}] c)) :
+  ¬interval_integrable g volume a b :=
+begin
+  obtain ⟨l, hl, hl', hle, hmem⟩ : ∃ l : filter ℝ, tendsto_Ixx_class Icc l l ∧ l.ne_bot ∧
+    l ≤ 𝓝 c ∧ [a, b] \ {c} ∈ l,
+  { cases (min_lt_max.2 hne).lt_or_lt c with hlt hlt,
+    { refine ⟨𝓝[<] c, infer_instance, infer_instance, inf_le_left, _⟩,
+      rw ← Iic_diff_right,
+      exact diff_mem_nhds_within_diff (Icc_mem_nhds_within_Iic ⟨hlt, hc.2⟩) _ },
+    { refine ⟨𝓝[>] c, infer_instance, infer_instance, inf_le_left, _⟩,
+      rw ← Ici_diff_left,
+      exact diff_mem_nhds_within_diff (Icc_mem_nhds_within_Ici ⟨hc.1, hlt⟩) _ } },
+  resetI,
+  have : l ≤ 𝓝[[a, b] \ {c}] c, from le_inf hle (le_principal_iff.2 hmem),
+  exact not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_filter l
+    (mem_of_superset hmem (diff_subset _ _))
+    (h_deriv.filter_mono this) (h_infty.mono_left this) (hg.mono this),
+end
+
+/-- If `f` is differentiable in a punctured neighborhood of `c`, `∥f x∥ → ∞` as `x → c` (more
+formally, along the filter `𝓝[≠] c`), and `f' = O(g)` along `𝓝[≠] c`, where `f'` is the derivative
+of `f`, then `g` is not interval integrable on any nontrivial interval `a..b` such that
+`c ∈ [a, b]`. -/
+lemma not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured {f : ℝ → E} {g : ℝ → F}
+  {a b c : ℝ} (h_deriv : ∀ᶠ x in 𝓝[≠] c, differentiable_at ℝ f x)
+  (h_infty : tendsto (λ x, ∥f x∥) (𝓝[≠] c) at_top) (hg : is_O (deriv f) g (𝓝[≠] c))
+  (hne : a ≠ b) (hc : c ∈ [a, b]) :
+  ¬interval_integrable g volume a b :=
+have 𝓝[[a, b] \ {c}] c ≤ 𝓝[≠] c, from nhds_within_mono _ (inter_subset_right _ _),
+not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_within_diff_singleton hne hc
+  (h_deriv.filter_mono this) (h_infty.mono_left this) (hg.mono this)
+
+/-- If `f` grows in the punctured neighborhood of `c : ℝ` at least as fast as `1 / (x - c)`,
+then it is not interval integrable on any nontrivial interval `a..b`, `c ∈ [a, b]`. -/
+lemma not_interval_integrable_of_sub_inv_is_O_punctured {f : ℝ → F} {a b c : ℝ}
+  (hf : is_O (λ x, (x - c)⁻¹) f (𝓝[≠] c)) (hne : a ≠ b) (hc : c ∈ [a, b]) :
+  ¬interval_integrable f volume a b :=
+begin
+  have A : ∀ᶠ x in 𝓝[≠] c, has_deriv_at (λ x, real.log (x - c)) (x - c)⁻¹ x,
+  { filter_upwards [self_mem_nhds_within],
+    intros x hx,
+    simpa using ((has_deriv_at_id x).sub_const c).log (sub_ne_zero.2 hx) },
+  have B : tendsto (λ x, ∥real.log (x - c)∥) (𝓝[≠] c) at_top,
+  { refine tendsto_abs_at_bot_at_top.comp (real.tendsto_log_nhds_within_zero.comp _),
+    rw ← sub_self c,
+    exact ((has_deriv_at_id c).sub_const c).tendsto_punctured_nhds one_ne_zero },
+  exact not_interval_integrable_of_tendsto_norm_at_top_of_deriv_is_O_punctured
+    (A.mono (λ x hx, hx.differentiable_at)) B
+    (hf.congr' (A.mono $ λ x hx, hx.deriv.symm) eventually_eq.rfl) hne hc
+end
+
+/-- The function `λ x, (x - c)⁻¹` is integrable on `a..b` if and only if `a = b` or `c ∉ [a, b]`. -/
+@[simp] lemma interval_integrable_sub_inv_iff {a b c : ℝ} :
+  interval_integrable (λ x, (x - c)⁻¹) volume a b ↔ a = b ∨ c ∉ [a, b] :=
+begin
+  split,
+  { refine λ h, or_iff_not_imp_left.2 (λ hne hc, _),
+    exact not_interval_integrable_of_sub_inv_is_O_punctured (is_O_refl _ _) hne hc h },
+  { rintro (rfl|h₀),
+    exacts [interval_integrable.refl,
+      interval_integrable_inv (λ x hx, sub_ne_zero.2 $ ne_of_mem_of_not_mem hx h₀)
+        (continuous_on_id.sub continuous_on_const)] }
+end
+
+/-- The function `λ x, x⁻¹` is integrable on `a..b` if and only if `a = b` or `0 ∉ [a, b]`. -/
+@[simp] lemma interval_integrable_inv_iff {a b : ℝ} :
+  interval_integrable (λ x, x⁻¹) volume a b ↔ a = b ∨ (0 : ℝ) ∉ [a, b] :=
+by simp only [← interval_integrable_sub_inv_iff, sub_zero]

src/data/set/intervals/unordered_interval.lean

@@ -46,7 +46,7 @@ by rw [interval, min_eq_left h, max_eq_right h]
 by { rw [interval, min_eq_right h, max_eq_left h] }
 
 lemma interval_swap (a b : α) : [a, b] = [b, a] :=
-or.elim (le_total a b) (by simp {contextual := tt}) (by simp {contextual := tt})
+by rw [interval, interval, min_comm, max_comm]
 
 lemma interval_of_lt (h : a < b) : [a, b] = Icc a b :=
 interval_of_le (le_of_lt h)
@@ -149,6 +149,13 @@ lemma forall_interval_oc_iff  {P : α → Prop} :
   (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ (∀ x ∈ Ioc b a, P x) :=
 by { dsimp [interval_oc], cases le_total a b with hab hab ; simp [hab] }
 
+lemma interval_oc_subset_interval_oc_of_interval_subset_interval {a b c d : α}
+  (h : [a, b] ⊆ [c, d]) : Ι a b ⊆ Ι c d :=
+Ioc_subset_Ioc (interval_subset_interval_iff_le.1 h).1 (interval_subset_interval_iff_le.1 h).2
+
+lemma interval_oc_swap (a b : α) : Ι a b = Ι b a :=
+by simp only [interval_oc, min_comm a b, max_comm a b]
+
 end linear_order
 
 open_locale interval

src/measure_theory/integral/interval_integral.lean

@@ -307,6 +307,16 @@ lemma mono_set_ae
   interval_integrable f μ c d :=
 interval_integrable_iff.mpr $ hf.def.mono_set_ae h
 
+lemma mono_fun {F : Type*} [normed_group F] [measurable_space F] {g : α → F}
+  (hf : interval_integrable f μ a b) (hgm : ae_measurable g (μ.restrict (Ι a b)))
+  (hle : (λ x, ∥g x∥) ≤ᵐ[μ.restrict (Ι a b)] (λ x, ∥f x∥)) : interval_integrable g μ a b :=
+interval_integrable_iff.2 $ hf.def.integrable.mono hgm hle
+
+lemma mono_fun' {g : α → ℝ} (hg : interval_integrable g μ a b)
+  (hfm : ae_measurable f (μ.restrict (Ι a b)))
+  (hle : (λ x, ∥f x∥) ≤ᵐ[μ.restrict (Ι a b)] g) : interval_integrable f μ a b :=
+interval_integrable_iff.2 $ hg.def.integrable.mono' hfm hle
+
 protected lemma ae_measurable (h : interval_integrable f μ a b) :
   ae_measurable f (μ.restrict (Ioc a b)):=
 h.1.ae_measurable
@@ -504,14 +514,22 @@ lemma integral_non_ae_measurable_of_le (h : a ≤ b)
   ∫ x in a..b, f x ∂μ = 0 :=
 integral_non_ae_measurable $ by rwa [interval_oc_of_le h]
 
-lemma norm_integral_eq_norm_integral_Ioc :
+lemma norm_integral_min_max (f : α → E) :
+  ∥∫ x in min a b..max a b, f x ∂μ∥ = ∥∫ x in a..b, f x ∂μ∥ :=
+by cases le_total a b; simp [*, integral_symm a b]
+
+lemma norm_integral_eq_norm_integral_Ioc (f : α → E) :
   ∥∫ x in a..b, f x ∂μ∥ = ∥∫ x in Ι a b, f x ∂μ∥ :=
-(integral_cases f a b).elim (congr_arg _) (λ h, (congr_arg _ h).trans (norm_neg _))
+by rw [← norm_integral_min_max, integral_of_le min_le_max, interval_oc]
+
+lemma abs_integral_eq_abs_integral_interval_oc (f : α → ℝ) :
+  |∫ x in a..b, f x ∂μ| = |∫ x in Ι a b, f x ∂μ| :=
+norm_integral_eq_norm_integral_Ioc f
 
 lemma norm_integral_le_integral_norm_Ioc :
   ∥∫ x in a..b, f x ∂μ∥ ≤ ∫ x in Ι a b, ∥f x∥ ∂μ :=
 calc ∥∫ x in a..b, f x ∂μ∥ = ∥∫ x in Ι a b, f x ∂μ∥ :
-  norm_integral_eq_norm_integral_Ioc
+  norm_integral_eq_norm_integral_Ioc f
 ... ≤ ∫ x in Ι a b, ∥f x∥ ∂μ :
   norm_integral_le_integral_norm f
 
@@ -1229,6 +1247,16 @@ begin
   exact set_integral_mono_set hfi.1 hf (Ioc_subset_Ioc hca hbd).eventually_le
 end
 
+lemma abs_integral_mono_interval {c d } (h : Ι a b ⊆ Ι c d)
+  (hf : 0 ≤ᵐ[μ.restrict (Ι c d)] f) (hfi : interval_integrable f μ c d) :
+  |∫ x in a..b, f x ∂μ| ≤ |∫ x in c..d, f x ∂μ| :=
+have hf' : 0 ≤ᵐ[μ.restrict (Ι a b)] f, from ae_mono (measure.restrict_mono h le_rfl) hf,
+calc |∫ x in a..b, f x ∂μ| = |∫ x in Ι a b, f x ∂μ| : abs_integral_eq_abs_integral_interval_oc f
+... = ∫ x in Ι a b, f x ∂μ : abs_of_nonneg (measure_theory.integral_nonneg_of_ae hf')
+... ≤ ∫ x in Ι c d, f x ∂μ : set_integral_mono_set hfi.def hf h.eventually_le
+... ≤ |∫ x in Ι c d, f x ∂μ| : le_abs_self _
+... = |∫ x in c..d, f x ∂μ| : (abs_integral_eq_abs_integral_interval_oc f).symm
+
 end mono
 
 end

src/order/filter/basic.lean

@@ -838,12 +838,7 @@ by rwa [inf_principal_eq_bot, compl_compl] at h
 
 lemma diff_mem_inf_principal_compl {f : filter α} {s : set α} (hs : s ∈ f) (t : set α) :
   s \ t ∈ f ⊓ 𝓟 tᶜ :=
-begin
-  rw mem_inf_principal,
-  filter_upwards [hs],
-  intros a has hat,
-  exact ⟨has, hat⟩
-end
+inter_mem_inf hs $ mem_principal_self tᶜ
 
 lemma principal_le_iff {s : set α} {f : filter α} :
   𝓟 s ≤ f ↔ ∀ V ∈ f, s ⊆ V :=

src/order/filter/interval.lean

@@ -174,7 +174,7 @@ tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Ioc_self)
 instance tendsto_Ioo_Iio_Iio {a : α} : tendsto_Ixx_class Ioo (𝓟 (Iio a)) (𝓟 (Iio a)) :=
 tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Ioc_self)
 
-instance tendsto_Icc_Icc_icc {a b : α} :
+instance tendsto_Icc_Icc_Icc {a b : α} :
   tendsto_Ixx_class Icc (𝓟 (Icc a b)) (𝓟 (Icc a b)) :=
 tendsto_Ixx_class_principal.mpr $ λ x hx y hy, Icc_subset_Icc hx.1 hy.2
 
@@ -206,10 +206,27 @@ section linear_order
 variables [linear_order α]
 
 instance tendsto_Icc_interval_interval {a b : α} : tendsto_Ixx_class Icc (𝓟 [a, b]) (𝓟 [a, b]) :=
-filter.tendsto_Icc_Icc_icc
+filter.tendsto_Icc_Icc_Icc
 
 instance tendsto_Ioc_interval_interval {a b : α} : tendsto_Ixx_class Ioc (𝓟 [a, b]) (𝓟 [a, b]) :=
-tendsto_Ixx_class_of_subset $ λ _ _, Ioc_subset_Icc_self
+filter.tendsto_Ioc_Icc_Icc
+
+instance tendsto_interval_of_Icc {l : filter α} [tendsto_Ixx_class Icc l l] :
+  tendsto_Ixx_class interval l l :=
+begin
+  refine ⟨λ s hs, mem_map.2 $ mem_prod_self_iff.2 _⟩,
+  obtain ⟨t, htl, hts⟩ : ∃ t ∈ l, ∀ p ∈ (t : set α).prod t, Icc (p : α × α).1 p.2 ∈ s,
+    from mem_prod_self_iff.1 (mem_map.1 (tendsto_fst.Icc tendsto_snd hs)),
+  refine ⟨t, htl, λ p hp, _⟩,
+  cases le_total p.1 p.2,
+  { rw [mem_preimage, interval_of_le h], exact hts p hp },
+  { rw [mem_preimage, interval_of_ge h], exact hts ⟨p.2, p.1⟩ ⟨hp.2, hp.1⟩ }
+end
+
+lemma tendsto.interval {l : filter α} [tendsto_Ixx_class Icc l l] {f g : β → α} {lb : filter β}
+  (hf : tendsto f lb l) (hg : tendsto g lb l) :
+  tendsto (λ x, [f x, g x]) lb (l.lift' powerset) :=
+tendsto_Ixx_class.tendsto_Ixx.comp $ hf.prod_mk hg
 
 end linear_order
 

src/topology/continuous_on.lean

@@ -76,10 +76,17 @@ lemma mem_nhds_within_iff_exists_mem_nhds_inter {t : set α} {a : α} {s : set 
   t ∈ 𝓝[s] a ↔ ∃ u ∈ 𝓝 a, u ∩ s ⊆ t :=
 (nhds_within_has_basis (𝓝 a).basis_sets s).mem_iff
 
-lemma diff_mem_nhds_within_compl {X : Type*} [topological_space X] {x : X} {s : set X}
-  (hs : s ∈ 𝓝 x) (t : set X) : s \ t ∈ 𝓝[tᶜ] x :=
+lemma diff_mem_nhds_within_compl {x : α} {s : set α} (hs : s ∈ 𝓝 x) (t : set α) :
+  s \ t ∈ 𝓝[tᶜ] x :=
 diff_mem_inf_principal_compl hs t
 
+lemma diff_mem_nhds_within_diff {x : α} {s t : set α} (hs : s ∈ 𝓝[t] x) (t' : set α) :
+  s \ t' ∈ 𝓝[t \ t'] x :=
+begin
+  rw [nhds_within, diff_eq, diff_eq, ← inf_principal, ← inf_assoc],
+  exact inter_mem_inf hs (mem_principal_self _)
+end
+
 lemma nhds_of_nhds_within_of_nhds
   {s t : set α} {a : α} (h1 : s ∈ 𝓝 a) (h2 : t ∈ 𝓝[s] a) : (t ∈ 𝓝 a) :=
 begin