 Joshua Potter
|
4f8c3383f1
|
Update to lean v4.3.0
|
2023-12-14 13:29:09 -07:00 |
|
Joshua Potter
|
7959c474a0
|
Enderton (set). Fixup the pigeonhole principle.
|
2023-09-16 17:54:41 -06:00 |
|
Joshua Potter
|
1c988dc9e9
|
Update mathlib4 links to Lean's hosted index instead.
|
2023-08-10 11:31:14 -06:00 |
|
Joshua Potter
|
d89200fd9d
|
Simplify lean link formatting.
|
2023-08-09 10:07:18 -06:00 |
|
Joshua Potter
|
e8aa984b98
|
Add icon to distinguish Lean definitions from custom ones.
Update to pending any proofs that were using already defined Lean
proofs.
|
2023-08-08 20:50:31 -06:00 |
|
Joshua Potter
|
c3b579aed1
|
Drop placeholders prior to Mathlib4 port.
|
2023-07-26 13:41:55 -06:00 |
|
Joshua Potter
|
e3205a1e5d
|
Add hyperref linking and fix other refs.
|
2023-07-12 10:54:35 -06:00 |
|
Joshua Potter
|
66df65c14b
|
Update toolchain and deps.
|
2023-05-20 11:11:27 -06:00 |
|
Joshua Potter
|
9ac70c15c9
|
Normalize formatting further, macros for lean commands.
|
2023-05-17 12:28:02 -06:00 |
|
Joshua Potter
|
68d46e1a7d
|
Redefine an `Orthogonal` rectangle as a subtype of a `Skew` one.
|
2023-05-15 14:07:42 -06:00 |
|
Joshua Potter
|
96dd9b5669
|
Revise geometry with different types of rectangles and lines.
|
2023-05-15 06:40:35 -06:00 |
|
Joshua Potter
|
1cff1c63c4
|
Update simple sequence summation proofs as verified.
|
2023-05-13 10:11:23 -06:00 |
|
Joshua Potter
|
ddcb0f9717
|
Perform same aggregation on Enderton and Sequence tex files.
|
2023-05-13 06:59:28 -06:00 |
|
Joshua Potter
|
e7e657950b
|
Aggregate Apostol LaTeX into single file.
|
2023-05-13 06:38:55 -06:00 |
|
Joshua Potter
|
da7f00753b
|
Common coloring across definitions/axioms/statements.
|
2023-05-12 18:29:02 -06:00 |
|
Joshua Potter
|
f5dfb9ff6b
|
Generalize concept of partitions and step functions.
|
2023-05-12 13:17:34 -06:00 |
|
Joshua Potter
|
56751a6f3b
|
Use a consistent naming convention.
|
2023-05-12 11:08:52 -06:00 |
|
Joshua Potter
|
60724c0b52
|
Generalize set functions and move partitions in anticipation
of Apostol 1.11 exercise 8.
|
2023-05-12 07:05:31 -06:00 |
|
Joshua Potter
|
3d0dc2b926
|
Continuing working on Apostol 1.11 exercises.
|
2023-05-11 13:35:05 -06:00 |
|
Joshua Potter
|
50d6b13574
|
Remove no longer needed `hyperlabel` command.
|
2023-05-10 20:27:46 -06:00 |
|
Joshua Potter
|
53a0bd1ebc
|
Add "defined" status and distinguish Lean links.
|
2023-05-10 20:19:18 -06:00 |
|
Joshua Potter
|
cadb07018a
|
Add support for cross-referencing PDFs.
|
2023-05-10 18:27:55 -06:00 |
|
Joshua Potter
|
8c5029f8ec
|
Add TeX for axiomatic area definition.
|
2023-05-10 17:45:55 -06:00 |
|
Joshua Potter
|
5256c4e81a
|
Add concept of "verified" to statements/theorems.
|
2023-05-10 10:45:42 -06:00 |
|
Joshua Potter
|
ed89078e76
|
Apostol. Begin working through floor/ceiling exercises.
Also discovered the basic interval module so replaced custom
interval syntax with it.
|
2023-05-08 16:44:52 -06:00 |
|
Joshua Potter
|
b0a30ed4b4
|
Rename `Bookshelf` to `Common`.
|
2023-05-08 14:08:48 -06:00 |