36 lines
1.0 KiB
Lean4
36 lines
1.0 KiB
Lean4
-- 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
|