一句话:在 Bishop 集合论中建立 Bishop 空间直接谱、正/逆极限及对偶定理。
本文把 Bishop 集合论(BST)的基本概念应用于 Bishop 空间理论——一种构造性拓扑的函数论进路。作者在 BST 中定义了集合的直接族、Bishop 空间的直接谱、直接谱的直接极限,以及反变直接谱的逆极限;随后在带可数多前提规则归纳定义的 BISH 扩展中,证明了关于 Bishop 空间谱的直接极限与逆极限的基本定理,以及二者之间的对偶原理。该工作为构造性拓扑中的谱与极限提供了统一框架,属于理论构造与构造性证明,并未涉及实验评估。
We apply fundamental notions of Bishop set theory (BST), an informal theory that complements Bishop's theory of sets, to the theory of Bishop spaces, a function-theoretic approach to constructive topology. Within BST we develop the notions of a direct family of sets, of a direct spectrum of Bishop spaces, of the direct limit of a direct spectrum of Bishop spaces, and of the inverse limit of a contravariant direct spectrum of Bishop spaces. Within the extension of Bishop's informal system of constructive mathematics BISH with inductive definitions with rules of countably many premises, we prove the fundamental theorems on the direct and inverse limits of spectra of Bishop spaces and the duality principle between them.