40 lines
986 B
Lean4
40 lines
986 B
Lean4
-- Library Import: Basic facts about real numbers and the root function
|
||
import Mathlib.Data.Real.Sqrt
|
||
open Real
|
||
|
||
-- In the following, x and y are real numbers
|
||
variable {x : ℝ} {y : ℝ}
|
||
|
||
-- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ)
|
||
def continuous (f : ℝ → ℝ) (x₀ : ℝ) :=
|
||
∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε
|
||
|
||
-- Definition: The square function
|
||
def squareFct : ℝ → ℝ := fun x ↦ x ^ 2
|
||
|
||
|
||
-- Reminder: Three facts from the library that we will use.
|
||
example : 0 < x → 0 < √x := sqrt_pos.2
|
||
|
||
example : x ^ 2 < y ↔ (-√y < x) ∧ (x < √y) := sq_lt
|
||
|
||
example : |x| < y ↔ -y < x ∧ x < y := abs_lt
|
||
|
||
|
||
-- Theorem: The square function is continuous at x₀ = 0
|
||
theorem ContinuousAt_sq :
|
||
continuous squareFct 0 := by
|
||
|
||
unfold continuous
|
||
|
||
intro ε hε
|
||
use √ε
|
||
|
||
constructor
|
||
· apply sqrt_pos.2
|
||
exact hε
|
||
· intro x hx
|
||
simp_all [squareFct]
|
||
apply sq_lt.2
|
||
exact abs_lt.1 hx
|