# 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

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`

.

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`

.

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.

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.

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.

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.

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.

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`

.

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`

.

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

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.

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.

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.

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.

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`

.

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`

.

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`

.

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`

.

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`

.

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`

.

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

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.

An order isomorphism between two linear order `OrderTopology`

spaces is a homeomorphism.

## Equations

- e.toHomeomorph = { toEquiv := e.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }