Monotonicity on intervals #
In this file we prove that a function is (strictly) monotone (or antitone) on a linear order α
provided that it is (strictly) monotone on (-∞, a]
and on [a, +∞)
. We also provide an order
isomorphism order_iso_Ioo_neg_one_one
between the open interval (-1, 1)
in a linear ordered
field and the whole field.
If f
is strictly monotone both on (-∞, a]
and [a, ∞)
, then it is strictly monotone on the
whole line.
If f
is strictly antitone both on (-∞, a]
and [a, ∞)
, then it is strictly antitone on the
whole line.
In a linear ordered field, the whole field is order isomorphic to the open interval (-1, 1)
.
We consider the actual implementation to be a "black box", so it is irreducible.
A function ψ
on a succ_order
is strictly monotone before some n
if for all m
such that
m < n
, we have ψ m < ψ (succ m)
.