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 #

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} [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) :

set.univ ⊆ f '' s

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

c ∈ set.range f

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 α] [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_preconnected.ord_connected {α : Type v} [linear_order α] [topological_space α] [order_closed_topology α] {s : set α} (h : is_preconnected s) :

s.ord_connected

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.

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

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 eq_Icc_cInf_cSup_of_connected_bdd_closed {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hc : is_connected s) (hb : bdd_below s) (ha : bdd_above s) (hcl : is_closed s) :

s = set.Icc (Inf s) (Sup s)

theorem is_preconnected.Ioi_cInf_subset {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_preconnected s) (hb : bdd_below s) (ha : ¬bdd_above s) :

set.Ioi (Inf s) ⊆ s

theorem is_preconnected.Iio_cSup_subset {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] {s : set α} (hs : is_preconnected s) (hb : ¬bdd_below s) (ha : bdd_above s) :

set.Iio (Sup s) ⊆ 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.

theorem set_of_is_preconnected_subset_of_ordered {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] :

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 b → s ∈ 𝓝[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.

theorem is_preconnected_Icc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a b : α} :

is_preconnected (set.Icc a b)

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

theorem is_preconnected_interval {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a b : α} :

is_preconnected [a, b]

theorem set.ord_connected.is_preconnected {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {s : set α} (h : s.ord_connected) :

is_preconnected s

theorem is_preconnected_iff_ord_connected {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {s : set α} :

is_preconnected s ↔ s.ord_connected

theorem is_preconnected_Ici {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a : α} :

is_preconnected (set.Ici a)

theorem is_preconnected_Iic {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a : α} :

is_preconnected (set.Iic a)

theorem is_preconnected_Iio {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a : α} :

is_preconnected (set.Iio a)

theorem is_preconnected_Ioi {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a : α} :

is_preconnected (set.Ioi a)

theorem is_preconnected_Ioo {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a b : α} :

is_preconnected (set.Ioo a b)

theorem is_preconnected_Ioc {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a b : α} :

is_preconnected (set.Ioc a b)

theorem is_preconnected_Ico {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {a b : α} :

is_preconnected (set.Ico a b)

@[protected, instance]

def ordered_connected_space {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] :

preconnected_space α

theorem set_of_is_preconnected_eq_of_ordered {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] :

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

theorem continuous.surjective {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {f : α → δ} (hf : continuous f) (h_top : filter.tendsto f filter.at_top filter.at_top) (h_bot : filter.tendsto f filter.at_bot filter.at_bot) :

function.surjective f

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

theorem continuous.surjective' {α : Type u} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {f : α → δ} (hf : continuous f) (h_top : filter.tendsto f filter.at_bot filter.at_top) (h_bot : filter.tendsto f filter.at_top filter.at_bot) :

function.surjective f

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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {f : α → δ} {s : set α} [s.ord_connected] (hs : s.nonempty) (hf : continuous_on f 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) :

set.surj_on f s set.univ

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} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [densely_ordered α] {δ : Type u_1} [linear_order δ] [topological_space δ] [order_closed_topology δ] {f : α → δ} {s : set α} [s.ord_connected] (hs : s.nonempty) (hf : continuous_on f 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) :

set.surj_on f s set.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.