Intermediate_Value_Theorem

Proved

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

analysisnamed-theoremsproofwiki

Let $f: S \to \R$ be a real function on some subset $S$ of $\R$ . Let $I \subseteq S$ be a real interval. Let $f: I \to \R$ be continuous on $I$ . Let $a, b \in I$ . Let $k \in \R$ lie between $\map f a$ and $\map f b$ . That is, either $\map f a < k < \map f b$ or $\map f b < k < \map f a$ Then $\exists c \in \openint a b$ such that $\map f c = k$ .

Preamble

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

Formal statement

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

theorem Intermediate_Value_Theorem (f : ℝ → ℝ) (a b : ℝ) (hab : a ≤ b) (hf : ContinuousOn f (Set.Icc a b)) (v : ℝ) (hv : f a ≤ v ∧ v ≤ f b ∨ f b ≤ v ∧ v ≤ f a) : ∃ c ∈ Set.Icc a b, f c = v := by sorry

Source

https://proofwiki.org/wiki/Intermediate_Value_Theorem

View graph