Mapping_is_Constant_iff_Increasing_and_Decreasing
Disprovedconstant-mappingsdecreasing-mappingsincreasing-mappingsproofwiki
A mapping between ordered sets is constant if and only if it is both increasing and decreasing.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Mapping_is_Constant_iff_Increasing_and_Decreasing
{alpha beta : Type _} [Preorder alpha] [PartialOrder beta]
(f : alpha -> beta) :
(Monotone f /\ Antitone f) <-> (forall a b : alpha, f a = f b) := by sorrySource