Maximum 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}\ y\le x\\\\ y & \mathrm{else} \end{cases}$
Discussion
Parents
Context
Non-strict partial order
Element of
Binary operation