English
If a function is monotone on a directed subset, and also antitone on that subset, it is constant on that subset.
Русский
Если функция монотонна и антимонотонна на направленном подмножстве, она константна на этом подмножестве.
LaTeX
$$$\forall f:\alpha\to \beta, \forall s\subseteq \alpha, IsMonotoneOn f s \land IsAntitoneOn f s \land DirectedOn (\le) s \Rightarrow \forall a\in s, \forall b\in s, f(a)=f(b).$$$
Lean4
/-- If `f` is monotone and antitone on a directed order, then `f` is constant. -/
theorem constant_of_monotone_antitone [IsDirected α (· ≤ ·)] (hf : Monotone f) (hf' : Antitone f) (a b : α) :
f a = f b := by
obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
exact le_antisymm ((hf hac).trans <| hf' hbc) ((hf hbc).trans <| hf' hac)
