From 0278ff4fa881a03754a78b42cd3d0a552345844b Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Sun, 8 Feb 2026 07:32:46 -0800 Subject: [PATCH] Fix lim_of_between statement (squeeze test) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The squeeze test concludes that b converges, given a ≤ b ≤ c and both a,c converge to L. The conclusion and hypothesis for c were swapped. Co-Authored-By: Claude Opus 4.6 --- analysis/Analysis/Section_6_4.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/analysis/Analysis/Section_6_4.lean b/analysis/Analysis/Section_6_4.lean index 89a65373..360cdfc9 100644 --- a/analysis/Analysis/Section_6_4.lean +++ b/analysis/Analysis/Section_6_4.lean @@ -213,8 +213,8 @@ theorem Sequence.liminf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m, /-- Corollary 6.4.14 (Squeeze test) / Exercise 6.4.5 -/ theorem Sequence.lim_of_between {a b c:Sequence} {L:ℝ} (hm: b.m = a.m ∧ c.m = a.m) - (hab: ∀ n ≥ a.m, a n ≤ b n ∧ b n ≤ c n) (ha: a.TendsTo L) (hb: b.TendsTo L) : - c.TendsTo L := by sorry + (hab: ∀ n ≥ a.m, a n ≤ b n ∧ b n ≤ c n) (ha: a.TendsTo L) (hb: c.TendsTo L) : + b.TendsTo L := by sorry /-- Example 6.4.15 -/ example : ((fun (n:ℕ) ↦ 2/(n+1:ℝ)):Sequence).TendsTo 0 := by