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ε