# 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, +∞)`

. This is a special case
of a more general statement where one deduces monotonicity on a union from monotonicity on each
set.

If `f`

is strictly monotone both on `s`

and `t`

, with `s`

to the left of `t`

and the center
point belonging to both `s`

and `t`

, then `f`

is strictly monotone on `s ∪ t`

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 `s`

and `t`

, with `s`

to the left of `t`

and the center
point belonging to both `s`

and `t`

, then `f`

is strictly antitone on `s ∪ t`

If `f`

is strictly antitone both on `(-∞, a]`

and `[a, ∞)`

, then it is strictly antitone on the
whole line.

If `f`

is monotone both on `s`

and `t`

, with `s`

to the left of `t`

and the center
point belonging to both `s`

and `t`

, then `f`

is monotone on `s ∪ t`

If `f`

is monotone both on `(-∞, a]`

and `[a, ∞)`

, then it is monotone on the whole line.

If `f`

is antitone both on `s`

and `t`

, with `s`

to the left of `t`

and the center
point belonging to both `s`

and `t`

, then `f`

is antitone on `s ∪ t`

If `f`

is antitone both on `(-∞, a]`

and `[a, ∞)`

, then it is antitone on the whole line.