小编Bru*_*uno的帖子

在https://www.cs.umd.edu/~rrand/vqc/Real.html#lab1中可以阅读：

\n

Coq 的标准库对实数采用了一种非常不同的方法：公理化方法。

\n

并且可以找到以下公理：

Axiom\n  completeness :\n    \xe2\x88\x80E:R \xe2\x86\x92 Prop,\n      bound E \xe2\x86\x92 (\xe2\x88\x83x : R, E x) \xe2\x86\x92 { m:R | is_lub E m }.\n

但在《为什么实数在 Coq 中公理化？》中没有提到该库。人们可以找到相同的描述：

\n

我想知道 Coq 是否将实数定义为柯西序列或 Dedekind 切割，所以我检查了 Coq.Reals.Raxioms ......这两个都不是。实数及其运算（作为参数和公理）被公理化。为什么会这样呢？

\n

\n

此外，实数紧密依赖于子集的概念，因为它们的定义属性之一是每个上界子集都有一个最小上限。Axiom 完整性将这些子集编码为 Props。”

\n

尽管如此，每当我查看https://coq.inria.fr/library/Coq.Reals.Raxioms.html时，我都没有看到任何公理化方法，特别是我们有以下引理：

Lemma completeness :\n    forall E:R -> Prop,\n      bound E -> (exists x : R, E x) …