coq - 如何明确地获得合奏的基数

Question

我正在尝试制作一个类似的函数Definition cardinality (A : Ensemble U) : nat.，以便为每个合奏我得到它的基数。我发现这是一个具有挑战性的问题，我想得到一些帮助。

顺便说一句，cardinal U A n如果|A| = n它成为真的，那是在哪里。

标签： coq

Answer 1

一个问题是你不能为任意集合定义这个函数：你需要假设它A是有限的。例如，您可以使用Finite谓词 in Coq.Sets.Finite_sets。您可能很想使用 的finite_cardinal引理Coq.Sets.Finite_sets_facts，它表示每个有限集都有一些基数。这将要求您从存在语句中提取一个自然数exists n, cardinal U A n，而这又需要某种形式的选择公理（例如choicein Coq.Logic.ClassicalChoice）。