# mathlib3documentation

topology.algebra.order.intermediate_value

# Intermediate Value Theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• is_preconnected_I?? : all intervals I?? are preconnected,
• is_preconnected.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 #

• is_closed.Icc_subset_of_forall_mem_nhds_within : “Continuous induction” principle; if s ∩ [a, b] is closed, a ∈ s, and for each x ∈ [a, b) ∩ s some of its right neighborhoods is included s, then [a, b] ⊆ s.
• is_closed.Icc_subset_of_forall_exists_gt, is_closed.mem_of_ge_of_forall_exists_gt : two other versions of the “continuous induction” principle.

## 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} [linear_order α] {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} [linear_order α] {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} [linear_order α] {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} [linear_order α] {s : set X} (hs : is_preconnected s) {a b : X} (ha : a s) (hb : b s) {f g : X α} (hf : s) (hg : 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} [linear_order α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l ) {f g : X α} (hf : s) (hg : 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} [linear_order α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ ) (hl₂ : l₂ ) {f g : X α} (hf : s) (hg : 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} [linear_order α] {s : set X} (hs : is_preconnected s) {a b : X} (ha : a s) (hb : b s) {f : X α} (hf : 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} [linear_order α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l ) {f : X α} (hf : s) {v : α} (ht : (nhds v)) :
set.Ico (f a) v f '' s
theorem is_preconnected.intermediate_value_Ioc {X : Type u} {α : Type v} [linear_order α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l ) {f : X α} (hf : s) {v : α} (ht : (nhds v)) :
(f a) f '' s
theorem is_preconnected.intermediate_value_Ioo {X : Type u} {α : Type v} [linear_order α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ ) (hl₂ : l₂ ) {f : X α} (hf : s) {v₁ v₂ : α} (ht₁ : l₁ (nhds v₁)) (ht₂ : l₂ (nhds v₂)) :
set.Ioo v₁ v₂ f '' s
theorem is_preconnected.intermediate_value_Ici {X : Type u} {α : Type v} [linear_order α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l ) {f : X α} (hf : s) (ht : filter.at_top) :
set.Ici (f a) f '' s
theorem is_preconnected.intermediate_value_Iic {X : Type u} {α : Type v} [linear_order α] {s : set X} (hs : is_preconnected s) {a : X} {l : filter X} (ha : a s) [l.ne_bot] (hl : l ) {f : X α} (hf : s) (ht : filter.at_bot) :
set.Iic (f a) f '' s
theorem is_preconnected.intermediate_value_Ioi {X : Type u} {α : Type v} [linear_order α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ ) (hl₂ : l₂ ) {f : X α} (hf : s) {v : α} (ht₁ : l₁ (nhds v)) (ht₂ : l₂ filter.at_top) :
f '' s
theorem is_preconnected.intermediate_value_Iio {X : Type u} {α : Type v} [linear_order α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ ) (hl₂ : l₂ ) {f : X α} (hf : s) {v : α} (ht₁ : l₁ filter.at_bot) (ht₂ : l₂ (nhds v)) :
f '' s
theorem is_preconnected.intermediate_value_Iii {X : Type u} {α : Type v} [linear_order α] {s : set X} (hs : is_preconnected s) {l₁ l₂ : filter X} [l₁.ne_bot] [l₂.ne_bot] (hl₁ : l₁ ) (hl₂ : l₂ ) {f : X α} (hf : s) (ht₁ : l₁ filter.at_bot) (ht₂ : l₂ filter.at_top) :
theorem intermediate_value_univ {X : Type u} {α : Type v} [linear_order α] (a b : X) {f : X α} (hf : continuous f) :
set.Icc (f a) (f b)

Intermediate Value Theorem for continuous functions on connected spaces.

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

Intermediate Value Theorem for continuous functions on connected spaces.

### (Pre)connected sets in a linear order #

In this section we prove the following results:

• is_preconnected.ord_connected: any preconnected set s in a linear order is ord_connected, i.e. a ∈ s and b ∈ s imply Icc a b ⊆ s;

• is_preconnected.mem_intervals: any preconnected set s in a conditionally complete linear order is one of the intervals set.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 as set.Ioi _.

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

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

theorem is_preconnected.ord_connected {α : Type v} [linear_order α] {s : set α} (h : is_preconnected s) :
theorem is_connected.Icc_subset {α : Type v} [linear_order α] {s : set α} (hs : is_connected s) {a b : α} (ha : a s) (hb : b s) :
b s

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

theorem is_preconnected.eq_univ_of_unbounded {α : Type v} [linear_order α] {s : set α} (hs : is_preconnected s) (hb : ¬) (ha : ¬) :

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} {s : set α} (hs : is_connected s) (hb : bdd_below s) (ha : bdd_above s) :

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

theorem eq_Icc_cInf_cSup_of_connected_bdd_closed {α : Type u} {s : set α} (hc : is_connected s) (hb : bdd_below s) (ha : bdd_above s) (hcl : is_closed s) :
theorem is_preconnected.Ioi_cInf_subset {α : Type u} {s : set α} (hs : is_preconnected s) (hb : bdd_below s) (ha : ¬) :
s
theorem is_preconnected.Iio_cSup_subset {α : Type u} {s : set α} (hs : is_preconnected s) (hb : ¬) (ha : bdd_above s) :
s
theorem is_preconnected.mem_intervals {α : Type u} {s : set α} (hs : is_preconnected 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} {a b : α} {s : set α} (hs : is_closed (s b)) (ha : a s) (hab : a b) (hgt : (x : α), x s b (s 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} {a b : α} {s : set α} (hs : is_closed (s b)) (ha : a s) (hgt : (x : α), x s b (y : α), y (s y).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 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} {a b : α} {s : set α} (hs : is_closed (s b)) (ha : a s) (hgt : (x : α), x s b s (set.Ioi x)) :
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.

theorem is_preconnected_Icc_aux {α : Type u} {a b : α} (x y : α) (s t : set α) (hxy : x y) (hs : is_closed s) (ht : is_closed t) (hab : b s t) (hx : x b s) (hy : y b t) :
(set.Icc a b (s t)).nonempty
theorem is_preconnected_Icc {α : Type u} {a b : α} :

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

theorem is_preconnected_uIcc {α : Type u} {a b : α} :
theorem set.ord_connected.is_preconnected {α : Type u} {s : set α} (h : s.ord_connected) :
theorem is_preconnected_iff_ord_connected {α : Type u} {s : set α} :
theorem is_preconnected_Ici {α : Type u} {a : α} :
theorem is_preconnected_Iic {α : Type u} {a : α} :
theorem is_preconnected_Iio {α : Type u} {a : α} :
theorem is_preconnected_Ioi {α : Type u} {a : α} :
theorem is_preconnected_Ioo {α : Type u} {a b : α} :
theorem is_preconnected_Ioc {α : Type u} {a b : α} :
theorem is_preconnected_Ico {α : Type u} {a b : α} :
theorem is_connected_Ici {α : Type u} {a : α} :
theorem is_connected_Iic {α : Type u} {a : α} :
theorem is_connected_Ioi {α : Type u} {a : α} [no_max_order α] :
theorem is_connected_Iio {α : Type u} {a : α} [no_min_order α] :
theorem is_connected_Icc {α : Type u} {a b : α} (h : a b) :
theorem is_connected_Ioo {α : Type u} {a b : α} (h : a < b) :
theorem is_connected_Ioc {α : Type u} {a b : α} (h : a < b) :
theorem is_connected_Ico {α : Type u} {a b : α} (h : a < b) :
@[protected, instance]

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} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Icc (f a) (f b) f '' b

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

theorem intermediate_value_Icc' {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Icc (f b) (f a) f '' b

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

theorem intermediate_value_uIcc {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} {f : α δ} (hf : (set.uIcc a b)) :
set.uIcc (f a) (f b) f '' b

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

theorem intermediate_value_Ico {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Ico (f a) (f b) f '' b
theorem intermediate_value_Ico' {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Ioc (f b) (f a) f '' b
theorem intermediate_value_Ioc {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Ioc (f a) (f b) f '' b
theorem intermediate_value_Ioc' {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Ico (f b) (f a) f '' b
theorem intermediate_value_Ioo {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Ioo (f a) (f b) f '' b
theorem intermediate_value_Ioo' {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Ioo (f b) (f a) f '' b
theorem continuous_on.surj_on_Icc {α : Type u} {δ : Type u_1} [linear_order δ] {s : set α} [hs : s.ord_connected] {f : α δ} (hf : s) {a b : α} (ha : a s) (hb : b s) :
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_uIcc {α : Type u} {δ : Type u_1} [linear_order δ] {s : set α} [hs : s.ord_connected] {f : α δ} (hf : s) {a b : α} (ha : a s) (hb : b s) :
s (set.uIcc (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].

theorem continuous.surjective {α : Type u} {δ : Type u_1} [linear_order δ] {f : α δ} (hf : continuous f) (h_top : filter.at_top) (h_bot : filter.at_bot) :

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

theorem continuous.surjective' {α : Type u} {δ : Type u_1} [linear_order δ] {f : α δ} (hf : continuous f) (h_top : filter.at_top) (h_bot : filter.at_bot) :

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

theorem continuous_on.surj_on_of_tendsto {α : Type u} {δ : Type u_1} [linear_order δ] {f : α δ} {s : set α} [s.ord_connected] (hs : s.nonempty) (hf : s) (hbot : filter.tendsto (λ (x : s), f x) filter.at_bot filter.at_bot) (htop : filter.tendsto (λ (x : s), f x) filter.at_top filter.at_top) :

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.

theorem continuous_on.surj_on_of_tendsto' {α : Type u} {δ : Type u_1} [linear_order δ] {f : α δ} {s : set α} [s.ord_connected] (hs : s.nonempty) (hf : s) (hbot : filter.tendsto (λ (x : s), f x) filter.at_bot filter.at_top) (htop : filter.tendsto (λ (x : s), f x) filter.at_top filter.at_bot) :

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.