FORMALIZED MATHEMATICS Volume 10, Number 2, 2002 University of Białystok

Upper and Lower Sequence on the Cage, Upper and Lower Arcs^{1}

Robert Milewski University of Białystok

MML Identifier: JORDAN1J.

The articles [25], [30], [2], [4], [3], [29], [5], [14], [27], [20], [24], [13], [1], [23], [10], [11], [8], [28], [16], [12], [21], [26], [7], [18], [19], [6], [22], [9], [15], and [17] provide the notation and terminology for this paper.

In this paper n is a natural number. The following propositions are true:

(1) Let G be a Go-board and i_{1}, i_{2}, j_{1}, j_{2} be natural numbers. Suppose 1 j_{1} and j_{1} widthG and 1 j_{2} and j_{2} widthG and 1 i_{1} and i_{1} < i_{2} and i_{2} lenG. Then (G ∘ (i_{1}, j_{1}))_{1} < (G ∘ (i_{2}, j_{2}))_{1}.

(2) Let G be a Go-board and i_{1}, i_{2}, j_{1}, j_{2} be natural numbers. Suppose 1 i_{1} and i_{1} lenG and 1 i_{2} and i_{2} lenG and 1 j_{1} and j_{1} < j_{2} and j_{2} widthG. Then (G ∘ (i_{1}, j_{1}))_{2} < (G ∘ (i_{2}, j_{2}))_{2}.

Let f be a non empty finite sequence and let g be a finite sequence. One can verify that f ⌢⌢ g is non empty.

The following propositions are true:

(3) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and n be a natural number. Then L̃(Cage(C, n)− :E-max L̃(Cage(C, n)))∩ L̃(Cage(C, n) :− E-max L̃(Cage(C, n))) = {N-min L̃(Cage(C, n)), E-max L̃(Cage(C, n))}.

(4) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds UpperSeq(C, n) = ((Cage(C, n))_{⟲}^{E-max L̃(Cage(C,n))}) :− W-min L̃(Cage(C, n)).

1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

(5) For every compact non vertical non horizontal subset C of E_{T}^{2} holds W-min L̃(Cage(C, n)) ∈ rngUpperSeq(C, n) and W-min L̃(Cage(C, n)) ∈ L̃(UpperSeq(C, n)).

(6) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds W-max L̃(Cage(C, n)) ∈ rngUpperSeq(C, n) and W-max L̃(Cage(C, n)) ∈ L̃(UpperSeq(C, n)).

(7) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds N-min L̃(Cage(C, n)) ∈ rngUpperSeq(C, n) and N-min L̃(Cage(C, n)) ∈ L̃(UpperSeq(C, n)).

(8) For every compact connected non vertical non horizontal subset C of E_{T}^{2} holds N-max L̃(Cage(C, n)) ∈ rngUpperSeq(C, n) and N-max L̃(Cage(C, n)) ∈ L̃(UpperSeq(C, n)).

(9) For every compact non vertical non horizontal subset C of E_{T}^{2} holds E-max L̃(Cage(C, n)) ∈ rngUpperSeq(C, n) and E-max L̃(Cage(C, n)) ∈ L̃(UpperSeq(C, n)).

(10) For every compact non vertical non horizontal subset C of E_{T}^{2} holds E-max L̃(Cage(C, n)) ∈ rngLowerSeq(C, n) and E-max L̃(Cage(C, n)) ∈ L̃(LowerSeq(C, n)).

(11) For every compact non vertical non horizontal subset C of E_{T}^{2} holds E-min L̃(Cage(C, n)) ∈ rngLowerSeq(C, n) and E-min L̃(Cage(C, n)) ∈ L̃(LowerSeq(C, n)).

(12) For every compact non vertical non horizontal subset C of E_{T}^{2} holds S-max L̃(Cage(C, n)) ∈ rngLowerSeq(C, n) and S-max L̃(Cage(C, n)) ∈ L̃(LowerSeq(C, n)).

(13) For every compact non vertical non horizontal subset C of E_{T}^{2} holds S-min L̃(Cage(C, n)) ∈ rngLowerSeq(C, n) and S-min L̃(Cage(C, n)) ∈ L̃(LowerSeq(C, n)).

(14) For every compact non vertical non horizontal subset C of E_{T}^{2} holds W-min L̃(Cage(C, n)) ∈ rngLowerSeq(C, n) and W-min L̃(Cage(C, n)) ∈ L̃(LowerSeq(C, n)).

(15) For all non empty compact subsets X, Y of E_{T}^{2} such that X ⊆ Y and N-minY ∈ X holds N-minX = N-minY.

(16) For all non empty compact subsets X, Y of E_{T}^{2} such that X ⊆ Y and N-maxY ∈ X holds N-maxX = N-maxY.

(17) For all non empty compact subsets X, Y of E_{T}^{2} such that X ⊆ Y and E-minY ∈ X holds E-minX = E-minY.

(18) For all non empty compact subsets X, Y of E_{T}^{2} such that X ⊆ Y and E-maxY ∈ X holds E-maxX = E-maxY.

(19) For all non empty compact subsets X, Y of E_{T}^{2} such that X ⊆ Y and S-minY ∈ X holds S-minX = S-minY.

(20) For all non empty compact subsets X, Y of E_{T}^{2} such that X ⊆ Y and S-maxY ∈ X holds S-maxX = S-maxY.

(21) For all non empty compact subsets X, Y of E_{T}^{2} such that X ⊆ Y and W-minY ∈ X holds W-minX = W-minY.

(22) For all non empty compact subsets X, Y of E_{T}^{2} such that X ⊆ Y and W-maxY ∈ X holds W-maxX = W-maxY.

(23) For all non empty compact subsets X, Y of E_{T}^{2} such that N-boundX < N-boundY holds N-boundX ∪ Y = N-boundY.

(24) For all non empty compact subsets X, Y of E_{T}^{2} such that E-boundX < E-boundY holds E-boundX ∪ Y = E-boundY.

(25) For all non empty compact subsets X, Y of E_{T}^{2} such that S-boundX < S-boundY holds S-boundX ∪ Y = S-boundX.

(26) For all non empty compact subsets X, Y of E_{T}^{2} such that W-boundX < W-boundY holds W-boundX ∪ Y = W-boundX.

(27) For all non empty compact subsets X, Y of E_{T}^{2} such that N-boundX < N-boundY holds N-minX ∪ Y = N-minY.

(28) For all non empty compact subsets X, Y of E_{T}^{2} such that N-boundX < N-boundY holds N-maxX ∪ Y = N-maxY.

(29) For all non empty compact subsets X, Y of E_{T}^{2} such that E-boundX < E-boundY holds E-minX ∪ Y = E-minY.

(30) For all non empty compact subsets X, Y of E_{T}^{2} such that E-boundX < E-boundY holds E-maxX ∪ Y = E-maxY.

(31) For all non empty compact subsets X, Y of E_{T}^{2} such that S-boundX < S-boundY holds S-minX ∪ Y = S-minX.

(32) For all non empty compact subsets X, Y of E_{T}^{2} such that S-boundX < S-boundY holds S-maxX ∪ Y = S-maxX.

(33) For all non empty compact subsets X, Y of E_{T}^{2} such that W-boundX < W-boundY holds W-minX ∪ Y = W-minX.

(34) For all non empty compact subsets X, Y of E_{T}^{2} such that W-boundX < W-boundY holds W-maxX ∪ Y = W-maxX.

(35) Let f be a non empty finite sequence of elements of E_{T}^{2} and p be a point of E_{T}^{2}. If f is a special sequence and p ∈ L̃(f), then (⇃ p, f)_{len ⇃ p,f} = f_{len f}.

(36) Let f be a non constant standard special circular sequence, p, q be points of E_{T}^{2}, and g be a connected subset of E_{T}^{2}. If p ∈ RightComp(f) and q ∈ LeftComp(f) and p ∈ g and q ∈ g, then g meets L̃(f).

One can verify that there exists special sequence finite sequence of elements of E_{T}^{2} which is non constant, standard, and s.c.c..

Next we state a number of propositions:

(37) For every S-sequence f in ℝ^{2} and for every point p of E_{T}^{2} such that p ∈ rngf holds ⇃ p, f = mid(f, p ↫ f, lenf).

(38) Let M be a Go-board and f be a S-sequence in ℝ^{2}. Suppose f is a sequence which elements belong to M. Let p be a point of E_{T}^{2}. If p ∈ rngf, then ⇂ f, p is a sequence which elements belong to M.

(39) Let M be a Go-board and f be a S-sequence in ℝ^{2}. Suppose f is a sequence which elements belong to M. Let p be a point of E_{T}^{2}. If p ∈ rngf, then ⇃ p, f is a sequence which elements belong to M.

(40) Let G be a Go-board and f be a finite sequence of elements of E_{T}^{2}. Suppose f is a sequence which elements belong to G. Let i, j be natural numbers. If 1 i and i lenG and 1 j and j widthG, then if G ∘ (i, j) ∈ L̃(f), then G ∘ (i, j) ∈ rngf.

(41) Let f be a S-sequence in ℝ^{2} and g be a finite sequence of elements of

E_{T}^{2}. Suppose that

(i) g is unfolded, s.n.c., and one-to-one, (ii) L̃(f) ∩ L̃(g) = {f_{1}}, (iii) f_{1} = g_{len g}, (iv) for every natural number i such that 1 i and i + 2 lenf holds

L(f, i) ∩ L(f_{len f}, g_{1}) = ∅, and

(v) for every natural number i such that 2 i and i + 1 leng holds L(g, i) ∩ L(f_{len f}, g_{1}) = ∅. Then f ^{⌢} g is s.c.c..

(42) Let C be a compact non vertical non horizontal non empty subset of E_{T}^{2}. Then there exists a natural number i such that 1 i and i + 1 lenGauge(C, n) and W-minC ∈ cell(Gauge(C, n), 1, i) and W-minC ≠ Gauge(C, n) ∘ (2, i).

(43) For every S-sequence f in ℝ^{2} and for every point p of E_{T}^{2} such that p ∈ L̃(f) and f(lenf) ∈ L̃(⇂ f, p) holds f(lenf) = p.

(44) For every non empty finite sequence f of elements of E_{T}^{2} and for every point p of E_{T}^{2} holds ⇂ f, p ≠ ∅.

(45) For every S-sequence f in ℝ^{2} and for every point p of E_{T}^{2} such that p ∈ L̃(f) holds (⇂ f, p)_{len ⇂ f,p} = p.

(46) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and p be a point of E_{T}^{2}. If p ∈ L̃(UpperSeq(C, n)) and p_{1} = E-bound L̃(Cage(C, n)), then p = E-max L̃(Cage(C, n)).

(47) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and p be a point of E_{T}^{2}. If p ∈ L̃(LowerSeq(C, n)) and p_{1} = W-bound L̃(Cage(C, n)), then p = W-min L̃(Cage(C, n)).

(48) Let G be a Go-board, f, g be finite sequences of elements of E_{T}^{2}, and k be a natural number. Suppose 1 k and k < lenf and f^{⌢} g is a sequence which elements belong to G. Then left cell(f ^{⌢} g, k, G) = left cell(f, k, G) and right cell(f ^{⌢} g, k, G) = right cell(f, k, G).

(49) Let D be a set, f, g be finite sequences of elements of D, and i be a natural number. If i lenf, then (f ⌢⌢ g)↾i = f↾i.

(50) For every set D and for all finite sequences f, g of elements of D holds (f ⌢⌢ g)↾ lenf = f.

(51) Let G be a Go-board, f, g be finite sequences of elements of E_{T}^{2}, and k be a natural number. Suppose 1 k and k < lenf and f ⌢⌢ g is a sequence which elements belong to G. Then left cell(f ⌢⌢ g, k, G) = left cell(f, k, G) and right cell(f ⌢⌢ g, k, G) = right cell(f, k, G).

(52) Let G be a Go-board, f be a S-sequence in ℝ^{2}, p be a point of E_{T}^{2}, and k be a natural number. Suppose 1 k and k < p ↫ f and f is a sequence which elements belong to G and p ∈ rngf. Then left cell(⇂ f, p, k, G) = left cell(f, k, G) and right cell(⇂ f, p, k, G) = right cell(f, k, G).

(53) Let G be a Go-board, f be a finite sequence of elements of E_{T}^{2}, p be a point of E_{T}^{2}, and k be a natural number. Suppose 1 k and k < p ↫ f and f is a sequence which elements belong to G. Then left cell(f − : p, k, G) = left cell(f, k, G) and right cell(f − : p, k, G) = right cell(f, k, G).

(54) Let f, g be finite sequences of elements of E_{T}^{2}. Suppose that (i) f is unfolded, s.n.c., and one-to-one, (ii) g is unfolded, s.n.c., and one-to-one, (iii) f_{len f} = g_{1}, and (iv) L̃(f) ∩ L̃(g) = {g_{1}}.

Then f ⌢⌢ g is s.n.c..

(55) Let f, g be finite sequences of elements of E_{T}^{2}. Suppose f is one-to-one and g is one-to-one and rngf ∩ rngg ⊆ {g_{1}}. Then f ⌢⌢ g is one-to-one.

(56) Let f be a finite sequence of elements of E_{T}^{2} and p be a point of E_{T}^{2}. If f is a special sequence and p ∈ rngf and p ≠ f(1), then Index(p, f)+1 = p ↫ f.

(57) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and k widthGauge(C, n) and Gauge(C, n) ∘ (i, k) ∈ L̃(UpperSeq(C, n)) and Gauge(C, n) ∘ (i, j) ∈ L̃(LowerSeq(C, n)). Then j ≠ k.

(58) Let C be a simple closed curve and i, j, k be natural numbers. Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (i, k)} and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (i, j)}. Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets LowerArcC.

(59) Let C be a simple closed curve and i, j, k be natural numbers.

Suppose 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ L̃(UpperSeq(C, n)) = {Gauge(C, n) ∘ (i, k)} and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ L̃(LowerSeq(C, n)) = {Gauge(C, n) ∘ (i, j)}. Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets UpperArcC.

(60) Let C be a simple closed curve and i, j, k be natural numbers. Suppose that 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and n > 0 and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ UpperArc L̃(Cage(C, n)) = {Gauge(C, n) ∘ (i, k)} and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ LowerArc L̃(Cage(C, n)) = {Gauge(C, n) ∘ (i, j)}. Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets LowerArcC.

(61) Let C be a simple closed curve and i, j, k be natural numbers. Suppose that 1 < i and i < lenGauge(C, n) and 1 j and j k and k widthGauge(C, n) and n > 0 and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ UpperArc L̃(Cage(C, n)) = {Gauge(C, n) ∘ (i, k)} and L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) ∩ LowerArc L̃(Cage(C, n)) = {Gauge(C, n) ∘ (i, j)}. Then L(Gauge(C, n) ∘ (i, j), Gauge(C, n) ∘ (i, k)) meets UpperArcC.

(62) Let C be a compact connected non vertical non horizontal subset of E_{T}^{2} and j be a natural number. Suppose Gauge(C, n+1)∘(CenterGauge(C, n+ 1), j) ∈ UpperArc L̃(Cage(C, n+1)) and 1 j and j widthGauge(C, n+ 1). Then L(Gauge(C, 1) ∘ (CenterGauge(C, 1), 1), Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j)) meets LowerArc L̃(Cage(C, n + 1)).

(63) Let C be a simple closed curve and j, k be natural numbers. Suppose

that

(i) 1 j, (ii) j k, (iii) k widthGauge(C, n + 1), (iv) L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j), Gauge(C, n +

1) ∘ (CenterGauge(C, n + 1), k)) ∩ UpperArc L̃(Cage(C, n + 1)) = {Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k)}, and

(v) L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j), Gauge(C, n + 1) ∘ (CenterGauge(C, n+1), k))∩LowerArc L̃(Cage(C, n+1)) = {Gauge(C, n+ 1) ∘ (CenterGauge(C, n + 1), j)}. Then L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j), Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k)) meets LowerArcC.

(64) Let C be a simple closed curve and j, k be natural numbers. Suppose

that

(i) 1 j, (ii) j k,

upper and lower sequence on the cage, upper … 79

(iii) k widthGauge(C, n + 1), (iv) L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j), Gauge(C, n +

1) ∘ (CenterGauge(C, n + 1), k)) ∩ UpperArc L̃(Cage(C, n + 1)) = {Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k)}, and

(v) L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j), Gauge(C, n + 1) ∘ (CenterGauge(C, n+1), k))∩LowerArc L̃(Cage(C, n+1)) = {Gauge(C, n+ 1) ∘ (CenterGauge(C, n + 1), j)}. Then L(Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), j), Gauge(C, n + 1) ∘ (CenterGauge(C, n + 1), k)) meets UpperArcC.

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[5] Czesław Byliński. Some properties of restrictions of finite sequences. Formalized Mathematics, 5(2):241–245, 1996.

[6] Czesław Byliński. Gauges. Formalized Mathematics, 8(1):25–27, 1999.

[7] Czesław Byliński. Some properties of cells on Go-board. Formalized Mathematics, 8(1):139–146, 1999.

[8] Czesław Byliński and Piotr Rudnicki. Bounding boxes for compact sets in E^{2}. Formalized Mathematics, 6(3):427–440, 1997.

[9] Czesław Byliński and Mariusz Żynel. Cages - the external approximation of Jordan’s curve. Formalized Mathematics, 9(1):19–24, 2001.

[10] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

[11] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[12] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

[13] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

[14] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

[15] Artur Korniłowicz, Robert Milewski, Adam Naumowicz, and Andrzej Trybulec. Gauges and cages. Part I. Formalized Mathematics, 9(3):501–509, 2001.

[16] Jarosław Kotowicz and Yatsuka Nakamura. Introduction to Go-board - part I. Formalized Mathematics, 3(1):107–115, 1992.

[17] Robert Milewski. Upper and lower sequence of a cage. Formalized Mathematics, 9(4):787– 790, 2001.

[18] Yatsuka Nakamura and Czesław Byliński. Extremal properties of vertices on special polygons. Part I. Formalized Mathematics, 5(1):97–102, 1996.

[19] Yatsuka Nakamura and Roman Matuszewski. Reconstructions of special sequences. Formalized Mathematics, 6(2):255–263, 1997.

[20] Yatsuka Nakamura and Piotr Rudnicki. Vertex sequences induced by chains. Formalized Mathematics, 5(3):297–304, 1996.

[21] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-board into cells. Formalized Mathematics, 5(3):323–328, 1996.

[22] Yatsuka Nakamura and Andrzej Trybulec. A decomposition of a simple closed curves and the order of their points. Formalized Mathematics, 6(4):563–572, 1997.

[23] Beata Padlewska. Connected spaces. Formalized Mathematics, 1(1):239–244, 1990.

80 robert milewski

[24] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[25] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[26] Andrzej Trybulec. Left and right component of the complement of a special closed curve. Formalized Mathematics, 5(4):465–468, 1996.

[27] Andrzej Trybulec. On the decomposition of finite sequences. Formalized Mathematics, 5(3):317–322, 1996.

[28] Andrzej Trybulec and Yatsuka Nakamura. On the order on a special polygon. Formalized Mathematics, 6(4):541–548, 1997.

[29] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[30] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

Received April 5, 2002

Fibonacci Numbers

Robert M. Solovay P. O. Box 5949 Eugene OR 97405 U. S. A.

Summary. We show that Fibonacci commutes with g.c.d.; we then derive the formula connecting the Fibonacci sequence with the roots of the polynomial x^{2} − x − 1.

MML Identifier: FIB NUM.

The terminology and notation used here are introduced in the following articles: [3], [9], [5], [1], [2], [4], [7], [6], and [8].

1. Fibonacci Commutes with gcd

One can prove the following three propositions:

(1) For all natural numbers m, n holds gcd(m, n) = gcd(m, n + m).

(2) For all natural numbers k, m, n such that gcd(k, m) = 1 holds gcd(k, m· n) = gcd(k, n).

(3) For every real number s such that s > 0 there exists a natural number n such that n > 0 and 0 < \frac{1}{n} and \frac{1}{n} s.

In this article we present several logical schemes. The scheme Fib Ind concerns a unary predicate P, and states that:

For every natural number k holds P[k] provided the following conditions are met:

• P[0],

• P[1], and

• For every natural number k such that P[k] and P[k + 1] holds P[k + 2].

The scheme Bin Ind concerns a binary predicate P, and states that:

For all natural numbers m, n holds P[m, n] provided the parameters satisfy the following conditions:

• For all natural numbers m, n such that P[m, n] holds P[n, m], and

• Let k be a natural number. Suppose that for all natural numbers m, n such that m < k and n < k holds P[m, n]. Let m be a natural number. If m k, then P[k, m].

We now state two propositions:

(4) For all natural numbers m, n holds Fib(m+(n+1)) = Fib(n)·Fib(m)+ Fib(n + 1) · Fib(m + 1).

(5) For all natural numbers m, n holds gcd(Fib(m), Fib(n)) = Fib(gcd(m, n)).

2. Fibonacci Numbers and the Golden Mean

Next we state the proposition

(6) Let x, a, b, c be real numbers. Suppose a ≠ 0 and Δ(a, b, c) 0. Then

a · x^{2} + b · x + c = 0 if and only if x = ^{\frac{− b−\sqrt{Δ(a,b,c)}}{2·a}} or x = ^{\frac{− b+\sqrt{Δ(a,b,c)}}{2·a}}.

The real number τ is defined by:

(Def. 1) τ = \frac{1+\sqrt{5}}{2}. The real number \overline{τ} is defined as follows:

(Def. 2) \overline{τ} = \frac{1−\sqrt{5}}{2} . One can prove the following propositions:

(7) For every natural number n holds Fib(n) = \frac{τ^{n}−\overline{τ}^{n}}{\sqrt{5}} .

(8) For every natural number n holds |Fib(n) − \frac{τ^{n}}{\sqrt{5}}| < 1.

(9) For all sequences F, G of real numbers such that for every natural number n holds F (n) = G(n) holds F = G.

(10) For all sequences f, g, h of real numbers such that g is non-zero holds (f/g) (g/h) = f/h.

(11) For all sequences f, g of real numbers and for every natural number n holds (f/g)(n) = \frac{f(n)}{g(n)} and (f/g)(n) = f(n) · g(n)^{−1} .

(12) Let F be a sequence of real numbers. Suppose that for every natural number n holds F (n) = \frac{Fib(n+1)}{Fib(n)}. Then F is convergent and limF = τ. fibonacci numbers 83

Acknowledgments

My thanks to Freek Wiedijk for helping me learn Mizar and to Piotr Rudnicki for instructive comments on an earlier version of this article. This article was finished while I was visiting Bialystok and Adam Naumowicz and Josef Urban helped me through some difficult moments.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek and Piotr Rudnicki. Two programs for scm. Part I - preliminaries. Formalized Mathematics, 4(1):69–72, 1993.

[3] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[4] Jarosław Kotowicz. Convergent sequences and the limit of sequences. Formalized Mathematics, 1(2):273–275, 1990.

[5] Jarosław Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269–272, 1990.

[6] Jan Popiołek. Some properties of functions modul and signum. Formalized Mathematics, 1(2):263–264, 1990.

[7] Jan Popiołek. Quadratic inequalities. Formalized Mathematics, 2(4):507–509, 1991.

[8] Konrad Raczkowski and Andrzej Nędzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213–216, 1991.

[9] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

Received April 19, 2002

Preparing the Internal Approximations of Simple Closed Curves^{1}

Andrzej Trybulec University of Białystok

Summary. We mean by an internal approximation of a simple closed curve a special polygon disjoint with it but sufficiently close to it, i.e. such that it is clock-wise oriented and its right cells meet the curve. We prove lemmas used in the next article to construct a sequence of internal approximations.

MML Identifier: JORDAN11.

The articles [18], [5], [20], [11], [1], [16], [2], [21], [4], [3], [12], [17], [7], [8], [9], [10], [13], [14], [15], [6], and [19] provide the terminology and notation for this paper.

In this paper j, k, n are natural numbers and C is a subset of E_{T}^{2} satisfying conditions of simple closed curve.

Let us consider C. The functor ApproxIndexC yielding a natural number is defined by:

(Def. 1) ApproxIndexC is sufficiently large for C and for every j such that j is

sufficiently large for C holds j ApproxIndexC. Next we state the proposition

(1) ApproxIndexC 1.

Let us consider C. The functor Y-InitStartC yields a natural number and is defined as follows:

(Def. 2) Y-InitStartC < widthGauge(C, ApproxIndexC) and cell(Gauge(C, ApproxIndexC), X-SpanStart(C, ApproxIndexC) − ′ 1, Y-InitStartC) ⊆ BDDC and for every j such that j < widthGauge(C, ApproxIndexC) and cell(Gauge(C, ApproxIndexC), X-SpanStart(C, ApproxIndexC) − ′1, j) ⊆ BDDC holds j Y-InitStartC.

1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

The following propositions are true:

(2) Y-InitStartC > 1.

(3) Y-InitStartC + 1 < widthGauge(C, ApproxIndexC). Let us consider C, n. Let us assume that n is sufficiently large for C. The

functor Y-SpanStart(C, n) yields a natural number and is defined by the conditions (Def. 3).

(Def. 3)(i) Y-SpanStart(C, n) widthGauge(C, n),

(ii) for every k such that Y-SpanStart(C, n) k and k 2^{n− ′ApproxIndex C} · (Y-InitStartC− ′2)+2 holds cell(Gauge(C, n), X-SpanStart(C, n)− ′1, k) ⊆ BDDC, and

(iii) for every j such that j widthGauge(C, n) and for every k such that j k and k 2^{n− ′ApproxIndex C} · (Y-InitStartC − ′ 2) + 2 holds cell(Gauge(C, n), X-SpanStart(C, n) − ′ 1, k) ⊆ BDDC holds j Y-SpanStart(C, n).

One can prove the following propositions:

(4) If n is sufficiently large for C, then X-SpanStart(C, n) = 2^{n− ′ApproxIndex C} · (X-SpanStart(C, ApproxIndexC) − 2) + 2.

(5) If n is sufficiently large for C, then Y-SpanStart(C, n) 2^{n− ′ApproxIndex C} · (Y-InitStartC − ′2) + 2.

(6) If n is sufficiently large for C, then cell(Gauge(C, n), X-SpanStart(C, n)− ′ 1, Y-SpanStart(C, n)) ⊆ BDDC.

(7) If n is sufficiently large for C, then 1 < Y-SpanStart(C, n) and Y-SpanStart(C, n) widthGauge(C, n).

(8) If n is sufficiently large for C, then ⟨⟨X-SpanStart(C, n), Y-SpanStart(C, n)⟩⟩∈ the indices of Gauge(C, n).

(9) If n is sufficiently large for C, then ⟨⟨X-SpanStart(C, n) − ′ 1, Y-SpanStart(C, n)⟩⟩∈ the indices of Gauge(C, n).

(10) If n is sufficiently large for C, then cell(Gauge(C, n), X-SpanStart(C, n)− ′ 1, Y-SpanStart(C, n) − ′1) meets C.

(11) If n is sufficiently large for C, then cell(Gauge(C, n), X-SpanStart(C, n)− ′ 1, Y-SpanStart(C, n)) misses C.

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek. Countable sets and Hessenberg’s theorem. Formalized Mathematics, 2(1):65–69, 1991.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164,

preparing the internal approximations … 87

[5] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[6] Czesław Byliński. Gauges. Formalized Mathematics, 8(1):25–27, 1999.

[7] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

[8] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[9] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

[10] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

[11] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[12] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

[13] Jarosław Kotowicz and Yatsuka Nakamura. Introduction to Go-board - part I. Formalized Mathematics, 3(1):107–115, 1992.

[14] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-board into cells. Formalized Mathematics, 5(3):323–328, 1996.

[15] Yatsuka Nakamura, Andrzej Trybulec, and Czesław Byliński. Bounded domains and unbounded domains. Formalized Mathematics, 8(1):1–13, 1999.

[16] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[17] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[18] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[19] Andrzej Trybulec. More on the external approximation of a continuum. Formalized Mathematics, 9(4):831–841, 2001.

[20] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[21] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

On the General Position of Special Polygons^{1}

Mariusz Giero University of Białystok

Summary. In this paper we introduce the notion of general position. We also show some auxiliary theorems for proving Jordan curve theorem. The following main theorems are proved:

1. End points of a polygon are in the same component of a complement of another polygon if number of common points of these polygons is even;

2. Two points of polygon L are in the same component of a complement of polygon M if two points of polygon M are in the same component of polygon L.

MML Identifier: JORDAN12.

The papers [23], [6], [26], [20], [2], [18], [22], [16], [27], [1], [8], [5], [3], [25], [11], [4], [21], [19], [9], [10], [14], [15], [12], [13], [17], [24], and [7] provide the terminology and notation for this paper.

1. Preliminaries

We adopt the following rules: i, j, k, n denote natural numbers, a, b, c, x denote sets, and r denotes a real number.

The following four propositions are true:

(1) If 1 < i, then 0 < i − ′1.

(2) If 1 i, then i − ′1 < i.

(3) 1 is odd.

(4) Let given n, f be a finite sequence of elements of E_{T}^{n}, and given i. If 1 i and i + 1 lenf, then f_{i} ∈ rngf and f_{i+1} ∈ rngf.

1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

Let us mention that every finite sequence of elements of E_{T}^{2} which is s.n.c. is also s.c.c..

Next we state two propositions:

(5) Let f, g be finite sequences of elements of E_{T}^{2}. If f ⌢⌢ g is unfolded and s.c.c. and leng 2, then f is unfolded and s.n.c..

(6) For all finite sequences g_{1}, g_{2} of elements of E_{T}^{2} holds L̃(g_{1}) ⊆ L̃(g_{1} ⌢⌢ g_{2}).

2. The Notion of General Position and Its Properties

Let us consider n and let f_{1}, f_{2} be finite sequences of elements of E_{T}^{n}. We say that f_{1} is in general position wrt f_{2} if and only if:

(Def. 1) L̃(f_{1}) misses rngf_{2} and for every i such that 1 i and i < lenf_{2} holds

L̃(f_{1}) ∩ L(f_{2}, i) is trivial. Let us consider n and let f_{1}, f_{2} be finite sequences of elements of E_{T}^{n}. We

say that f_{1} and f_{2} are in general position if and only if: (Def. 2) f_{1} is in general position wrt f_{2} and f_{2} is in general position wrt f_{1}.

Let us note that the predicate f_{1} and f_{2} are in general position is symmetric. The following propositions are true:

(7) Let f_{1}, f_{2} be finite sequences of elements of E_{T}^{2}. Suppose f_{1} and f_{2} are in general position. Let f be a finite sequence of elements of E_{T}^{2}. If f = f_{2}↾ Segk, then f_{1} and f are in general position.

(8) Let f_{1}, f_{2}, g_{1}, g_{2} be finite sequences of elements of E_{T}^{2}. Suppose f_{1} ⌢⌢ f_{2} and g_{1} ⌢⌢ g_{2} are in general position. Then f_{1} ⌢⌢ f_{2} and g_{1} are in general position.

In the sequel f, g are finite sequences of elements of E_{T}^{2}. The following propositions are true:

(9) For all k, f, g such that 1 k and k + 1 leng and f and g are in general position holds g(k) ∈ (L̃(f))^{c} and g(k + 1) ∈ (L̃(f))^{c}.

(10) Let f_{1}, f_{2} be finite sequences of elements of E_{T}^{2}. Suppose f_{1} and f_{2} are in general position. Let given i, j. If 1 i and i + 1 lenf_{1} and 1 j and j + 1 lenf_{2}, then L(f_{1}, i) ∩ L(f_{2}, j) is trivial.

(11) For all f, g holds {L(f, i) : 1 i ∧ i + 1 lenf} ⋒ {L(g, j) : 1 j ∧ j + 1 leng} is finite.

(12) For all f, g such that f and g are in general position holds L̃(f) ∩ L̃(g) is finite.

(13) For all f, g such that f and g are in general position and for every k holds L̃(f) ∩ L(g, k) is finite.

3. Properties of Being in the Same Component of a Complement of a Polygon

We use the following convention: f is a non constant standard special circular sequence, g is a special finite sequence of elements of E_{T}^{2}, and p, p_{1}, p_{2}, q are points of E_{T}^{2}.

One can prove the following propositions:

(14) For all f, p_{1}, p_{2} such that L(p_{1}, p_{2}) misses L̃(f) there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and p_{1} ∈ C and p_{2} ∈ C.

(15) There exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and a ∈ C and b ∈ C if and only if a ∈ RightComp(f) and b ∈ RightComp(f) or a ∈ LeftComp(f) and b ∈ LeftComp(f).

(16) a ∈ (L̃(f))^{c} and b ∈ (L̃(f))^{c} and it is not true that there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and a ∈ C and b ∈ C if and only if a ∈ LeftComp(f) and b ∈ RightComp(f) or a ∈ RightComp(f) and b ∈ LeftComp(f).

(17) Let given f, a, b, c. Suppose that

(i) there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and a ∈ C and b ∈ C, and

(ii) there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and b ∈ C and c ∈ C. Then there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and a ∈ C and c ∈ C.

(18) Let given f, a, b, c. Suppose that (i) a ∈ (L̃(f))^{c}, (ii) b ∈ (L̃(f))^{c}, (iii) c ∈ (L̃(f))^{c}, (iv) it is not true that there exists a subset C of E_{T}^{2} such that C is a

component of (L̃(f))^{c} and a ∈ C and b ∈ C, and

(v) it is not true that there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and b ∈ C and c ∈ C. Then there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and a ∈ C and c ∈ C.

4. Cells Are Convex

In the sequel G denotes a Go-board. One can prove the following propositions:

(19) If i lenG, then vstrip(G, i) is convex.

(20) If j widthG, then hstrip(G, j) is convex.

(21) If i lenG and j widthG, then cell(G, i, j) is convex.

(22) For all f, k such that 1 k and k + 1 lenf holds leftcell(f, k) is convex.

(23) For all f, k such that 1 k and k + 1 lenf holds left cell(f, k, the Go-board of f) is convex and right cell(f, k, the Go-board of f) is convex.

5. Properties of Points Lying on the Same Line

The following propositions are true:

(24) Let given p_{1}, p_{2}, f and r be a point of E_{T}^{2}. Suppose r ∈ L(p_{1}, p_{2}) and there exists x such that L̃(f) ∩ L(p_{1}, p_{2}) = {x} and r ∉ L̃(f). Then L̃(f) misses L(p_{1}, r) or L̃(f) misses L(r, p_{2}).

(25) For all points p, q, r, s of E_{T}^{2} such that L(p, q) is vertical and L(r, s) is vertical and L(p, q) meets L(r, s) holds p_{1} = r_{1}.

(26) For all p, p_{1}, p_{2} such that p ∉ L(p_{1}, p_{2}) and (p_{1})_{2} = (p_{2})_{2} and (p_{2})_{2} = p_{2} holds p_{1} ∈ L(p, p_{2}) or p_{2} ∈ L(p, p_{1}).

(27) For all p, p_{1}, p_{2} such that p ∉ L(p_{1}, p_{2}) and (p_{1})_{1} = (p_{2})_{1} and (p_{2})_{1} = p_{1} holds p_{1} ∈ L(p, p_{2}) or p_{2} ∈ L(p, p_{1}).

(28) If p ≠ p_{1} and p ≠ p_{2} and p ∈ L(p_{1}, p_{2}), then p_{1} ∉ L(p, p_{2}).

(29) Let given p, p_{1}, p_{2}, q. Suppose q ∉ L(p_{1}, p_{2}) and p ∈ L(p_{1}, p_{2}) and p ≠ p_{1} and p ≠ p_{2} and (p_{1})_{1} = (p_{2})_{1} and (p_{2})_{1} = q_{1} or (p_{1})_{2} = (p_{2})_{2} and (p_{2})_{2} = q_{2}. Then p_{1} ∈ L(q, p) or p_{2} ∈ L(q, p).

(30) Let p_{1}, p_{2}, p_{3}, p_{4}, p be points of E_{T}^{2}. Suppose (p_{1})_{1} = (p_{2})_{1} and (p_{3})_{1} = (p_{4})_{1} or (p_{1})_{2} = (p_{2})_{2} and (p_{3})_{2} = (p_{4})_{2} but L(p_{1}, p_{2}) ∩ L(p_{3}, p_{4}) = {p}. Then p = p_{1} or p = p_{2} or p = p_{3}.

6. The Position of the Points of a Polygon with Respect to Another Polygon

We now state several propositions:

(31) Let given p, p_{1}, p_{2}, f. Suppose L̃(f) ∩ L(p_{1}, p_{2}) = {p}. Let r be a point

of E_{T}^{2}. Suppose that

(i) r ∉ L(p_{1}, p_{2}), (ii) p_{1} ∉ L̃(f), (iii) p_{2} ∉ L̃(f), (iv) (p_{1})_{1} = (p_{2})_{1} and (p_{1})_{1} = r_{1} or (p_{1})_{2} = (p_{2})_{2} and (p_{1})_{2} = r_{2},

(v) there exists i such that 1 i and i+1 lenf and r ∈ right cell(f, i, the Go-board of f) or r ∈ left cell(f, i, the Go-board of f) and p ∈ L(f, i), and

(vi) r ∉ L̃(f).

Then (vii) there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c}

and r ∈ C and p_{1} ∈ C, or (viii) there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c}

and r ∈ C and p_{2} ∈ C.

(32) Let given f, p_{1}, p_{2}, p. Suppose L̃(f) ∩ L(p_{1}, p_{2}) = {p}. Let r_{1}, r_{2} be

points of E_{T}^{2}. Suppose that

(i) p_{1} ∉ L̃(f), (ii) p_{2} ∉ L̃(f), (iii) (p_{1})_{1} = (p_{2})_{1} and (p_{1})_{1} = (r_{1})_{1} and (r_{1})_{1} = (r_{2})_{1} or (p_{1})_{2} = (p_{2})_{2} and

(p_{1})_{2} = (r_{1})_{2} and (r_{1})_{2} = (r_{2})_{2}, (iv) there exists i such that 1 i and i+1 lenf and r_{1} ∈ left cell(f, i, the

Go-board of f) and r_{2} ∈ right cell(f, i, the Go-board of f) and p ∈ L(f, i),

(v) r_{1} ∉ L̃(f), and (vi) r_{2} ∉ L̃(f).

Then it is not true that there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and p_{1} ∈ C and p_{2} ∈ C.

(33) Let given p, f, p_{1}, p_{2}. Suppose L̃(f) ∩ L(p_{1}, p_{2}) = {p} and (p_{1})_{1} = (p_{2})_{1} or (p_{1})_{2} = (p_{2})_{2} and p_{1} ∉ L̃(f) and p_{2} ∉ L̃(f) and rngf misses L(p_{1}, p_{2}). Then it is not true that there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and p_{1} ∈ C and p_{2} ∈ C.

(34) Let f be a non constant standard special circular sequence and g be a special finite sequence of elements of E_{T}^{2}. Suppose f and g are in general

position. Let given k. Suppose 1 k and k+1 leng. Then \overline{\overline{L̃(f) ∩ L(g, k)}} is an even natural number if and only if there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f))^{c} and g(k) ∈ C and g(k + 1) ∈ C.

(35) Let f_{1}, f_{2}, g_{1} be special finite sequences of elements of E_{T}^{2}. Suppose that (i) f_{1} ⌢⌢ f_{2} is a non constant standard special circular sequence, (ii) f_{1} ⌢⌢ f_{2} and g_{1} are in general position, (iii) leng_{1} 2, and (iv) g_{1} is unfolded and s.n.c..

Then \overline{\overline{L̃(f_{1} ⌢⌢ f_{2}) ∩ L̃(g_{1})}} is an even natural number if and only if there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f_{1} ⌢⌢ f_{2}))^{c} and g_{1}(1) ∈ C and g_{1}(leng_{1}) ∈ C.

(36) Let f_{1}, f_{2}, g_{1}, g_{2} be special finite sequences of elements of E_{T}^{2}. Suppose

that

(i) f_{1} ⌢⌢ f_{2} is a non constant standard special circular sequence, (ii) g_{1} ⌢⌢ g_{2} is a non constant standard special circular sequence, (iii) L̃(f_{1}) misses L̃(g_{2}), (iv) L̃(f_{2}) misses L̃(g_{1}), and 94 mariusz giero

(v) f_{1} ⌢⌢ f_{2} and g_{1} ⌢⌢ g_{2} are in general position. Let p_{1}, p_{2}, q_{1}, q_{2} be points of E_{T}^{2}. Suppose that f_{1}(1) = p_{1} and f_{1}(lenf_{1}) = p_{2} and g_{1}(1) = q_{1} and g_{1}(leng_{1}) = q_{2} and (f_{1})_{len f_{1}} = (f_{2})_{1} and (g_{1})_{len g_{1}} = (g_{2})_{1} and p_{1} ≠ p_{2} and q_{1} ≠ q_{2} and p_{1} ∈ L̃(f_{1})∩L̃(f_{2}) and q_{1} ∈ L̃(g_{1})∩L̃(g_{2}) and there exists a subset C of E_{T}^{2} such that C is a component of (L̃(f_{1} ⌢ ⌢ f_{2}))^{c} and q_{1} ∈ C and q_{2} ∈ C. Then there exists a subset C of E_{T}^{2} such that C is a component of (L̃(g_{1} ⌢⌢ g_{2}))^{c} and p_{1} ∈ C and p_{2} ∈ C.

Acknowledgments

I would like to thank Prof. Andrzej Trybulec for his help in preparation of this article. I also thank Adam Grabowski, Robert Milewski and Adam Naumowicz for their helpful comments.

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Józef Białas. Group and field definitions. Formalized Mathematics, 1(3):433–439, 1990.

[5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[6] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.

[7] Czesław Byliński. Some properties of cells on Go-board. Formalized Mathematics, 8(1):139–146, 1999.

[8] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.

[9] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[10] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

[11] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

[12] Jarosław Kotowicz and Yatsuka Nakamura. Introduction to Go-board - part I. Formalized Mathematics, 3(1):107–115, 1992.

[13] Jarosław Kotowicz and Yatsuka Nakamura. Introduction to Go-board - part II. Formalized Mathematics, 3(1):117–121, 1992.

[14] Yatsuka Nakamura and Czesław Byliński. Extremal properties of vertices on special polygons. Part I. Formalized Mathematics, 5(1):97–102, 1996.

[15] Yatsuka Nakamura and Jarosław Kotowicz. The Jordan’s property for certain subsets of the plane. Formalized Mathematics, 3(2):137–142, 1992.

[16] Yatsuka Nakamura and Piotr Rudnicki. Vertex sequences induced by chains. Formalized Mathematics, 5(3):297–304, 1996.

[17] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-board into cells. Formalized Mathematics, 5(3):323–328, 1996.

[18] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[19] Beata Padlewska. Connected spaces. Formalized Mathematics, 1(1):239–244, 1990.

[20] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990.

[21] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[22] Piotr Rudnicki and Andrzej Trybulec. Abian’s fixed point theorem. Formalized Mathematics, 6(3):335–338, 1997.

on the general position … 95

[23] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[24] Andrzej Trybulec. Left and right component of the complement of a special closed curve. Formalized Mathematics, 5(4):465–468, 1996.

[25] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[26] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[27] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

Introducing Spans^{1}

Andrzej Trybulec University of Białystok

Summary. A sequence of internal approximations of simple closed curves is introduced. They are called spans.

MML Identifier: JORDAN13.

The notation and terminology used here are introduced in the following papers: [23], [17], [26], [2], [18], [27], [5], [4], [1], [3], [4], [25], [11], [12], [21], [7], [9], [10], [10], [12], [14], [28], [6], [7], [19], and [23].

Let C be a non vertical non horizontal non empty subset of E_{T}^{2} satisfying conditions of simple closed curve and let n be a natural number. Let us assume that n is sufficiently large for C. The functor Span(C, n) yielding a clockwise oriented standard non constant special circular sequence is defined by the conditions (Def. 1).

(Def. 1)(i) Span(C, n) is a sequence which elements belong to Gauge(C, n), (ii) (Span(C, n))_{1} = Gauge(C, n)∘(X-SpanStart(C, n), Y-SpanStart(C, n)), (iii) (Span(C, n))_{2} = Gauge(C, n) ∘ (X-SpanStart(C, n) − ′1,

Y-SpanStart(C, n)), and (iv) for every natural number k such that 1 k and k + 2

lenSpan(C, n) holds if front right cell(Span(C, n), k, Gauge(C, n)) misses C and front left cell(Span(C, n), k, Gauge(C, n)) misses C, then Span(C, n) turns left k, Gauge(C, n) and if front right cell(Span(C, n), k, Gauge(C, n)) misses C and front left cell(Span(C, n), k, Gauge(C, n)) meets C, then Span(C, n) goes straight k, Gauge(C, n) and if front right cell(Span(C, n), k, Gauge(C, n)) meets C, then Span(C, n) turns right k, Gauge(C, n).

1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

98 andrzej trybulec

References

[1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.

[5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[6] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[7] Czesław Byliński. Gauges. Formalized Mathematics, 8(1):25–27, 1999.

[8] Czesław Byliński. Some properties of cells on Go-board. Formalized Mathematics, 8(1):139–146, 1999.

[9] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

[10] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[11] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

[12] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

[13] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

[14] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.

[15] Jarosław Kotowicz and Yatsuka Nakamura. Introduction to Go-board - part I. Formalized Mathematics, 3(1):107–115, 1992.

[16] Yatsuka Nakamura and Czesław Byliński. Extremal properties of vertices on special polygons. Part I. Formalized Mathematics, 5(1):97–102, 1996.

[17] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-board into cells. Formalized Mathematics, 5(3):323–328, 1996.

[18] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[19] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[20] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[21] Andrzej Trybulec. More on the external approximation of a continuum. Formalized Mathematics, 9(4):831–841, 2001.

[22] Andrzej Trybulec. Preparing the internal approximations of simple closed curves. Formalized Mathematics, 10(2):85–87, 2002.

[23] Andrzej Trybulec and Yatsuka Nakamura. On the order on a special polygon. Formalized Mathematics, 6(4):541–548, 1997.

[24] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[25] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[26] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

General Fashoda Meet Theorem for Unit Circle

Yatsuka Nakamura Shinshu University Nagano

Summary. Outside and inside Fashoda theorems are proven for points in general position on unit circle. Four points must be ordered in a sense of ordering for simple closed curve. For preparation of proof, the relation between the order and condition of coordinates of points on unit circle is discussed.

MML Identifier: JGRAPH 5.

The articles [11], [9], [17], [21], [3], [4], [20], [5], [10], [1], [18], [7], [8], [12], [19], [16], [6], [2], [15], [14], and [13] provide the terminology and notation for this paper.

1. Preliminaries

In this paper x, a are real numbers. Next we state a number of propositions:

(1) If a 0 and (x − a) · (x + a) 0, then − a x or x a.

(2) If a 0 and x < a, then x^{2} > a^{2}.

(3) For every point p of E_{T}^{2} such that |p| 1 holds − 1 p_{1} and p_{1} 1 and − 1 p_{2} and p_{2} 1.

(4) For every point p of E_{T}^{2} such that |p| 1 and p_{1} ≠ 0 and p_{2} ≠ 0 holds − 1 < p_{1} and p_{1} < 1 and − 1 < p_{2} and p_{2} < 1.

(5) Let a, b, d, e, r_{3} be real numbers, P_{1}, P_{2} be non empty metric structures, x be an element of the carrier of P_{1}, and x_{2} be an element of the carrier of P_{2}. Suppose d a and a b and b e and P_{1} = [a, b]_{M} and P_{2} = [d, e]_{M} and x = x_{2} and x ∈ the carrier of P_{1} and x_{2} ∈ the carrier of P_{2}. Then Ball(x, r_{3}) ⊆ Ball(x_{2}, r_{3}).

(6) Let a, b, d, e be real numbers and B be a subset of [d, e]_{T}. If d a and a b and b e and B = [a, b], then [a, b]_{T} = [d, e]_{T}↾B.

(7) For all real numbers a, b and for every subset B of 𝕀 such that 0 a and a b and b 1 and B = [a, b] holds [a, b]_{T} = 𝕀↾B.

(8) Let X be a topological structure, Y, Z be non empty topological structures, f be a map from X into Y, and h be a map from Y into Z. If h is a homeomorphism and f is continuous, then h · f is continuous.

(9) Let X, Y, Z be topological structures, f be a map from X into Y, and h be a map from Y into Z. If h is a homeomorphism and f is one-to-one, then h · f is one-to-one.

(10) Let X be a topological structure, S, V be non empty topological structures, B be a non empty subset of S, f be a map from X into S↾B, g be a map from S into V, and h be a map from X into V. If h = g · f and f is continuous and g is continuous, then h is continuous.

(11) Let a, b, d, e, s_{1}, s_{2}, t_{1}, t_{2} be real numbers and h be a map from [a, b]_{T} into [d, e]_{T}. Suppose h is a homeomorphism and h(s_{1}) = t_{1} and h(s_{2}) = t_{2} and h(a) = d and h(b) = e and d e and t_{1} t_{2} and s_{1} ∈ [a, b] and s_{2} ∈ [a, b]. Then s_{1} s_{2}.

(12) Let a, b, d, e, s_{1}, s_{2}, t_{1}, t_{2} be real numbers and h be a map from [a, b]_{T} into [d, e]_{T}. Suppose h is a homeomorphism and h(s_{1}) = t_{1} and h(s_{2}) = t_{2} and h(a) = e and h(b) = d and e d and t_{1} t_{2} and s_{1} ∈ [a, b] and s_{2} ∈ [a, b]. Then s_{1} s_{2}.

(13) For every natural number n holds − 0_{E_{T}^{n}} = 0_{E_{T}^{n}}.

2. Fashoda Meet Theorems for Circle in Special Case

Next we state two propositions:

(14) Let f, g be maps from 𝕀 into E_{T}^{2}, a, b, c, d be real numbers, and O, I be points of 𝕀. Suppose that O = 0 and I = 1 and f is continuous and one-to-one and g is continuous and one-to-one and a ≠ b and c ≠ d and f(O)_{1} = a and c f(O)_{2} and f(O)_{2} d and f(I)_{1} = b and c f(I)_{2} and f(I)_{2} d and g(O)_{2} = c and a g(O)_{1} and g(O)_{1} b and g(I)_{2} = d and a g(I)_{1} and g(I)_{1} b and for every point r of 𝕀 holds a f(r)_{1} or f(r)_{1} b or c f(r)_{2} or f(r)_{2} d but a g(r)_{1} or g(r)_{1} b or c g(r)_{2} or g(r)_{2} d. Then rngf meets rngg.

(15) Let f be a map from 𝕀 into E_{T}^{2}. Suppose f is continuous and one-to-one. Then there exists a map f_{2} from 𝕀 into E_{T}^{2} such that f_{2}(0) = f(1) and f_{2}(1) = f(0) and rngf_{2} = rngf and f_{2} is continuous and one-to-one.

In the sequel p, q denote points of E_{T}^{2}. Next we state several propositions:

(16) Let f, g be maps from 𝕀 into E_{T}^{2}, C_{0}, K_{1}, K_{2}, K_{3}, K_{4} be subsets of E_{T}^{2}, and O, I be points of 𝕀. Suppose that O = 0 and I = 1 and f is continuous and one-to-one and g is continuous and one-to-one and C_{0} = {p : |p| 1} and K_{1} = {q_{1}; q_{1} ranges over points of E_{T}^{2}: |q_{1}| = 1 ∧ (q_{1})_{2} (q_{1})_{1} ∧ (q_{1})_{2} − (q_{1})_{1}} and K_{2} = {q_{2}; q_{2} ranges over points of E_{T}^{2}: |q_{2}| = 1 ∧ (q_{2})_{2} (q_{2})_{1} ∧ (q_{2})_{2} − (q_{2})_{1}} and K_{3} = {q_{3}; q_{3} ranges over points of E_{T}^{2}: |q_{3}| = 1 ∧ (q_{3})_{2} (q_{3})_{1} ∧ (q_{3})_{2} − (q_{3})_{1}} and K_{4} = {q_{4}; q_{4} ranges over points of E_{T}^{2}: |q_{4}| = 1 ∧ (q_{4})_{2} (q_{4})_{1} ∧ (q_{4})_{2} − (q_{4})_{1}} and f(O) ∈ K_{2} and f(I) ∈ K_{1} and g(O) ∈ K_{3} and g(I) ∈ K_{4} and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg.

(17) Let f, g be maps from 𝕀 into E_{T}^{2}, C_{0}, K_{1}, K_{2}, K_{3}, K_{4} be subsets of E_{T}^{2}, and O, I be points of 𝕀. Suppose that O = 0 and I = 1 and f is continuous and one-to-one and g is continuous and one-to-one and C_{0} = {p : |p| 1} and K_{1} = {q_{1}; q_{1} ranges over points of E_{T}^{2}: |q_{1}| = 1 ∧ (q_{1})_{2} (q_{1})_{1} ∧ (q_{1})_{2} − (q_{1})_{1}} and K_{2} = {q_{2}; q_{2} ranges over points of E_{T}^{2}: |q_{2}| = 1 ∧ (q_{2})_{2} (q_{2})_{1} ∧ (q_{2})_{2} − (q_{2})_{1}} and K_{3} = {q_{3}; q_{3} ranges over points of E_{T}^{2}: |q_{3}| = 1 ∧ (q_{3})_{2} (q_{3})_{1} ∧ (q_{3})_{2} − (q_{3})_{1}} and K_{4} = {q_{4}; q_{4} ranges over points of E_{T}^{2}: |q_{4}| = 1 ∧ (q_{4})_{2} (q_{4})_{1} ∧ (q_{4})_{2} − (q_{4})_{1}} and f(O) ∈ K_{2} and f(I) ∈ K_{1} and g(O) ∈ K_{4} and g(I) ∈ K_{3} and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg.

(18) Let f, g be maps from 𝕀 into E_{T}^{2}, C_{0}, K_{1}, K_{2}, K_{3}, K_{4} be subsets of E_{T}^{2}, and O, I be points of 𝕀. Suppose that O = 0 and I = 1 and f is continuous and one-to-one and g is continuous and one-to-one and C_{0} = {p : |p| 1} and K_{1} = {q_{1}; q_{1} ranges over points of E_{T}^{2}: |q_{1}| = 1 ∧ (q_{1})_{2} (q_{1})_{1} ∧ (q_{1})_{2} − (q_{1})_{1}} and K_{2} = {q_{2}; q_{2} ranges over points of E_{T}^{2}: |q_{2}| = 1 ∧ (q_{2})_{2} (q_{2})_{1} ∧ (q_{2})_{2} − (q_{2})_{1}} and K_{3} = {q_{3}; q_{3} ranges over points of E_{T}^{2}: |q_{3}| = 1 ∧ (q_{3})_{2} (q_{3})_{1} ∧ (q_{3})_{2} − (q_{3})_{1}} and K_{4} = {q_{4}; q_{4} ranges over points of E_{T}^{2}: |q_{4}| = 1 ∧ (q_{4})_{2} (q_{4})_{1} ∧ (q_{4})_{2} − (q_{4})_{1}} and f(O) ∈ K_{2} and f(I) ∈ K_{1} and g(O) ∈ K_{3} and g(I) ∈ K_{4} and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg.

(19) Let f, g be maps from 𝕀 into E_{T}^{2} and C_{0} be a subset of E_{T}^{2}. Suppose that C_{0} = {q : |q| 1} and f is continuous and one-to-one and g is continuous and one-to-one and f(0) = [− 1, 0] and f(1) = [1, 0] and g(1) = [0, 1] and g(0) = [0, − 1] and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg.

(20) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and C_{0} be a subset of E_{T}^{2}. Suppose that (i) C_{0} = {p : |p| 1}, (ii) |p_{1}| = 1, (iii) |p_{2}| = 1, (iv) |p_{3}| = 1,

(v) |p_{4}| = 1, and (vi) there exists a map h from E_{T}^{2} into E_{T}^{2} such that h is a homeomorphism and h^{∘}C_{0} ⊆ C_{0} and h(p_{1}) = [− 1, 0] and h(p_{2}) = [0, 1] and h(p_{3}) = [1, 0] and h(p_{4}) = [0, − 1]. Let f, g be maps from 𝕀 into E_{T}^{2}. Suppose that f is continuous and oneto-one and g is continuous and one-to-one and f(0) = p_{1} and f(1) = p_{3} and g(0) = p_{4} and g(1) = p_{2} and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg.

3. Properties of Fan Morphisms

The following propositions are true:

(21) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} > 0. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphN(q), then p_{2} > 0.

(22) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} 0. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphN(q), then p_{2} 0.

(23) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} 0 and \frac{q_{1}}{|q|} < c_{1} and |q| ≠ 0. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphN(q), then p_{2} 0 and p_{1} < 0.

(24) Let c_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and (q_{1})_{2} 0 and (q_{2})_{2} 0 and |q_{1}| ≠ 0 and |q_{2}| ≠ 0 and \frac{(q_{1})_{1}}{|q_{1}|} < \frac{(q_{2})_{1}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = c_{1} -FanMorphN(q_{1}) and

p_{2} = c_{1} -FanMorphN(q_{2}), then \frac{(p_{1})_{1}}{|p_{1}|} < \frac{(p_{2})_{1}}{|p_{2}|} .

(25) Let s_{3} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < s_{3} and s_{3} < 1 and q_{1} > 0. Let p be a point of E_{T}^{2}. If p = s_{3} -FanMorphE(q), then p_{1} > 0.

(26) Let s_{3} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < s_{3} and s_{3} < 1 and q_{1} 0 and \frac{q_{2}}{|q|} < s_{3} and |q| ≠ 0. Let p be a point of E_{T}^{2}. If p = s_{3} -FanMorphE(q), then p_{1} 0 and p_{2} < 0.

(27) Let s_{3} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < s_{3} and s_{3} < 1 and (q_{1})_{1} 0 and (q_{2})_{1} 0 and |q_{1}| ≠ 0 and |q_{2}| ≠ 0 and \frac{(q_{1})_{2}}{|q_{1}|} < \frac{(q_{2})_{2}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = s_{3} -FanMorphE(q_{1}) and

p_{2} = s_{3} -FanMorphE(q_{2}), then \frac{(p_{1})_{2}}{|p_{1}|} < \frac{(p_{2})_{2}}{|p_{2}|} .

(28) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} < 0. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphS(q), then p_{2} < 0.

(29) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} < 0 and \frac{q_{1}}{|q|} > c_{1}. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphS(q), then p_{2} < 0 and p_{1} > 0.

(30) Let c_{1} be a real number and q_{1}, q_{2} be points of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and (q_{1})_{2} 0 and (q_{2})_{2} 0 and |q_{1}| ≠ 0 and |q_{2}| ≠ 0 and \frac{(q_{1})_{1}}{|q_{1}|} < \frac{(q_{2})_{1}}{|q_{2}|} . Let p_{1}, p_{2} be points of E_{T}^{2}. If p_{1} = c_{1} -FanMorphS(q_{1}) and

p_{2} = c_{1} -FanMorphS(q_{2}), then \frac{(p_{1})_{1}}{|p_{1}|} < \frac{(p_{2})_{1}}{|p_{2}|} .

4. Order of Points on Circle

One can prove the following propositions:

(31) For every compact non empty subset P of E_{T}^{2} such that P = {q : |q| = 1} holds W-boundP = − 1 and E-boundP = 1 and S-boundP = − 1 and N-boundP = 1.

(32) For every compact non empty subset P of E_{T}^{2} such that P = {q : |q| = 1} holds W-minP = [− 1, 0].

(33) For every compact non empty subset P of E_{T}^{2} such that P = {q : |q| = 1} holds E-maxP = [1, 0].

(34) For every map f from E_{T}^{2} into ℝ^{1} such that for every point p of E_{T}^{2} holds f(p) = proj1(p) holds f is continuous.

(35) For every map f from E_{T}^{2} into ℝ^{1} such that for every point p of E_{T}^{2} holds f(p) = proj2(p) holds f is continuous.

(36) For every compact non empty subset P of E_{T}^{2} such that P = {q; q ranges over points of E_{T}^{2}: |q| = 1} holds UpperArcP ⊆ P and LowerArcP ⊆ P.

(37) Let P be a compact non empty subset of E_{T}^{2}. Suppose P = {q; q ranges over points of E_{T}^{2}: |q| = 1}. Then UpperArcP = {p; p ranges over points of E_{T}^{2}: p ∈ P ∧ p_{2} 0}.

(38) Let P be a compact non empty subset of E_{T}^{2}. Suppose P = {q; q ranges over points of E_{T}^{2}: |q| = 1}. Then LowerArcP = {p; p ranges over points of E_{T}^{2}: p ∈ P ∧ p_{2} 0}.

(39) Let a, b, d, e be real numbers. Suppose a b and e > 0. Then there exists a map f from [a, b]_{T} into [e · a + d, e · b + d]_{T} such that f is a homeomorphism and for every real number r such that r ∈ [a, b] holds f(r) = e · r + d.

(40) Let a, b, d, e be real numbers. Suppose a b and e < 0. Then there exists a map f from [a, b]_{T} into [e · b + d, e · a + d]_{T} such that f is a homeomorphism and for every real number r such that r ∈ [a, b] holds f(r) = e · r + d.

(41) There exists a map f from 𝕀 into [− 1, 1]_{T} such that f is a homeomorphism and for every real number r such that r ∈ [0, 1] holds f(r) = (− 2) · r + 1 and f(0) = 1 and f(1) = − 1.

(42) There exists a map f from 𝕀 into [− 1, 1]_{T} such that f is a homeomorphism and for every real number r such that r ∈ [0, 1] holds f(r) = 2·r −1 and f(0) = − 1 and f(1) = 1.

(43) Let P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1}. Then there exists a map f from [− 1, 1]_{T} into (E_{T}^{2})↾ LowerArcP such that f is a homeomorphism and for every point q of E_{T}^{2} such that q ∈ LowerArcP holds f(q_{1}) = q and f(− 1) = W-minP and f(1) = E-maxP.

(44) Let P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1}. Then there exists a map f from [− 1, 1]_{T} into (E_{T}^{2})↾ UpperArcP such that f is a homeomorphism and for every point q of E_{T}^{2} such that q ∈ UpperArcP holds f(q_{1}) = q and f(− 1) = W-minP and f(1) = E-maxP.

(45) Let P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1}. Then there exists a map f from 𝕀 into (E_{T}^{2})↾ LowerArcP such that

(i) f is a homeomorphism, (ii) for all points q_{1}, q_{2} of E_{T}^{2} and for all real numbers r_{1}, r_{2} such that

f(r_{1}) = q_{1} and f(r_{2}) = q_{2} and r_{1} ∈ [0, 1] and r_{2} ∈ [0, 1] holds r_{1} < r_{2} iff (q_{1})_{1} > (q_{2})_{1},

(iii) f(0) = E-maxP, and (iv) f(1) = W-minP.

(46) Let P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1}. Then there exists a map f from 𝕀 into (E_{T}^{2})↾ UpperArcP such that

(i) f is a homeomorphism, (ii) for all points q_{1}, q_{2} of E_{T}^{2} and for all real numbers r_{1}, r_{2} such that

f(r_{1}) = q_{1} and f(r_{2}) = q_{2} and r_{1} ∈ [0, 1] and r_{2} ∈ [0, 1] holds r_{1} < r_{2} iff (q_{1})_{1} < (q_{2})_{1},

(iii) f(0) = W-minP, and (iv) f(1) = E-maxP.

(47) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. If P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and p_{2} ∈ UpperArcP and LE(p_{1}, p_{2}, P), then p_{1} ∈ UpperArcP.

(48) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and p_{1} ≠ p_{2} and (p_{1})_{1} < 0 and (p_{2})_{1} < 0 and (p_{1})_{2} < 0 and (p_{2})_{2} < 0. Then (p_{1})_{1} > (p_{2})_{1} and (p_{1})_{2} < (p_{2})_{2}.

(49) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and p_{1} ≠ p_{2} and (p_{1})_{1} < 0 and (p_{2})_{1} < 0 and (p_{1})_{2} 0 and (p_{2})_{2} 0.

Then (p_{1})_{1} < (p_{2})_{1} and (p_{1})_{2} < (p_{2})_{2}.

(50) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and p_{1} ≠ p_{2} and (p_{1})_{2} 0 and (p_{2})_{2} 0. Then (p_{1})_{1} < (p_{2})_{1}.

(51) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and p_{1} ≠ p_{2} and (p_{1})_{2} 0 and (p_{2})_{2} 0 and p_{1} ≠ W-minP. Then (p_{1})_{1} > (p_{2})_{1}.

(52) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} but (p_{2})_{2} 0 or (p_{2})_{1} 0 but LE(p_{1}, p_{2}, P). Then (p_{1})_{2} 0 or (p_{1})_{1} 0.

(53) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and p_{1} ≠ p_{2} and (p_{1})_{1} 0 and (p_{2})_{1} 0. Then (p_{1})_{2} > (p_{2})_{2}.

(54) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and p_{1} ∈ P and p_{2} ∈ P and (p_{1})_{1} < 0 and (p_{2})_{1} < 0 and (p_{1})_{2} < 0 and (p_{2})_{2} < 0 and (p_{1})_{1} (p_{2})_{1} or (p_{1})_{2} (p_{2})_{2}. Then LE(p_{1}, p_{2}, P).

(55) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and p_{1} ∈ P and p_{2} ∈ P and (p_{1})_{1} > 0 and (p_{2})_{1} > 0 and (p_{1})_{2} < 0 and (p_{2})_{2} < 0 and (p_{1})_{1} (p_{2})_{1} or (p_{1})_{2} (p_{2})_{2}. Then LE(p_{1}, p_{2}, P).

(56) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and p_{1} ∈ P and p_{2} ∈ P and (p_{1})_{1} < 0 and (p_{2})_{1} < 0 and (p_{1})_{2} 0 and (p_{2})_{2} 0 and (p_{1})_{1} (p_{2})_{1} or (p_{1})_{2} (p_{2})_{2}. Then LE(p_{1}, p_{2}, P).

(57) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and p_{1} ∈ P and p_{2} ∈ P and (p_{1})_{2} 0 and (p_{2})_{2} 0 and (p_{1})_{1} (p_{2})_{1}. Then LE(p_{1}, p_{2}, P).

(58) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and p_{1} ∈ P and p_{2} ∈ P and (p_{1})_{1} 0 and (p_{2})_{1} 0 and (p_{1})_{2} (p_{2})_{2}. Then LE(p_{1}, p_{2}, P).

(59) Let p_{1}, p_{2} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and p_{1} ∈ P and p_{2} ∈ P and (p_{1})_{2} 0 and (p_{2})_{2} 0 and p_{2} ≠ W-minP and (p_{1})_{1} (p_{2})_{1}. Then LE(p_{1}, p_{2}, P).

(60) Let c_{1} be a real number and q be a point of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and q_{2} 0. Let p be a point of E_{T}^{2}. If p = c_{1} -FanMorphS(q), then p_{2} 0.

(61) Let c_{1} be a real number, p_{1}, p_{2}, q_{1}, q_{2} be points of E_{T}^{2}, and P be a compact non empty subset of E_{T}^{2}. Suppose − 1 < c_{1} and c_{1} < 1 and P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and q_{1} = c_{1} -FanMorphS(p_{1}) and q_{2} = c_{1} -FanMorphS(p_{2}). Then LE(q_{1}, q_{2}, P).

(62) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose that P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P) and (p_{1})_{1} < 0 and (p_{1})_{2} 0 and (p_{2})_{1} < 0 and (p_{2})_{2} 0 and (p_{3})_{1} < 0 and (p_{3})_{2} 0 and (p_{4})_{1} < 0 and (p_{4})_{2} 0. Then there exists a map f from E_{T}^{2} into E_{T}^{2} and there exist points q_{1}, q_{2}, q_{3}, q_{4} of E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and q_{1} = f(p_{1}) and q_{2} = f(p_{2}) and q_{3} = f(p_{3}) and q_{4} = f(p_{4}) and (q_{1})_{1} < 0 and (q_{1})_{2} < 0 and (q_{2})_{1} < 0 and (q_{2})_{2} < 0 and (q_{3})_{1} < 0 and (q_{3})_{2} < 0 and (q_{4})_{1} < 0 and (q_{4})_{2} < 0 and LE(q_{1}, q_{2}, P) and LE(q_{2}, q_{3}, P) and LE(q_{3}, q_{4}, P).

(63) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P) and (p_{1})_{2} 0 and (p_{2})_{2} 0 and (p_{3})_{2} 0 and (p_{4})_{2} > 0. Then there exists a map f from E_{T}^{2} into E_{T}^{2} and there exist points q_{1}, q_{2}, q_{3}, q_{4} of E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and q_{1} = f(p_{1}) and q_{2} = f(p_{2}) and q_{3} = f(p_{3}) and q_{4} = f(p_{4}) and (q_{1})_{1} < 0 and (q_{1})_{2} 0 and (q_{2})_{1} < 0 and (q_{2})_{2} 0 and (q_{3})_{1} < 0 and (q_{3})_{2} 0 and (q_{4})_{1} < 0 and (q_{4})_{2} 0 and LE(q_{1}, q_{2}, P) and LE(q_{2}, q_{3}, P) and LE(q_{3}, q_{4}, P).

(64) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P) and (p_{1})_{2} 0 and (p_{2})_{2} 0 and (p_{3})_{2} 0 and (p_{4})_{2} > 0. Then there exists a map f from E_{T}^{2} into E_{T}^{2} and there exist points q_{1}, q_{2}, q_{3}, q_{4} of E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and q_{1} = f(p_{1}) and q_{2} = f(p_{2}) and q_{3} = f(p_{3}) and q_{4} = f(p_{4}) and (q_{1})_{1} < 0 and (q_{1})_{2} < 0 and (q_{2})_{1} < 0 and (q_{2})_{2} < 0 and (q_{3})_{1} < 0 and (q_{3})_{2} < 0 and (q_{4})_{1} < 0 and (q_{4})_{2} < 0 and LE(q_{1}, q_{2}, P) and LE(q_{2}, q_{3}, P) and LE(q_{3}, q_{4}, P).

(65) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose that P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P) and (p_{1})_{2} 0 or (p_{1})_{1} 0 and (p_{2})_{2} 0 or (p_{2})_{1} 0 and (p_{3})_{2} 0 or (p_{3})_{1} 0 and (p_{4})_{2} > 0 or (p_{4})_{1} > 0. Then there exists a map f from E_{T}^{2} into E_{T}^{2} and there exist points q_{1}, q_{2}, q_{3}, q_{4} of E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and q_{1} = f(p_{1}) and q_{2} = f(p_{2}) and q_{3} = f(p_{3}) and q_{4} = f(p_{4}) and (q_{1})_{2} 0 and (q_{2})_{2} 0 and (q_{3})_{2} 0 and (q_{4})_{2} > 0 and LE(q_{1}, q_{2}, P) and LE(q_{2}, q_{3}, P) and LE(q_{3}, q_{4}, P).

(66) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose that P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P) and (p_{1})_{2} 0 or (p_{1})_{1} 0 and (p_{2})_{2} 0 or (p_{2})_{1} 0 and (p_{3})_{2} 0 or (p_{3})_{1} 0 and (p_{4})_{2} > 0 or (p_{4})_{1} > 0. Then there exists a map f from E_{T}^{2} into E_{T}^{2} and there exist points q_{1}, q_{2}, q_{3}, q_{4} of E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and q_{1} = f(p_{1}) and q_{2} = f(p_{2}) and q_{3} = f(p_{3}) and q_{4} = f(p_{4}) and (q_{1})_{1} < 0 and (q_{1})_{2} < 0 and (q_{2})_{1} < 0 and (q_{2})_{2} < 0 and (q_{3})_{1} < 0 and (q_{3})_{2} < 0 and (q_{4})_{1} < 0 and (q_{4})_{2} < 0 and LE(q_{1}, q_{2}, P) and LE(q_{2}, q_{3}, P) and LE(q_{3}, q_{4}, P).

(67) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and p_{4} = W-minP and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P). Then there exists a map f from E_{T}^{2} into E_{T}^{2} and there exist points q_{1}, q_{2}, q_{3}, q_{4} of E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and q_{1} = f(p_{1}) and q_{2} = f(p_{2}) and q_{3} = f(p_{3}) and q_{4} = f(p_{4}) and (q_{1})_{1} < 0 and (q_{1})_{2} < 0 and (q_{2})_{1} < 0 and (q_{2})_{2} < 0 and (q_{3})_{1} < 0 and (q_{3})_{2} < 0 and (q_{4})_{1} < 0 and (q_{4})_{2} < 0 and LE(q_{1}, q_{2}, P) and LE(q_{2}, q_{3}, P) and LE(q_{3}, q_{4}, P).

(68) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P). Then there exists a map f from E_{T}^{2} into E_{T}^{2} and there exist points q_{1}, q_{2}, q_{3}, q_{4} of E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and q_{1} = f(p_{1}) and q_{2} = f(p_{2}) and q_{3} = f(p_{3}) and q_{4} = f(p_{4}) and (q_{1})_{1} < 0 and (q_{1})_{2} < 0 and (q_{2})_{1} < 0 and (q_{2})_{2} < 0 and (q_{3})_{1} < 0 and (q_{3})_{2} < 0 and (q_{4})_{1} < 0 and (q_{4})_{2} < 0 and LE(q_{1}, q_{2}, P) and LE(q_{2}, q_{3}, P) and LE(q_{3}, q_{4}, P).

5. General Fashoda Theorems

One can prove the following propositions:

(69) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose that P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P) and p_{1} ≠ p_{2} and p_{2} ≠ p_{3} and p_{3} ≠ p_{4} and (p_{1})_{1} < 0 and (p_{2})_{1} < 0 and (p_{3})_{1} < 0 and (p_{4})_{1} < 0 and (p_{1})_{2} < 0 and (p_{2})_{2} < 0 and (p_{3})_{2} < 0 and (p_{4})_{2} < 0. Then there exists a map f from E_{T}^{2} into E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and [− 1, 0] = f(p_{1}) and [0, 1] = f(p_{2}) and [1, 0] = f(p_{3}) and [0, − 1] = f(p_{4}).

(70) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2} and P be a compact non empty subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P) and p_{1} ≠ p_{2} and p_{2} ≠ p_{3} and p_{3} ≠ p_{4}. Then there exists a map f from E_{T}^{2} into E_{T}^{2} such that f is a homeomorphism and for every point q of E_{T}^{2} holds |f(q)| = |q| and [− 1, 0] = f(p_{1}) and [0, 1] = f(p_{2}) and [1, 0] = f(p_{3}) and [0, − 1] = f(p_{4}).

(71) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2}, P be a compact non empty subset of E_{T}^{2}, and C_{0} be a subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P). Let f, g be maps from 𝕀 into E_{T}^{2}. Suppose that f is continuous and one-to-one and g is continuous and one-to-one and C_{0} = {p : |p| 1} and f(0) = p_{1} and f(1) = p_{3} and g(0) = p_{2} and g(1) = p_{4} and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg.

(72) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2}, P be a compact non empty subset of E_{T}^{2}, and C_{0} be a subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P). Let f, g be maps from 𝕀 into E_{T}^{2}. Suppose that f is continuous and one-to-one and g is continuous and one-to-one and C_{0} = {p : |p| 1} and f(0) = p_{1} and f(1) = p_{3} and g(0) = p_{4} and g(1) = p_{2} and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg.

(73) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2}, P be a compact non empty subset of E_{T}^{2}, and C_{0} be a subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P). Let f, g be maps from 𝕀 into E_{T}^{2}. Suppose that f is continuous and one-to-one and g is continuous and one-to-one and C_{0} = {p : |p| 1} and f(0) = p_{1} and f(1) = p_{3} and g(0) = p_{4} and g(1) = p_{2} and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg.

(74) Let p_{1}, p_{2}, p_{3}, p_{4} be points of E_{T}^{2}, P be a compact non empty subset of E_{T}^{2}, and C_{0} be a subset of E_{T}^{2}. Suppose P = {p; p ranges over points of E_{T}^{2}: |p| = 1} and LE(p_{1}, p_{2}, P) and LE(p_{2}, p_{3}, P) and LE(p_{3}, p_{4}, P). Let f, g be maps from 𝕀 into E_{T}^{2}. Suppose that f is continuous and one-to-one and g is continuous and one-to-one and C_{0} = {p : |p| 1} and f(0) = p_{1} and f(1) = p_{3} and g(0) = p_{2} and g(1) = p_{4} and rngf ⊆ C_{0} and rngg ⊆ C_{0}. Then rngf meets rngg. general fashoda meet theorem … 109

References

[1] Leszek Borys. Paracompact and metrizable spaces. Formalized Mathematics, 2(4):481– 485, 1991.

[2] Czesław Byliński. Binary operations. Formalized Mathematics, 1(1):175–180, 1990.

[3] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55– 65, 1990.

[4] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990.

[5] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990.

[6] Czesław Byliński and Piotr Rudnicki. Bounding boxes for compact sets in E^{2}. Formalized Mathematics, 6(3):427–440, 1997.

[7] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

[8] Agata Darmochwał. Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics, 1(2):257–261, 1990.

[9] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[10] Agata Darmochwał and Yatsuka Nakamura. Metric spaces as topological spaces - fundamental concepts. Formalized Mathematics, 2(4):605–608, 1991.

[11] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[12] Stanisława Kanas, Adam Lecko, and Mariusz Startek. Metric spaces. Formalized Mathematics, 1(3):607–610, 1990.

[13] Yatsuka Nakamura. Fan homeomorphisms in the plane. Formalized Mathematics, 10(1):1– 19, 2002.

[14] Yatsuka Nakamura and Andrzej Trybulec. A decomposition of a simple closed curves and the order of their points. Formalized Mathematics, 6(4):563–572, 1997.

[15] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[16] Konrad Raczkowski and Paweł Sadowski. Topological properties of subsets in real numbers. Formalized Mathematics, 1(4):777–780, 1990.

[17] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[18] Andrzej Trybulec. A Borsuk theorem on homotopy types. Formalized Mathematics, 2(4):535–545, 1991.

[19] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.

[20] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[21] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.

Received June 24, 2002

Properties of the Internal Approximation of Jordan’s Curve^{1}

Robert Milewski University of Białystok

MML Identifier: JORDAN14.

The articles [19], [25], [14], [10], [1], [16], [2], [3], [24], [11], [18], [9], [26], [6], [17], [7], [8], [12], [13], [20], [15], [4], [5], [21], [23], and [22] provide the notation and terminology for this paper.

One can prove the following propositions:

(1) For every non constant standard special circular sequence f holds BDD L̃(f) = RightComp(f) or BDD L̃(f) = LeftComp(f).

(2) For every non constant standard special circular sequence f holds UBD L̃(f) = RightComp(f) or UBD L̃(f) = LeftComp(f).

(3) Let G be a Go-board, f be a finite sequence of elements of E_{T}^{2}, and k be a natural number. Suppose 1 k and k + 1 lenf and f is a sequence which elements belong to G. Then left cell(f, k, G) is closed.

(4) Let G be a Go-board, p be a point of E_{T}^{2}, and i, j be natural numbers. Suppose 1 i and i + 1 lenG and 1 j and j + 1 widthG. Then p ∈ Intcell(G, i, j) if and only if the following conditions are satisfied:

(i) (G ∘ (i, j))_{1} < p_{1}, (ii) p_{1} < (G ∘ (i + 1, j))_{1}, (iii) (G ∘ (i, j))_{2} < p_{2}, and (iv) p_{2} < (G ∘ (i, j + 1))_{2}.

(5) For every non constant standard special circular sequence f holds BDD L̃(f) is connected.

Let f be a non constant standard special circular sequence. Observe that BDD L̃(f) is connected.

1This work has been partially supported by CALCULEMUS grant HPRN-CT-2000-00102.

Let C be a simple closed curve and let n be a natural number. The functor SpanStart(C, n) yields a point of E_{T}^{2} and is defined as follows:

(Def. 1) SpanStart(C, n) = Gauge(C, n)∘(X-SpanStart(C, n), Y-SpanStart(C, n)). The following four propositions are true:

(6) Let C be a simple closed curve and n be a natural number. If n is sufficiently large for C, then (Span(C, n))_{1} = SpanStart(C, n).

(7) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds SpanStart(C, n) ∈ BDDC.

(8) Let C be a simple closed curve and n, k be natural numbers. Suppose n is sufficiently large for C. Suppose 1 k and k + 1 lenSpan(C, n). Then right cell(Span(C, n), k, Gauge(C, n)) misses C and left cell(Span(C, n), k, Gauge(C, n)) meets C.

(9) Let C be a simple closed curve and n be a natural number. If n is sufficiently large for C, then C misses L̃(Span(C, n)).

Let C be a simple closed curve and let n be a natural number. Observe that \overline{RightComp(Span(C, n))} is compact.

Next we state a number of propositions:

(10) Let C be a simple closed curve and n be a natural number. If n is sufficiently large for C, then C meets LeftComp(Span(C, n)).

(11) Let C be a simple closed curve and n be a natural number. If n is sufficiently large for C, then C misses RightComp(Span(C, n)).

(12) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds C ⊆ LeftComp(Span(C, n)).

(13) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds C ⊆ UBD L̃(Span(C, n)).

(14) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds BDD L̃(Span(C, n)) ⊆ BDDC.

(15) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds UBDC ⊆ UBD L̃(Span(C, n)).

(16) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds RightComp(Span(C, n)) ⊆ BDDC.

(17) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds UBDC ⊆ LeftComp(Span(C, n)).

(18) Let C be a simple closed curve and n be a natural number. If n is sufficiently large for C, then UBDC misses BDD L̃(Span(C, n)).

(19) Let C be a simple closed curve and n be a natural number. If n is sufficiently large for C, then UBDC misses RightComp(Span(C, n)).

(20) Let C be a simple closed curve, P be a subset of E_{T}^{2}, and n be a natural number. Suppose n is sufficiently large for C. If P is outside component

of C, then P misses L̃(Span(C, n)).

(21) Let C be a simple closed curve and n be a natural number. If n is sufficiently large for C, then UBDC misses L̃(Span(C, n)).

(22) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds L̃(Span(C, n)) ⊆ BDDC.

(23) Let C be a simple closed curve and i, j, k, n be natural numbers. Suppose n is sufficiently large for C and 1 k and k lenSpan(C, n) and ⟨⟨i, j⟩⟩∈ the indices of Gauge(C, n) and (Span(C, n))_{k} = Gauge(C, n) ∘ (i, j). Then i > 1.

(24) Let C be a simple closed curve and i, j, k, n be natural numbers. Suppose n is sufficiently large for C and 1 k and k lenSpan(C, n) and ⟨⟨i, j⟩⟩∈ the indices of Gauge(C, n) and (Span(C, n))_{k} = Gauge(C, n) ∘ (i, j). Then i < lenGauge(C, n).

(25) Let C be a simple closed curve and i, j, k, n be natural numbers. Suppose n is sufficiently large for C and 1 k and k lenSpan(C, n) and ⟨⟨i, j⟩⟩∈ the indices of Gauge(C, n) and (Span(C, n))_{k} = Gauge(C, n) ∘ (i, j). Then j > 1.

(26) Let C be a simple closed curve and i, j, k, n be natural numbers. Suppose n is sufficiently large for C and 1 k and k lenSpan(C, n) and ⟨⟨i, j⟩⟩∈ the indices of Gauge(C, n) and (Span(C, n))_{k} = Gauge(C, n) ∘ (i, j). Then j < widthGauge(C, n).

(27) For every simple closed curve C and for every natural number n such that n is sufficiently large for C holds Y-SpanStart(C, n) < widthGauge(C, n).

(28) Let C be a compact non vertical non horizontal subset of E_{T}^{2} and n, m be natural numbers. If m n and n 1, then X-SpanStart(C, m) = 2^{m− ′n} · (X-SpanStart(C, n) − 2) + 2.

(29) Let C be a compact non vertical non horizontal subset of E_{T}^{2} and n, m be natural numbers. Suppose n m and n is sufficiently large for C. Then m is sufficiently large for C.

(30) Let G be a Go-board, f be a finite sequence of elements of E_{T}^{2}, and i, j be natural numbers. Suppose f is a sequence which elements belong to G and special and i lenG and j widthG. Then cell(G, i, j) \ L̃(f) is connected.

(31) Let C be a simple closed curve and n, k be natural numbers. Suppose n is sufficiently large for C and Y-SpanStart(C, n) k and k 2^{n− ′ApproxIndex C} · (Y-InitStartC − ′ 2) + 2. Then cell(Gauge(C, n), X-SpanStart(C, n) − ′1, k) \ L̃(Span(C, n)) ⊆ BDD L̃(Span(C, n)).

(32) Let C be a subset of E_{T}^{2} and n, m, i be natural numbers. If m n and 1 < i and i + 1 < lenGauge(C, m), then 2^{n− ′m} · (i − 2) + 2 + 1 < 114 robert milewski

lenGauge(C, n).

(33) Let C be a simple closed curve and n, m be natural numbers. If n is sufficiently large for C and n m, then RightComp(Span(C, n)) meets RightComp(Span(C, m)).

(34) Let G be a Go-board and f be a finite sequence of elements of E_{T}^{2}. Suppose f is a sequence which elements belong to G and special. Let i, j be natural numbers. If i lenG and j widthG, then Intcell(G, i, j) ⊆ (L̃(f))^{c}.

(35) Let C be a simple closed curve and n, m be natural numbers. If n is sufficiently large for C and n m, then L̃(Span(C, m)) ⊆ \overline{LeftComp(Span(C, n))}.

(36) Let C be a simple closed curve and n, m be natural numbers. If n is sufficiently large for C and n m, then RightComp(Span(C, n)) ⊆ RightComp(Span(C, m)).

(37) Let C be a simple closed curve and n, m be natural numbers. If n is sufficiently large for C and n m, then LeftComp(Span(C, m)) ⊆ LeftComp(Span(C, n)).

References

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.

[2] Grzegorz Bancerek. Countable sets and Hessenberg’s theorem. Formalized Mathematics, 2(1):65–69, 1991.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.

[4] Czesław Byliński. Gauges. Formalized Mathematics, 8(1):25–27, 1999.

[5] Czesław Byliński. Some properties of cells on Go-board. Formalized Mathematics, 8(1):139–146, 1999.

[6] Agata Darmochwał. Compact spaces. Formalized Mathematics, 1(2):383–386, 1990.

[7] Agata Darmochwał. The Euclidean space. Formalized Mathematics, 2(4):599–603, 1991.

[8] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Arcs, line segments and special polygonal arcs. Formalized Mathematics, 2(5):617–621, 1991.

[9] Agata Darmochwał and Yatsuka Nakamura. The topological space E_{T}^{2}. Simple closed curves. Formalized Mathematics, 2(5):663–664, 1991.

[10] Krzysztof Hryniewiecki. Basic properties of real numbers. Formalized Mathematics, 1(1):35–40, 1990.

[11] Katarzyna Jankowska. Matrices. Abelian group of matrices. Formalized Mathematics, 2(4):475–480, 1991.

[12] Jarosław Kotowicz and Yatsuka Nakamura. Introduction to Go-board - part I. Formalized Mathematics, 3(1):107–115, 1992.

[13] Yatsuka Nakamura and Czesław Byliński. Extremal properties of vertices on special polygons. Part I. Formalized Mathematics, 5(1):97–102, 1996.

[14] Yatsuka Nakamura and Andrzej Trybulec. Decomposing a Go-board into cells. Formalized Mathematics, 5(3):323–328, 1996.

[15] Yatsuka Nakamura, Andrzej Trybulec, and Czesław Byliński. Bounded domains and unbounded domains. Formalized Mathematics, 8(1):1–13, 1999.

[16] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Formalized Mathematics, 4(1):83–86, 1993.

[17] Beata Padlewska. Connected spaces. Formalized Mathematics, 1(1):239–244, 1990.

properties of the internal approximation … 115

[18] Beata Padlewska and Agata Darmochwał. Topological spaces and continuous functions. Formalized Mathematics, 1(1):223–230, 1990.

[19] Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990.

[20] Andrzej Trybulec. Left and right component of the complement of a special closed curve. Formalized Mathematics, 5(4):465–468, 1996.

[21] Andrzej Trybulec. More on the external approximation of a continuum. Formalized Mathematics, 9(4):831–841, 2001.

[22] Andrzej Trybulec. Introducing spans. Formalized Mathematics, 10(2):97–98, 2002.

[23] Andrzej Trybulec. Preparing the internal approximations of simple closed curves. Formalized Mathematics, 10(2):85–87, 2002.

[24] Wojciech A. Trybulec. Pigeon hole principle. Formalized Mathematics, 1(3):575–579, 1990.

[25] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.

[26] Mirosław Wysocki and Agata Darmochwał. Subsets of topological spaces. Formalized Mathematics, 1(1):231–237, 1990.

Received June 27, 2002

Contents Formaliz. Math. 10 (2)

Upper and Lower Sequence on the Cage, Upper and Lower Arcs

By Robert Milewski  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

Fibonacci Numbers

By Robert M. Solovay  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81

Preparing the Internal Approximations of Simple Closed Curves

By Andrzej Trybulec  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

On the General Position of Special Polygons

By Mariusz Giero  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

Introducing Spans

By Andrzej Trybulec  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

General Fashoda Meet Theorem for Unit Circle

By Yatsuka Nakamura  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99

Properties of the Internal Approximation of Jordan’s Curve

By Robert Milewski  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111

Continued on inside back cover