数学联邦政治世界观
超小超大

形式化大数数学(1.2-Veblen函数)二 (2-1)

定义 四元Veblen函数‬

φ:=Φ Tri. φ

φ : Ord → Ord → Ord → Ord → Ord

φ = Φ Tri.φ

例 第一个参数从无效到刚开始生效, 由定义, 有以下等式成立.

φ₀=Tri. φ

φ₁,₀,₀=fixpt λα,Tri. φα,₀ 0

φ-0 : φ 0 ≡ Tri.φ

φ-0 = refl

φ-1-0-0 : φ 1 0 0 ≡ fixpt (λ α → Tri.φ α 0 0)

φ-1-0-0 = refl

定理 中间两个参数为零, 讨论第一个参数为后继和极限的情况, 由定义, 有以下等式成立.

φα⁺,₀,₀=fixpt λβ,φα,ᵦ,₀ 0

φₗᵢₘ f,₀,₀=jump λβ,lim λn,φ f ₙ,ᵦ,₀ 0

φ-suc-0-0 : φ (suc α) 0 0 ≡ fixpt λ β → φ α β 0 0

φ-suc-0-0 = refl

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

φ-lim-0-0 = refl

定理 将 φα 看作一个固定的函数, 类似地, 有以下等式成立.

φα,ᵦ⁺,₀=fixpt λᵧ,φα,ᵦ,ᵧ 0

φα,ₗᵢₘ g,₀=jump λᵧ,lim λn,φα,g ₙ,ᵧ 0

φ-α-suc-0 : φ α (suc β) 0 ≡ fixpt λ γ → φ α β γ 0

φ-α-suc-0 {α = zero} = refl

φ-α-suc-0 {α = suc _} = refl

φ-α-suc-0 {α = lim f} = refl

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

φ-α-lim-0 {α = zero} = refl

φ-α-lim-0 {α = suc _} = refl

φ-α-lim-0 {α = lim f} = refl

定理 将 φα,ᵦ 看作一个固定的函数, 类似地, 有以下等式成立.

φα,ᵦ,ᵧ⁺=fixpt φα,ᵦ,ᵧ

φα,ᵦ,ₗᵢₘ ₕ=jump λδ,lim λn,φα,ᵦ,ₕ ₙ δ

φ-α-β-suc : φ α β (suc γ) ≡ fixpt (φ α β γ)

φ-α-β-suc {α = zero} {β = zero} = refl

φ-α-β-suc {α = zero} {β = suc _} = refl

φ-α-β-suc {α = zero} {β = lim _} = refl

φ-α-β-suc {α = suc _} {β = zero} = refl

φ-α-β-suc {α = suc _} {β = suc _} = refl

φ-α-β-suc {α = suc _} {β = lim _} = refl

φ-α-β-suc {α = lim _} {β = zero} = refl

φ-α-β-suc {α = lim _} {β = suc _} = refl

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

相关小说

爱留恋一世 连载中
爱留恋一世
倾倾墨秦
爱情
0.2万字9个月前
快穿之梦境奇遇记 连载中
快穿之梦境奇遇记
柠柒念
一次意外的相遇,使两个不同世界的人有了交际。命运的齿轮不断转动,原来的轨迹早已改变。一场场梦境之旅就此展开。第一个梦境:神医王妃第二个梦境:......
17.9万字9个月前
魔女成长笔记 连载中
魔女成长笔记
盈清晚
剧情奇葩,作者鸽子,女主心机,剧情感情各占一半夏清涟习惯了算计和演戏在这个世界单纯的人都没有什么好的经历要能被反复伤害,要么被杀死某男配表示......
12.9万字9个月前
ALL祺:朱雀 连载中
ALL祺:朱雀
结绮
不能透露剧情的哦,可以猜一猜,期待的收藏哦!作者学生,要写作业,可能不会天天更,有时间给你们更!
0.7万字9个月前
救赎与浮生 连载中
救赎与浮生
一颗圆白菜er
被世界掌控的女孩桑元和神明顾白相互救赎,相互陪伴的故事。桑元本以为陈景泽会是她唯一一个爱的人。“又木棉花开,晓这浮生的若梦,你是我的无法救赎......
3.6万字9个月前
ch法英花香满醉心中人 连载中
ch法英花香满醉心中人
棕色的药丸
法英虐文,不会太刀,后面甜的
0.2万字9个月前