Intermediate value theorem for two functions: if f and g are two continuous functions on a preconnected space and f a ≤ g a and g b ≤ f b, then for some x we have f x = g x.

Intermediate value theorem for two functions: if f and g are two functions continuous on a preconnected set s and for some a b ∈ s we have f a ≤ g a and g b ≤ f b, then for some x ∈ s we have f x = g x.

Intermediate Value Theorem for continuous functions on connected sets.

Intermediate Value Theorem for continuous functions on connected spaces.

Intermediate Value Theorem for continuous functions on connected spaces.

If a preconnected set contains endpoints of an interval, then it includes the whole interval.

If a preconnected set contains endpoints of an interval, then it includes the whole interval.

If preconnected set in a linear order space is unbounded below and above, then it is the whole space.

A bounded connected subset of a conditionally complete linear order includes the open interval (Inf s, Sup s).

A preconnected set in a conditionally complete linear order is either one of the intervals [Inf s, Sup s], [Inf s, Sup s), (Inf s, Sup s], (Inf s, Sup s), [Inf s, +∞), (Inf s, +∞), (-∞, Sup s], (-∞, Sup s), (-∞, +∞), or ∅. The converse statement requires α to be densely ordererd.

A preconnected set is either one of the intervals Icc, Ico, Ioc, Ioo, Ici, Ioi, Iic, Iio, or univ, or ∅. The converse statement requires α to be densely ordered. Though one can represent ∅ as (Inf s, Inf s), we include it into the list of possible cases to improve readability.

A "continuous induction principle" for a closed interval: if a set s meets [a, b] on a closed subset, contains a, and the set s ∩ [a, b) has no maximal point, then b ∈ s.

A "continuous induction principle" for a closed interval: if a set s meets [a, b] on a closed subset, contains a, and for any a ≤ x < y ≤ b, x ∈ s, the set s ∩ (x, y] is not empty, then [a, b] ⊆ s.

A "continuous induction principle" for a closed interval: if a set s meets [a, b] on a closed subset, contains a, and for any x ∈ s ∩ [a, b) the set s includes some open neighborhood of x within (x, +∞), then [a, b] ⊆ s.

A closed interval in a densely ordered conditionally complete linear order is preconnected.

In a dense conditionally complete linear order, the set of preconnected sets is exactly the set of the intervals Icc, Ico, Ioc, Ioo, Ici, Ioi, Iic, Iio, (-∞, +∞), or ∅. Though one can represent ∅ as (Inf s, Inf s), we include it into the list of possible cases to improve readability.

Intermediate Value Theorem for continuous functions on closed intervals, case f a ≤ t ≤ f b.

Intermediate Value Theorem for continuous functions on closed intervals, case f a ≥ t ≥ f b.

Intermediate Value Theorem for continuous functions on closed intervals, unordered case.

Intermediate value theorem: if f is continuous on an order-connected set s and a, b are two points of this set, then f sends s to a superset of Icc (f x) (f y).

Intermediate value theorem: if f is continuous on an order-connected set s and a, b are two points of this set, then f sends s to a superset of [f x, f y].

A continuous function which tendsto at_top at_top and to at_bot at_bot is surjective.

A continuous function which tendsto at_bot at_top and to at_top at_bot is surjective.

If a function f : α → β is continuous on a nonempty interval s, its restriction to s tends to at_bot : filter β along at_bot : filter ↥s and tends to at_top : filter β along at_top : filter ↥s, then the restriction of f to s is surjective. We formulate the conclusion as surj_on f s univ.

If a function f : α → β is continuous on a nonempty interval s, its restriction to s tends to at_top : filter β along at_bot : filter ↥s and tends to at_bot : filter β along at_top : filter ↥s, then the restriction of f to s is surjective. We formulate the conclusion as surj_on f s univ.