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 < b \land b < c \land \bigl( (f(a) < f(b) \land f(c) < f(b)) \lor (f(b) < f(a) \land f(b) < f(c)) \bigr).$$$
Lean4
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
theorem not_monotoneOn_not_antitoneOn_iff_exists_le_le :
¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
∃ᵉ (a ∈ s) (b ∈ s) (c ∈ s), a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) :=
by
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
not_monotone_not_antitone_iff_exists_le_le, @and_left_comm (_ ∈ s)]
