-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathLeanUA.lean
More file actions
33 lines (25 loc) · 902 Bytes
/
LeanUA.lean
File metadata and controls
33 lines (25 loc) · 902 Bytes
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
/-
Main module for LeanUA project
This imports all the chapter modules for Understanding Analysis
-/
import LeanUA.Basic
-- import LeanUA.Chapter01.Basic
-- import LeanUA.Chapter02.Basic
-- Add more chapter imports as you create them
/-!
# Understanding Analysis in Lean 4
This is the main entry point for the LeanUA project.
Each chapter from Stephen Abbott's "Understanding Analysis" is formalized
in separate modules.
## How to use this project:
1. Start with Chapter 1 to understand the basic setup
2. Work through proofs systematically
3. Use `sorry` as placeholders for proofs you want to complete later
4. Build the project with `lake build` to check for errors
## Lean 4 Tips:
- Use `#check` to examine types
- Use `#print` to see definitions
- Use `example` for practice proofs
- Use `theorem` for named results you want to reuse
- Use `-- TODO:` comments to mark incomplete work
-/