Section 3 : functions
=====================

This short section is an introduction to "abstract" functions in Lean. We've seen functions from the naturals to the reals, but here we'll be talking about functions between types ``X`` and ``Y``.

Lean is a functional programming language, and functional programmers realised a long time ago that brackets which mathematicians put into their work are often not necessary. If ``f : X  → Y`` and ``x : X`` then write ``f x`` in Lean instead of ``f(x)`` (which doesn't actually work
in Lean at all). Brackets can be used -- but you have to leave a space (so ``f (x)``) and they are optional anyway.

Be warned though -- functions in Lean are *greedy*: they will eat the next thing they see. For example ``f n + 1`` means ``(f n) + 1`` and not ``f (n + 1)``. If you want ``f (n+1)`` then you need to use the brackets. Similarly, composite of functions ``f : X  → Y`` and ``g : Y  → Z`` evaluated at ``x : X`` needs to be written ``g (f x)`` otherwise ``g`` would eat ``f`` and then choke because ``f`` doesn't have the right type.

The problem sheets
------------------

For the first sheet you should be able to get away with what you already know. In the second one I explain how to make types with finitely many terms, and how to make functions from these types. In the last sheet I show how to use these to make counterexamples to various assertions about injective and surjective functions.