Monotonicity on intervals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that
set.Ici etc are monotone/antitone functions. We also prove some lemmas
about functions monotone on intervals in
ψ on a
succ_order is strictly monotone before some
n if for all
m such that
m < n, we have
ψ m < ψ (succ m).