位置性和明显的亚位置

摘要：

位置性是构造性数学的基本概念之一。肯定性谓词在场所上的存在，即场所是公开的或开放的，已被证明是建构性场所理论的基础。我们表明，这两个概念是密切相关的。Bishop定义一个度量空间是紧的，如果它是完备的和完全有界的。全有界集的子集又是全有界的当且仅当它被定位。所以Bishop紧集的闭子集是Bishop紧的当且仅当它被定位。我们把这个结果转化为形式拓扑。“主教契约”被翻译成紧密和公开的。给出了形式拓扑中子空间上的定位谓词的定义。如果一个子区域可以用一个带有located谓词的形式拓扑来表示，我们称之为located。证明了紧致正则区域的闭子区域有定位谓词当且仅当它是公开的。此外，一个完全度量空间的Bishop闭子集是Bishop紧的--也就是说，是完全有界的和完备的--当且仅当它的局部完备化是紧的公开的。最后，我们证明了初等方法，一个紧凑的正规区域的Vietoris区域的点正是它的紧凑的公开sublocales。我们的工作是建设性的，预测性的，避免使用可数选择公理。因此，我们的所有结果在任何谓词topos都是有效的。

英文摘要：

Locatedness is one of the fundamental notions in constructive mathematics. The existence of a positivity predicate on a locale, i.e. the locale being overt, or open, has proved to be fundamental in constructive locale theory. We show that the two notions are intimately connected. Bishop defines a metric space to be compact if it is complete and totally bounded. A subset of a totally bounded set is again totally bounded iff it is located. So a closed subset of a Bishop compact set is Bishop compact iff it is located. We translate this result to formal topology. `Bishop compact' is translated as compact and overt. We propose a definition of located predicate on subspaces in formal topology. We call a sublocale located if it can be presented by a formal topology with a located predicate. We prove that a closed sublocale of a compact regular locale has a located predicate iff it is overt. Moreover, a Bishop-closed subset of a complete metric space is Bishop compact -- that is, totally bounded and complete -- iff its localic completion is compact overt. Finally, we show by elementary methods that the points of the Vietoris locale of a compact regular locale are precisely its compact overt sublocales. We work constructively, predicatively and avoid the use of the axiom of countable choice. Consequently, all our results are valid in any predicative topos.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。