TOPMETR3: Sequences of Metric Spaces and an Abstract Intermediate Value Theorem

:: Sequences of Metric Spaces and an Abstract Intermediate Value Theorem
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received September 11, 2002
:: Copyright (c) 2002-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, XXREAL_0, SEQ_4, XXREAL_2, ARYTM_1, CARD_1, ARYTM_3, METRIC_1, NAT_1, PCOMPS_1, SEQ_2, FUNCT_1, RCOMP_1, ORDINAL2, TARSKI, REAL_1, STRUCT_0, PRE_TOPC, RELAT_1, SEQ_1, COMPLEX1, XXREAL_1, TOPMETR, VALUED_0, BORSUK_1, EUCLID, TOPREAL1, TOPREAL2, PSCOMP_1, JORDAN6, TOPS_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_2, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, NAT_1, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_2, COMPTS_1, PCOMPS_1, RCOMP_1, EUCLID, PSCOMP_1, TOPMETR, SEQ_1, SEQ_2, SEQM_3, SEQ_4, TBSP_1, JORDAN6, TOPREAL1, TOPREAL2;
definitions TARSKI, XXREAL_2;
theorems PRE_TOPC, TOPMETR, XREAL_0, TBSP_1, XBOOLE_0, METRIC_1, FUNCT_1, XBOOLE_1, FUNCT_2, JGRAPH_2, GOBOARD6, SEQ_2, TREAL_1, SEQ_4, NAT_1, SEQM_3, UNIFORM1, BORSUK_1, JORDAN6, TOPREAL1, TOPS_2, TARSKI, RELAT_1, TOPREAL3, JORDAN5B, PREPOWER, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1, EUCLID, ORDINAL1;
schemes FUNCT_2, RECDEF_1, NAT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, EUCLID, TOPMETR, COMPTS_1, VALUED_0, SEQ_4;
constructors HIDDEN, REAL_1, COMPLEX1, RCOMP_1, TOPS_2, COMPTS_1, TBSP_1, TOPMETR, TOPREAL1, PSCOMP_1, JORDAN5C, JORDAN6, SEQ_4, BINOP_2, SEQ_2, PCOMPS_1, COMSEQ_2, BINOP_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0;
expansions TARSKI, XXREAL_2;

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 Nat holds S . n in F ) & F is closed holds
lim S in F

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th5: :: TOPMETR3:5

for a, b being Real
for s being Real_Sequence st rng s c= [.a,b.] holds
s is sequence of (Closed-Interval-MSpace (a,b))

proof end;

theorem Th6: :: TOPMETR3:6

for a, b being Real
for S being sequence of (Closed-Interval-MSpace (a,b)) st a <= b holds
S is sequence of RealSpace

proof end;

theorem Th7: :: TOPMETR3:7

for a, b being Real
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 ) )

proof end;

theorem Th8: :: TOPMETR3:8

for a, b being Real
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 )

proof end;

theorem :: TOPMETR3:9

for a, b being Real
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

proof end;

theorem :: TOPMETR3:10

for a, b being Real
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

proof end;

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 )

proof end;

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 )

proof end;

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 )

proof end;

theorem Th14: :: TOPMETR3:14

for n being 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

proof end;

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

proof end;