lean_workbook_plus_59352
ProvedFind such that for all satisfying .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59352 (ε : ℝ) : ∃ δ : ℝ, ∀ x : ℝ, |x - 2| < δ → |x ^ 2 - 4| < ε := by sorry
Source
Find such that for all satisfying .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59352 (ε : ℝ) : ∃ δ : ℝ, ∀ x : ℝ, |x - 2| < δ → |x ^ 2 - 4| < ε := by sorry