Mechanized Mathematics and Its Applications, Vol. 6, No. 1, November 2007, 15:22

The Fashoda Meet Theorem and Its Variants

Jarosław Kotowicz

Institute of Mathematics University of Białystok Akademicka 2 15-267 Białystok Poland

kotowicz@math.uwb.edu.pl

tel./fax: +48 85 745 75 44

Abstract – In this paper, we describe results of the formalization in Mizar of an extension of the Goboard Theorem called the Fashoda Meet Theorem [4]. This theorem states that the graphs of two continuous functions which take values in the Euclidean plane always have at least one common point if these functions satisfy certain conditions.

Keywords – the Go-board Theorem, the Fashoda Meet Theorem.

1. Introduction

There are many fundamental and well-known theorems in every branch of mathematics. In general topology, especially in topology of two-dimensional Euclidean space, the Jordan Curve Theorem is a one such theorem. At the beginning of the 1990s, members of the Association of Mizar Users (SUM)^{1} from Poland and Japan decided to formalize the proof of it in Mizar. After some research and discussion, leaders of SUM chose to formalize the proof presented by Takeuchi and Nakamura ([1]) because it depended only on elementary facts of general topology. The main step of this proof was based on the Go-board^{2} Theorem.

The first steps of this formalization, i.e., topological preliminaries, were done by Nakamura and Darmochwał (see for instance [2]) during Darmochwał’s stay at Shinshu University^{3} in Nagano in 1991. I had the pleasure to continue these works with Professor Yatsuka Nakamura in 1992. Unfortunately, we only had time to formalize the Go-board notation and the Go-board Theorem for a special polygonal arc on a Go-board ([3, Theorem 1]) and a special polygonal arc^{4} ([3, Theorem 8]). Further collaboration among members of SUM on the formalization of the Jordan Curve Theorem made it possible to prove many interesting properties of curves^{5} and functions which take values in the Euclidean plane. During this time it was observed that the Go-board Theorem could either be generalized or reformulated and then generalized. In

1 In Polish: Stowarzyszenie Użytkowników Mizara. 2 The terminology of a Go-board was introduced by T. Shibata in 1980. Unfortunately the author could not translate the title of his paper from Japanese into English (see the references in [1]). 3 Agata Darmochwał visited the Kiso Laboratory of the Department of Information Engineering, Faculty of Engineering. 4 Definition 1.2 and Remark 1.13 in [1] or Definition 1 in this article. 5 The word ”curve” in the formalization is used to mean the graph of a curve.

Manuscript received August 9, 2007; revised October 22, 2007.

the first case, special polygonal arcs are first substituted by arcs ([4, Theorem 62]) and then by paths ([11, Theorem 4]).

The reformulation of the Go-board Theorem in the language of continuous functions was called the Fashoda Meet Theorem and was done by Nakamura in 1998 ([4]). He continued this work in his papers from the beginning of this century – see [5] for the Outside Fashoda Meet Theorem, [6], [8], [9] for the Fashoda Meet Theorem for a circle and a square, and the joint work with Trybulec [10] for a rectangle (the Fashoda Fashoda Meet Theorem). The recent and the most general result of the formalization of the Fashoda Meet Theorem and the Go-board Theorem was obtained by Nakamura, Trybulec, and Korniłowicz in 2005 ([11]).

In this article I would like to briefly review the most important variants of the Fashoda Meet Theorem which can be found in the Mizar Mathematical Library (MML) and which have been published in Formalized Mathematics (a computer assisted approach). This means that I am not going to discuss all variants of this theorem that have been included to the MML since 1998, because there are 55 different variants in [4] – [11].

This paper is divided into three main parts. In the first part, we describe the Go-board Theorem because it is a predecessor of the Fashoda Meet Theorem. In the next section, we discuss the Fashoda Meet Theorem, its variants, and generalizations. Finally, in the appendix, we present selected theorems from the MML^{6} to illustrate the formalization.

Although the same notion is used for an open interval and a point of the Euclidean plane, I think it will not cause confusion. Also, a circle, a square, and a rectangle are plane figures for us, so they are neither simple closed curves nor the graphs of simple closed curves. This point of view distinguishes our article from the formalization, although we follow the terminology of [4]

– [11].

2. The Go-board Theorem

In this section we want to keep our attention sharply focused on the Go-board Theorem because it is a predecessor of the Fashoda Meet Theorem. We would also like to look for a way of reformulating this theorem in the language of continuous functions.

Throughout this section, lower case letters denote points of the Euclidean plane and L(p,q) denotes the line segment joining points p and q, i.e., the following set

L(p,q) := {(x,y) : (x,y) = (1 − λ)p + λq,λ ∈ [0,1]}.

For the convenience of the reader we repeat the definition of a special polygonal arc (see e.g., [1, Definition 1.2] and [2] for the formalization in Mizar), thus making our exposition selfcontained.

Definition 1. Let p,q be points of the Euclidean plane and P be a subset of the plane. P is said to be a special polygonal arc joining points p and q if there exists a finite sequence of distinct

6 To be precise, we select theorems neither from the original Mizar articles nor from articles which have been published in Formalized Mathematics, but only from abstract files (see the distribution of the Mizar system http://mizar.org).

points of the plane (p_{1},...,p_{n}) such that n is no smaller than 2, and

(1) p_{1} = p and p_{n} = q,
(2) P = ⋃_{i=1}^{n−1} L(p_{i},p_{i+1} ),
(3) L(p_{i},p_{i+1} ) ∩ L(p_{i+1} ,p_{i+2} ) = \{p_{i+1} \} for alli ∈ \overline{1,n − 2} ,
(4) L(p_{i},p_{i+1} ) ∩ L(p_{j},p_{j+1} ) = ∅ for alli,j ∈ \overline{1,n − 1} and |i − j| > 1,
(5) (p_{i})_{x} = (p_{i+1} )_{x} or (p_{i})_{y} = (p_{i+1} )_{y} for alli ∈ \overline{1,n − 1} ,

where p_{x} (respectively p_{y}) denotes the first (respectively the second) coordinate of a point p.

One can see that a special polygonal arc joining two points of the plane can be regarded as the set of values of a piecewise-linear, continuous, and 1-1 function which fulfills some other conditions. This is also the first point at which it is possible to think about a generalization and/or reformulation of the Go-board Theorem.

Using the concept of a special polygonal arc, the following result was proved (see [1, Theorem 1.18] or [3, Theorem 8]):

Theorem 1 (Go-board Theorem). Let p,q,r,s be points of the Euclidean plane, P be a special polygonal arc joining points p and q, and Q be a special polygonal arc joining points r and s. If

a_{x} ≥ p_{x}∧ a_{x} ≤ q_{x}∧ a_{y} ≥ r_{y}∧ a_{y} ≤ s_{y} for alla ∈ P ∪ Q,

then P ∩ Q ≠ ∅.

Since there are no Go-boards in the formulation of Theorem 1 it should be explained why it is called the Go-board Theorem. The reason is very simple. The proof in [1] and also the formalization in [3] are based on the basic version of the Go-board Theorem ([1, Theorem 1.16], [3, Theorem 1]). In both of the cases it is necessary to introduce the Go-boards and special polygonal arcs on a Go-board.

As we mentioned in the introduction, the Go-board Theorem was extended by relaxing its assumptions. The first step was done by replacing a special polygonal arc with an arc. In this step, although maybe not explicitly, the language was also changed. Even though an arc is still considered a subset of the Euclidean plane, it is also the set of values of a homeomorphism satisfying the following conditions:

– the domain of it is equal to the closed unit interval,

– the endpoints of the graph of it are points joined by the arc.

Here, the notation of continuous functions is used for the first time. I believe it is the most important reason for talking about the Go-board Theorem only in the language of continuous functions and for changing the name of it to the Fashoda Meet Theorem.

It is natural to consider the next possible way of relaxing the assumptions of the theorem. The answer is easy to see. One can replace a homeomorphism by a continuous function without changing other conditions^{7} and this variant of the Go-board Theorem was been proved by Nakamura, Trybulec, and Korniłowicz ([11, Theorem 4]).

7 Such a function is called a path (see [12] and [13] for the formalization in Mizar).

3. The Fashoda Meet Theorem and its Generalizations

In this section we formulate the Fashoda Meet Theorem and investigate possible variants of it. We already observed in the previous section that a reformulation of the Go-board Theorem can be done in the language of continuous functions. The first version of this reformulation is called the Fashoda Meet Theorem and it was proved by Nakamura ([4, Theorem 65]) at the same time as the formalization of the first extension of the Go-board Theorem. Nakamura obtained the following result:

Theorem 2 (Fashoda Meet Theorem). Let f,g: [0,1] → ℝ^{2} be continuous and 1-1 functions,

a,b,c,d be real numbers such that (f(0))_{x} = a, (f(1))_{x} = b, (g(0))_{y} = c, (g(1))_{y} = d and

(f(r))_{x},(g(r))_{x} ∈ [a,b] ∧ (f(r))_{y},(g(r))_{y} ∈ [c,d] for allr ∈ [0,1].

Then f([0,1]) ∩ g([0,1]) ≠ ∅.

In the next article by Nakamura relating to the Fashoda Meet Theorem he proves the so called Outside Fashoda Meet Theorem ([5]). In the summary of this article, the author explains in a demonstrative way the theorem that ”... if Britain and France intended to set the courses of ships to the opposite side of Africa, they must also meet.”. But, we can formulate the Outside Fashoda Meet Theorem in the following way ([5, Theorem 54^{8}]):

Theorem 3 (Outside Fashoda Meet Theorem). Let f,g: [0,1] → ℝ^{2} be continuous and 1-1 functions, a,b,c,d be real numbers. Suppose that

(1) a < b ∧ c < d,
(2) (f(0))_{x} = a ∧ (f(1))_{x} = b ∧ (f(0))_{y},(f(1))_{y} ∈ [c,d],
(3) (g(0))_{y} = c ∧ (g(1))_{y} = d ∧ (g(0))_{x},(g(1))_{x} ∈ [a,b],
(4) there is no r ∈ [0,1] such that (f(r))_{x} ∈ (a,b) ∧ (f(r))_{y} ∈ (c,d),
(5) there is no r ∈ [0,1] such that (g(r))_{x} ∈ (a,b) ∧ (g(r))_{y} ∈ (c,d).

Then f([0,1]) ∩ g([0,1]) ≠ ∅.

We can also find another version of this theorem with small modifications of its assumptions in [8, Theorem 14].

The next work of extending the Fashoda Meet Theorem was done in two complementary directions. In the first approach, the graphs of special simple closed curves in the Euclidean plane, in which the endpoints of the graphs of functions should belong, are considered and in the second, the assumptions are relaxed. The preliminary results of the first method were proved by Nakamura [6] in 2001. In this article the author defines homeomorphism from the Euclidean plane to itself, which maps a square to a circle^{9}. Using this homeomorphism he proved that boundaries of the unit circle^{10} and the square with vertices at points (−1,1),(−1,1),(1,1),

8 The proof is based on an earlier version of this theorem ([5, Theorem 52]) where a = c = −1 and b = d = 1. 9 In the article and in the formalization both of these objects are simple closed curves. 10 In the latter part of the article we will use the terminology the 1-dimensional sphere for the boundary of the unit

circle.

(1,1) are simple closed curves ([6, Theorems 35 and 36]). Finally, the following Fashoda Meet Theorem for the unit circle was formulated and proved ([6, Theorem 55]):

Theorem 4. Let f,g: [0,1] → ℝ^{2} be continuous and 1-1 functions. If

(1) f([0,1]) ∪ g([0,1]) ⊂ {r ∈ ℝ^{2} : ∥r∥ ≤ 1},
(2) f(0) ∈ {r ∈ ℝ^{2} : ∥r∥ = 1 ∧ (r)_{y} ≥ (r)_{x}∧ (r)_{y} ≤ −(r)_{x}},
(3) f(1) ∈ {r ∈ ℝ^{2} : ∥r∥ = 1 ∧ (r)_{y} ≤ (r)_{x}∧ (r)_{y} ≥ −(r)_{x}},
(4) g(0) ∈ {r ∈ ℝ^{2} : ∥r∥ = 1 ∧ (r)_{y} ≤ (r)_{x}∧ (r)_{y} ≤ −(r)_{x}},
(5) g(1) ∈ {r ∈ ℝ^{2} : ∥r∥ = 1 ∧ (r)_{y} ≥ (r)_{x}∧ (r)_{y} ≥ −(r)_{x}}.

Then f([0,1]) ∩ g([0,1]) ≠ ∅.

We see that one endpoint of the graph of the first function ought to lie on the west arc of the 1dimensional sphere and the other on the east arc and we have a similar situation for the second function and the north and south arcs. All other variants of this theorem appear in subsequent articles by Nakamura ([8, Theorem 16], [9, Theorems 23 and 24]). The Outside Fashoda Meet Theorem for the unit circle was also proved one year later ([8, Theorems 17 – 20^{11}]). Here, let us mention that Theorems 17 and 18 in [8] are exactly analogous to our Theorem 4, and Theorem 19 is a special case of Theorem 17 (the endpoints of the graphs of both functions are the points of intersection of the axes and the 1-dimensional sphere). From among these theorems, the most general variant of the Outside Fashoda Meet Theorem for the unit circle can be formulated as follows ([8, Theorem 20]):

Theorem 5. Let p_{1},p_{2},p_{3},p_{4} be points of the Euclidean plane. Assume that the following conditions hold

(1) p_{1},p_{2},p_{3},p_{4} ∈ {r ∈ ℝ^{2} : ∥r∥ = 1},

and there exists a homeomorphism h from ℝ^{2} onto ℝ^{2} that

(2) h({r: ∥r∥ ≥ 1}) ⊂ {r: ∥r∥ ≥ 1} ∧
h(p_{1}) = (−1,0) ∧ h(p_{2}) = (0,1) ∧ h(p_{3}) = (1,0) ∧ h(p_{4}) = (0,−1).

If f,g: [0,1] → ℝ^{2} are continuous and 1-1 functions such that f(0) = p_{1},f(1) = p_{3},g(0) =

p_{4} and g(1) = p_{2} and f([0,1]) ∪ g([0,1]) ⊂ {r ∈ ℝ^{2} : ∥r∥ ≥ 1}, then f([0,1]) ∩ g([0,1]) ≠ ∅.

The next generalization of this theorem for special simple closed curves was done by Nakamura in 2002 ([8, §5. General Fashoda Theorems]). The author, using his earlier works on the Fan morphisms ([7]), discusses the connection between the order of points on the 1dimensional sphere and their coordinates. These considerations allowed the author to prove

11 Condition (1) in Theorem 4 was replaced in these theorems by

f([0,1]) ∪ g([0,1]) ⊂ {r ∈ ℝ^{2} : ∥r∥ ≥ 1}.

the Fashoda Meet Theorem for the unit circle assuming that the endpoints of the graph of the first function lie on two distinct but complementary arcs of the 1-dimensional sphere, where the endpoints are the endpoints of the graph of the second function ([8, Theorems 71 and 72]). The Outside Fashoda Meet Theorem for the unit circle with analogous assumptions was also proved in this article ([8, Theorems 73 and 74]).

The next step in this work was done in [9] one year later. The Fashoda Meet Theorem for the square with vertices at points (−1,−1),(−1,1),(1,−1) and (1,1) was proved ([9, Theorem 89]) under the assumption that the endpoints of the graph of the first function lie on the boundary of the square between the endpoints of the graph of the second one. This theorem was proved by Nakamura and Trybulec for a general rectangle in the Euclidean plane [10] in 2005. The authors enumerated and proved the Fashoda Meet Theorem for all possibilities of orders of points, i.e., the endpoints of the graphs of both functions, on the boundary of a rectangle. It is interesting to note that we have 35 such possibilities^{12}.

Since 2001, there was no progress in generalizations (i.e., relaxing of the assumptions) of the Fashoda Meet Theorem until finally in 2005 a relaxing of its assumptions was done in [11, Theorem 5]. The authors obtained:

Theorem 6. Let f,g: [0,1] → ℝ^{2} be continuous functions, a,b,c,d be real numbers. Assume

that (f(0))_{x} = a, (f(1))_{x} = b, (g(0))_{y} = c, (g(1))_{y} = d and for all r ∈ [0,1]

(f(r))_{x},(g(r))_{x} ∈ [a,b] ∧ (f(r))_{y},(g(r))_{y} ∈ [c,d],

Then f([0,1]) ∩ g([0,1]) ≠ ∅.

Notice that it is not necessary to assume that both functions are 1-1 functions.

We close this section with one remark about further possible work on the Fashoda Meet Theorem in Mizar. The Outside Fashoda Meet Theorem for continuous functions, i.e., the counterpart of Theorem 6, should be formalized as soon as possible, but I believe this can be done by people who want to study how the Mizar system and the formalization in Mizar work.

4. Conclusion

The complete proof of the Jordan Curve Theorem in Mizar was formalized by A. Korniłowicz in 2005. Unfortunately, he did not use the Go-board Theorem or the Fashoda Meet Theorem in his proof, so one could say that the works concerning the Fashoda Meet Theorem were unnecessary, but all of these efforts contributed significantly to the development of Mizar and the MML and encouraged cooperation between members of SUM in Poland and Japan.

Finally, I would like to thank Professor Yatsuka Nakamura of Shinshu University for the invitation, hospitality, and successful collaboration during the formalization of the Go-board Theorem in Nagano in 1992.

12 In textbooks, we will see only one theorem because the following sentence is usually used “Without loss of generality we can assume ...”.

References

[1] Y. Takeuchi and Y. Nakamura, On the Jordan Curve Theorem, Technical Report 19804, Dept. of Information Eng., Shinshu University, 500 Wakasato, Nagano City, Japan, April 1980.

[2] A. Darmochwał and Y. Nakamura, The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs, Formalized Mathematics, Vol. 2, No. 5, 1991, pp.617–621, http://mizar.org/JFM/Vol2/topreal1.html.

[3] J. Kotowicz and Y. Nakamura, Go-board Theorem, Formalized Mathematics, Vol. 3, No. 1, 1992, pp.125–129, http://mizar.org/JFM/Vol3/goboard4.html.

[4] Y. Nakamura, Graph theoretical properties of arcs in the plane and Fashoda Meet Theorem, Formalized Mathematics, Vol. 7, No. 2, 1998, pp.193–201, http://mizar.org/JFM/Vol7/jgraph_1.html.

[5] Y. Nakamura, On Outside Fashoda Meet Theorem, Formalized Mathematics, Vol. 9, No. 4, 2001, pp.697–704, http://mizar.org/JFM/Vol9/jgraph_2.html.

[6] Y. Nakamura, On the simple closed curve property of the circle and the Fashoda Meet Theorem, Formalized Mathematics, Vol. 9, No. 4, 2001, pp.801–808, http://mizar.org/JFM/Vol9/jgraph_3.html.

[7] Y. Nakamura, Fan Homeomorphisms in the Plane, Formalized Mathematics, Vol. 10, No. 1, 2002, pp.1–19, http://mizar.org/JFM/Vol10/jgraph_4.html.

[8] Y. Nakamura, General Fashoda Meet Theorem for the unit circle, Formalized Mathematics, Vol. 10, No. 2, 2002, pp.99–109, http://mizar.org/JFM/Vol10/jgraph_5.html.

[9] Y. Nakamura, General Fashoda Meet Theorem for the unit circle and square, Formalized Mathematics, Vol. 11, No. 3, 2003, pp.213–224, http://mizar.org/JFM/Vol11/jgraph_6.html.

[10] Y. Nakamura and A. Trybulec, The Fashoda Meet Theorem for rectangle, Formalized Mathematics, Vol. 13, No. 2, 2005, pp.209–219, http://mizar.org/JFM/Vol13/jgraph_7.html.

[11] Y. Nakamura, A. Trybulec, and A. Korniłowicz, The Fashoda Meet Theorem for continuous mappings, Formalized Mathematics, Vol. 13, No. 4, 2005, pp.467–469, http://mizar.org/JFM/Vol13/jgraph_8.html.

[12] M. J. Greenberg, Lectures on Algebraic Topology, W. A. Benjamin, Inc., 1973.

[13] A. Grabowski, Introduction to Homotopy Theory, Formalized Mathematics, Vol. 6, No. 4, 1997, pp.449–454, http://mizar.org/JFM/Vol6/borsuk_2.html.

A The Fashoda Meet Theorem in Mizar

In this appendix we would like to show how the formalization of the Fashoda Meet Theorem looks in Mizar.

The Fashoda Meet Theorem ([4, JGRAPH_1.abs]) and the Outside Fashoda Meet Theorem ([5, JGRAPH_2.abs]):

theorem :: JGRAPH_1:65 for f,g being Function of I[01],TOP-REAL 2,

a,b,c,d being real number, O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is continuous one-to-one & (f.O)‘1=a & (f.I)‘1=b & (g.O)‘2=c & (g.I)‘2=d & (for r being Point of I[01] holds

a <=(f.r)‘1 & (f.r)‘1<=b & a <=(g.r)‘1 & (g.r)‘1<=b & c <=(f.r)‘2 & (f.r)‘2<=d & c <=(g.r)‘2 & (g.r)‘2<=d) holds rng f meets rng g;

theorem :: JGRAPH_2:55 for f,g being Function of I[01],TOP-REAL 2,

a,b,c,d being real number, O,I being Point of I[01] st O=0 & I=1 & f is continuous one-to-one & g is continuous one-to-one & (f.O)‘1=a & (f.I)‘1=b & c <=(f.O)‘2 & (f.O)‘2<=d & c <=(f.I)‘2 & (f.I)‘2<=d & (g.O)‘2=c & (g.I)‘2=d & a<=(g.O)‘1 & (g.O)‘1<=b & a<=(g.I)‘1 & (g.I)‘1<=b & a < b & c < d & not (ex r being Point of I[01] st

a<(f.r)‘1 & (f.r)‘1<b & c <(f.r)‘2 & (f.r)‘2<d)& not (ex r being Point of I[01] st

a<(g.r)‘1 & (g.r)‘1<b & c <(g.r)‘2 & (g.r)‘2<d) holds rng f meets rng g;

The general Fashoda Meet Theorem from [11, JGRAPH_8.abs]:

theorem :: JGRAPH_8:5 for f,g being continuous Function of I[01],TOP-REAL 2, a,b,c,d being real number, O,I being Point of I[01] st O=0 & I=1 & (f.O)‘1=a & (f.I)‘1=b & (g.O)‘2=c & (g.I)‘2=d & (for r being Point of I[01] holds

a <=(f.r)‘1 & (f.r)‘1<=b & a <=(g.r)‘1 & (g.r)‘1<=b & c <=(f.r)‘2 & (f.r)‘2<=d & c <=(g.r)‘2 & (g.r)‘2<=d) holds rng f meets rng g;

Explanation of the symbols:

for/ex - for every/there exists

(the universal and existential quantifiers),

not/& - a negation/a conjunction,
I[01]  - the closed interval [0,1] in the Euclidean plane

(considered as a topological space),

TOP-REAL 2 - the Euclidean plane with the Euclid metric,
’1 (resp. ’2) - the first (resp. the second) coordinate of a point,
<=  - less than or equal to (≤),
rng  - the set of values of a function,
X meets Y- the sets X and Y have a non empty intersection.