Mizar formalization of Jordan Curve Theorem
The proof of Jordan curve theorem for special polygons is the first part of the formalization of general Jordan curve theorem for simple closed curves:
Jordan curve theorem - the theorem that states that every simple closed curve divides a plane
into two parts and is the common boundary between them
(see The American Heritage Dictionary of the English Language).
Some other related links:
This theorem seems quite obvious, however it is common knowledge
that it is very difficult to it prove rigorously.
Mizar formalization follows the script 'On the Jordan curve theorem' by Y. Nakamura and Y. Takeuchi.
The work actually started in 1992 with the article JORDAN1 by Y. Nakamura and J. Kotowicz in which the Jordan property was introduced.
That article was preceded by several other articles in which Euclidean spaces and special polygonal arcs were defined.
A polygonal curve is called special if its line segments
are parallel to the axes.
Another useful concept of so called Go-boards was also defined before
the submission of JORDAN1.
By a Go-board the authors ment a matrix of points of the plane as below
with the property that ordinates of points in the same column are equal
as well as abscissae of points in rows and, moreover,
xi<xj and yi<yj for i<j.
Using the techniques of Go-boards the following theorem was proved in GOBOARD4:
Every two special arcs lying in a rectangle R such that the first
arc joins the upper and lower sides of R and the second arc joins the
left and right sides of R have a non empty intersection.
Together with several subsequent articles devoted to further development of
the theory of Go-boards, the above lemma made it possible to complete the first
part of the Jordan theorem (saying that the complement of the curve is the union of
two components) in GOBRD12.
Later, the second part (stating that these components are different) was proved in
SPRECT_4, and finally, the complete theorem was proved in GOBRD14.
The preliminary work on the proof of general Jordan curve theorem started
with defining the external (so called Cages) and internal
(so called Spans) approximation of the curve by special polygons
in JORDAN9 and
Recently, we work on proofs of lemmas left to complete the whole proof.
74 articles devoted to this theorem have been collected so far, which
makes about 10% of the Mizar Mathematical Library.
However, some of the articles contain suplementary theory, only indirectly relevant to the proof.
Last modified: January 21, 2003