The workhorses of mathematics
The basic idea of a function is simple: it takes some input and converts it to some output. Its simplicity results in robustness of applications.
We have already seen in Lean how functions are a basic ingredient used to represent implication, universal quantification, predicates,…
Due to our familiarity, we will reverse the previous order of presentation and discuss functions in Lean first. Later we will turn to definition so functions in term of sets.