Documentation

Mathlib.Topology.Order.IntermediateValue

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

theorem intermediate_value_univ₂ {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {a : X} {b : X} {f : Xα} {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} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {a : X} {l : Filter X} [l.NeBot] {f : Xα} {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} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] {l₁ : Filter X} {l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] {f : Xα} {g : Xα} (hf : Continuous f) (hg : Continuous g) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
∃ (x : X), f x = g x
theorem IsPreconnected.intermediate_value₂ {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {b : X} (ha : a s) (hb : b s) {f : Xα} {g : Xα} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a g a) (hb' : g b f b) :
xs, 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 IsPreconnected.intermediate_value₂_eventually₁ {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a s) [l.NeBot] (hl : l Filter.principal s) {f : Xα} {g : Xα} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a g a) (he : g ≤ᶠ[l] f) :
xs, f x = g x
theorem IsPreconnected.intermediate_value₂_eventually₂ {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ : Filter X} {l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ Filter.principal s) (hl₂ : l₂ Filter.principal s) {f : Xα} {g : Xα} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) :
xs, f x = g x
theorem IsPreconnected.intermediate_value {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {b : X} (ha : a s) (hb : b s) {f : Xα} (hf : ContinuousOn f s) :
Set.Icc (f a) (f b) f '' s

Intermediate Value Theorem for continuous functions on connected sets.

theorem IsPreconnected.intermediate_value_Ico {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a s) [l.NeBot] (hl : l Filter.principal s) {f : Xα} (hf : ContinuousOn f s) {v : α} (ht : Filter.Tendsto f l (nhds v)) :
Set.Ico (f a) v f '' s
theorem IsPreconnected.intermediate_value_Ioc {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a s) [l.NeBot] (hl : l Filter.principal s) {f : Xα} (hf : ContinuousOn f s) {v : α} (ht : Filter.Tendsto f l (nhds v)) :
Set.Ioc v (f a) f '' s
theorem IsPreconnected.intermediate_value_Ioo {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ : Filter X} {l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ Filter.principal s) (hl₂ : l₂ Filter.principal s) {f : Xα} (hf : ContinuousOn 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 IsPreconnected.intermediate_value_Ici {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a s) [l.NeBot] (hl : l Filter.principal s) {f : Xα} (hf : ContinuousOn f s) (ht : Filter.Tendsto f l Filter.atTop) :
Set.Ici (f a) f '' s
theorem IsPreconnected.intermediate_value_Iic {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a s) [l.NeBot] (hl : l Filter.principal s) {f : Xα} (hf : ContinuousOn f s) (ht : Filter.Tendsto f l Filter.atBot) :
Set.Iic (f a) f '' s
theorem IsPreconnected.intermediate_value_Ioi {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ : Filter X} {l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ Filter.principal s) (hl₂ : l₂ Filter.principal s) {f : Xα} (hf : ContinuousOn f s) {v : α} (ht₁ : Filter.Tendsto f l₁ (nhds v)) (ht₂ : Filter.Tendsto f l₂ Filter.atTop) :
Set.Ioi v f '' s
theorem IsPreconnected.intermediate_value_Iio {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ : Filter X} {l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ Filter.principal s) (hl₂ : l₂ Filter.principal s) {f : Xα} (hf : ContinuousOn f s) {v : α} (ht₁ : Filter.Tendsto f l₁ Filter.atBot) (ht₂ : Filter.Tendsto f l₂ (nhds v)) :
Set.Iio v f '' s
theorem IsPreconnected.intermediate_value_Iii {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ : Filter X} {l₂ : Filter X} [l₁.NeBot] [l₂.NeBot] (hl₁ : l₁ Filter.principal s) (hl₂ : l₂ Filter.principal s) {f : Xα} (hf : ContinuousOn f s) (ht₁ : Filter.Tendsto f l₁ Filter.atBot) (ht₂ : Filter.Tendsto f l₂ Filter.atTop) :
Set.univ f '' s
theorem intermediate_value_univ {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace X] (a : X) (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} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace 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 IsPreconnected.Icc_subset {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : IsPreconnected 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 IsPreconnected.ordConnected {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (h : IsPreconnected s) :
s.OrdConnected
theorem IsConnected.Icc_subset {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : IsConnected 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 IsPreconnected.eq_univ_of_unbounded {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s) (ha : ¬BddAbove s) :
s = Set.univ

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

theorem IsPreconnected.mem_intervals {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : IsPreconnected s) :
s {Set.Icc (sInf s) (sSup s), Set.Ico (sInf s) (sSup s), Set.Ioc (sInf s) (sSup s), Set.Ioo (sInf s) (sSup s), Set.Ici (sInf s), Set.Ioi (sInf s), Set.Iic (sSup s), Set.Iio (sSup 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 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 ∅, Inf ∅), 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 OrdConnected set) in a dense conditionally complete linear order is preconnected.

theorem IsClosed.mem_of_ge_of_forall_exists_gt {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} {b : α} {s : Set α} (hs : IsClosed (s Set.Icc a b)) (ha : a s) (hab : a b) (hgt : xs 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 IsClosed.Icc_subset_of_forall_exists_gt {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {a : α} {b : α} {s : Set α} (hs : IsClosed (s Set.Icc a b)) (ha : a s) (hgt : xs Set.Ico a b, ySet.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 IsClosed.Icc_subset_of_forall_mem_nhdsWithin {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} {s : Set α} (hs : IsClosed (s Set.Icc a b)) (ha : a s) (hgt : xs Set.Ico a b, s nhdsWithin 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.

theorem isPreconnected_Icc_aux {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (x : α) (y : α) (s : Set α) (t : Set α) (hxy : x y) (hs : IsClosed s) (ht : IsClosed t) (hab : Set.Icc a b s t) (hx : x Set.Icc a b s) (hy : y Set.Icc a b t) :
(Set.Icc a b (s t)).Nonempty

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

theorem isConnected_Ioo {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) :
theorem isConnected_Ioc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) :
theorem isConnected_Ico {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) :

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.

theorem isTotallyDisconnected_iff_lt {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {s : Set α} :
IsTotallyDisconnected s xs, ys, x < yzs, z Set.Ioo x y

This lemmas characterizes when a subset s of a densely ordered conditionally complete linear order is totally disconnected with respect to the order topology: between any two distinct points of s must lie a point not in s.

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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn 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_uIcc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} {f : αδ} (hf : ContinuousOn f (Set.uIcc a b)) :
Set.uIcc (f a) (f b) f '' Set.uIcc a b

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

theorem exists_mem_uIcc_isFixedPt {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} {f : αα} (hf : ContinuousOn f (Set.uIcc a b)) (ha : a f a) (hb : f b b) :
cSet.uIcc a b, Function.IsFixedPt f c

If f : α → α is continuous on [[a, b]], a ≤ f a, and f b ≤ b, then f has a fixed point on [[a, b]].

theorem exists_mem_Icc_isFixedPt {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} {f : αα} (hf : ContinuousOn f (Set.Icc a b)) (hle : a b) (ha : a f a) (hb : f b b) :
cSet.Icc a b, Function.IsFixedPt f c

If f : α → α is continuous on [a, b], a ≤ b, a ≤ f a, and f b ≤ b, then f has a fixed point on [a, b].

In particular, if [a, b] is forward-invariant under f, then f has a fixed point on [a, b], see exists_mem_Icc_isFixedPt_of_mapsTo.

theorem exists_mem_Icc_isFixedPt_of_mapsTo {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} {f : αα} (hf : ContinuousOn f (Set.Icc a b)) (hle : a b) (hmaps : Set.MapsTo f (Set.Icc a b) (Set.Icc a b)) :
cSet.Icc a b, Function.IsFixedPt f c

If a closed interval is forward-invariant under a continuous map f : α → α, then this map has a fixed point on this interval.

theorem intermediate_value_Ico {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Ico (f a) (f b) f '' Set.Ico a b
theorem intermediate_value_Ico' {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Ioc (f b) (f a) f '' Set.Ico a b
theorem intermediate_value_Ioc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Ioc (f a) (f b) f '' Set.Ioc a b
theorem intermediate_value_Ioc' {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Ico (f b) (f a) f '' Set.Ioc a b
theorem intermediate_value_Ioo {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Ioo (f a) (f b) f '' Set.Ioo a b
theorem intermediate_value_Ioo' {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} (hab : a b) {f : αδ} (hf : ContinuousOn f (Set.Icc a b)) :
Set.Ioo (f b) (f a) f '' Set.Ioo a b
theorem ContinuousOn.surjOn_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {s : Set α} [hs : s.OrdConnected] {f : αδ} (hf : ContinuousOn f s) {a : α} {b : α} (ha : a s) (hb : b s) :
Set.SurjOn 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 ContinuousOn.surjOn_uIcc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {s : Set α} [hs : s.OrdConnected] {f : αδ} (hf : ContinuousOn f s) {a : α} {b : α} (ha : a s) (hb : b s) :
Set.SurjOn f 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} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : αδ} (hf : Continuous f) (h_top : Filter.Tendsto f Filter.atTop Filter.atTop) (h_bot : Filter.Tendsto f Filter.atBot Filter.atBot) :

A continuous function which tendsto Filter.atTop along Filter.atTop and to atBot along at_bot is surjective.

theorem Continuous.surjective' {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : αδ} (hf : Continuous f) (h_top : Filter.Tendsto f Filter.atBot Filter.atTop) (h_bot : Filter.Tendsto f Filter.atTop Filter.atBot) :

A continuous function which tendsto Filter.atBot along Filter.atTop and to Filter.atTop along atBot is surjective.

theorem ContinuousOn.surjOn_of_tendsto {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : αδ} {s : Set α} [s.OrdConnected] (hs : s.Nonempty) (hf : ContinuousOn f s) (hbot : Filter.Tendsto (fun (x : s) => f x) Filter.atBot Filter.atBot) (htop : Filter.Tendsto (fun (x : s) => f x) Filter.atTop Filter.atTop) :
Set.SurjOn 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 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.

theorem ContinuousOn.surjOn_of_tendsto' {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : αδ} {s : Set α} [s.OrdConnected] (hs : s.Nonempty) (hf : ContinuousOn f s) (hbot : Filter.Tendsto (fun (x : s) => f x) Filter.atBot Filter.atTop) (htop : Filter.Tendsto (fun (x : s) => f x) Filter.atTop Filter.atBot) :
Set.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.

theorem Continuous.strictMonoOn_of_inj_rigidity {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : αδ} (hf_c : Continuous f) (hf_i : Function.Injective f) {a : α} {b : α} (hab : a < b) (hf_mono : StrictMonoOn f (Set.Icc a b)) :

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

theorem ContinuousOn.strictMonoOn_of_injOn_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} {f : αδ} (hab : a b) (hfab : f a f b) (hf_c : ContinuousOn f (Set.Icc a b)) (hf_i : Set.InjOn f (Set.Icc a b)) :

Suppose f : [a, b] → δ is continuous and injective. Then f is strictly monotone (increasing) if f(a) ≤ f(b).

theorem ContinuousOn.strictAntiOn_of_injOn_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} {f : αδ} (hab : a b) (hfab : f b f a) (hf_c : ContinuousOn f (Set.Icc a b)) (hf_i : Set.InjOn f (Set.Icc a b)) :

Suppose f : [a, b] → δ is continuous and injective. Then f is strictly antitone (decreasing) if f(b) ≤ f(a).

theorem ContinuousOn.strictMonoOn_of_injOn_Icc' {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} {f : αδ} (hab : a b) (hf_c : ContinuousOn f (Set.Icc a b)) (hf_i : Set.InjOn f (Set.Icc a b)) :

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

theorem ContinuousOn.strictMonoOn_of_injOn_Ioo {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {a : α} {b : α} {f : αδ} (hab : a < b) (hf_c : ContinuousOn f (Set.Ioo a b)) (hf_i : Set.InjOn f (Set.Ioo a b)) :

Every continuous injective f : (a, b) → δ is strictly monotone or antitone (increasing or decreasing).