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

• IsPreconnected_I?? : all intervals I?? are preconnected,
• IsPreconnected.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

• IsClosed.Icc_subset_of_forall_mem_nhdsWithin : “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.
• IsClosed.Icc_subset_of_forall_exists_gt, IsClosed.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 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, 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} [Filter.NeBot l] {f : X → α} {g : X → α} (hf : Continuous f) (hg : Continuous g) (ha : f a ≤ g a) (he : g ≤ᶠ[l] f) : ∃ 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} [Filter.NeBot l₁] [Filter.NeBot l₂] {f : X → α} {g : X → α} (hf : Continuous f) (hg : Continuous g) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) : ∃ 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) : ∃ x, 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 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) [Filter.NeBot l] (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) : ∃ x, x ∈ s ∧ 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} [Filter.NeBot l₁] [Filter.NeBot l₂] (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) : ∃ x, x ∈ s ∧ 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) [Filter.NeBot l] (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) [Filter.NeBot l] (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} [Filter.NeBot l₁] [Filter.NeBot l₂] (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) [Filter.NeBot l] (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) [Filter.NeBot l] (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} [Filter.NeBot l₁] [Filter.NeBot l₂] (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} [Filter.NeBot l₁] [Filter.NeBot l₂] (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} [Filter.NeBot l₁] [Filter.NeBot l₂] (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, f a ≤ c) (h₂ : ∃ b, 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:

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

• IsPreconnected.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 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) : Set.OrdConnected s

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.

theorem IsConnected.Ioo_csInf_csSup_subset {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : IsConnected s) (hb : BddBelow s) (ha : BddAbove s) : Set.Ioo (sInf s) (sSup s) ⊆ s

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

theorem eq_Icc_csInf_csSup_of_connected_bdd_closed {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hc : IsConnected s) (hb : BddBelow s) (ha : BddAbove s) (hcl : IsClosed s) : s = Set.Icc (sInf s) (sSup s)

theorem IsPreconnected.Ioi_csInf_subset {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : IsPreconnected s) (hb : BddBelow s) (ha : ¬BddAbove s) : Set.Ioi (sInf s) ⊆ s

theorem IsPreconnected.Iio_csSup_subset {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {s : Set α} (hs : IsPreconnected s) (hb : ¬BddBelow s) (ha : BddAbove s) : Set.Iio (sSup s) ⊆ 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.

theorem setOf_isPreconnected_subset_of_ordered {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] : {s | IsPreconnected s} ⊆ Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪ Set.range (Function.uncurry Set.Ioo) ∪ (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})

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 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 : ∀ (x : α), x ∈ s ∩ Set.Ico a b → Set.Nonempty (s ∩ Set.Ioc x b)) : 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 : ∀ (x : α), x ∈ s ∩ Set.Ico a b → ∀ (y : α), y ∈ Set.Ioi x → Set.Nonempty (s ∩ Set.Ioc x y)) : 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 : ∀ (x : α), x ∈ s ∩ 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.Nonempty (Set.Icc a b ∩ (s ∩ t))

theorem isPreconnected_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} : IsPreconnected (Set.Icc a b)

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

theorem isPreconnected_uIcc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} : IsPreconnected (Set.uIcc a b)

theorem Set.OrdConnected.isPreconnected {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (h : Set.OrdConnected s) : IsPreconnected s

theorem isPreconnected_iff_ordConnected {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {s : Set α} : IsPreconnected s ↔ Set.OrdConnected s

theorem isPreconnected_Ici {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsPreconnected (Set.Ici a)

theorem isPreconnected_Iic {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsPreconnected (Set.Iic a)

theorem isPreconnected_Iio {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsPreconnected (Set.Iio a)

theorem isPreconnected_Ioi {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsPreconnected (Set.Ioi a)

theorem isPreconnected_Ioo {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} : IsPreconnected (Set.Ioo a b)

theorem isPreconnected_Ioc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} : IsPreconnected (Set.Ioc a b)

theorem isPreconnected_Ico {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} : IsPreconnected (Set.Ico a b)

theorem isConnected_Ici {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsConnected (Set.Ici a)

theorem isConnected_Iic {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} : IsConnected (Set.Iic a)

theorem isConnected_Ioi {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} [NoMaxOrder α] : IsConnected (Set.Ioi a)

theorem isConnected_Iio {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} [NoMinOrder α] : IsConnected (Set.Iio a)

theorem isConnected_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a ≤ b) : IsConnected (Set.Icc a b)

theorem isConnected_Ioo {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) : IsConnected (Set.Ioo a b)

theorem isConnected_Ioc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) : IsConnected (Set.Ioc a b)

theorem isConnected_Ico {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} {b : α} (h : a < b) : IsConnected (Set.Ico a b)

instance ordered_connected_space {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] : PreconnectedSpace α

Equations

• @ordered_connected_space = @ordered_connected_space.proof_1

theorem setOf_isPreconnected_eq_of_ordered {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] : {s | IsPreconnected s} = Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪ Set.range (Function.uncurry Set.Ioo) ∪ (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})

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.

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 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 : Set.OrdConnected s] {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 : Set.OrdConnected s] {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) : Function.Surjective f

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) : Function.Surjective f

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 α} [Set.OrdConnected s] (hs : Set.Nonempty s) (hf : ContinuousOn f s) (hbot : Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atBot) (htop : Filter.Tendsto (fun x => 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 α} [Set.OrdConnected s] (hs : Set.Nonempty s) (hf : ContinuousOn f s) (hbot : Filter.Tendsto (fun x => f ↑x) Filter.atBot Filter.atTop) (htop : Filter.Tendsto (fun x => 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.