点集拓扑学之杨忠道定理的一个机械化证明  

A mechanical proof of the C.T.Yang's Theorem related to a property of derived sets in general topology

作　　者：曾振柄[1] 王建林 杨争峰[3] 小林英恒 Zhenbing Zeng;Jianlin Wang;Zhengfeng Yang;Hidetsune Kobayashi

机构地区：[1]上海大学数学系,上海200444 [2]河南大学计算机与信息工程学院,开封475004 [3]华东师范大学上海市高可信计算重点实验室,上海200062 [4]Department of Mathematics,College of Science and Technology,Nihon University,Tokyo 101-8308,Japan

出　　处：《中国科学：数学》2021年第1期257-288,共32页Scientia Sinica：Mathematica

基　　金：国家自然科学基金(批准号:11471209和61772203)资助项目。

摘　　要：本文给出一种用高阶逻辑自动证明语言Isabelle在计算机中表示拓扑空间中开集、闭集、邻域和导集等基本概念的方法,在此基础上证明点集拓扑学中著名的杨忠道定理,即一拓扑空间的任意单点集的导集为闭集,则其任意子集的导集亦为闭集.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.

关 键 词：拓扑空间 开集 闭集 导集 杨忠道定理 机器证明 

分 类 号：O189.11[理学—数学]