预集

1. 概述

在 Bishop 风格的构造性数学中, 预集 是已经规定了元素如何形成、但尚未指定所采用之相等关系的对象总体. 为预集配备一个 等价关系 后, 便得到一个带有明确相等概念的集合; 这种结构也常称为 setoid.

2. 定义

定义 1 (预集)

一个已明确规定其元素的对象总体 称为 预集. 若在 上另给定 等价关系 , 则把二元组 视为一个集合, 并以：

作为该集合中的相等关系.

注记 2 (与经典集合的区别)

在经典集合论中, 元素相等通常直接使用对象本身的相等; 预集 方法则把“哪些表示应被视为同一个元素”作为结构的一部分明确给出.

3. 例子

例子 3 (由分数表示构造有理数)

取 预集：

并在 上定义：

不同的分数表示, 如 与 , 在此关系下表示同一个 有理数. 因而 给出了有理数集的一种构造.

4. 相关性质

命题 4 (预集上的相等与映射)

设 与 是由 预集 形成的集合, 则：

1. 等价关系 的自反性、对称性与传递性保证 具有相等关系的基本性质;
2. 一个函数 表示这些集合之间的 映射, 当且仅当它保持所给等价关系, 即

证明 5 (预集上的相等与映射)

1. 这是 为 等价关系 的直接含义.
2. 若等价的表示对应同一个元素, 则映射必须把它们送到 中等价的表示; 反之, 该条件保证 的取值不依赖于代表元的选择.
   

5. 相关概念

• 等价关系
• 等价类
• 商集
• 公理化集合论

6. 术语翻译

中文	英文
预集	preset
集合胚	setoid

集合论 构造性数学