From 6ffb158eed39c1d73ac233510abed69eb660897f Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Sun, 19 Apr 2026 16:25:31 -0700 Subject: [PATCH] =?UTF-8?q?Section=209.4:=20add=20=E2=89=A4-variant=20as?= =?UTF-8?q?=20a=20fourth=20item=20in=20ContinuousWithinAt.tfae?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tao's Proposition 9.4.7 (Exercise 9.4.1) states the ε-δ definition with both strict and non-strict inequalities. Add the non-strict variant as a fourth TFAE clause so the exercise matches the book. Co-Authored-By: Claude Opus 4.7 (1M context) --- Analysis/Section_9_4.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Analysis/Section_9_4.lean b/Analysis/Section_9_4.lean index 35affd11..962e6310 100644 --- a/Analysis/Section_9_4.lean +++ b/Analysis/Section_9_4.lean @@ -63,7 +63,8 @@ theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x [ ContinuousWithinAt f X x₀, ∀ a:ℕ → ℝ, (∀ n, a n ∈ X) → Filter.atTop.Tendsto a (nhds x₀) → Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (f x₀)), - ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x-x₀| < δ → |f x - f x₀| < ε + ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x-x₀| < δ → |f x - f x₀| < ε, + ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x-x₀| ≤ δ → |f x - f x₀| ≤ ε ].TFAE := by sorry