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.
| Translated title of the contribution | A mechanical proof of the C. T. Yang's Theorem related to a property of derived sets in general topology |
|---|---|
| Original language | Chinese (Traditional) |
| Pages (from-to) | 257-288 |
| Number of pages | 32 |
| Journal | Scientia Sinica Mathematica |
| Volume | 51 |
| Issue number | 1 |
| DOIs | |
| State | Published - Jan 2021 |