A function $f$ is a mapping / [[Relation]] between an input [[Set]] ([[Domain]]) to an output [[Set]] ([[Codomain]]).
To denote a function that maps the [[Domain]] $X$ to the [[Codomain]] $Y$.
$\huge
\huge f: X\mapsto Y
$
#### Formal
A [[Function]] with [[Domain]] $X$ and [[Codomain]] $Y$ is a [[Binary Relation]] $R$ between $X$ and $Y$ that satisfies:
- $\forall x\in X$ there exists $\exists y\in Y$ such that $(x, y) \in R$.
- If $(x,y)\in R$ and $(x,z)\in R$, then $y=z$.