Joshua Potter
cdba12f161
Drop Theorem 6A references.
2023-11-12 11:44:57 -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
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
66ca483671
Enderton (set). Isomorphism from ℕ to peano systems.
2023-09-09 05:15:52 -06:00
Joshua Potter
21a3e78106
Enderton (set). Continue refining ordering theorems/exercises.
2023-08-11 18:58:36 -06:00
Joshua Potter
83699dd58e
Enderton. Continue actually verifying set theorems.
2023-08-09 15:44:40 -06:00
Joshua Potter
7fe780e72f
Drop `Common.Set.Interval` and `Common.Set.Partition`.
2023-07-25 07:28:20 -06:00
Joshua Potter
db6074f1a1
Enderton. Peano postulate theorem/exercise drafts.
2023-07-23 12:13:24 -06:00
Joshua Potter
f328440797
Enderton. Peano systems.
2023-07-21 14:25:36 -06:00
Joshua Potter
dd4340c4bd
Move `OrderedPair` and `Relation` to Enderton.
...
These modules probably won't be very useful in general; there exist
better representations in Lean when dealing with ordered pairs or
relations already.
2023-06-29 15:25:59 -06:00
Joshua Potter
644660d197
Enderton. Verify theorem 3I.
2023-06-26 15:11:19 -06:00
Joshua Potter
9b6af648f2
Enderton. Theorem 3H and helper theorems.
2023-06-26 13:11:55 -06:00
Joshua Potter
931e617161
Enderton. Formally verify theorem 3G.
2023-06-26 07:08:25 -06:00
Joshua Potter
a6e6251627
Enderton. Continue through theorem 3 set.
2023-06-25 07:27:35 -06:00
Joshua Potter
27372eb160
Enderton. Add additional definitions and prove Theorem 3E.
2023-06-23 15:47:55 -06:00
Joshua Potter
8b5736397c
Enderton. Break out relations/ordered pairs. Exercise 6.7.
2023-06-20 15:02:09 -06:00
Joshua Potter
f5d1fc546a
Enderton. Move Kuratowski's definition of an ordered pair into chapter; not
...
likely to be used outside this book.
2023-06-10 16:02:22 -06:00
Joshua Potter
6d3a2d8ad0
Fix build errors in `Chapter_2.lean`.
2023-06-10 12:09:24 -06:00
Joshua Potter
64d8324657
Enderton. Finish exercises 5 in LaTeX.
2023-06-10 05:51:42 -06:00
Joshua Potter
ad3e31764b
Enderton. Exercise 5.(1|2a|2b).
2023-06-09 21:03:06 -06:00
Joshua Potter
49bd4871fe
Enderton. Theorem 3A.
2023-06-06 20:16:06 -06:00
Joshua Potter
2dff3f5794
Enderton. Chapter 2 exercises, 11-25.
2023-06-04 17:34:42 -06:00
Joshua Potter
4624d58924
Enderton. Continue proofs/exercises of "Axioms and Operations."
2023-05-23 15:38:33 -06:00
Joshua Potter
8279131d74
Enderton, basic axioms/unions exercises.
2023-05-21 18:32:59 -06:00
Joshua Potter
c0f8895686
Derive a more constructive `StepFunction` definition.
2023-05-15 13:37:01 -06:00
Joshua Potter
96dd9b5669
Revise geometry with different types of rectangles and lines.
2023-05-15 06:40:35 -06:00
Joshua Potter
3fc293579d
Add concept of glossary.
2023-05-12 19:31:44 -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