Lean 序数与基数
引言
在数学中，序数和基数是描述集合顺序和大小的基本概念。序数用于表示顺序，而基数用于表示数量。在Lean中，这些概念被形式化并用于证明和构建数学理论。本文将带你了解Lean中的序数与基数，并通过代码示例和实际案例帮助你理解它们的应用。
什么是序数？
序数是用来表示顺序的数。例如，自然数 1, 2, 3, ... 可以看作是序数，因为它们表示了一个顺序。在Lean中，序数被定义为一种特殊的集合，具有以下性质：
- 传递性：如果
x是y的元素，且y是序数，那么x也是序数。 - 良序性：序数的元素在某种顺序下是良序的。
代码示例：定义序数
在Lean中，序数可以通过以下方式定义：
import set_theory.ordinal
def my_ordinal : ordinal := ω + 1
这里，ω 表示最小的无限序数，即自然数的序数。ω + 1 表示在自然数之后添加一个元素。
什么是基数？
基数是用来表示集合大小的数。例如，集合 {a, b, c} 的基数是 3，因为它有三个元素。在Lean中，基数被定义为序数的等价类，其中两个序数是等价的，如果它们之间存在一个双射。
代码示例：定义基数
在Lean中，基数可以通过以下方式定义：
import set_theory.cardinal
def my_cardinal : cardinal := ℵ₀
这里，ℵ₀ 表示最小的无限基数，即自然数的基数。
序数与基数的关系
序数和基数之间有着密切的关系。每个基数都可以看作是一个特殊的序数，即最小的序数，其大小等于该基数。例如，基数 ℵ₀ 对应的序数是 ω。
代码示例：序数与基数的转换
在Lean中，可以通过以下方式将序数转换为基数：
import set_theory.ordinal
import set_theory.cardinal
def my_ordinal_to_cardinal : cardinal := cardinal.mk my_ordinal
这里，cardinal.mk 函数将序数转换为基数。
实际应用案例
案例1：无限集合的比较
在数学中，我们经常需要比较无限集合的大小。例如，自然数集和实数集的基数不同。自然数集的基数是 ℵ₀，而实数集的基数是 2^ℵ₀。
案例2：序数在递归定义中的应用
在编程中，序数可以用于递归定义。例如，定义一个函数，它在每个序数上执行不同的操作。
def recursive_function : ordinal → ℕ
| 0 := 0
| (ordinal.succ n) := recursive_function n + 1
| (ordinal.limit f) := ⨆ (i : ℕ), recursive_function (f i)
这里，ordinal.succ 表示序数的后继，ordinal.limit 表示序数的极限。
总结
序数和基数是数学中描述顺序和大小的重要概念。在Lean中，这些概念被形式化并用于证明和构建数学理论。通过本文的学习，你应该对Lean中的序数与基数有了初步的了解，并能够通过代码示例和实际案例应用这些概念。
附加资源与练习
- 练习1：尝试在Lean中定义一个序数，并将其转换为基数。
- 练习2：编写一个递归函数，使用序数作为参数。
- 附加资源：阅读Lean官方文档中关于序数和基数的部分，进一步深入学习这些概念。
如果你在学习过程中遇到困难，可以尝试在Lean社区中寻求帮助，或者参考相关的数学教材。