Minimum function

Set

 context $X$ context $\le$ … non-strict partial order over $X$
 definiendum $\mathrm{max}:X\times X\to X$ definiendum $\mathrm{max}(x,y) := \begin{cases} x & \mathrm{if}\ x\le y\\\\ y & \mathrm{else} \end{cases}$