The intermediate value theorem

Content created by Louis Wasserman.

Created on 2026-02-04.
Last modified on 2026-02-04.

{-# OPTIONS --lossy-unification #-}

module analysis.intermediate-value-theorem where
Imports 




Idea


The
intermediate value theorem
states that for a
pointwise ε-δ continuous endomap
f on the real numbers, real numbers
a and b with a
less than or equal to b such that
f a is negative and f b is
positive, there exists a c with
a ≤ c ≤ b such that f c is zero.


Lab states that this theorem is known to be invalid in constructive contexts.


This contrasts with the
constructive intermediate value theorem,
which states merely that for any
positive rational ε,
there exists a c with a ≤ c ≤ b with |f c| ≤ ε.


Proof


This has yet to be proved.


See also





Recent changes