EDB — 1Y6

[1Y6] Given two sets \(A,B\), a function \(f:A→ B\) is a triple

(where \(A\) is said domain and \(B\) codomain) and \(F\) is a relation \(F⊆ A× B\) such that

i.e. it enjoys the properties of being functional and total (defined in [23X]↺↻).

Being the element \(y\) unique, we can write \(y=f(x)\) to say that \(y\) is the only element in relation \(xFy\) with \(x\).

The set \(F\) is also called graph of the function.