| Popis: |
It is a wish for Wu Wen-tsun to implement the mechanical proving of theorems in topology. Topological spaces constitute a fundamental concept of general topology, which is significant in understanding the essential content of general topology. Based on the machine proof system of axiomatic set theory, we presented a computer formalization of topological spaces in Coq. Basic examples of topological spaces are formalized, including indiscrete topological spaces and discrete topological spaces. Furthermore, the formal description of some well-known equivalent definitions of topological spaces are provided, and the machine proof of equivalent definitions based on neighborhood system and closure is presented. All the proof code has been verified in Coq, and the process of proof is standardized, rigorous and reliable. |
