:: Sequences of Metric Spaces and an Abstract Intermediate Value Theorem :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received September 11, 2002 :: Copyright (c) 2002-2012 Association of Mizar Users begin theorem Th1: :: TOPMETR3:1 for X being non empty MetrSpace for S being sequence of X for F being Subset of (TopSpaceMetr X) st S is convergent & ( for n being Element of NAT holds S . n in F ) & F is closed holds lim S in F proofend; theorem Th2: :: TOPMETR3:2 for X, Y being non empty MetrSpace for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y) for S being sequence of X holds f * S is sequence of Y proofend; theorem Th3: :: TOPMETR3:3 for X, Y being non empty MetrSpace for f being Function of (TopSpaceMetr X),(TopSpaceMetr Y) for S being sequence of X for T being sequence of Y st S is convergent & T = f * S & f is continuous holds T is convergent proofend; theorem Th4: :: TOPMETR3:4 for s being Real_Sequence for S being sequence of RealSpace st s = S holds ( ( s is convergent implies S is convergent ) & ( S is convergent implies s is convergent ) & ( s is convergent implies lim s = lim S ) ) proofend; theorem Th5: :: TOPMETR3:5 for a, b being real number for s being Real_Sequence st rng s c= [.a,b.] holds s is sequence of (Closed-Interval-MSpace (a,b)) proofend; theorem Th6: :: TOPMETR3:6 for a, b being real number for S being sequence of (Closed-Interval-MSpace (a,b)) st a <= b holds S is sequence of RealSpace proofend; theorem Th7: :: TOPMETR3:7 for a, b being real number for S1 being sequence of (Closed-Interval-MSpace (a,b)) for S being sequence of RealSpace st S = S1 & a <= b holds ( ( S is convergent implies S1 is convergent ) & ( S1 is convergent implies S is convergent ) & ( S is convergent implies lim S = lim S1 ) ) proofend; theorem Th8: :: TOPMETR3:8 for a, b being real number for s being Real_Sequence for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is convergent holds ( S is convergent & lim s = lim S ) proofend; theorem :: TOPMETR3:9 for a, b being real number for s being Real_Sequence for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-decreasing holds S is convergent proofend; theorem :: TOPMETR3:10 for a, b being real number for s being Real_Sequence for S being sequence of (Closed-Interval-MSpace (a,b)) st S = s & a <= b & s is non-increasing holds S is convergent proofend; theorem Th11: :: TOPMETR3:11 for R being non empty Subset of REAL st R is bounded_above holds ex s being Real_Sequence st ( s is non-decreasing & s is convergent & rng s c= R & lim s = upper_bound R ) proofend; theorem Th12: :: TOPMETR3:12 for R being non empty Subset of REAL st R is bounded_below holds ex s being Real_Sequence st ( s is non-increasing & s is convergent & rng s c= R & lim s = lower_bound R ) proofend; theorem Th13: :: TOPMETR3:13 for X being non empty MetrSpace for f being Function of I[01],(TopSpaceMetr X) for F1, F2 being Subset of (TopSpaceMetr X) for r1, r2 being Real st 0 <= r1 & r2 <= 1 & r1 <= r2 & f . r1 in F1 & f . r2 in F2 & F1 is closed & F2 is closed & f is continuous & F1 \/ F2 = the carrier of X holds ex r being Real st ( r1 <= r & r <= r2 & f . r in F1 /\ F2 ) proofend; theorem Th14: :: TOPMETR3:14 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for P, P1 being non empty Subset of (TOP-REAL n) st P is_an_arc_of p1,p2 & P1 is_an_arc_of p2,p1 & P1 c= P holds P1 = P proofend; theorem :: TOPMETR3:15 for P, P1 being non empty compact Subset of (TOP-REAL 2) st P is being_simple_closed_curve & P1 is_an_arc_of W-min P, E-max P & P1 c= P & not P1 = Upper_Arc P holds P1 = Lower_Arc P proofend;