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}$

Discussion

Parents

Context

Non-strict partial order

Element of

Binary operation

Maximum function