Content
@
0 reply
0 recast
0 reaction
Agost Biro
@agostbiro
Did a few more exercises in the Logic section of Mathematics in Lean. I like that they're introducing a bit of analysis with monotone and even/odd functions in this section to make it less dry. The exercises went quickly as I managed to guess the required theorem names the first or second time. This was previously a source of frustration, but it looks like I'm getting the hang of it. The naming is logical. One interesting bit is that I managed to write a simpler solution than the book for one of the exercises (dark picture is mine and bright is the book). The reason is probably the pattern matching in the rewrite tactic becoming more powerful since the book was written. https://github.com/agostbiro/mathematics_in_lean/commit/f0e5f3b3d40f3ca7d8b7810f7e58b49d24196021
0 reply
2 recasts
3 reactions
