科学文献

FORMALIZED MATHEMATICS

Volume10,Number3,2002

University of Bia?ystok

Sequences of Metric Spaces and

an Abstract Intermediate Value Theorem1

Yatsuka Nakamura Shinshu University

Nagano

Andrzej Trybulec University of Bia?ystok

Summary.Relations of convergence of real sequences and convergence of metric spaces are investigated.An abstract intermediate value theorem for

two closed sets in the range is presented.At the end,it is proven that an arc

connecting the west minimal point and the east maximal point in a simple closed

curve must be identical to the upper arc or lower arc of the closed curve.

MML Identi?er:TOPMETR3.

The notation and terminology used here are introduced in the following papers: [21],[22],[23],[3],[4],[2],[12],[18],[6],[1],[20],[7],[5],[8],[16],[14],[13],[15], [11],[19],[17],[9],and[10].

The following propositions are true:

(1)Let R be a non empty subset of R and r0be a real number.If for every

real number r such that r∈R holds r r0,then sup R r0.

(2)Let X be a non empty metric space,S be a sequence of X,and F be a

subset of X top.Suppose S is convergent and for every natural number n holds S(n)∈F and F is closed.Then lim S∈F.

(3)Let X,Y be non empty metric spaces,f be a map from X top into Y top,

and S be a sequence of X.Then f·S is a sequence of Y.

(4)Let X,Y be non empty metric spaces,f be a map from X top into Y top,

S be a sequence of X,and T be a sequence of Y.If S is convergent and T=f·S and f is continuous,then T is convergent.

1This work has been partially supported by the European Community TYPES grant IST-1999-29001and CALCULEMUS grant HPRN-CT-2000-00102.

159c 2002University of Bia?ystok

ISSN1426–2630

160yatsuka nakamura and andrzej trybulec

(5)For every non empty metric space X holds every function from N into

the carrier of X is a sequence of X.

(6)Let s be a sequence of real numbers and S be a sequence of the metric

space of real numbers such that s=S.Then

(i)s is convergent i?S is convergent,and

(ii)if s is convergent,then lim s=lim S.

(7)Let a,b be real numbers and s be a sequence of real numbers.If rng s?

[a,b],then s is a sequence of[a,b]M.

(8)Let a,b be real numbers and S be a sequence of[a,b]M.Suppose a b.

Then S is a sequence of the metric space of real numbers.

(9)Let a,b be real numbers,S1be a sequence of[a,b]M,and S be a sequence

of the metric space of real numbers such that S=S1and a b.Then

(i)S is convergent i?S1is convergent,and

(ii)if S is convergent,then lim S=lim S1.

(10)Let a,b be real numbers,s be a sequence of real numbers,and S be a

sequence of[a,b]M.If S=s and a b and s is convergent,then S is convergent and lim s=lim S.

(11)Let a,b be real numbers,s be a sequence of real numbers,and S be a

sequence of[a,b]M.If S=s and a b and s is non-decreasing,then S is convergent.

(12)Let a,b be real numbers,s be a sequence of real numbers,and S be a

sequence of[a,b]M.If S=s and a b and s is non-increasing,then S is convergent.

(13)Let s be a sequence of real numbers and r0be a real number.Suppose

for every natural number n holds s(n) r0and s is convergent.Then lim s r0.

(14)Let s be a sequence of real numbers and r0be a real number.Suppose

for every natural number n holds s(n) r0and s is convergent.Then lim s r0.

(15)Let R be a non empty subset of R.Suppose R is upper bounded.Then

there exists a sequence s of real numbers such that s is non-decreasing and rng s?R and lim s=sup R.

(16)Let R be a non empty subset of R.Suppose R is lower bounded.Then

there exists a sequence s of real numbers such that s is non-increasing and rng s?R and lim s=inf R.

(17)Let X be a non empty metric space,f be a map from I into X top,F1,F2

be subsets of X top,and r1,r2be real numbers.Suppose that0 r1and r2 1and r1 r2and f(r1)∈F1and f(r2)∈F2and F1is closed and F2 is closed and f is continuous and F1∪F2=the carrier of X.Then there exists a real number r such that r1 r and r r2and f(r)∈F1∩F2.

sequences of metric spaces and (161)

(18)Let n be a natural number,p1,p2be points of E n T,and P,P1be non

empty subsets of the carrier of E n T.If P is an arc from p1to p2and P1is

an arc from p2to p1and P1?P,then P1=P.

(19)Let P,P1be compact non empty subsets of E2T.Suppose P is a simple

closed curve and P1is an arc from W-min P to E-max P and P1?P.

Then P1=UpperArc P or P1=LowerArc P.

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 and Piotr Rudnicki.Bounding boxes for compact sets in E2.Formalized

Mathematics,6(3):427–440,1997.

[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.Metric spaces as topological spaces-funda-

mental concepts.Formalized Mathematics,2(4):605–608,1991.

[9]Agata Darmochwa?and Yatsuka Nakamura.The topological space E2T.Arcs,line segments

and special polygonal arcs.Formalized Mathematics,2(5):617–621,1991.

[10]Agata Darmochwa?and Yatsuka Nakamura.The topological space E2T.Simple closed

curves.Formalized Mathematics,2(5):663–664,1991.

[11]Alicia de la Cruz.Totally bounded metric spaces.Formalized Mathematics,2(4):559–562,

1991.

[12]Stanis?awa Kanas,Adam Lecko,and Mariusz Startek.Metric spaces.Formalized Mathe-

matics,1(3):607–610,1990.

[13]Jaros?aw Kotowicz.Convergent real sequences.Upper and lower bound of sets of real

numbers.Formalized Mathematics,1(3):477–481,1990.

[14]Jaros?aw Kotowicz.Convergent sequences and the limit of sequences.Formalized Mathe-

matics,1(2):273–275,1990.

[15]Jaros?aw Kotowicz.Monotone real sequences.Subsequences.Formalized Mathematics,

1(3):471–475,1990.

[16]Jaros?aw Kotowicz.Real sequences and basic operations on them.Formalized Mathema-

tics,1(2):269–272,1990.

[17]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.

[18]Beata Padlewska and Agata Darmochwa?.Topological spaces and continuous functions.

Formalized Mathematics,1(1):223–230,1990.

[19]Jan Popio?ek.Real normed space.Formalized Mathematics,2(1):111–115,1991.

[20]Konrad Raczkowski and Pawe?Sadowski.Topological properties of subsets in real num-

bers.Formalized Mathematics,1(4):777–780,1990.

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

1990.

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

[23]Edmund Woronowicz.Relations and their basic properties.Formalized Mathematics,

1(1):73–83,1990.

Received September11,2002