The abstract of the Mizar article:

Sequences of Metric Spaces and an Abstract Intermediate Value Theorem

by

Yatsuka Nakamura, and

Andrzej Trybulec

Received September 11, 2002

MML identifier: TOPMETR3

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, PRE_TOPC, SUBSET_1, COMPTS_1, BOOLE, RELAT_1, ORDINAL2,
      FUNCT_1, METRIC_1, RCOMP_1, ABSVALUE, ARYTM_1, PCOMPS_1, EUCLID,
      BORSUK_1, ARYTM_3, TOPMETR, SEQ_2, SEQ_1, NORMSP_1, PROB_1, PSCOMP_1,
      SEQ_4, SQUARE_1, JORDAN6, TOPREAL1, TOPS_2, JORDAN5C, TOPREAL2, MCART_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, STRUCT_0, METRIC_1,
      PRE_TOPC, TOPS_2, COMPTS_1, PCOMPS_1, RCOMP_1, ABSVALUE, EUCLID,
      PSCOMP_1, TOPMETR, SEQ_1, SEQ_2, SEQ_4, SEQM_3, TBSP_1, NORMSP_1,
      SQUARE_1, JORDAN6, TOPREAL1, JORDAN5C, TOPREAL2;
 constructors REAL_1, TOPS_2, RCOMP_1, ABSVALUE, TREAL_1, NAT_1, INT_1, TBSP_1,
      SQUARE_1, JORDAN6, TOPREAL1, JORDAN5C, TOPREAL2, PSCOMP_1;
 clusters FUNCT_1, PRE_TOPC, STRUCT_0, XREAL_0, METRIC_1, RELSET_1, EUCLID,
      TOPMETR, INT_1, PCOMPS_1, PSCOMP_1, MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin

theorem :: TOPMETR3:1
 for R being non empty Subset of REAL,r0 being real number st
  for r being real number st r in R holds r <= r0
 holds upper_bound R <= r0;

theorem :: TOPMETR3:2
for X being non empty MetrSpace, S being sequence of X,
 F being Subset of TopSpaceMetr(X) st
 S is convergent & (for n being Nat holds S.n in F) & F is closed
 holds lim S in F;

theorem :: TOPMETR3:3
for X,Y being non empty MetrSpace,
 f being map of TopSpaceMetr(X),TopSpaceMetr(Y),S being sequence of X
 holds f*S is sequence of Y;

theorem :: TOPMETR3:4
for X,Y being non empty MetrSpace,
 f being map of TopSpaceMetr(X),TopSpaceMetr(Y),S being sequence of X,
 T being sequence of Y st
 S is convergent & T= f*S & f is continuous holds T is convergent;

theorem :: TOPMETR3:5
for X being non empty MetrSpace,
S being Function of NAT,the carrier of X holds S is sequence of X;

theorem :: TOPMETR3:6
for s being Real_Sequence,S being sequence of RealSpace st
 s=S holds (s is convergent iff S is convergent) &
 (s is convergent implies lim s=lim S);

theorem :: TOPMETR3:7
for a,b being real number,s being Real_Sequence st
 rng s c= [.a,b.] holds
 s is sequence of Closed-Interval-MSpace(a,b);

theorem :: TOPMETR3:8
for a,b being real number,
 S being sequence of Closed-Interval-MSpace(a,b) st a<=b holds
 S is sequence of RealSpace;

theorem :: TOPMETR3:9
for a,b being real number,
S1 being sequence of Closed-Interval-MSpace(a,b),
S being sequence of RealSpace st S=S1 & a<=b holds
 (S is convergent iff S1 is convergent)&
 (S is convergent implies lim S=lim S1);

theorem :: TOPMETR3:10
for a,b being real number,s being Real_Sequence,
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;

theorem :: TOPMETR3:11
for a,b being real number,s being Real_Sequence,
S being sequence of Closed-Interval-MSpace(a,b) st S=s & a<=b &
s is non-decreasing holds S is convergent;

theorem :: TOPMETR3:12
for a,b being real number,s being Real_Sequence,
S being sequence of Closed-Interval-MSpace(a,b) st S=s & a<=b &
s is non-increasing holds S is convergent;

canceled 2;

theorem :: TOPMETR3:15
for R being non empty Subset of REAL
 st R is bounded_above
 holds ex s being Real_Sequence
  st s is non-decreasing convergent & rng s c= R & lim s=upper_bound R;

theorem :: TOPMETR3:16
for R being non empty Subset of REAL
 st R is bounded_below
 holds ex s being Real_Sequence
  st s is non-increasing convergent & rng s c= R & lim s=lower_bound R;

theorem :: TOPMETR3:17
  :: An Abstract Intermediate Value Theorem for Closed Sets
 for X being non empty MetrSpace, f being map of I[01],TopSpaceMetr(X),
 F1,F2 being Subset of TopSpaceMetr(X),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
 ex r being Real st r1<=r & r<=r2 & f.r in F1 /\ F2;

theorem :: TOPMETR3:18
for n being Nat,p1,p2 being Point of TOP-REAL n,
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;

theorem :: TOPMETR3:19
   for P,P1 being compact non empty Subset of TOP-REAL 2
 st P is_simple_closed_curve & P1 is_an_arc_of W-min(P),E-max(P) & P1 c= P
 holds P1=Upper_Arc(P) or P1=Lower_Arc(P);