Intermediate Value Theorem #
In this file we prove the Intermediate Value Theorem: if f : α → β is a function defined on a
connected set s that takes both values ≤ a and values ≥ a on s, then it is equal to a at
some point of s. We also prove that intervals in a dense conditionally complete order are
preconnected and any preconnected set is an interval. Then we specialize IVT to functions continuous
on intervals.
Main results #
IsPreconnected_I??: all intervalsI??are preconnected,IsPreconnected.intermediate_value,intermediate_value_univ: Intermediate Value Theorem for connected sets and connected spaces, respectively;intermediate_value_Icc,intermediate_value_Icc': Intermediate Value Theorem for functions on closed intervals.
Miscellaneous facts #
IsClosed.Icc_subset_of_forall_mem_nhdsWithin: “Continuous induction” principle; ifs ∩ [a, b]is closed,a ∈ s, and for eachx ∈ [a, b) ∩ ssome of its right neighborhoods is includeds, then[a, b] ⊆ s.IsClosed.Icc_subset_of_forall_exists_gt,IsClosed.mem_of_ge_of_forall_exists_gt: two other versions of the “continuous induction” principle.ContinuousOn.StrictMonoOn_of_InjOn_Ioo: Every continuous injectivef : (a, b) → δis strictly monotone or antitone (increasing or decreasing).
Tags #
intermediate value theorem, connected space, connected set
Intermediate value theorem on a (pre)connected space #
In this section we prove the following theorem (see IsPreconnected.intermediate_value₂): if f
and g are two functions continuous on a preconnected set s, f a ≤ g a at some a ∈ s and
g b ≤ f b at some b ∈ s, then f c = g c at some c ∈ s. We prove several versions of this
statement, including the classical IVT that corresponds to a constant function g.
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.
(Pre)connected sets in a linear order #
In this section we prove the following results:
-
IsPreconnected.ordConnected: any preconnected setsin a linear order isord_connected, i.e.a ∈ sandb ∈ simplyIcc a b ⊆ s; -
IsPreconnected.mem_intervals: any preconnected setsin a conditionally complete linear order is one of the intervalsSet.Icc,set.Ico,set.Ioc,set.Ioo, ``Set.Ici,Set.Iic,Set.Ioi,Set.Iio; note that this is false for non-complete orders: e.g., inℝ \ {0}, the set of positive numbers cannot be represented asSet.Ioi _.
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 ordered.
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.
Intervals are connected #
In this section we prove that a closed interval (hence, any ord_connected set) in a dense
conditionally complete linear order is preconnected.
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.
Equations
- ⋯ = ⋯
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 (sInf s, sInf s), we include it into the list of
possible cases to improve readability.
Intermediate Value Theorem on an interval #
In this section we prove several versions of the Intermediate Value Theorem for a function continuous on an interval.
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 Filter.atTop along Filter.atTop and to atBot along
at_bot is surjective.
A continuous function which tendsto Filter.atBot along Filter.atTop and to Filter.atTop
along atBot 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 Filter.atTop : Filter β along
Filter.atTop : Filter ↥s, then the restriction of f to s is surjective. We formulate the
conclusion as Function.surjOn f s Set.univ.
If a function f : α → β is continuous on a nonempty interval s, its restriction to s
tends to Filter.atTop : Filter β along Filter.atBot : Filter ↥s and tends to
Filter.atBot : Filter β along Filter.atTop : Filter ↥s, then the restriction of f to s is
surjective. We formulate the conclusion as Function.surjOn f s Set.univ.
Suppose α is equipped with a conditionally complete linear dense order and f : α → δ is
continuous and injective. Then f is strictly monotone (increasing) if
it is strictly monotone (increasing) on some closed interval [a, b].
Suppose f : [a, b] → δ is
continuous and injective. Then f is strictly monotone (increasing) if f(a) ≤ f(b).
Suppose f : [a, b] → δ is
continuous and injective. Then f is strictly antitone (decreasing) if f(b) ≤ f(a).
Suppose f : [a, b] → δ is continuous and injective. Then f is strictly monotone
or antitone (increasing or decreasing).
Suppose α is equipped with a conditionally complete linear dense order and f : α → δ is
continuous and injective. Then f is strictly monotone or antitone (increasing or decreasing).
Every continuous injective f : (a, b) → δ is strictly monotone
or antitone (increasing or decreasing).