---
title: "L 内部的 Cantor–Schröder–Bernstein 定理"
module: L.CantorBernstein
lang: zh
site: "Bedrock"
description: "L 内部的 Cantor–Schröder–Bernstein 定理"
stage: "序数、单射与基数"
reading_order: 94
canonical: https://bedrock.institute/zh/L.CantorBernstein.html
html: L.CantorBernstein.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/CantorBernstein.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.CantorBernstein, L.Constructible, L.Cardinal, L.Coding.Injection]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.CantorBernstein.md, https://bedrock.institute/ja/L.CantorBernstein.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L 内部的 Cantor–Schröder–Bernstein 定理

设两个可构造集合之间存在双向的编码单射，那么它们的成员类型之间仅仅存在一个双射。这是本章采用的 Cantor–Schröder–Bernstein 定理的内部形式：假设用 `L` 的语言表述，所得双射则比较这两个集合对应的普通类型。

论证在两个层面之间进行。`L` 的集合带有外围累积层级中的底层集合，其成员组成普通类型 `⟪ fst a ⟫`。编码单射属于对象理论，而这些成员类型之间的函数属于元理论。

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
```

要使用类型层的定理，每个成员类型都必须是h-集合。累积层级已经保证这一性质：两个成员之间的路径不再含有更高层的额外信息。因此，`setPL` 为每个呈现给出所需的h-集合证书。

```agda
open import V.CantorBernstein {ℓ} (lowerLEM lem)
  using ( small-set; module MutualInj )
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.Coding.Injection {ℓ} lem using ( module Small )
```

一个单射码由一个可构造图、三条满足事实和一条值域条件组成。它们分别说明该图是单值的、具有指定定义域、满足单射性，并把每个输入送入指定陪域。这些条件恰好足以恢复一条元理论中的单射。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open hPropStructure 𝒮ʟ using ( S )
setPL : (a : S) → isSet (⟪ fst a ⟫)
```

函数 `readL` 完成这一转换。给定从 `a` 到 `b` 的编码图，它返回一个从 `a` 的成员到 `b` 的成员的实际函数，并证明输出相等必有输入相等。这一构造来自前面对编码单射的分析。

```agda
setPL a = small-set (fst a)
readL : (a b : S) → Σ[ F ∈ S ] InjCode F a b
      → Σ[ f ∈ (⟪ fst a ⟫ → ⟪ fst b ⟫) ]
          ((x y : ⟪ fst a ⟫) → f x ≡ f y → x ≡ y)
readL a b (F , sv , dm , ij , ran) = SM.small , SM.small-inj
```

现在可以把抽象的 Cantor–Schröder–Bernstein 论证应用于这一情形：对象取可构造集合，呈现取其成员类型，单射取编码图。h-集合证书与 `readL` 验证了所需的两项结构条件。同一次实例化既给出使用显式见证的版本，也给出仅仅假定见证存在的版本。

```agda
  where
  module SM = Small F a b sv dm ij ran

module MutualInjL = MutualInj S (λ a → ⟪ fst a ⟫)
  (λ a b → Σ[ F ∈ S ] InjCode F a b) setPL readL
mutual-inj→bijection : (a b : S) → InjL a b → InjL b a
```

公开的定理采用后一种形式，因为 `InjL` 只保留单射码的命题截断。因此，两个截断的假设导出一个截断的双射。排中律在底层类型论证明中用来区分 Cantor–Schröder–Bernstein 构造的各种情形；唯一原像由单射性与h-集合条件恢复，并不依赖任何选择原理。

```agda
  → ∥ Σ[ h ∈ (⟪ fst a ⟫ → ⟪ fst b ⟫) ]
       (((x y : ⟪ fst a ⟫) → h x ≡ h y → x ≡ y)
     × ((y : ⟪ fst b ⟫) → ∥ Σ[ x ∈ ⟪ fst a ⟫ ] (h x ≡ y) ∥₁)) ∥₁
mutual-inj→bijection = MutualInjL.∃bijection
```