English
A function that is neither monotone nor antitone yields a triple a < b < c with either f(a) < f(b) and f(c) < f(b), or f(b) < f(a) and f(b) < f(c).
Русский
Функция, которая не монотонна и не антимонотонна, порождает тройку a < b < c с одними из двух вариантов неравенств на образах.
LaTeX
$$$ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) $$$
Lean4
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
theorem not_monotone_not_antitone_iff_exists_lt_lt :
¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c) :=
by
simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]
refine exists₃_congr (fun a b c ↦ and_congr_left <| fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_) <;>
(rintro rfl; simp at h)
