---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# L 内部的 Cantor–Schröder–Bernstein 定理

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

固定宇宙层级 `ℓ`，并假设 `lem : LEM (ℓ-suc ℓ)`。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

```agda
open import FOL.ZFStructure using ( module hPropView )
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 )
```

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

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

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

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

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )

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

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

```agda
setPL a = small-set (a .fst)
readL : (a b : S) → Σ[ F ∶ S ] InjCode F a b
      → Σ[ f ∶ (⟪ a .fst ⟫ → ⟪ b .fst ⟫) ]
          ((x y : ⟪ a .fst ⟫) → 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 → ⟪ a .fst ⟫)
  (λ 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 ∶ (⟪ a .fst ⟫ → ⟪ b .fst ⟫) ]
       (((x y : ⟪ a .fst ⟫) → h x ≡ h y → x ≡ y)
     × ((y : ⟪ b .fst ⟫) → ∥ Σ[ x ∶ ⟪ a .fst ⟫ ] (h x ≡ y) ∥₁)) ∥₁
mutual-inj→bijection = MutualInjL.∃bijection
```