Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### 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);

Back to top