mathlib documentation

topology.algebra.order.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 filter.principal 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₁ filter.principal s) (hl₂ : l₂ filter.principal 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 filter.principal s) {f : X → α} (hf : continuous_on f s) {v : α} (ht : filter.tendsto f l (nhds 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 filter.principal s) {f : X → α} (hf : continuous_on f s) {v : α} (ht : filter.tendsto f l (nhds 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₁ filter.principal s) (hl₂ : l₂ filter.principal s) {f : X → α} (hf : continuous_on f s) {v₁ v₂ : α} (ht₁ : filter.tendsto f l₁ (nhds v₁)) (ht₂ : filter.tendsto f l₂ (nhds 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 filter.principal 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 filter.principal 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₁ filter.principal s) (hl₂ : l₂ filter.principal s) {f : X → α} (hf : continuous_on f s) {v : α} (ht₁ : filter.tendsto f l₁ (nhds 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₁ filter.principal s) (hl₂ : l₂ filter.principal s) {f : X → α} (hf : continuous_on f s) {v : α} (ht₁ : filter.tendsto f l₁ filter.at_bot) (ht₂ : filter.tendsto f l₂ (nhds 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₁ filter.principal s) (hl₂ : l₂ filter.principal 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.

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.

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 nhds_within x (set.Ioi 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 (set.interval a b)) :
set.interval (f a) (f b) f '' set.interval 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 (set.interval (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.