# 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.
- `ContinuousOn.StrictMonoOn_of_InjOn_Ioo` : Every continuous injective `f : (a, b) → δ` is strictly monotone or antitone (increasing or decreasing).

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

source
theorem intermediate_value_univ₂ {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace 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`.

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

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

source
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
source
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
source
theorem IsPreconnected.intermediate_value_Ioo {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ 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
source
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
source
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
source
theorem IsPreconnected.intermediate_value_Ioi {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ 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
source
theorem IsPreconnected.intermediate_value_Iio {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ 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
source
theorem IsPreconnected.intermediate_value_Iii {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set X} (hs : IsPreconnected s) {l₁ 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
source
theorem intermediate_value_univ {X : Type u} {α : Type v} [TopologicalSpace X] [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] [PreconnectedSpace 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.

source
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) :
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 `OrdConnected`, 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 _`.

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

source
theorem IsPreconnected.ordConnected {α : Type v} [LinearOrder α] [TopologicalSpace α] [OrderClosedTopology α] {s : Set α} (h : IsPreconnected s) :
s.OrdConnected
source
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.

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

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

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

source
theorem setOf_isPreconnected_subset_of_ordered {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] :
{s : Set α | 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 ∅, 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.

source
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 ∈ 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`.

source
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 ∈ s ∩ Set.Ico a b, ∀ 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`.

source
theorem IsClosed.mem_of_ge_of_forall_exists_lt {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {a b : α} {s : Set α} (hs : IsClosed (s ∩ Set.Icc a b)) (hb : b ∈ s) (hab : a ≤ b) (hgt : ∀ x ∈ s ∩ Set.Ioc a b, (s ∩ Set.Ico a x).Nonempty) :
a ∈ s

A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]` on a closed subset, contains `b`, and the set `s ∩ (a, b]` has no minimal point, then `a ∈ s`.

source
theorem IsClosed.Icc_subset_of_forall_exists_lt {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] {a b : α} {s : Set α} (hs : IsClosed (s ∩ Set.Icc a b)) (hb : b ∈ s) (hgt : ∀ x ∈ s ∩ Set.Ioc a b, ∀ y ∈ Set.Iio x, (s ∩ Set.Ico y x).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 `b`, and for any `a ≤ y < x ≤ b`, `x ∈ s`, the set `s ∩ [y, x)` is not empty, then `[a, b] ⊆ s`.

source
theorem IsClosed.Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} {s : Set α} (hs : IsClosed (s ∩ Set.Icc a b)) (ha : a ∈ s) (h : ∀ t ∈ Set.Ico a b, Set.Icc a t ⊆ s → s ∈ nhdsWithin t (Set.Ioi t)) :
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 ∈ [a, b)` such that `[a, x]` is included in `s`, the set `s` includes some open neighborhood of `x` within `(x, +∞)`, then `[a, b] ⊆ s`.

source
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 ∈ 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`.

source
theorem isPreconnected_Icc_aux {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} (x y : α) (s 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
source
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.

source
theorem isPreconnected_uIcc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} :
IsPreconnected (Set.uIcc a b)
source
theorem Set.OrdConnected.isPreconnected {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {s : Set α} (h : s.OrdConnected) :
IsPreconnected s
source
theorem isPreconnected_iff_ordConnected {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {s : Set α} :
IsPreconnected s ↔ s.OrdConnected
source
theorem isPreconnected_Ici {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} :
IsPreconnected (Set.Ici a)
source
theorem isPreconnected_Iic {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} :
IsPreconnected (Set.Iic a)
source
theorem isPreconnected_Iio {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} :
IsPreconnected (Set.Iio a)
source
theorem isPreconnected_Ioi {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} :
IsPreconnected (Set.Ioi a)
source
theorem isPreconnected_Ioo {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} :
IsPreconnected (Set.Ioo a b)
source
theorem isPreconnected_Ioc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} :
IsPreconnected (Set.Ioc a b)
source
theorem isPreconnected_Ico {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} :
IsPreconnected (Set.Ico a b)
source
theorem isConnected_Ici {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} :
IsConnected (Set.Ici a)
source
theorem isConnected_Iic {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} :
IsConnected (Set.Iic a)
source
theorem isConnected_Ioi {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} [NoMaxOrder α] :
IsConnected (Set.Ioi a)
source
theorem isConnected_Iio {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a : α} [NoMinOrder α] :
IsConnected (Set.Iio a)
source
theorem isConnected_Icc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} (h : a ≤ b) :
IsConnected (Set.Icc a b)
source
theorem isConnected_Ioo {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} (h : a < b) :
IsConnected (Set.Ioo a b)
source
theorem isConnected_Ioc {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} (h : a < b) :
IsConnected (Set.Ioc a b)
source
theorem isConnected_Ico {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α} (h : a < b) :
IsConnected (Set.Ico a b)
source
@[instance 100]
instance ordered_connected_space {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] :
PreconnectedSpace α
source
theorem setOf_isPreconnected_eq_of_ordered {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] :
{s : Set α | 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.

source
theorem isTotallyDisconnected_iff_lt {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {s : Set α} :
IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, 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.

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

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

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

source
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) :
∃ c ∈ Set.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]]`.

source
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) :
∃ c ∈ Set.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`.

source
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)) :
∃ c ∈ Set.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.

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

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

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

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

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

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

source
theorem Continuous.strictMono_of_inj_boundedOrder {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf : f ⊥ ≤ f ⊤) (hf_i : Function.Injective f) :
StrictMono f
source
theorem Continuous.strictAnti_of_inj_boundedOrder {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf : f ⊤ ≤ f ⊥) (hf_i : Function.Injective f) :
StrictAnti f
source
theorem Continuous.strictMono_of_inj_boundedOrder' {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] [BoundedOrder α] {f : α → δ} (hf_c : Continuous f) (hf_i : Function.Injective f) :
StrictMono f ∨ StrictAnti f
source
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)) :
StrictMono f

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

source
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)) :
StrictMonoOn f (Set.Icc a b)

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

source
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)) :
StrictAntiOn f (Set.Icc a b)

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

source
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)) :
StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b)

Suppose `f : [a, b] → δ` is continuous and injective. Then `f` is strictly monotone or antitone (increasing or decreasing).

source
theorem Continuous.strictMono_of_inj {α : Type u} [ConditionallyCompleteLinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {δ : Type u_1} [LinearOrder δ] [TopologicalSpace δ] [OrderClosedTopology δ] {f : α → δ} (hf_c : Continuous f) (hf_i : Function.Injective f) :
StrictMono f ∨ StrictAnti f

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

source
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)) :
StrictMonoOn f (Set.Ioo a b) ∨ StrictAntiOn f (Set.Ioo a b)

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