Combination_Theorem_for_Limits_of_Functions
Provedlimits-of-functionsproofwiki
If lim f(x) = lf and lim g(x) = lg as x -> a, then lim (f+g)(x) = lf+lg and lim (fg)(x) = lflg.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Combination_Theorem_for_Limits_of_Functions (f g : ℝ → ℝ) (a lf lg : ℝ) (hf : Filter.Tendsto f (nhds a) (nhds lf)) (hg : Filter.Tendsto g (nhds a) (nhds lg)) : Filter.Tendsto (fun x => f x + g x) (nhds a) (nhds (lf + lg)) ∧ Filter.Tendsto (fun x => f x * g x) (nhds a) (nhds (lf * lg)) := by sorry
Source