无点连续性的原理
The principle of pointfree continuity
AI总结：
本文在构造性无点拓扑中提出无点连续性原理，通过拓扑基间关系定义连续运算，并证明在双空间性下成立，且与形式贝尔空间和单位区间的空间性等价，重新表述了空间性、条形归纳和紧致性的关系。
摘要：
在构造性无点拓扑的框架中，我们引入了无点拓扑之间连续运算的概念以及相应的无点连续性原理。如果无点拓扑的点之间的一个运算由拓扑基之间的一个关系所诱导，则该运算是连续的；这为布劳威尔连续性原理成立提供了一个严格的条件。对于无点拓扑 $\mathcal{S}$ 和 $\mathcal{T}$，无点连续性原理断言：任何诱导点间连续运算的关系都是从 $\mathcal{S}$ 到 $\mathcal{T}$ 的一个态射。该原理在 $\mathcal{S}$ 的双空间性假设下成立。当 $\mathcal{S}$ 是形式贝尔空间或形式单位区间，且 $\mathcal{T}$ 是自然数的形式拓扑时，该原理分别等价于形式贝尔空间和形式单位区间的空间性。空间性、条形归纳和单位区间紧致性之间的一些众所周知的关系被重新表述为我们的连续性原理。我们采用最小主义基础作为我们的构造性基础，并采用正拓扑作为无点拓扑的概念。这使我们能够区分理想对象与构造性对象，特别是将选择序列解释为形式贝尔空间的点。
英文摘要：
In the setting of constructive pointfree topology, we introduce a notion of continuous operation between pointfree topologies and the corresponding principle of pointfree continuity. An operation between points of pointfree topologies is continuous if it is induced by a relation between the bases of the topologies; this gives a rigorous condition for Brouwer's continuity principle to hold. The principle of pointfree continuity for pointfree topologies $\mathcal{S}$ and $\mathcal{T}$ says that any relation which induces a continuous operation between points is a morphism from $\mathcal{S}$ to $\mathcal{T}$. The principle holds under the assumption of bi-spatiality of $\mathcal{S}$. When $\mathcal{S}$ is the formal Baire space or the formal unit interval and $\mathcal{T}$ is the formal topology of natural numbers, the principle is equivalent to spatiality of the formal Baire space and formal unit interval, respectively. Some of the well-known connections between spatiality, bar induction, and compactness of the unit interval are recast in terms of our principle of continuity. We adopt the Minimalist Foundation as our constructive foundation, and positive topology as the notion of pointfree topology. This allows us to distinguish ideal objects from constructive ones, and in particular, to interpret choice sequences as points of the formal Baire space.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
