离散Jordan曲线定理：一个用超映射形式化的Coq证明
Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
摘要：
本文给出了若当曲线定理的一个离散形式的形式化证明。它是基于超映射模型的平面细分，正式规范和证明辅助Coq系统。基本性质由结构或诺特归纳证明：亏格定理，欧拉公式，建设性平面性准则。本文归纳地定义了面环的概念，并证明了平面超映射的若当曲线定理。
英文摘要：
This paper presents a formalized proof of a discrete form of the Jordan Curve Theorem. It is based on a hypermap model of planar subdivisions, formal specifications and proofs assisted by the Coq system. Fundamental properties are proven by structural or noetherian induction: Genus Theorem, Euler's Formula, constructive planarity criteria. A notion of ring of faces is inductively defined and a Jordan Curve Theorem is stated and proven for any planar hypermap.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
