 Joshua Potter
|
4f8c3383f1
|
Update to lean v4.3.0
|
2023-12-14 13:29:09 -07:00 |
|
Joshua Potter
|
cdba12f161
|
Drop Theorem 6A references.
|
2023-11-12 11:44:57 -07:00 |
|
Joshua Potter
|
b596478a36
|
More LaTeX proof embedding. Finish up "Set Difference Size".
|
2023-11-12 11:21:00 -07:00 |
|
Joshua Potter
|
f215a3180a
|
Enderton (set). Chapter 6 formatting.
More consistent header levels throughout.
|
2023-11-11 15:15:03 -07:00 |
|
Joshua Potter
|
b97b8fbbca
|
Use swap theorems in pigeonhole principle proof.
Establish precedent for embedding LaTeX proof into code.
|
2023-11-11 09:48:12 -07:00 |
|
Joshua Potter
|
857d0ea83e
|
Enderton (Set). Additions to exercise set 6. (#8)
|
2023-11-10 10:02:25 -07:00 |
|
Joshua Potter
|
edef7e9b58
|
Enderton (set). Partially work on finite set exercises.
|
2023-09-27 19:32:50 -06:00 |
|
Joshua Potter
|
2a85d526d7
|
Enderton (set). Finish equinumerosity theorems.
|
2023-09-19 08:39:34 -06:00 |
|
Joshua Potter
|
7959c474a0
|
Enderton (set). Fixup the pigeonhole principle.
|
2023-09-16 17:54:41 -06:00 |
|
Joshua Potter
|
f1a10c6877
|
Enderton (set). Wrap original pigeonhole expression into aux.
|
2023-09-14 10:00:39 -06:00 |
|
Joshua Potter
|
91fc8436da
|
Prove the pigeonhole principle. (#7)
|
2023-09-14 09:00:28 -06:00 |
|
Joshua Potter
|
3bf6f13055
|
Enderton (set). Add Lean scaffolding for finite set theorems/bijections.
|
2023-08-26 18:43:44 -06:00 |
|
Joshua Potter
|
306acd2975
|
Enderton (set). Begin adding Chapter 6 lean theorems.
|
2023-08-23 18:23:28 -06:00 |
|
Joshua Potter
|
f990a7a30a
|
Enderton. Reorder theorems in Lean modules and add set/logic prompts.
|
2023-08-17 18:04:20 -06:00 |
|
Joshua Potter
|
2c1547aee9
|
Enderton (set). Equinumerosity theorems.
|
2023-08-17 12:56:39 -06:00 |
|
Joshua Potter
|
8f833f9353
|
Enderton (set). Begin chapter 6 exercises.
|
2023-08-16 12:46:16 -06:00 |