【发布时间】：2018-05-06 01:01:56
【问题描述】：
我需要在某个谓词 P 定义的特定子集上表达可数属性。我的第一个想法是明确声明存在一个函数 f，它在我的子集和自然数之间是双射的。在标准库中是否有另一种更通用的方式来表达该属性？
提前谢谢你
【问题讨论】：
-
从子集到自然数的单射函数就足够了，不是吗？
-
我还想确保我的子集是无限的，这就是为什么我希望函数是双射的。我应该提到这一点，尽管这并没有太大改变问题。
-
在 Agda 中不可数集合是什么样子的？
-
我不明白为什么集合必须是可数的。例如，定义为有理数的实数是不可数的。虽然我不知道 Agda 是否已经实现了。