| 点集拓扑学之杨忠道定理的一个机械化证明 |
| |
| 引用本文： | 曾振柄,王建林,杨争峰,小林英恒.点集拓扑学之杨忠道定理的一个机械化证明[J].中国科学:数学,2021(1). |
| |
| 作者姓名： | 曾振柄 王建林 杨争峰 小林英恒 |
| |
| 作者单位： | 上海大学数学系;河南大学计算机与信息工程学院;华东师范大学上海市高可信计算重点实验室;Department of Mathematics |
| |
| 基金项目： | 国家自然科学基金(批准号:11471209和61772203)资助项目。 |
| |
| 摘 要： | 本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.
|
| 关 键 词： | 拓扑空间 开集 闭集 导集 杨忠道定理 机器证明 |
A mechanical proof of the C.T.Yang's Theorem related to a property of derived sets in general topology |
| |
| Abstract: | In this paper,we presented a formalization of the basic concepts of topological spaces including open sets,neighborhoods,closed sets and closures using the higher order logic interactive assistant tool Isabelle,and gave a mechanical proof of the C.T.Yang's Theorem which states that in any topological space(X,T),if the derived set of {x} is closed for all the points x∈X,then the derived set of any subset S■X is also closed. |
| |
| Keywords: | topological space open set closed set derived set C T Yang's Theorem machine proof |
| 本文献已被 CNKI 维普 等数据库收录！ |
|
