def C03S06.ConvergesTo (s : ℕ → ℝ) (a : ℝ) : Prop

Equations

• C03S06.ConvergesTo s a = ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |s n - a| < ε

theorem C03S06.convergesTo_const (a : ℝ) : C03S06.ConvergesTo (fun (x : ℕ) => a) a

theorem C03S06.convergesTo_add {s : ℕ → ℝ} {t : ℕ → ℝ} {a : ℝ} {b : ℝ} (cs : C03S06.ConvergesTo s a) (ct : C03S06.ConvergesTo t b) : C03S06.ConvergesTo (fun (n : ℕ) => s n + t n) (a + b)

theorem C03S06.convergesTo_mul_const {s : ℕ → ℝ} {a : ℝ} (c : ℝ) (cs : C03S06.ConvergesTo s a) : C03S06.ConvergesTo (fun (n : ℕ) => c * s n) (c * a)

theorem C03S06.exists_abs_le_of_convergesTo {s : ℕ → ℝ} {a : ℝ} (cs : C03S06.ConvergesTo s a) : ∃ (N : ℕ) (b : ℝ), ∀ (n : ℕ), N ≤ n → |s n| < b

theorem C03S06.aux {s : ℕ → ℝ} {t : ℕ → ℝ} {a : ℝ} (cs : C03S06.ConvergesTo s a) (ct : C03S06.ConvergesTo t 0) : C03S06.ConvergesTo (fun (n : ℕ) => s n * t n) 0

theorem C03S06.convergesTo_mul {s : ℕ → ℝ} {t : ℕ → ℝ} {a : ℝ} {b : ℝ} (cs : C03S06.ConvergesTo s a) (ct : C03S06.ConvergesTo t b) : C03S06.ConvergesTo (fun (n : ℕ) => s n * t n) (a * b)

theorem C03S06.convergesTo_unique {s : ℕ → ℝ} {a : ℝ} {b : ℝ} (sa : C03S06.ConvergesTo s a) (sb : C03S06.ConvergesTo s b) : a = b

def C03S06.ConvergesTo' {α : Type u_1} [LinearOrder α] (s : α → ℝ) (a : ℝ) : Prop

Equations

• C03S06.ConvergesTo' s a = ∀ ε > 0, ∃ (N : α), ∀ n ≥ N, |s n - a| < ε