Topology and analysis · existing Mathlib theorem

Intermediate Value Theorem

If f is continuous from a to b and f(a) is below f(b), then no value between those endpoint outputs can be skipped: each one equals f(x) for some x between a and b.

intermediate values
continuity
closed intervals
connectedness
image inclusion

Four separate status axes

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed page2 of 3 presentation reviews recorded

Accepted Atlas resultNot recorded for the preferred artifact

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.

The theorem at a glance

Intermediate Value Theorem — exact interval-image form

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

Editorial theorem poster states the ordered closed-interval hypotheses, shows a continuous curve meeting an intermediate horizontal level, and explains the four-step preimage conclusion. — The selected Mathlib declaration states the increasing endpoint-value orientation as an interval-image inclusion.

A continuous warm-ivory curve travels between two green endpoint markers while an antique-gold horizontal level meets the curve above a point inside the interval. — Continuity forces each value between f(a) and f(b) to occur at some point of the closed interval.

Complementary intuition

A mathematical landmark

The Intermediate Value Theorem captures the no-jumps consequence of continuity. It is central to real analysis, root existence, connectedness, and numerical bracketing arguments.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

theorem intermediate_value_Icc {α : Type*} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type*} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b

Selected evidence declaration text

theorem intermediate_value_Icc {α : Type*} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type*} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Set.Icc a b)) : Set.Icc (f a) (f b) ⊆ f '' Set.Icc a b

Claim boundary

No new theorem is claimed

This target indexes Mathlib's ordered interval-image inclusion for a continuous function on [a,b]: every value between f(a) and f(b) occurs when a is at most b. The selected orientation uses Icc(f a)(f b), so it does not separately state the reversed-endpoint form.

The selected declaration fixes the endpoint-value orientation from f(a) to f(b).
Reversed and unordered endpoint-value forms are separate Mathlib declarations.
ProofAtlas is indexing an existing Mathlib theorem, not claiming new mathematics.

Provenance

Origin and evidence stay separate

Existing declaration: intermediate_value_Icc in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.intermediate-value-theorem.v001
Source handling: Verified upstream reference; no mirrored source package