基于Coq的Tychonoff乘积定理的机器证明

基于Coq的Tychonoff乘积定理的机器证明

论文摘要

布尔巴基学派的序、代数、拓扑三大母结构是现代数学的基础.利用交互式定理证明工具Coq,可以完整构建这三大母结构的形式化系统.本文在初等集论形式化的基础上,给出点集拓扑学形式化的构架,通过对拓扑、基、子基、积空间及紧致性等相关定义和Tukey引理、Alexander子基定理等相关定理的形式化,给出点集拓扑学中著名的Tychonoff乘积定理的完整形式化证明.所有形式化过程已被Coq验证.体现了Coq的可靠性、可读性和严谨性。

论文目录

  • 摘要
  • Abstract
  • 引言
  • 第一章 Coq简介及公理化集合论形式化系统
  •   1.1 Coq简介
  •   1.2 公理化集合论形式化系统
  • 第二章 基本定义
  •   2.1 预备概念
  •   2.2 拓扑空间
  •   2.3 积空间
  •   2.4 覆盖
  •   2.5 紧致空间
  • 第三章 预备引理的证明
  • 第四章 预备定理的证明
  • 第五章 Tychonoff 乘积定理的形式化证明
  •   5.1 Alexander 子基定理
  •   5.2 Tychonoff 乘积定理
  • 第六章 结论
  • 参考文献
  • 致谢
  • 作者简介
  • 导师评阅表
  • 文章来源

    类型: 硕士论文

    作者: 糟晓燕

    导师: 郁文生

    关键词: 布尔巴基学派,拓扑,子基定理,乘积定理

    来源: 伊犁师范大学

    年度: 2019

    分类: 基础科学

    专业: 数学

    单位: 伊犁师范大学

    分类号: O189

    总页数: 34

    文件大小: 660K

    下载量: 25

    相关论文文献

    • [1].运用塞瓦定理证明一类等角中的等角问题[J]. 中学数学教学 2008(03)
    • [2].角和定理与平行公理的等价性[J]. 数学学习与研究 2016(23)
    • [3].余弦定理的证明方法赏析[J]. 数学之友 2017(02)
    • [4].整体单元化设计理念下的“正弦、余弦定理”教学[J]. 中小学数学(高中版) 2017(06)
    • [5].从对定理证明的考查看对课本回归的理解(上)[J]. 新高考(高三语数外) 2011(12)
    • [6].联想类比在近世代数定理证明中的运用[J]. 教育教学论坛 2020(38)
    • [7].基于高阶逻辑的定理证明方法及其对策的应用[J]. 计算机应用与软件 2017(11)
    • [8].值得思考的一道定理证明[J]. 考试周刊 2013(37)
    • [9].关于替换定理证明中的发散思维能力培养[J]. 甘肃高师学报 2016(09)
    • [10].拉格朗日中值定理的证法研究[J]. 高等数学研究 2020(05)
    • [11].对《一个有趣的和积互换公式》一文的异见[J]. 数学通讯 2010(22)
    • [12].余弦定理的证明方法赏析[J]. 中学生数学 2017(19)
    • [13].重视定理证明中所蕴含的思想方法[J]. 中学生数理化(八年级数学)(配合人教社教材) 2014(Z1)
    • [14].基于核心素养的定理教学微课设计[J]. 中学数学教学参考 2019(14)
    • [15].数学的教与学[J]. 文存阅刊 2018(19)
    • [16].基于核心素养的定理教学基本原则[J]. 中学数学杂志 2017(10)
    • [17].一种新的基于扩展规则的定理证明算法[J]. 计算机研究与发展 2009(01)
    • [18].利用完全覆盖定理证明二维空间的几个完备性定理[J]. 河北北方学院学报(自然科学版) 2008(02)
    • [19].巧用余弦定理证明一类三元无理不等式[J]. 中学数学研究 2018(06)
    • [20].几何教学中学生思维能力的训练例谈[J]. 新课程(教研版) 2009(05)
    • [21].样例在泛函分析教学中的应用[J]. 高师理科学刊 2008(01)
    • [22].关于Minkowski定理证明的注记[J]. 河北师范大学学报(自然科学版) 2009(04)
    • [23].基于PVS的ITL定理证明方法[J]. 郑州大学学报(理学版) 2009(04)
    • [24].关系扩展规则[J]. 吉林大学学报(理学版) 2008(03)
    • [25].高中数学“慢悟”教学探究——例谈余弦定理证明之情景创设[J]. 数学学习与研究 2015(01)
    • [26].线面平行判定定理的证明[J]. 安徽教育科研 2018(02)
    • [27].加强定理证明教学,提高学生解题能力[J]. 科教文汇(下旬刊) 2014(08)
    • [28].对教材中一个定理证明的修改建议[J]. 中小学数学(初中版) 2012(09)
    • [29].巧用塞瓦定理证明三线共点问题[J]. 数学学习与研究 2015(17)
    • [30].活动启思维,证法显本质——“三角形内角和定理证明”教学感悟[J]. 中学数学 2019(02)

    标签:;  ;  ;  ;  

    基于Coq的Tychonoff乘积定理的机器证明
    下载Doc文档

    猜你喜欢