形式化大数数学（1.2-Veblen函数）一 (5-5)

定理 对于第一个参数为极限的情况, 我们对第二个参数分情况讨论, 由定义, 有以下等式成立.

φₗᵢₘ f，₀＝jump λβ，lim λn，φ f ₙ，ᵦ 0

φₗᵢₘ f，ᵦ⁺＝fixpt φlim f，ᵦ

φₗᵢₘ f，lim g＝jump λᵧ，lim λn，φₗᵢₘ f，g ₙ γ

φ-lim-0 : φ (lim f) 0 ≡ jump λ β → lim λ n → φ (f n) β 0

φ-lim-0 = refl

φ-lim-suc : φ (lim f) (suc β) ≡ fixpt (φ (lim f) β)

φ-lim-suc = refl

φ-lim-lim : φ (lim f) (lim g) ≡ jump λ γ → lim λ n → φ (lim f) (g n) γ

φ-lim-lim = refl

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。