Limit_of_Composite_Function
Provedlimits-of-functionsproofwiki
If lim_{x->a} f(x) = b and lim_{y->b} g(y) = c, then lim_{x->a} g(f(x)) = c.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Limit_of_Composite_Function (f : ℝ → ℝ) (g : ℝ → ℝ) (a b c : ℝ) (hf : Filter.Tendsto f (nhds a) (nhds b)) (hg : Filter.Tendsto g (nhds b) (nhds c)) : Filter.Tendsto (g ∘ f) (nhds a) (nhds c) := by sorry
Source