English
Same as above with strict inequalities: there exist a,b,c ∈ s with a < b and b < c and the same disjunction of inequalities on f-values.
Русский
Точно так же с неравенствами строго: существуют a,b,c ∈ s с a < b < c и та же дизъюнкция неравенств на значениях f.
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_lt_lt :
¬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_lt_lt, @and_left_comm (_ ∈ s)]
