intro ε εpos
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => s n + t n) (a + b)
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n + t n) n - (a + b)| < ε