mathlib documentation

topology.algebra.ordered.intermediate_value

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 #

Miscellaneous facts #

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 is_preconnected.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.

theorem intermediate_value_univ₂ {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] [preconnected_space X] {a b : X} {f g : X → α} (hf : continuous f) (hg : continuous g) (ha : f a g a) (hb : g b f b) :
∃ (x : X), f x = g x

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.

theorem intermediate_value_univ₂_eventually₁ {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] [preconnected_space X] {a : X} {l : filter X} [l.ne_bot] {f g : X → α} (hf : continuous f) (hg : continuous g) (ha : f a g a) (he : g ≤ᶠ[l] f) :
∃ (x : X), f x = g x
theorem intermediate_value_univ₂_eventually₂ {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] [preconnected_space X] {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] {f g : X → α} (hf : continuous f) (hg : continuous g) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
∃ (x : X), f x = g x
theorem is_preconnected.intermediate_value₂ {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {a b : X} (ha : a s) (hb : b s) {f g : X → α} (hf : continuous_on f s) (hg : continuous_on g s) (ha' : f a g a) (hb' : g b f b) :
∃ (x : X) (H : x s), 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.

theorem is_preconnected.intermediate_value₂_eventually₁ {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f g : X → α} (hf : continuous_on f s) (hg : continuous_on g s) (ha' : f a g a) (he : g ≤ᶠ[l] f) :
∃ (x : X) (H : x s), f x = g x
theorem is_preconnected.intermediate_value₂_eventually₂ {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f g : X → α} (hf : continuous_on f s) (hg : continuous_on g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
∃ (x : X) (H : x s), f x = g x
theorem is_preconnected.intermediate_value {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {a b : X} (ha : a s) (hb : b s) {f : X → α} (hf : continuous_on f s) :
set.Icc (f a) (f b) f '' s

Intermediate Value Theorem for continuous functions on connected sets.

theorem is_preconnected.intermediate_value_Ico {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f : X → α} (hf : continuous_on f s) {v : α} (ht : filter.tendsto f l (𝓝 v)) :
set.Ico (f a) v f '' s
theorem is_preconnected.intermediate_value_Ioc {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f : X → α} (hf : continuous_on f s) {v : α} (ht : filter.tendsto f l (𝓝 v)) :
set.Ioc v (f a) f '' s
theorem is_preconnected.intermediate_value_Ioo {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f : X → α} (hf : continuous_on f s) {v₁ v₂ : α} (ht₁ : filter.tendsto f l₁ (𝓝 v₁)) (ht₂ : filter.tendsto f l₂ (𝓝 v₂)) :
set.Ioo v₁ v₂ f '' s
theorem is_preconnected.intermediate_value_Ici {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f : X → α} (hf : continuous_on f s) (ht : filter.tendsto f l filter.at_top) :
set.Ici (f a) f '' s
theorem is_preconnected.intermediate_value_Iic {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l 𝓟 s) {f : X → α} (hf : continuous_on f s) (ht : filter.tendsto f l filter.at_bot) :
set.Iic (f a) f '' s
theorem is_preconnected.intermediate_value_Ioi {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f : X → α} (hf : continuous_on f s) {v : α} (ht₁ : filter.tendsto f l₁ (𝓝 v)) (ht₂ : filter.tendsto f l₂ filter.at_top) :
set.Ioi v f '' s
theorem is_preconnected.intermediate_value_Iio {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f : X → α} (hf : continuous_on f s) {v : α} (ht₁ : filter.tendsto f l₁ filter.at_bot) (ht₂ : filter.tendsto f l₂ (𝓝 v)) :
set.Iio v f '' s
theorem is_preconnected.intermediate_value_Iii {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ 𝓟 s) (hl₂ : l₂ 𝓟 s) {f : X → α} (hf : continuous_on f s) (ht₁ : filter.tendsto f l₁ filter.at_bot) (ht₂ : filter.tendsto f l₂ filter.at_top) :
theorem intermediate_value_univ {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] [preconnected_space X] (a b : X) {f : X → α} (hf : continuous f) :
set.Icc (f a) (f b) set.range f

Intermediate Value Theorem for continuous functions on connected spaces.

theorem mem_range_of_exists_le_of_exists_ge {X : Type u} {α : Type v} [topological_space X] [linear_order α] [topological_space α] [order_closed_topology α] [preconnected_space X] {c : α} {f : X → α} (hf : continuous f) (h₁ : ∃ (a : X), f a c) (h₂ : ∃ (b : X), c f b) :

Intermediate Value Theorem for continuous functions on connected spaces.

(Pre)connected sets in a linear order #

In this section we prove the following results:

theorem is_preconnected.Icc_subset {α : Type v} [linear_order α] [topological_space α] [order_closed_topology α] {s : set α} (hs : is_preconnected s) {a b : α} (ha : a s) (hb : b s) :
set.Icc a b s

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

theorem is_connected.Icc_subset {α : Type v} [linear_order α] [topological_space α] [order_closed_topology α] {s : set α} (hs : is_connected s) {a b : α} (ha : a s) (hb : b s) :
set.Icc a b s

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.

theorem is_connected.Ioo_cInf_cSup_subset {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_connected s) (hb : bdd_below s) (ha : bdd_above s) :
set.Ioo (Inf s) (Sup s) s

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

theorem is_preconnected.mem_intervals {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_preconnected s) :
s {set.Icc (Inf s) (Sup s), set.Ico (Inf s) (Sup s), set.Ioc (Inf s) (Sup s), set.Ioo (Inf s) (Sup s), set.Ici (Inf s), set.Ioi (Inf s), set.Iic (Sup s), set.Iio (Sup s), set.univ, }

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.

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.

theorem is_closed.mem_of_ge_of_forall_exists_gt {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {a b : α} {s : set α} (hs : is_closed (s set.Icc a b)) (ha : a s) (hab : a b) (hgt : ∀ (x : α), x s set.Ico a b(s set.Ioc x b).nonempty) :
b s

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.

theorem is_closed.Icc_subset_of_forall_exists_gt {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {a b : α} {s : set α} (hs : is_closed (s set.Icc a b)) (ha : a s) (hgt : ∀ (x : α), x s set.Ico a b∀ (y : α), y set.Ioi x(s set.Ioc x y).nonempty) :
set.Icc 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 a ≤ x < y ≤ b, x ∈ s, the set s ∩ (x, y] is not empty, then [a, b] ⊆ s.

theorem is_closed.Icc_subset_of_forall_mem_nhds_within {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a b : α} {s : set α} (hs : is_closed (s set.Icc a b)) (ha : a s) (hgt : ∀ (x : α), x s set.Ico a bs 𝓝[set.Ioi x] x) :
set.Icc 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 on an interval #

In this section we prove several versions of the Intermediate Value Theorem for a function continuous on an interval.

theorem intermediate_value_Icc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Icc (f a) (f b) f '' set.Icc a b

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

theorem intermediate_value_Icc' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Icc (f b) (f a) f '' set.Icc a b

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

theorem intermediate_value_interval {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} {f : α → δ} (hf : continuous_on f [a, b]) :
[f a, f b] f '' [a, b]

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

theorem intermediate_value_Ico {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ico (f a) (f b) f '' set.Ico a b
theorem intermediate_value_Ico' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ioc (f b) (f a) f '' set.Ico a b
theorem intermediate_value_Ioc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ioc (f a) (f b) f '' set.Ioc a b
theorem intermediate_value_Ioc' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ico (f b) (f a) f '' set.Ioc a b
theorem intermediate_value_Ioo {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ioo (f a) (f b) f '' set.Ioo a b
theorem intermediate_value_Ioo' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {a b : α} (hab : a b) {f : α → δ} (hf : continuous_on f (set.Icc a b)) :
set.Ioo (f b) (f a) f '' set.Ioo a b
theorem continuous_on.surj_on_Icc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {s : set α} [hs : s.ord_connected] {f : α → δ} (hf : continuous_on f s) {a b : α} (ha : a s) (hb : b s) :
set.surj_on f s (set.Icc (f a) (f b))

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).

theorem continuous_on.surj_on_interval {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {s : set α} [hs : s.ord_connected] {f : α → δ} (hf : continuous_on f s) {a b : α} (ha : a s) (hb : b s) :
set.surj_on f s [f a, f b]

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.