At the end of [12.2.4](https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf#subsection.12.2.4) there are four examples about local inverses. Before those examples, change "The next one states" to " The next ones state". In the fourth example, the assumptions "`{f : E → F} {f' : E 'L[ℸ] F} {a : E}`" could be dropped.
At the end of 12.2.4 there are four examples about local inverses.
Before those examples, change "The next one states" to " The next ones state".
In the fourth example, the assumptions "
{f : E → F} {f' : E 'L[ℸ] F} {a : E}" could be dropped.