English
If f is neither monotone nor antitone on s (in a linear order), there exist a,b,c ∈ s with a ≤ b ≤ c such that either f(a) < f(b) and f(c) < f(b) or f(b) < f(a) and f(b) < f(c).
Русский
Если функция f на линейном порядке не монотонна и не антимонотонна на s, то существуют a,b,c ∈ s такие, что a ≤ b ≤ c и выполняется либо f(a) < f(b) и f(c) < f(b), либо f(b) < f(a) и f(b) < f(c).
LaTeX
$$$ \neg \operatorname{MonotoneOn}(f,s) \land \neg \operatorname{AntitoneOn}(f,s) \iff \exists a,b,c \in s,\ a \le b \land b \le c \land \bigl( (f(a) < f(b) \land f(c) < f(b)) \lor (f(b) < f(a) \land f(b) < f(c)) \bigr).$$$
Lean4
theorem strictAntiOn_iff_strictAnti : StrictAntiOn f s ↔ StrictAnti fun a : s => f a := by
simp [StrictAnti, StrictAntiOn]
