可构造宇宙满足 GCH

前几章已经建立了比较无穷内部基数的幂集与其后继基数所需的三项估计。它们与 L 上的 ZF 模型结构合在一起，证明可构造宇宙满足广义连续统假设。唯一的经典假设，仍是构造该模型及其内部基数理论时始终采用的同一个排中律实例。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.GCH.Theorem {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import L.Model {ℓ} lem using ( L⊨ZF )

目标是 GCHStatement L⊨ZF。它量化 L 中这样的 κ：其底层集合是序数，κ 是内部基数，并且 κ ∉ ω。结论仅仅要求存在后继基数 δ，以及 𝒫 κ 与 δ 之间两个方向的内部编码单射；这里的幂集由 L⊨ZF 确定。

open import L.GCH {ℓ} lem using ( GCHStatement )
open import L.GCH.Assembly {ℓ} lem using ( gch-from-internal-bill )
open import L.GCH.StageInjection {ℓ} lem using ( stage-counted )
open import L.GCH.SuccessorIntoPowerSet {ℓ} lem using ( succ-into-power )
open import L.GCH.BoundedSubset {ℓ} lem using ( internal-bounded-subset )

固定这样的 κ。一般蕴涵先取得它的内部后继基数 δ。对每个 y ∈ 𝒫 κ，有界子集定理给出序数 β，使 y ∈ Lset β 且 β 单射入 κ。δ 是内部基数且 κ ∈ δ，这些事实与序数三分法合起来迫使 β ∈ δ，因而 y ∈ Lset δ。于是整个幂集先单射入 Lset δ，层计数定理再把这一层单射入 δ，得到 InjL (𝒫 κ) δ。最后，succ-into-power 利用 κ 的无穷性和 δ 的后继基数性质，把这一比较转化为 InjL δ (𝒫 κ)。两个方向的单射给出所需的 GCH 实例，并记作 L⊨GCH。

L⊨GCH : GCHStatement L⊨ZF
L⊨GCH = gch-from-internal-bill L⊨ZF stage-counted internal-bounded-subset
          (succ-into-power L⊨ZF)