1. The Result
How to read this document. A proof assistant will not let you skip a step, and it makes you write the missing premise into the theorem's own statement. So there is one fixed place to look. Read the statement, then read the definitions it names, and you have seen everything the result depends on. Two conditions sit one level down, inside the structures the theorem takes as arguments — and they are on the manifest too, because the command that derives it reads one level in. There is no longer anywhere for an assumption to sit unlisted.
Every docstring in this document is pulled out of the library when it is built. What you read is what was checked.
- 1.1. The horses
- 1.2. The finding
- 1.3. The other findings
- 1.4. The claims
- 1.5. The conditions
- 1.6. The theorems
- 1.7. The manifest
- 1.8. Mises's route
- 1.9. The circle
- 1.10. The ladder as a history
- 1.11. Exchange
- 1.12. Time preference
- 1.13. The regression theorem
- 1.14. The horses in Lean
- 1.15. The vocabulary
- 1.16. Claims no theorem uses