ThmDex – An index of mathematical definitions, results, and conjectures.
Formulation F3893 on D428: Antitone map
F3893
Formulation 1
Let $P_X = (X, {\preceq_X})$ and $P_Y = (Y, {\preceq_Y})$ each be a D1103: Partially ordered set.
A D18: Map $f : X \to Y$ is antitone from $P_X$ to $P_Y$ if and only if \begin{equation} \forall \, x, y \in X \left( x \preceq_X y \quad \implies \quad f(y) \preceq_Y f(x) \right) \end{equation}