Max_and_Min_of_Function_on_Closed_Real_Interval

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

max-and-min-of-function-on-closed-real-intervalproofwikireal-intervals

Let $f$ be a real function which is continuous on the closed interval $\closedint a b$ . Then $f$ reaches a maximum and a minimum on $\closedint a b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Topology.Order.Basic

theorem Max_and_Min_of_Function_on_Closed_Real_Interval (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hf : ContinuousOn f (Set.Icc a b)) : ∃ c ∈ Set.Icc a b, ∀ x ∈ Set.Icc a b, f x ≤ f c := by sorry

Source

https://proofwiki.org/wiki/Max_and_Min_of_Function_on_Closed_Real_Interval

View graph