Combination_Theorem_for_Sequences_Real
Provedanalysislimitsproofwikisequences
Let and be sequences in . Let and be convergent to the following limits Let . Then the following results hold === Sum Rule === === Difference Rule === === Multiple Rule === === Combined Sum Rule === === Product Rule === === Quotient Rule ===
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Combination_Theorem_for_Sequences_Real {x y : ℕ → ℝ} {a b : ℝ} (hx : Filter.Tendsto x Filter.atTop (nhds a)) (hy : Filter.Tendsto y Filter.atTop (nhds b)) : Filter.Tendsto (fun n => x n + y n) Filter.atTop (nhds (a + b)) := by sorrySource