From 3456e167d39ef1ebde16db53ca014ee4c06e0bdc Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 28 Nov 2025 15:41:39 +0100
Subject: [PATCH] Update Basic.lean

---
 Aristotle/Basic.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Aristotle/Basic.lean b/Aristotle/Basic.lean
index 13bd18f..592f7e3 100644
--- a/Aristotle/Basic.lean
+++ b/Aristotle/Basic.lean
@@ -5,6 +5,24 @@ import Mathlib.Analysis.Calculus.Deriv.Shift
 
 open MeromorphicOn Metric Real Set Classical
 
+theorem eventually_eventually_nhdsWithin₁
+    {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} [IsClosed s] :
+    (∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhds y, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x := by
+  nth_rw 2 [← eventually_eventually_nhdsWithin]
+  constructor
+  · intro h
+    filter_upwards [h] with y hy
+    exact eventually_nhdsWithin_of_eventually_nhds hy
+  · intro h
+    filter_upwards [h] with y hy
+    have : y ∉ s := by sorry
+    rw [eventually_nhdsWithin_iff] at hy
+    rw [Filter.Eventually] at *
+    apply Filter.mem_of_superset hy
+    intro x hx
+    simp_all
+    sorry
+
 variable
   {𝕜 : Type*} [NontriviallyNormedField 𝕜]
   {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]