Monotone functions on an order topology #
This file contains lemmas about limits and continuity for monotone / antitone functions on
linearly-ordered sets (with the order topology). For example, we prove that a monotone function
has left and right limits at any point (Monotone.tendsto_nhdsLT
, Monotone.tendsto_nhdsGT
).
If a function is monotone on a set in a second countable topological space, then there are only countably many points that have several preimages.
If a function is monotone in a second countable topological space, then there are only countably many points that have several preimages.
If a function is antitone on a set in a second countable topological space, then there are only countably many points that have several preimages.
If a function is antitone in a second countable topological space, then there are only countably many points that have several preimages.
In a second countable space, the set of points where a monotone function is not right-continuous
within a set is at most countable. Superseded by MonotoneOn.countable_not_continuousWithinAt
which gives the two-sided version.
In a second countable space, the set of points where a monotone function is not left-continuous
within a set is at most countable. Superseded by MonotoneOn.countable_not_continuousWithinAt
which gives the two-sided version.
In a second countable space, the set of points where a monotone function is not continuous within a set is at most countable.
In a second countable space, the set of points where a monotone function is not continuous is at most countable.
In a second countable space, the set of points where an antitone function is not continuous within a set is at most countable.
In a second countable space, the set of points where an antitone function is not continuous is at most countable.
A monotone function continuous at the supremum of a nonempty set sends this supremum to the supremum of the image of this set.
A monotone function continuous at the supremum of a nonempty set sends this supremum to the supremum of the image of this set.
A monotone function continuous at the indexed supremum over a nonempty Sort
sends this indexed
supremum to the indexed supremum of the composition.
A monotone function continuous at the infimum of a nonempty set sends this infimum to the infimum of the image of this set.
A monotone function continuous at the infimum of a nonempty set sends this infimum to the infimum of the image of this set.
A monotone function continuous at the indexed infimum over a nonempty Sort
sends this indexed
infimum to the indexed infimum of the composition.
An antitone function continuous at the infimum of a nonempty set sends this infimum to the supremum of the image of this set.
An antitone function continuous at the infimum of a nonempty set sends this infimum to the supremum of the image of this set.
An antitone function continuous at the indexed infimum over a nonempty Sort
sends this indexed
infimum to the indexed supremum of the composition.
An antitone function continuous at the supremum of a nonempty set sends this supremum to the infimum of the image of this set.
An antitone function continuous at the supremum of a nonempty set sends this supremum to the infimum of the image of this set.
An antitone function continuous at the indexed supremum over a nonempty Sort
sends this
indexed supremum to the indexed infimum of the composition.
A monotone function f
sending bot
to bot
and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set.
A monotone function f
sending bot
to bot
and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set.
If a monotone function sending bot
to bot
is continuous at the indexed supremum over
a Sort
, then it sends this indexed supremum to the indexed supremum of the composition.
A monotone function f
sending top
to top
and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set.
A monotone function f
sending top
to top
and continuous at the infimum of a set sends
this infimum to the infimum of the image of this set.
If a monotone function sending top
to top
is continuous at the indexed infimum over
a Sort
, then it sends this indexed infimum to the indexed infimum of the composition.
An antitone function f
sending bot
to top
and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set.
An antitone function f
sending bot
to top
and continuous at the supremum of a set sends
this supremum to the infimum of the image of this set.
An antitone function sending bot
to top
is continuous at the indexed supremum over
a Sort
, then it sends this indexed supremum to the indexed supremum of the composition.
An antitone function f
sending top
to bot
and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set.
An antitone function f
sending top
to bot
and continuous at the infimum of a set sends
this infimum to the supremum of the image of this set.
If an antitone function sending top
to bot
is continuous at the indexed infimum over
a Sort
, then it sends this indexed infimum to the indexed supremum of the composition.
Alias of MonotoneOn.tendsto_nhdsLT
.
Alias of MonotoneOn.tendsto_nhdsGT
.
A monotone map has a limit to the left of any point x
, equal to sSup (f '' (Iio x))
.
Alias of Monotone.tendsto_nhdsLT
.
A monotone map has a limit to the left of any point x
, equal to sSup (f '' (Iio x))
.
A monotone map has a limit to the right of any point x
, equal to sInf (f '' (Ioi x))
.
Alias of Monotone.tendsto_nhdsGT
.
A monotone map has a limit to the right of any point x
, equal to sInf (f '' (Ioi x))
.
Alias of AntitoneOn.tendsto_nhdsLT
.
Alias of AntitoneOn.tendsto_nhdsGT
.
An antitone map has a limit to the left of any point x
, equal to sInf (f '' (Iio x))
.
Alias of Antitone.tendsto_nhdsLT
.
An antitone map has a limit to the left of any point x
, equal to sInf (f '' (Iio x))
.
An antitone map has a limit to the right of any point x
, equal to sSup (f '' (Ioi x))
.
Alias of Antitone.tendsto_nhdsGT
.
An antitone map has a limit to the right of any point x
, equal to sSup (f '' (Ioi x))
.