# Continuity of monotone functions #

In this file we prove the following fact: if `f` is a monotone function on a neighborhood of `a` and the image of this neighborhood is a neighborhood of `f a`, then `f` is continuous at `a`, see `continuousWithinAt_of_monotoneOn_of_image_mem_nhds`, as well as several similar facts.

We also prove that an `OrderIso` is continuous.

## Tags #

continuous, monotone

source
theorem StrictMonoOn.continuousWithinAt_right_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b) :
ContinuousWithinAt f (Set.Ici a) a

If `f` is a function strictly monotone on a right neighborhood of `a` and the image of this neighborhood under `f` meets every interval `(f a, b]`, `b > f a`, then `f` is continuous at `a` from the right.

The assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` is required because otherwise the function `f : ℝ → ℝ` given by `f x = if x ≤ 0 then x else x + 1` would be a counter-example at `a = 0`.

source
theorem continuousWithinAt_right_of_monotoneOn_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b) :
ContinuousWithinAt f (Set.Ici a) a

If `f` is a monotone function on a right neighborhood of `a` and the image of this neighborhood under `f` meets every interval `(f a, b)`, `b > f a`, then `f` is continuous at `a` from the right.

The assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b` cannot be replaced by the weaker assumption `hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b` we use for strictly monotone functions because otherwise the function `ceil : ℝ → ℤ` would be a counter-example at `a = 0`.

source
theorem continuousWithinAt_right_of_monotoneOn_of_closure_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : closure (f '' s) ∈ nhdsWithin (f a) (Set.Ici (f a))) :
ContinuousWithinAt f (Set.Ici a) a

If a function `f` with a densely ordered codomain is monotone on a right neighborhood of `a` and the closure of the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is continuous at `a` from the right.

source
theorem continuousWithinAt_right_of_monotoneOn_of_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : f '' s ∈ nhdsWithin (f a) (Set.Ici (f a))) :
ContinuousWithinAt f (Set.Ici a) a

If a function `f` with a densely ordered codomain is monotone on a right neighborhood of `a` and the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is continuous at `a` from the right.

source
theorem StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : closure (f '' s) ∈ nhdsWithin (f a) (Set.Ici (f a))) :
ContinuousWithinAt f (Set.Ici a) a

If a function `f` with a densely ordered codomain is strictly monotone on a right neighborhood of `a` and the closure of the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is continuous at `a` from the right.

source
theorem StrictMonoOn.continuousWithinAt_right_of_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : f '' s ∈ nhdsWithin (f a) (Set.Ici (f a))) :
ContinuousWithinAt f (Set.Ici a) a

If a function `f` with a densely ordered codomain is strictly monotone on a right neighborhood of `a` and the image of this neighborhood under `f` is a right neighborhood of `f a`, then `f` is continuous at `a` from the right.

source
theorem StrictMonoOn.continuousWithinAt_right_of_surjOn {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Ici a)) (hfs : Set.SurjOn f s (Set.Ioi (f a))) :
ContinuousWithinAt f (Set.Ici a) a

If a function `f` is strictly monotone on a right neighborhood of `a` and the image of this neighborhood under `f` includes `Ioi (f a)`, then `f` is continuous at `a` from the right.

source
theorem StrictMonoOn.continuousWithinAt_left_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)) :
ContinuousWithinAt f (Set.Iic a) a

If `f` is a strictly monotone function on a left neighborhood of `a` and the image of this neighborhood under `f` meets every interval `[b, f a)`, `b < f a`, then `f` is continuous at `a` from the left.

The assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)` is required because otherwise the function `f : ℝ → ℝ` given by `f x = if x < 0 then x else x + 1` would be a counter-example at `a = 0`.

source
theorem continuousWithinAt_left_of_monotoneOn_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)) :
ContinuousWithinAt f (Set.Iic a) a

If `f` is a monotone function on a left neighborhood of `a` and the image of this neighborhood under `f` meets every interval `(b, f a)`, `b < f a`, then `f` is continuous at `a` from the left.

The assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)` cannot be replaced by the weaker assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)` we use for strictly monotone functions because otherwise the function `floor : ℝ → ℤ` would be a counter-example at `a = 0`.

source
theorem continuousWithinAt_left_of_monotoneOn_of_closure_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (hf : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : closure (f '' s) ∈ nhdsWithin (f a) (Set.Iic (f a))) :
ContinuousWithinAt f (Set.Iic a) a

If a function `f` with a densely ordered codomain is monotone on a left neighborhood of `a` and the closure of the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is continuous at `a` from the left

source
theorem continuousWithinAt_left_of_monotoneOn_of_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : f '' s ∈ nhdsWithin (f a) (Set.Iic (f a))) :
ContinuousWithinAt f (Set.Iic a) a

If a function `f` with a densely ordered codomain is monotone on a left neighborhood of `a` and the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is continuous at `a` from the left.

source
theorem StrictMonoOn.continuousWithinAt_left_of_closure_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : closure (f '' s) ∈ nhdsWithin (f a) (Set.Iic (f a))) :
ContinuousWithinAt f (Set.Iic a) a

If a function `f` with a densely ordered codomain is strictly monotone on a left neighborhood of `a` and the closure of the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is continuous at `a` from the left.

source
theorem StrictMonoOn.continuousWithinAt_left_of_image_mem_nhdsWithin {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : f '' s ∈ nhdsWithin (f a) (Set.Iic (f a))) :
ContinuousWithinAt f (Set.Iic a) a

If a function `f` with a densely ordered codomain is strictly monotone on a left neighborhood of `a` and the image of this neighborhood under `f` is a left neighborhood of `f a`, then `f` is continuous at `a` from the left.

source
theorem StrictMonoOn.continuousWithinAt_left_of_surjOn {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhdsWithin a (Set.Iic a)) (hfs : Set.SurjOn f s (Set.Iio (f a))) :
ContinuousWithinAt f (Set.Iic a) a

If a function `f` is strictly monotone on a left neighborhood of `a` and the image of this neighborhood under `f` includes `Iio (f a)`, then `f` is continuous at `a` from the left.

source
theorem StrictMonoOn.continuousAt_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhds a) (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ico b (f a)) (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioc (f a) b) :
ContinuousAt f a

If a function `f` is strictly monotone on a neighborhood of `a` and the image of this neighborhood under `f` meets every interval `[b, f a)`, `b < f a`, and every interval `(f a, b]`, `b > f a`, then `f` is continuous at `a`.

source
theorem StrictMonoOn.continuousAt_of_closure_image_mem_nhds {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhds a) (hfs : closure (f '' s) ∈ nhds (f a)) :
ContinuousAt f a

If a function `f` with a densely ordered codomain is strictly monotone on a neighborhood of `a` and the closure of the image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is continuous at `a`.

source
theorem StrictMonoOn.continuousAt_of_image_mem_nhds {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : StrictMonoOn f s) (hs : s ∈ nhds a) (hfs : f '' s ∈ nhds (f a)) :
ContinuousAt f a

If a function `f` with a densely ordered codomain is strictly monotone on a neighborhood of `a` and the image of this set under `f` is a neighborhood of `f a`, then `f` is continuous at `a`.

source
theorem continuousAt_of_monotoneOn_of_exists_between {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhds a) (hfs_l : ∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)) (hfs_r : ∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b) :
ContinuousAt f a

If `f` is a monotone function on a neighborhood of `a` and the image of this neighborhood under `f` meets every interval `(b, f a)`, `b < f a`, and every interval `(f a, b)`, `b > f a`, then `f` is continuous at `a`.

source
theorem continuousAt_of_monotoneOn_of_closure_image_mem_nhds {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhds a) (hfs : closure (f '' s) ∈ nhds (f a)) :
ContinuousAt f a

If a function `f` with a densely ordered codomain is monotone on a neighborhood of `a` and the closure of the image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is continuous at `a`.

source
theorem continuousAt_of_monotoneOn_of_image_mem_nhds {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α} {a : α} (h_mono : MonotoneOn f s) (hs : s ∈ nhds a) (hfs : f '' s ∈ nhds (f a)) :
ContinuousAt f a

If a function `f` with a densely ordered codomain is monotone on a neighborhood of `a` and the image of this neighborhood under `f` is a neighborhood of `f a`, then `f` is continuous at `a`.

source
theorem Monotone.continuous_of_denseRange {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} (h_mono : Monotone f) (h_dense : DenseRange f) :
Continuous f

A monotone function with densely ordered codomain and a dense range is continuous.

source
theorem Monotone.continuous_of_surjective {α : Type u_1} {β : Type u_2} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [LinearOrder β] [TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} (h_mono : Monotone f) (h_surj : Function.Surjective f) :
Continuous f

A monotone surjective function with a densely ordered codomain is continuous.

### Continuity of order isomorphisms #

In this section we prove that an `OrderIso` is continuous, hence it is a `Homeomorph`. We prove this for an `OrderIso` between to partial orders with order topology.

source
theorem OrderIso.continuous {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
Continuous ⇑e
source
instance OrderIso.instHomeomorphClass {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] :
HomeomorphClass (α ≃o β) α β
source
@[reducible, inline]
abbrev OrderIso.toHomeomorph {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
α ≃ₜ β

An order isomorphism between two linear order `OrderTopology` spaces is a homeomorphism.

Equations

- e.toHomeomorph = ↑e

Instances For

source
theorem OrderIso.coe_toHomeomorph {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
⇑e.toHomeomorph = ⇑e
source
@[simp]
theorem OrderIso.coe_toHomeomorph_symm {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] [TopologicalSpace α] [TopologicalSpace β] [OrderTopology α] [OrderTopology β] (e : α ≃o β) :
⇑e.toHomeomorph.symm = ⇑e.symm