Mathematics in Lean

• 1. 引言
  • 1.1. 入门指南
  • 1.2. 概述
• 2. 基础
  • 2.1. 计算
  • 2.2. 证明代数结构中的等式
  • 2.3. 使用定理和引理
  • 2.4. apply 和 rw 的更多例子
  • 2.5. 证明关于代数结构的命题
• 3. 逻辑
  • 3.1. 蕴含和全称量词
  • 3.2. 存在量词
  • 3.3. 否定
  • 3.4. 合取和双向蕴含
  • 3.5. 析取
  • 3.6. 序列和收敛
• 4. 集合和函数
  • 4.1. 集合
  • 4.2. 函数
  • 4.3. 施罗德-伯恩斯坦定理
• 5. 初等数论
  • 5.1. 无理数根
  • 5.2. 归纳与递归
  • 5.3. 无穷多个素数
• 6. 结构体（Structures）
  • 6.1. 定义结构体
  • 6.2. 代数结构
  • 6.3. 构建高斯整数
• 7. 层次结构
  • 7.1. 基础
  • 7.2. 态射
  • 7.3. 子对象
• 8. 群与环
  • 8.1. 幺半群与群
  • 8.2. 环
• 9. Linear algebra
  • 9.1. Vector spaces and linear maps
  • 9.2. Subspaces and quotients
  • 9.3. Endomorphisms
  • 9.4. Matrices, bases and dimension
• 10. 拓扑学
  • 10.1. 滤子
  • 10.2. 度量空间
  • 10.3. 拓扑空间
• 11. 微分学
  • 11.1. 初等微分学
  • 11.2. 赋范空间中的微分学
• 12. 积分和测度论
  • 12.1. 初等积分
  • 12.2. 测度论
  • 12.3. 积分