-- Library Import: Basic facts about real numbers
import Mathlib.Data.Real.Basic
open Real

-- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ)
def continuous (f : ℝ → ℝ) (x₀ : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε

-- Definition: Sequence (u : ℕ → ℝ) converges to limit (l : ℝ)
def limit (u : ℕ → ℝ) (l : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| < ε

-- In the following, f is a function, u is a sequence, and x₀ a real number
variable {f : ℝ → ℝ} {u : ℕ → ℝ} {x₀ : ℝ}

-- Theorem: If f is continuous at x₀ and the sequence u converges to x₀, then
-- the sequence f ∘ u converges to f x₀.
theorem continuity_and_limits
  (hyp_f : continuous f x₀) (hyp_u : limit u x₀) :
    limit (f ∘ u) (f x₀) := by

  unfold limit at *
  unfold continuous at *

  intro ε hε

  obtain ⟨δ, h₁δ, h₂δ⟩ := hyp_f ε hε

  obtain ⟨N, hN⟩ := hyp_u δ h₁δ

  use N
  intro n hn
  apply h₂δ
  apply hN
  exact hn