编辑“︁Lean序数与基数”︁（章节）

== 实际案例 ==  

=== 案例1：序数算术 ===  
在游戏理论中，序数用于描述无限回合的顺序。例如，`ω + 1`表示无限回合后追加一个回合：  
<mermaid>  
graph LR  
    A[回合0] --> B[回合1] --> C[回合2] --> D[...] --> E[回合ω] --> F[回合ω+1]  
</mermaid>  

=== 案例2：基数比较 ===  
验证两个集合的等势性：  
<syntaxhighlight lang="lean">  
import Mathlib.Data.Real.Basic  

-- 证明整数集与自然数集等势  
theorem Z_equiv_N : Cardinal.mk ℤ = Cardinal.mk ℕ := by  
  apply Cardinal.eq.2  
  exact ⟨⟨Int.toNat, Int.toNat_injective⟩⟩  
</syntaxhighlight>  

'''解释'''：通过构造双射函数（如整数到自然数的映射），证明两者基数相同。