If f is continuous at a and the limit of u(n) is a, then the limit of f(u(n)) is f(a)
In Lean4, we can define that \(a\) is the limit of the sequence \(u\) by:
def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε
and that \(f\) is continuous at \(a\) by:
def continuous_at (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε
To prove that if the function \(f\) is continuous at the point \(a\), and the sequence \(u(n)\) converges to \(a\), then the sequence \(f(u(n))\) converges to \(f(a)\).
To do this, complete the following Lean4 theory:
import Mathlib.Data.Real.Basic variable {f : ℝ → ℝ} variable {a : ℝ} variable {u : ℕ → ℝ} def is_limit (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε def continuous_at (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε example (hf : continuous_at f a) (hu : is_limit u a) : is_limit (f ∘ u) (f a) := by sorry