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

Zhenbing Zeng; Jianlin Wang; Zhengfeng Yang; Hidetsune Kobayashi

doi:10.1360/SSM-2019-0301

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

Zhenbing Zeng
, Jianlin Wang^*
, Zhengfeng Yang
, Hidetsune Kobayashi

^*此作品的通讯作者

软件工程学院

科研成果: 期刊稿件 › 文章 › 同行评审

1 引用（Scopus）

摘要

In this paper, we presented a formalization of the basic concepts of topological spaces including open sets, neighborhoods, closed setsand closures using the higher order logic interactive assistant tool textmdIsabelle and gave a mechanical proof ofthe 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.

投稿的翻译标题	A mechanical proof of the C. T. Yang's Theorem related to a property of derived sets in general topology
源语言	繁体中文
页（从-至）	257-288
页数	32
期刊	Scientia Sinica Mathematica
卷	51
期	1
DOI	https://doi.org/10.1360/SSM-2019-0301
出版状态	已出版 - 1月 2021

关键词

C. T. Yang's Theorem
Closed set
Derived set
Machine proof
Open set
Topological space

访问文件

10.1360/SSM-2019-0301

其它文件与链接

链接到 Scopus 的出版物

引用此

@article{df0ac31f41ca44b1ac38bbfd96d7e4c6,

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

abstract = "In this paper, we presented a formalization of the basic concepts of topological spaces including open sets, neighborhoods, closed setsand closures using the higher order logic interactive assistant tool textmdIsabelle and gave a mechanical proof ofthe 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 = "C. T. Yang's Theorem, Closed set, Derived set, Machine proof, Open set, Topological space",

author = "Zhenbing Zeng and Jianlin Wang and Zhengfeng Yang and Hidetsune Kobayashi",

year = "2021",

month = jan,

doi = "10.1360/SSM-2019-0301",

language = "繁体中文",

volume = "51",

pages = "257--288",

journal = "Scientia Sinica Mathematica",

issn = "1674-7216",

publisher = "Science Press ",

number = "1",

}

TY - JOUR

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

AU - Zeng, Zhenbing

AU - Wang, Jianlin

AU - Yang, Zhengfeng

AU - Kobayashi, Hidetsune

PY - 2021/1

Y1 - 2021/1

N2 - In this paper, we presented a formalization of the basic concepts of topological spaces including open sets, neighborhoods, closed setsand closures using the higher order logic interactive assistant tool textmdIsabelle and gave a mechanical proof ofthe 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.

AB - In this paper, we presented a formalization of the basic concepts of topological spaces including open sets, neighborhoods, closed setsand closures using the higher order logic interactive assistant tool textmdIsabelle and gave a mechanical proof ofthe 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.

KW - C. T. Yang's Theorem

KW - Closed set

KW - Derived set

KW - Machine proof

KW - Open set

KW - Topological space

UR - https://www.scopus.com/pages/publications/85099765260

U2 - 10.1360/SSM-2019-0301

DO - 10.1360/SSM-2019-0301

M3 - 文章

AN - SCOPUS:85099765260

SN - 1674-7216

VL - 51

SP - 257

EP - 288

JO - Scientia Sinica Mathematica

JF - Scientia Sinica Mathematica

IS - 1

ER -

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

摘要

关键词

访问文件

其它文件与链接

指纹

引用此