From 340783cf05be24413d0aa840d4921224fc438924 Mon Sep 17 00:00:00 2001 From: Roger-Zhou0 Date: Thu, 16 Oct 2025 23:26:12 -0400 Subject: [PATCH] Refactor SqueezeThm statement to include N parameter --- Game/Levels/L6Levels/L06_Squeeze.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Game/Levels/L6Levels/L06_Squeeze.lean b/Game/Levels/L6Levels/L06_Squeeze.lean index ca2b703..b8291a4 100644 --- a/Game/Levels/L6Levels/L06_Squeeze.lean +++ b/Game/Levels/L6Levels/L06_Squeeze.lean @@ -27,8 +27,8 @@ TheoremDoc SqueezeThm as "SqueezeThm" in "Theorems" /-- Prove this -/ -Statement SqueezeThm (a b c : ℕ → ℝ) (L : ℝ) (aToL : SeqLim a L) -(cToL : SeqLim c L) (aLeb : ∀ n, a n ≤ b n) (bLec : ∀ n, b n ≤ c n) : +Statement SqueezeThm (a b c N : ℕ → ℝ) (L : ℝ) (aToL : SeqLim a L) +(cToL : SeqLim c L) (aLeb : ∀ n ≥ N, a n ≤ b n) (bLec : ∀ n ≥ N, b n ≤ c n) : SeqLim b L := by intro ε hε specialize aToL ε hε