English
For a function f and a subset s, either f is monotone on s or antipone on s if and only if for every a,b,c in s with c in the unordered interval between a and b, f(c) lies in the unordered interval between f(a) and f(b).
Русский
Для функции f и множества s верно: либо f монотонна на s, либо антитонна на s, если и только если для любых a,b,c в s с c в неупорядоченном интервале между a и b выполняется f(c) в неупорядоченном интервале между f(a) и f(b).
LaTeX
$$$ (\\mathrm{MonotoneOn}\ f\ rsub s \\lor \\mathrm{AntitoneOn}\\ f\ rsub s) \\iff \\forall a,b,c\\ (a,b,c \\in s) , c \\in [[a,b]] \\implies f(c) \\in [[f(a),f(b)]] $$$
Lean4
theorem monotoneOn_or_antitoneOn_iff_uIcc :
MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ᵉ (a ∈ s) (b ∈ s) (c ∈ s), c ∈ [[a, b]] → f c ∈ [[f a, f b]] := by
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, monotone_or_antitone_iff_uIcc, mem_uIcc]
