Condition_for_Continuity_on_Interval
Provedcontinuityproofwiki
A function f is continuous on [a,b] iff for every x in [a,b] and every epsilon > 0 there exists delta > 0 such that |x-y| < delta implies |f(x)-f(y)| < epsilon for y in [a,b].
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Condition_for_Continuity_on_Interval (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) : ContinuousOn f (Set.Icc a b) ↔ ∀ x ∈ Set.Icc a b, ∀ ε > 0, ∃ δ > 0, ∀ y ∈ Set.Icc a b, |x - y| < δ → |f x - f y| < ε := by sorry
Source