• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >A constructive function-theoretic approach to topological compactness
【24h】

A constructive function-theoretic approach to topological compactness

机译：一种建设性的拓扑紧凑性的理论方法

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We introduce 2-compactness, a constructive function-theoretic alternative to topological compactness, based on the notions of Bishop space and Bishop morphism, which are constructive function-theoretic alternatives to topological space and continuous function, respectively. We show that the notion of Bishop morphism is reduced to uniform continuity in important cases, overcoming one of the obstacles in developing constructive general topology posed by Bishop. We prove that 2-compactness generalizes metric compactness, namely that the uniformly continuous real-valued functions on a compact metric space form a 2-compact Bishop topology. Among other properties of 2-compact Bishop spaces, the countable Tychonoff compactness theorem is proved for them. We work within BISH*, Bishop's informal system of constructive mathematics BISH equipped with inductive definitions with rules of countably many premises, a system strongly connected to Martin-L?f's Type Theory.
机译：基于主教空间和主教态势的概念，我们介绍了2紧凑，这是一种拓扑紧凑性的建设性函数 - 理论的替代品，它们分别是拓扑空间和连续功能的建设性函数理论替代品。我们表明，在重要情况下，主教态势的概念减少到统一的连续性，克服了主教造成的建设性总体拓扑中的障碍之一。我们证明了2紧凑性概括了公制紧凑性，即在紧凑型度量空间上均匀连续的实际函数形成2紧凑的主教拓扑。除了2紧凑的主教空间的其他特性之外，还证明了可数Tychonoff紧凑性定理。我们在Bish *内工作，Bishop的建设性数学系统的非正式制度，配备了归纳定义，其中有许多房屋的规则，一个系统强烈地连接到Martin-L？F的类型理论。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号