def ContinuousFunctions.AchievesAbsMin (f : ℝ → ℝ) (S : Set ℝ) (c : ℝ) : Prop

AchievesAbsMin f S c states that f achieves its absolute minimum on S at the point c, i.e. c ∈ S and f c ≤ f x for every x ∈ S.

def ContinuousFunctions.AchievesAbsMax (f : ℝ → ℝ) (S : Set ℝ) (d : ℝ) : Prop

AchievesAbsMax f S d states that f achieves its absolute maximum on S at the point d, i.e. d ∈ S and f x ≤ f d for every x ∈ S.

theorem ContinuousFunctions.continuous_at_iff_eps_delta (f : ℝ → ℝ) (S : Set ℝ) (c : ℝ) (_hc : c ∈ S) : ContinuousWithinAt f S c ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ S, |x - c| < δ → |f x - f c| < ε

Continuity of f at a point c ∈ S (relative to S) is equivalent to the classical ε-δ formulation: for every ε > 0 there is δ > 0 such that for all x ∈ S, |x - c| < δ implies |f x - f c| < ε.

def ContinuousFunctions.IsBoundedOn (f : ℝ → ℝ) (S : Set ℝ) : Prop

IsBoundedOn f S states that f is bounded on S: there exists a nonnegative real number B such that |f x| ≤ B for every x ∈ S.

theorem ContinuousFunctions.continuous_on_Icc_bounded (f : ℝ → ℝ) (a b : ℝ) (_hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) : ∃ (B : ℝ), ∀ x ∈ Set.Icc a b, |f x| ≤ B

A real-valued function that is continuous on a closed bounded interval [a, b] is bounded: there exists B ∈ ℝ such that |f x| ≤ B for all x ∈ [a, b].

theorem ContinuousFunctions.extreme_value_theorem (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) : (∃ c ∈ Set.Icc a b, ∀ x ∈ Set.Icc a b, f c ≤ f x) ∧ ∃ d ∈ Set.Icc a b, ∀ x ∈ Set.Icc a b, f x ≤ f d

Extreme Value (Min-Max) Theorem: a continuous function on a closed bounded interval [a, b] attains both an absolute minimum at some point c ∈ [a, b] and an absolute maximum at some point d ∈ [a, b].