Continuity of monotone functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
continuous_at_of_monotone_on_of_image_mem_nhds, as well as several similar facts.
We also prove that an order_iso 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 order_iso is continuous, hence it is a homeomorph. We prove
this for an order_iso between to partial orders with order topology.
An order isomorphism between two linear order order_topology spaces is a homeomorphism.
Equations
- e.to_homeomorph = {to_equiv := e.to_equiv, continuous_to_fun := _, continuous_inv_fun := _}