:: Sequences of Metric Spaces and an Abstract Intermediate Value Theorem
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received September 11, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies 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 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;
constructors 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;
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;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XXREAL_2;
equalities STRUCT_0;
expansions 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;
begin
theorem Th1:
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
proof
let X be non empty MetrSpace, S be sequence of X, F be Subset of
TopSpaceMetr(X);
assume that
A1: S is convergent and
A2: for n being Nat holds S.n in F and
A3: F is closed;
A4: for G being Subset of TopSpaceMetr(X) st G is open holds lim S in G
implies F meets G
proof
let G be Subset of TopSpaceMetr(X);
assume
A5: G is open;
now
assume lim S in G;
then consider r1 being Real such that
A6: r1>0 and
A7: Ball(lim S,r1) c= G by A5,TOPMETR:15;
reconsider r2=r1 as Real;
consider n being Nat such that
A8: for m being Nat st m>=n holds dist(S.m,lim S)<r2 by A1,A6,
TBSP_1:def 3;
dist(S.n,lim S)<r2 by A8;
then
A9: S.n in Ball(lim S,r1) by METRIC_1:11;
S.n in F by A2;
then S.n in F /\ G by A7,A9,XBOOLE_0:def 4;
hence F meets G by XBOOLE_0:def 7;
end;
hence thesis;
end;
reconsider F0=F as Subset of TopSpaceMetr(X);
lim S in the carrier of X;
then lim S in the carrier of TopSpaceMetr(X) by TOPMETR:12;
then lim S in Cl F0 by A4,PRE_TOPC:def 7;
hence thesis by A3,PRE_TOPC:22;
end;
theorem Th2:
for X,Y being non empty MetrSpace, f being Function of
TopSpaceMetr(X),TopSpaceMetr(Y),S being sequence of X holds f*S is sequence of
Y
proof
let X,Y be non empty MetrSpace, f be Function of TopSpaceMetr(X),
TopSpaceMetr(Y),S be sequence of X;
A1: dom f=the carrier of TopSpaceMetr(X) by FUNCT_2:def 1
.=the carrier of X by TOPMETR:12;
dom S=NAT & rng S c= the carrier of X by FUNCT_2:def 1;
then dom (f*S)=NAT by A1,RELAT_1:27;
hence thesis by FUNCT_2:def 1,TOPMETR:12;
end;
theorem Th3:
for X,Y being non empty MetrSpace, f being Function 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
proof
let X,Y be non empty MetrSpace, f be Function of TopSpaceMetr(X),
TopSpaceMetr(Y),S be sequence of X,T be sequence of Y;
assume that
A1: S is convergent and
A2: T= f*S and
A3: f is continuous;
set z0=lim S;
reconsider p=z0 as Point of TopSpaceMetr(X) by TOPMETR:12;
A4: dom f=the carrier of TopSpaceMetr(X) by FUNCT_2:def 1
.=the carrier of X by TOPMETR:12;
then f.(lim S) in rng f by FUNCT_1:def 3;
then reconsider x0=f.(lim S) as Element of Y by TOPMETR:12;
for r being Real st r>0
ex n being Nat st for m being Nat st n<=m holds dist(T.m,x0)<r
proof
let r be Real;
reconsider V=Ball(x0,r) as Subset of TopSpaceMetr(Y) by TOPMETR:12;
assume r>0;
then V is open & x0 in V by GOBOARD6:1,TOPMETR:14;
then consider W being Subset of TopSpaceMetr(X) such that
A5: p in W & W is open and
A6: f.:W c= V by A3,JGRAPH_2:10;
consider r0 being Real such that
A7: r0>0 and
A8: Ball(z0,r0) c= W by A5,TOPMETR:15;
reconsider r00=r0 as Real;
consider n0 being Nat such that
A9: for m being Nat st n0<=m holds dist(S.m,z0)<r00 by A1,A7,
TBSP_1:def 3;
for m being Nat st n0<=m holds dist(T.m,x0)<r
proof
let m be Nat;
assume n0<=m;
then dist(S.m,z0)<r0 by A9;
then S.m in Ball(z0,r0) by METRIC_1:11;
then
A10: f.(S.m) in f.:W by A4,A8,FUNCT_1:def 6;
A11: m in NAT by ORDINAL1:def 12;
dom T=NAT by FUNCT_2:def 1;
then T.m in f.:W by A2,A10,FUNCT_1:12,A11;
hence thesis by A6,METRIC_1:11;
end;
hence thesis;
end;
hence thesis by TBSP_1:def 2;
end;
theorem Th4:
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)
proof
let s be Real_Sequence,S be sequence of RealSpace;
assume
A1: s=S;
A2: s is convergent implies S is convergent
proof
assume s is convergent;
then consider g being Real such that
A3: for p being Real st 0<p ex n being Nat st for m
being Nat st n<=m holds |.s.m-g.| < p by SEQ_2:def 6;
reconsider g0=g as Real;
reconsider x0=g as Point of RealSpace by METRIC_1:def 13,XREAL_0:def 1;
for r being Real st r>0 ex n being Nat st for m being
Nat st n<=m holds dist(S.m,x0)<r
proof
let r be Real;
assume r>0;
then consider n0 being Nat such that
A4: for m being Nat st n0<=m holds |.s.m-g.| < r by A3;
for m being Nat st n0<=m holds dist(S.m,x0)<r
proof
let m be Nat;
assume
A5: n0<=m;
reconsider t=s.m as Real;
dist(S.m,x0)=real_dist.(t,g) by A1,METRIC_1:def 1,def 13
.=|.t-g0.| by METRIC_1:def 12;
hence thesis by A4,A5;
end;
hence thesis;
end;
hence thesis by TBSP_1:def 2;
end;
S is convergent implies s is convergent
proof
assume S is convergent;
then consider x being Element of RealSpace such that
A6: for r being Real st r>0 ex n being Nat st for m being
Nat st n<=m holds dist(S.m,x)<r by TBSP_1:def 2;
reconsider g0=x as Real;
for p being Real st 0<p ex n being Nat st for m
being Nat st n<=m holds |.s.m-g0.| < p
proof
let p be Real;
reconsider p0=p as Real;
assume 0<p;
then consider n0 being Nat such that
A7: for m being Nat st n0<=m holds dist(S.m,x)<p0 by A6;
for m being Nat st n0<=m holds |.s.m-g0.| < p
proof
let m be Nat;
assume
A8: n0<=m;
reconsider t=s.m as Real;
dist(S.m,x)=real_dist.(t,g0) by A1,METRIC_1:def 1,def 13
.=|.t-g0.| by METRIC_1:def 12;
hence thesis by A7,A8;
end;
hence thesis;
end;
hence thesis by SEQ_2:def 6;
end;
hence s is convergent iff S is convergent by A2;
thus s is convergent implies lim s=lim S
proof
reconsider g0=lim S as Real;
assume
A9: s is convergent;
for r being Real st 0 < r ex m being Nat st for n
being Nat st m <= n holds |.s.n-g0.| < r
proof
let r be Real;
reconsider r0=r as Real;
assume 0 < r;
then consider m0 being Nat such that
A10: for n being Nat st m0<=n holds dist(S.n,lim S)<r0 by A2,A9,
TBSP_1:def 3;
for n being Nat st m0 <= n holds |.s.n -g0.| < r
proof
let n be Nat;
assume
A11: m0 <= n;
dist(S.n,lim S)=real_dist.(s.n,g0) by A1,METRIC_1:def 1,def 13
.=|.s.n-g0.| by METRIC_1:def 12;
hence thesis by A10,A11;
end;
hence thesis;
end;
hence thesis by A9,SEQ_2:def 7;
end;
end;
theorem Th5:
for a,b being Real,s being Real_Sequence st rng s c= [.a,b
.] holds s is sequence of Closed-Interval-MSpace(a,b)
proof
let a,b be Real,s be Real_Sequence;
assume
A1: rng s c= [.a,b.];
reconsider t=s.0 as Real;
A2: dom s=NAT by FUNCT_2:def 1;
then s.0 in rng s by FUNCT_1:def 3;
then a<=t & t<=b by A1,XXREAL_1:1;
then the carrier of Closed-Interval-MSpace(a,b)=[.a,b.] by TOPMETR:10
,XXREAL_0:2;
hence thesis by A1,A2,FUNCT_2:2;
end;
theorem Th6:
for a,b being Real, S being sequence of
Closed-Interval-MSpace(a,b) st a<=b holds S is sequence of RealSpace
proof
let a,b be Real, S be sequence of Closed-Interval-MSpace(a,b);
assume a<=b;
then the carrier of Closed-Interval-MSpace(a,b)=[.a,b.] by TOPMETR:10;
then dom S=NAT & rng S c= the carrier of RealSpace by FUNCT_2:def 1
,METRIC_1:def 13,XBOOLE_1:1;
hence thesis by FUNCT_2:2;
end;
theorem Th7:
for a,b being Real, 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)
proof
let a,b be Real, S1 be sequence of Closed-Interval-MSpace(a,b), S be
sequence of RealSpace;
assume that
A1: S=S1 and
A2: a<=b;
reconsider P=[.a,b.] as Subset of R^1 by TOPMETR:17;
A3: the carrier of Closed-Interval-MSpace(a,b)=[.a,b.] by A2,TOPMETR:10;
A4: S is convergent implies S1 is convergent
proof
A5: for m being Nat holds S.m in [.a,b.]
proof
let m be Nat;
A6: m in NAT by ORDINAL1:def 12;
dom S1=NAT by FUNCT_2:def 1;
then S1.m in rng S1 by FUNCT_1:def 3,A6;
hence thesis by A1,A3;
end;
A7: P is closed by TREAL_1:1;
assume
A8: S is convergent;
then consider x0 being Element of RealSpace such that
A9: for r being Real st r>0 ex n being Nat st for m being
Nat st n<=m holds dist(S.m,x0)<r by TBSP_1:def 2;
x0=lim S by A8,A9,TBSP_1:def 3;
then reconsider x1=x0 as Element of Closed-Interval-MSpace(a,b) by A3,A8,A5
,A7,Th1,TOPMETR:def 6;
for r being Real st r>0 ex n being Nat st for m being
Nat st n<=m holds dist(S1.m,x1)<r
proof
let r be Real;
assume r>0;
then consider n0 being Nat such that
A10: for m being Nat st n0<=m holds dist(S.m,x0)<r by A9;
for m being Nat st n0<=m holds dist(S1.m,x1)<r
proof
let m be Nat;
assume
A11: n0<=m;
dist(S1.m,x1) =(the distance of Closed-Interval-MSpace(a,b)).(S1.
m,x1) by METRIC_1:def 1
.=(the distance of RealSpace).(S1.m,x1) by TOPMETR:def 1
.=dist(S.m,x0) by A1,METRIC_1:def 1;
hence thesis by A10,A11;
end;
hence thesis;
end;
hence thesis by TBSP_1:def 2;
end;
S1 is convergent implies S is convergent
proof
assume S1 is convergent;
then consider x0 being Element of Closed-Interval-MSpace(a,b) such that
A12: for r being Real st r>0 ex n being Nat st for m being
Nat st n<=m holds dist(S1.m,x0)<r by TBSP_1:def 2;
x0 in [.a,b.] by A3;
then reconsider x1=x0 as Element of RealSpace by METRIC_1:def 13;
for r being Real st r>0 ex n being Nat st for m being
Nat st n<=m holds dist(S.m,x1)<r
proof
let r be Real;
assume r>0;
then consider n0 being Nat such that
A13: for m being Nat st n0<=m holds dist(S1.m,x0)<r by A12;
for m being Nat st n0<=m holds dist(S.m,x1)<r
proof
let m be Nat;
assume
A14: n0<=m;
dist(S1.m,x0) =(the distance of Closed-Interval-MSpace(a,b)).(S1.
m,x0) by METRIC_1:def 1
.=(the distance of RealSpace).(S1.m,x0) by TOPMETR:def 1
.=dist(S.m,x1) by A1,METRIC_1:def 1;
hence thesis by A13,A14;
end;
hence thesis;
end;
hence thesis by TBSP_1:def 2;
end;
hence S is convergent iff S1 is convergent by A4;
thus S is convergent implies lim S=lim S1
proof
lim S1 in the carrier of Closed-Interval-MSpace(a,b);
then reconsider t0=lim S1 as Point of RealSpace by A3,METRIC_1:def 13;
assume
A15: S is convergent;
for r1 being Real st 0 < r1 ex m1 being Nat st for n1
being Nat st m1 <= n1 holds dist(S.n1,t0) < r1
proof
let r1 being Real;
assume 0<r1;
then consider m1 being Nat such that
A16: for n1 being Nat st m1 <= n1 holds dist(S1.n1,lim S1
) < r1 by A4,A15,TBSP_1:def 3;
for n1 being Nat st m1 <= n1 holds dist(S.n1,t0) < r1
proof
let n1 be Nat;
assume
A17: m1 <= n1;
dist(S1.n1,lim S1) =(the distance of Closed-Interval-MSpace(a,b))
.(S1.n1,lim S1) by METRIC_1:def 1
.=(the distance of RealSpace).(S1.n1,lim S1) by TOPMETR:def 1
.=dist(S.n1,t0) by A1,METRIC_1:def 1;
hence thesis by A16,A17;
end;
hence thesis;
end;
hence thesis by A15,TBSP_1:def 3;
end;
end;
theorem Th8:
for a,b being Real,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
proof
let a,b be Real,s be Real_Sequence, S be sequence of
Closed-Interval-MSpace(a,b);
assume that
A1: S=s and
A2: a<=b and
A3: s is convergent;
reconsider S0=S as sequence of RealSpace by A2,Th6;
A4: S0 is convergent by A1,A3,Th4;
hence S is convergent by A2,Th7;
lim S0=lim S by A2,A4,Th7;
hence thesis by A1,A3,Th4;
end;
theorem
for a,b being Real,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
proof
let a,b be Real,s be Real_Sequence, S be sequence of
Closed-Interval-MSpace(a,b);
assume that
A1: S=s and
A2: a<=b and
A3: s is non-decreasing;
for n being Nat holds s.n<b+1
proof
let n be Nat;
A4: b<b+1 by XREAL_1:29;
A5: n in NAT by ORDINAL1:def 12;
dom S=NAT by FUNCT_2:def 1;
then
A6: s.n in rng S by A1,FUNCT_1:def 3,A5;
the carrier of Closed-Interval-MSpace(a,b)=[.a,b.] by A2,TOPMETR:10;
then s.n <=b by A6,XXREAL_1:1;
hence thesis by A4,XXREAL_0:2;
end;
then s is bounded_above by SEQ_2:def 3;
hence thesis by A1,A2,A3,Th8;
end;
theorem
for a,b being Real,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
proof
let a,b be Real,s be Real_Sequence, S be sequence of
Closed-Interval-MSpace(a,b);
assume that
A1: S=s and
A2: a<=b and
A3: s is non-increasing;
for n being Nat holds s.n>a-1
proof
let n be Nat;
a<a+1 by XREAL_1:29;
then
A4: a-1<a by XREAL_1:19;
A5: n in NAT by ORDINAL1:def 12;
dom S=NAT by FUNCT_2:def 1;
then
A6: s.n in rng S by A1,FUNCT_1:def 3,A5;
the carrier of Closed-Interval-MSpace(a,b)=[.a,b.] by A2,TOPMETR:10;
then a<=s.n by A6,XXREAL_1:1;
hence thesis by A4,XXREAL_0:2;
end;
then s is bounded_below by SEQ_2:def 4;
hence thesis by A1,A2,A3,Th8;
end;
theorem Th11:
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
proof
let R be non empty Subset of REAL;
reconsider rs=upper_bound R as Real;
defpred X[Nat, Real] means ($2 in R & (for r00 being Real
st r00=$2 holds (rs)-(1/($1+1) qua Real)<r00));
assume
A1: R is bounded_above;
A2: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof
let n be Element of NAT;
(n+1)">0;
then 1/(n+1)>0 by XCMPLX_1:215;
then consider r0 being Real such that
A3: r0 in R and
A4: (rs) -(1/(n+1) qua Real)<r0 by A1,SEQ_4:def 1;
for r00 being Real st r00=r0 holds (rs)-(1/(n+1) qua Real)<r00 by A4;
hence thesis by A3;
end;
ex s1 being sequence of REAL st
for n being Element of NAT holds X[n,s1.n] from FUNCT_2:sch 3(A2);
then consider s1 being sequence of REAL such that
A5: for n being Element of NAT holds s1.n in R & for r0 being Real
st r0=s1.n holds (rs)-(1/(n+1) qua Real)<r0;
defpred P[set,set,set] means ($2 is Real implies (for r1,r2 being
Real,n1 being Nat st r1=$2 & r2=s1.(n1+1) & n1=$1 holds (r1>=r2 implies
$3=$2)&(r1<r2 implies $3=s1.(n1+1)))) & (not $2 is Real implies $3=1);
A6: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat;
thus for x being set ex y being set st P[n,x,y]
proof
let x be set;
now
per cases;
case
not x is Real;
hence thesis;
end;
case
A7: x is Real;
then reconsider r10=x as Real;
reconsider r20=s1.(n+1) as Real;
now
per cases;
case
r10>=r20;
then for r1,r2 being Real,n1 being Nat st r1=x & r2=s1.(
n1+1) & n1=n holds (r1>=r2 implies x=x)&(r1<r2 implies x=s1.(n1+1));
hence thesis by A7;
end;
case
r10<r20;
then for r1,r2 being Real,n1 being Nat st r1=x & r2=s1.(
n1+1) & n1=n holds (r1>=r2 implies s1.(n+1)=x)& (r1<r2 implies s1.(n+1)=s1.(n1+
1));
hence thesis by A7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
ex f being Function st dom f = NAT & f.0 = s1.0 &
for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 1(A6);
then consider s2 being Function such that
A8: dom s2 = NAT and
A9: s2.0 = s1.0 and
A10: for n being Nat holds P[n,s2.n,s2.(n+1)];
A11: rng s2 c= REAL
proof
defpred X[Nat] means s2.$1 in REAL;
let y be object;
assume y in rng s2;
then consider x being object such that
A12: x in dom s2 and
A13: y=s2.x by FUNCT_1:def 3;
reconsider n=x as Nat by A8,A12;
A14: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
reconsider r2=s1.(k+1) as Real;
assume
A15: s2.k in REAL;
then reconsider r1=s2.k as Real;
now
per cases;
case
r1>=r2;
hence thesis by A10,A15;
end;
case
r1<r2;
then s2.(k+1)=s1.(k+1) by A10;
hence thesis;
end;
end;
hence thesis;
end;
A16: X[0] by A9;
for m being Nat holds X[m] from NAT_1:sch 2(A16,A14);
then s2.n in REAL;
hence thesis by A13;
end;
then reconsider s3=s2 as Real_Sequence by A8,FUNCT_2:2;
defpred X[Nat] means s1.$1<=s3.$1;
A17: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
A18: k in NAT by ORDINAL1:def 12;
assume s1.k<=s3.k;
reconsider r2=s1.(k+1) as Real;
s2.k in rng s2 by A8,FUNCT_1:def 3,A18;
then reconsider r1=s2.k as Real by A11;
now
per cases;
case
r1>=r2;
hence thesis by A10;
end;
case
r1<r2;
hence thesis by A10;
end;
end;
hence thesis;
end;
A19: X[0] by A9;
A20: for n4 being Nat holds X[n4] from NAT_1:sch 2(A19,A17);
defpred X[Nat] means 0<=$1 implies s3.0<=s3.$1;
A21: for n4 being Nat holds s3.n4<=s3.(n4+1)
proof
let n4 be Nat;
reconsider r2=s1.(n4+1) as Real;
dom s3=NAT by FUNCT_2:def 1;
then reconsider r1=s2.n4 as Real;
now
per cases;
case
r1>=r2;
hence thesis by A10;
end;
case
r1<r2;
hence thesis by A10;
end;
end;
hence thesis;
end;
A22: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume
A23: 0<=k implies s3.0<=s3.k;
now
assume 0<=k+1;
A24: s3.k<=s3.(k+1) by A21;
now
per cases;
case
0<k;
thus s3.0<=s3.(k+1) by A23,A24,XXREAL_0:2;
end;
case
0=k;
hence s3.0<=s3.(k+1) by A21;
end;
end;
hence s3.0<=s3.(k+1);
end;
hence thesis;
end;
defpred Y[Nat] means for n4 being Nat st $1<=n4 holds s3.$1<=s3.
n4;
A25: for k being Nat st Y[k] holds Y[k+1]
proof
let k be Nat;
assume for n5 being Nat st k<=n5 holds s3.k<=s3.n5;
defpred Z[Nat] means k+1<=$1 implies s3.(k+1)<=s3.$1;
A26: for i being Nat st Z[i] holds Z[i+1]
proof
let i be Nat;
A27: i in NAT by ORDINAL1:def 12;
reconsider r2=s1.(i+1) as Real;
s2.i in rng s2 by A8,FUNCT_1:def 3,A27;
then reconsider r1=s2.i as Real by A11;
A28: now
per cases;
case
r1>=r2;
hence s3.i<=s3.(i+1) by A10;
end;
case
r1<r2;
hence s3.i<=s3.(i+1) by A10;
end;
end;
assume
A29: k+1<=i implies s3.(k+1)<=s3.i;
now
assume
A30: k+1<=i+1;
now
per cases by A30,XXREAL_0:1;
case
k+1< i+1;
hence s3.(k+1)<=s3.(i+1) by A29,A28,NAT_1:13,XXREAL_0:2;
end;
case
k+1=i+1;
hence s3.(k+1)<=s3.(i+1);
end;
end;
hence s3.(k+1)<=s3.(i+1);
end;
hence thesis;
end;
A31: Z[0];
for n4 being Nat holds Z[n4] from NAT_1:sch 2(A31,A26);
hence thesis;
end;
A32: X[0];
for n4 being Nat holds X[n4] from NAT_1:sch 2(A32,A22);
then
A33: Y[0];
for m4 being Nat holds Y[m4] from NAT_1:sch 2(A33,A25);
then for m4,n4 being Nat st m4 in dom s3 & n4 in dom s3 & m4 <=
n4 holds s3.m4 <= s3.n4;
then
A34: s3 is non-decreasing by SEQM_3:def 3;
A35: rng s3 c= R
proof
defpred X[set] means s3.$1 in R;
let y be object;
assume y in rng s3;
then
A36: ex x being object st x in dom s3 & y=s3.x by FUNCT_1:def 3;
A37: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
A38: k in NAT by ORDINAL1:def 12;
reconsider r2=s1.(k+1) as Real;
s2.k in rng s2 by A8,FUNCT_1:def 3,A38;
then reconsider r1=s2.k as Real by A11;
assume
A39: s3.k in R;
now
per cases;
case
r1>=r2;
hence thesis by A10,A39;
end;
case
r1<r2;
then s2.(k+1)=s1.(k+1) by A10;
hence thesis by A5;
end;
end;
hence thesis;
end;
A40: X[0] by A5,A9;
for nn being Nat holds X[nn] from NAT_1:sch 2(A40,A37);
hence thesis by A36;
end;
for n being Nat holds s3.n < upper_bound R +1
proof
let n be Nat;
A41: n in NAT by ORDINAL1:def 12;
s3.n in rng s3 by A8,FUNCT_1:def 3,A41;
then
A42: s3.n <=upper_bound R by A1,A35,SEQ_4:def 1;
upper_bound R < upper_bound R +1 by XREAL_1:29;
hence thesis by A42,XXREAL_0:2;
end;
then
A43: s3 is bounded_above by SEQ_2:def 3;
A44: for r being Real st r>0 holds upper_bound R -r<lim s3
proof
let r be Real;
assume
A45: r>0;
consider n2 being Nat such that
A46: 1/r<n2 by SEQ_4:3;
A47: n2 in NAT by ORDINAL1:def 12;
n2<n2+1 by XREAL_1:29;
then 1/r<n2+1 by A46,XXREAL_0:2;
then 1/r*r<(n2+1)*r by A45,XREAL_1:68;
then 1<(n2+1)*r by A45,XCMPLX_1:106;
then 1/(n2+1)<(n2+1)*r/(n2+1) by XREAL_1:74;
then 1/(n2+1)<r by XCMPLX_1:89;
then rs-1/(n2+1)>rs-r by XREAL_1:10;
then
A48: rs-r<s1.n2 by A5,XXREAL_0:2,A47;
A49: s3.n2<=lim s3 by A34,A43,SEQ_4:37;
s1.n2<=s3.n2 by A20;
then rs-r<s3.n2 by A48,XXREAL_0:2;
hence thesis by A49,XXREAL_0:2;
end;
A50: now
reconsider r=upper_bound R -lim s3 as Real;
assume upper_bound R>lim s3;
then r>0 by XREAL_1:50;
then upper_bound R -r<lim s3 by A44;
hence contradiction;
end;
A51: for n being Nat holds s3.n <=upper_bound R
proof
let n be Nat;
A52: n in NAT by ORDINAL1:def 12;
dom s3=NAT by FUNCT_2:def 1;
then s3.n in rng s3 by FUNCT_1:def 3,A52;
hence thesis by A1,A35,SEQ_4:def 1;
end;
for n being Nat holds s3.n < upper_bound R +1
proof
let n be Nat;
upper_bound R<upper_bound R +1 & s3.n<=upper_bound R by A51,XREAL_1:29;
hence thesis by XXREAL_0:2;
end;
then
A53: s3 is bounded_above by SEQ_2:def 3;
then lim s3<=upper_bound R by A34,A51,PREPOWER:2;
hence thesis by A34,A35,A53,A50,XXREAL_0:1;
end;
theorem Th12:
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
proof
let R be non empty Subset of REAL;
reconsider rs=lower_bound R as Real;
defpred X[Nat, Real] means ($2 in R & (for r00 being Real
st r00=$2 holds (rs)+(1/($1+1) qua Real)>r00));
assume
A1: R is bounded_below;
A2: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof
let n be Element of NAT;
(n+1)">0;
then 1/(n+1)>0 by XCMPLX_1:215;
then consider r0 being Real such that
A3: r0 in R and
A4: (rs) +(1/(n+1) qua Real)>r0 by A1,SEQ_4:def 2;
for r00 being Real st r00=r0 holds (rs)+(1/(n+1) qua Real)>r00 by A4;
hence thesis by A3;
end;
ex s1 being sequence of REAL st
for n being Element of NAT holds X[
n,s1.n] from FUNCT_2:sch 3(A2);
then consider s1 being sequence of REAL such that
A5: for n being Element of NAT holds s1.n in R & for r0 being Real
st r0=s1.n holds (rs)+(1/(n+1) qua Real)>r0;
defpred P[set,set,set] means ($2 is Real implies (for r1,r2 being
Real,n1 being Nat st r1=$2 & r2=s1.(n1+1) & n1=$1 holds (r1<=r2 implies
$3=$2)&(r1>r2 implies $3=s1.(n1+1)))) & (not $2 is Real implies $3=1);
A6: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat;
thus for x being set ex y being set st P[n,x,y]
proof
let x be set;
now
per cases;
case
not x is Real;
hence ex y being set st (x is Real implies for r1,r2 being
Real,n1 being Nat st r1=x & r2=s1.(n1+1) & n1=n holds (r1>=r2 implies y=
x)&(r1<r2 implies y=s1.(n1+1)) ) &(not x is Real implies y=1);
end;
case
A7: x is Real;
then reconsider r10=x as Real;
reconsider r20=s1.(n+1) as Real;
now
per cases;
case
r10<=r20;
then for r1,r2 being Real,n1 being Nat st r1=x & r2=s1.(
n1+1) & n1=n holds (r1<=r2 implies x=x)&(r1>r2 implies x=s1.(n1+1));
hence thesis by A7;
end;
case
r10>r20;
then for r1,r2 being Real,n1 being Nat st r1=x & r2=s1.(
n1+1) & n1=n holds (r1<=r2 implies s1.(n+1)=x)& (r1>r2 implies s1.(n+1)=s1.(n1+
1));
hence thesis by A7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
ex f being Function st dom f = NAT & f.0 = s1.0 &
for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 1(A6);
then consider s2 being Function such that
A8: dom s2 = NAT and
A9: s2.0 = s1.0 and
A10: for n being Nat holds P[n,s2.n,s2.(n+1)];
A11: rng s2 c= REAL
proof
defpred X[Nat] means s2.$1 in REAL;
let y be object;
assume y in rng s2;
then consider x being object such that
A12: x in dom s2 and
A13: y=s2.x by FUNCT_1:def 3;
reconsider n=x as Nat by A8,A12;
A14: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
reconsider r2=s1.(k+1) as Real;
assume
A15: s2.k in REAL;
then reconsider r1=s2.k as Real;
now
per cases;
case
r1<=r2;
hence thesis by A10,A15;
end;
case
r1>r2;
then s2.(k+1)=s1.(k+1) by A10;
hence thesis;
end;
end;
hence thesis;
end;
A16: X[0] by A9;
for m being Nat holds X[m] from NAT_1:sch 2(A16,A14);
then s2.n in REAL;
hence thesis by A13;
end;
then reconsider s3=s2 as Real_Sequence by A8,FUNCT_2:2;
defpred X[Nat] means s1.$1>=s3.$1;
A17: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
A18: k in NAT by ORDINAL1:def 12;
assume s1.k>=s3.k;
reconsider r2=s1.(k+1) as Real;
s2.k in rng s2 by A8,FUNCT_1:def 3,A18;
then reconsider r1=s2.k as Real by A11;
now
per cases;
case
r1<=r2;
hence thesis by A10;
end;
case
r1>r2;
hence thesis by A10;
end;
end;
hence thesis;
end;
A19: X[0] by A9;
A20: for n4 being Nat holds X[n4] from NAT_1:sch 2(A19,A17);
defpred X[Nat] means 0<=$1 implies s3.0>=s3.$1;
A21: for n4 being Nat holds s3.n4>=s3.(n4+1)
proof
let n4 be Nat;
reconsider r2=s1.(n4+1) as Real;
dom s3=NAT by FUNCT_2:def 1;
then reconsider r1=s2.n4 as Real;
now
per cases;
case
r1<=r2;
hence thesis by A10;
end;
case
r1>r2;
hence thesis by A10;
end;
end;
hence thesis;
end;
A22: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume
A23: 0<=k implies s3.0>=s3.k;
now
assume 0<=k+1;
A24: s3.k>=s3.(k+1) by A21;
now
per cases;
case
0<k+1;
thus s3.0>=s3.(k+1) by A23,A24,XXREAL_0:2;
end;
case
0=k+1;
hence s3.0>=s3.(k+1);
end;
end;
hence s3.0>=s3.(k+1);
end;
hence thesis;
end;
defpred Y[Nat] means for n4 being Nat st $1<=n4 holds s3.$1>=s3.
n4;
A25: for k being Nat st Y[k] holds Y[k+1]
proof
let k be Nat;
assume for n5 being Nat st k<=n5 holds s3.k>=s3.n5;
defpred X[Nat] means k+1<=$1 implies s3.(k+1)>=s3.$1;
A26: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat;
A27: i in NAT by ORDINAL1:def 12;
reconsider r2=s1.(i+1) as Real;
s2.i in rng s2 by A8,FUNCT_1:def 3,A27;
then reconsider r1=s2.i as Real by A11;
A28: now
per cases;
case
r1<=r2;
hence s3.i>=s3.(i+1) by A10;
end;
case
r1>r2;
hence s3.i>=s3.(i+1) by A10;
end;
end;
assume
A29: k+1<=i implies s3.(k+1)>=s3.i;
now
assume
A30: k+1<=i+1;
now
per cases by A30,XXREAL_0:1;
case
k+1<i+1;
hence s3.(k+1)>=s3.(i+1) by A29,A28,NAT_1:13,XXREAL_0:2;
end;
case
k+1=i+1;
hence s3.(k+1)>=s3.(i+1);
end;
end;
hence s3.(k+1)>=s3.(i+1);
end;
hence thesis;
end;
A31: X[0];
thus for n4 being Nat holds X[n4] from NAT_1:sch 2(A31, A26);
end;
A32: X[0];
for n4 being Nat holds X[n4] from NAT_1:sch 2(A32,A22);
then
A33: Y[0];
for m4 being Nat holds Y[m4] from NAT_1:sch 2(A33,A25);
then for m4,n4 being Nat st m4 in dom s3 & n4 in dom s3 & m4 <=
n4 holds s3.m4 >= s3.n4;
then
A34: s3 is non-increasing by SEQM_3:def 4;
A35: rng s3 c= R
proof
defpred Z[Nat] means s3.$1 in R;
let y be object;
assume y in rng s3;
then
A36: ex x being object st x in dom s3 & y=s3.x by FUNCT_1:def 3;
A37: for k being Nat st Z[k] holds Z[k+1]
proof
let k be Nat;
A38: k in NAT by ORDINAL1:def 12;
reconsider r2=s1.(k+1) as Real;
s2.k in rng s2 by A8,FUNCT_1:def 3,A38;
then reconsider r1=s2.k as Real by A11;
assume
A39: s3.k in R;
now
per cases;
case
r1<=r2;
hence thesis by A10,A39;
end;
case
r1>r2;
then s2.(k+1)=s1.(k+1) by A10;
hence thesis by A5;
end;
end;
hence thesis;
end;
A40: Z[0] by A5,A9;
for nn being Nat holds Z[nn] from NAT_1:sch 2(A40,A37);
hence thesis by A36;
end;
for n being Nat holds s3.n > lower_bound R -1
proof
let n be Nat;
A41: n in NAT by ORDINAL1:def 12;
lower_bound R < lower_bound R +1 by XREAL_1:29;
then
A42: lower_bound R > lower_bound R -1 by XREAL_1:19;
s3.n in rng s3 by A8,FUNCT_1:def 3,A41;
then s3.n >=lower_bound R by A1,A35,SEQ_4:def 2;
hence thesis by A42,XXREAL_0:2;
end;
then
A43: s3 is bounded_below by SEQ_2:def 4;
A44: for r being Real st r>0 holds lower_bound R +r>lim s3
proof
let r be Real;
assume
A45: r>0;
consider n2 being Nat such that
A46: 1/r<n2 by SEQ_4:3;
A47: n2 in NAT by ORDINAL1:def 12;
n2<n2+1 by XREAL_1:29;
then 1/r<n2+1 by A46,XXREAL_0:2;
then 1/r*r<(n2+1)*r by A45,XREAL_1:68;
then 1<(n2+1)*r by A45,XCMPLX_1:106;
then 1/(n2+1)<(n2+1)*r/(n2+1) by XREAL_1:74;
then 1/(n2+1)<r by XCMPLX_1:89;
then rs+1/(n2+1)<rs+r by XREAL_1:8;
then
A48: rs+r>s1.n2 by A5,XXREAL_0:2,A47;
A49: s3.n2>=lim s3 by A34,A43,SEQ_4:38;
s1.n2>=s3.n2 by A20;
then rs+r>s3.n2 by A48,XXREAL_0:2;
hence thesis by A49,XXREAL_0:2;
end;
A50: now
reconsider r=(lim s3) -lower_bound R as Real;
assume lower_bound R<lim s3;
then r>0 by XREAL_1:50;
then lower_bound R +((lim s3)+-lower_bound R)>lim s3 by A44;
hence contradiction;
end;
A51: for n being Nat holds s3.n >=lower_bound R
proof
let n be Nat;
A52: n in NAT by ORDINAL1:def 12;
dom s3=NAT by FUNCT_2:def 1;
then s3.n in rng s3 by FUNCT_1:def 3,A52;
hence thesis by A1,A35,SEQ_4:def 2;
end;
for n being Nat holds s3.n > lower_bound R -1
proof
let n be Nat;
lower_bound R<lower_bound R +1 by XREAL_1:29;
then
A53: lower_bound R>lower_bound R -1 by XREAL_1:19;
s3.n>=lower_bound R by A51;
hence thesis by A53,XXREAL_0:2;
end;
then
A54: s3 is bounded_below by SEQ_2:def 4;
then lim s3>=lower_bound R by A34,A51,PREPOWER:1;
hence thesis by A34,A35,A54,A50,XXREAL_0:1;
end;
theorem Th13:
:: An Abstract Intermediate Value Theorem for Closed Sets
for X being non empty MetrSpace, f being Function 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
proof
let X be non empty MetrSpace, f be Function of I[01],TopSpaceMetr(X), F1,F2
be Subset of TopSpaceMetr(X),r1,r2 be Real;
assume that
A1: 0<=r1 and
A2: r2<=1 and
A3: r1<=r2 & f.r1 in F1 and
A4: f.r2 in F2 and
A5: F1 is closed and
A6: F2 is closed and
A7: f is continuous and
A8: F1 \/ F2 =the carrier of X;
A9: r1 in {r3 where r3 is Real: r1<=r3 & r3<=r2 & f.r3 in F1} by A3;
{r3 where r3 is Real: r1<=r3 & r3<=r2 & f.r3 in F1} c= REAL
proof
let x be object;
assume x in {r3 where r3 is Real: r1<=r3 & r3<=r2 & f.r3 in F1};
then ex r3 being Real st r3=x & r1<=r3 & r3<=r2 & f.r3 in F1;
hence thesis by XREAL_0:def 1;
end;
then reconsider R={r3 where r3 is Real:
r1<=r3 & r3<=r2 & f.r3 in F1} as non
empty Subset of REAL by A9;
A10: for r being Real st r in R holds r<=r2
proof
let r be Real;
assume r in R;
then ex r3 being Real st r3=r & r1<=r3 & r3<=r2 & f.r3 in F1;
hence thesis;
end;
r2 is UpperBound of R
proof
let r be ExtReal;
assume r in R;
then ex r3 being Real st r3=r & r1<=r3 & r3<=r2 & f.r3 in F1;
hence thesis;
end;
then
A11: R is bounded_above;
then consider s1 being Real_Sequence such that
A12: s1 is non-decreasing convergent and
A13: rng s1 c= R and
A14: lim s1=upper_bound R by Th11;
{r3 where r3 is Real: r1<=r3 & r3<=r2 & f.r3 in F1} c= [.0,1.]
proof
let x be object;
assume x in {r3 where r3 is Real: r1<=r3 & r3<=r2 & f.r3 in F1};
then consider r3 being Real such that
A15: r3=x & r1<=r3 and
A16: r3<=r2 and
f.r3 in F1;
r3<=1 by A2,A16,XXREAL_0:2;
hence thesis by A1,A15,XXREAL_1:1;
end;
then reconsider S1=s1 as sequence of Closed-Interval-MSpace(0,1) by A13,Th5,
XBOOLE_1:1;
A17: I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by TOPMETR:20,def 7;
then reconsider S00=f*S1 as sequence of X by Th2;
A18: S00 is convergent by A7,A12,A17,Th3,Th8;
dom f=the carrier of I[01] by FUNCT_2:def 1
.=the carrier of Closed-Interval-MSpace(0,1) by A17,TOPMETR:12;
then f.(lim S1) in rng f by FUNCT_1:3;
then reconsider t1=f.(lim S1) as Point of X by TOPMETR:12;
reconsider S2=s1 as sequence of RealSpace by METRIC_1:def 13;
A19: S1 is convergent by A12,Th8;
then S2 is convergent by Th7;
then lim S2=lim S1 by Th7;
then
A20: lim s1=lim S1 by A12,Th4;
A21: for r being Real st r>0 ex n being Nat st for m being
Nat st m>=n holds dist(S00.m,t1)<r
proof
let r be Real;
assume r>0;
then consider r7 being Real such that
A22: r7>0 and
A23: for w being Point of Closed-Interval-MSpace(0,1), w1 being Point
of X st w1=f.w & dist(lim S1,w)<r7 holds dist(t1,w1)<r by A7,A17,UNIFORM1:4
;
consider n0 being Nat such that
A24: for m being Nat st m>=n0 holds dist(S1.m,lim S1)<r7 by A19,A22,
TBSP_1:def 3;
for m being Nat st m>=n0 holds dist(S00.m,t1)<r
proof
let m be Nat;
A25: m in NAT by ORDINAL1:def 12;
dom S00=NAT by TBSP_1:4;
then
A26: S00.m=f.(S1.m) by FUNCT_1:12,A25;
assume m>=n0;
then dist(lim S1,S1.m)<r7 by A24;
hence thesis by A23,A26;
end;
hence thesis;
end;
A27: r2>=upper_bound R by A10,SEQ_4:144;
then
A28: r2 in {r3 where r3 is Real:
upper_bound R <=r3 & r3<=r2 & f.r3 in F2}
by A4;
{r3 where r3 is Real: upper_bound R<=r3 & r3<=r2 & f.r3 in F2} c= REAL
proof
let x be object;
assume x in {r3 where r3 is Real:
upper_bound R<=r3 & r3<=r2 & f.r3 in F2};
then ex r3 being Real
st r3=x & upper_bound R<=r3 & r3<=r2 & f.r3 in F2;
hence thesis by XREAL_0:def 1;
end;
then reconsider
R2={r3 where r3 is Real: upper_bound R<=r3 & r3<=r2 & f.r3 in F2}
as non empty Subset of REAL by A28;
A29: for r being Real st r in R2 holds r>=upper_bound R
proof
let r be Real;
assume r in R2;
then ex r3 being Real
st r3=r & upper_bound R<=r3 & r3<=r2 & f.r3 in F2;
hence thesis;
end;
upper_bound R is LowerBound of R2
proof
let r be ExtReal;
assume r in R2;
then ex r3 being Real
st r3=r & upper_bound R<=r3 & r3<=r2 & f.r3 in F2;
hence thesis;
end;
then
A30: R2 is bounded_below;
then consider s2 being Real_Sequence such that
A31: s2 is non-increasing convergent and
A32: rng s2 c= R2 and
A33: lim s2=lower_bound R2 by Th12;
A34: 0<=upper_bound R by A1,A9,A11,SEQ_4:def 1;
{r3 where r3 is Real:
upper_bound R <=r3 & r3<=r2 & f.r3 in F2} c= [.0, 1.]
proof
let x be object;
assume x in {r3 where r3 is Real:
upper_bound R<=r3 & r3<=r2 & f.r3 in F2};
then consider r3 being Real such that
A35: r3=x & upper_bound R<=r3 and
A36: r3<=r2 and
f.r3 in F2;
r3<=1 by A2,A36,XXREAL_0:2;
hence thesis by A34,A35,XXREAL_1:1;
end;
then reconsider S1=s2 as sequence of Closed-Interval-MSpace(0,1) by A32,Th5,
XBOOLE_1:1;
reconsider S2=s2 as sequence of RealSpace by METRIC_1:def 13;
A37: S1 is convergent by A31,Th8;
then S2 is convergent by Th7;
then lim S2=lim S1 by Th7;
then
A38: lim s2=lim S1 by A31,Th4;
for n4 being Nat holds S00.n4 in F1
proof
let n4 be Nat;
A39: n4 in NAT by ORDINAL1:def 12;
dom s1=NAT by FUNCT_2:def 1;
then s1.n4 in rng s1 by FUNCT_1:def 3,A39;
then s1.n4 in R by A13;
then dom S00=NAT &
ex r3 being Real st r3=s1.n4 & r1<=r3 & r3<=r2 & f.r3
in F1 by TBSP_1:4;
hence thesis by FUNCT_1:12,A39;
end;
then lim S00 in F1 by A5,A7,A19,A17,Th1,Th3;
then
A40: f.(lim s1) in F1 by A20,A18,A21,TBSP_1:def 3;
A41: I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by TOPMETR:20,def 7;
then reconsider S00=f*S1 as sequence of X by Th2;
dom f=the carrier of I[01] by FUNCT_2:def 1
.=the carrier of Closed-Interval-MSpace(0,1) by A41,TOPMETR:12;
then f.(lim S1) in rng f by FUNCT_1:3;
then reconsider t1=f.(lim S1) as Point of X by TOPMETR:12;
A42: for r being Real st r>0 ex n being Nat st for m being
Nat st m>=n holds dist(S00.m,t1)<r
proof
let r be Real;
assume r>0;
then consider r7 being Real such that
A43: r7>0 and
A44: for w being Point of Closed-Interval-MSpace(0,1), w1 being Point
of X st w1=f.w & dist(lim S1,w)<r7 holds dist(t1,w1)<r by A7,A41,UNIFORM1:4
;
consider n0 being Nat such that
A45: for m being Nat st m>=n0 holds dist(S1.m,lim S1)<r7
by A37,A43,TBSP_1:def 3;
for m being Nat st m>=n0 holds dist(S00.m,t1)<r
proof
let m be Nat;
A46: m in NAT by ORDINAL1:def 12;
dom S00=NAT by TBSP_1:4;
then
A47: S00.m=f.(S1.m) by FUNCT_1:12,A46;
assume m>=n0;
then dist(lim S1,S1.m)<r7 by A45;
hence thesis by A44,A47;
end;
hence thesis;
end;
A48: r1<= upper_bound R by A9,A11,SEQ_4:def 1;
for s being Real st 0<s ex r being Real st r in R2 & r<
upper_bound R+s
proof
let s be Real;
assume
A49: 0<s;
now
assume
A50: for r being Real st r<upper_bound R+s holds not r in R2;
now
per cases by A27,XREAL_1:48;
case
r2-upper_bound R=0;
hence contradiction by A28,A49,A50,XREAL_1:29;
end;
case
A51: r2-upper_bound R>0;
set rs0=min(r2-upper_bound R,s);
set r0=upper_bound R + rs0/2;
A52: rs0>0 by A49,A51,XXREAL_0:21;
then
A53: upper_bound R<r0 by XREAL_1:29,215;
rs0<=r2-upper_bound R by XXREAL_0:17;
then
A54: upper_bound R +rs0<=upper_bound R +(r2-upper_bound R) by XREAL_1:7;
A55: rs0/2<rs0 by A52,XREAL_1:216;
then upper_bound R +rs0/2<upper_bound R +rs0 by XREAL_1:8;
then
A56: r0<=r2 by A54,XXREAL_0:2;
then r0<=1 by A2,XXREAL_0:2;
then r0 in the carrier of I[01] by A1,A48,A52,BORSUK_1:40,XXREAL_1:1;
then r0 in dom f by FUNCT_2:def 1;
then f.r0 in rng f by FUNCT_1:def 3;
then f.r0 in the carrier of TopSpaceMetr(X);
then f.r0 in the carrier of X by TOPMETR:12;
then
A57: f.r0 in F1 or f.r0 in F2 by A8,XBOOLE_0:def 3;
upper_bound R <= upper_bound R + rs0/2 by A52,XREAL_1:29,215;
then
A58: r1<=r0 by A48,XXREAL_0:2;
rs0<=s by XXREAL_0:17;
then rs0/2<s by A55,XXREAL_0:2;
then r0<upper_bound R+s by XREAL_1:8;
then
A59: not r0 in R2 by A50;
upper_bound R <r0 by A52,XREAL_1:29,215;
then r0 in R by A59,A58,A56,A57;
hence contradiction by A11,A53,SEQ_4:def 1;
end;
end;
hence contradiction;
end;
hence thesis;
end;
then
A60: upper_bound R=lower_bound R2 by A29,A30,SEQ_4:def 2;
S00 is convergent by A7,A31,A41,Th3,Th8;
then
A61: f.(lim S1)=lim S00 by A42,TBSP_1:def 3;
for n4 being Nat holds S00.n4 in F2
proof
let n4 be Nat;
A62: n4 in NAT by ORDINAL1:def 12;
dom s2=NAT by FUNCT_2:def 1;
then s2.n4 in rng s2 by FUNCT_1:def 3,A62;
then s2.n4 in R2 by A32;
then dom S00=NAT &
ex r3 being Real st r3=s2.n4 & upper_bound R<=r3 & r3
<= r2 & f.r3 in F2 by TBSP_1:4;
hence thesis by FUNCT_1:12,A62;
end;
then lim S00 in F2 by A6,A7,A37,A41,Th1,Th3;
then f.(lim s1) in F1 /\ F2 by A60,A14,A40,A33,A38,A61,XBOOLE_0:def 4;
hence thesis by A27,A48,A14;
end;
theorem Th14:
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
proof
let n be Nat,p1,p2 be Point of TOP-REAL n, P,P1 be non empty
Subset of TOP-REAL n;
assume that
A1: P is_an_arc_of p1,p2 and
A2: P1 is_an_arc_of p2,p1 and
A3: P1 c= P;
P1 is_an_arc_of p1,p2 by A2,JORDAN5B:14;
hence thesis by A1,A3,JORDAN6:46;
end;
theorem
for P,P1 being compact non empty 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 holds
P1=Upper_Arc(P) or P1=Lower_Arc(P)
proof
let P,P1 be compact non empty Subset of TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: P1 is_an_arc_of W-min(P),E-max(P) and
A3: P1 c= P;
A4: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
A5: the carrier of (TOP-REAL 2)|P=[#]((TOP-REAL 2)|P) .=P by PRE_TOPC:def 5;
then reconsider U2=Upper_Arc(P) as Subset of (TOP-REAL 2)|P by A1,JORDAN6:61;
reconsider U3=Lower_Arc(P) as Subset of (TOP-REAL 2)|P by A1,A5,JORDAN6:61;
A6: Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9;
U2=Upper_Arc(P) /\ P by A1,JORDAN6:61,XBOOLE_1:28;
then
A7: U2 is closed by A4,JORDAN6:2,11;
A8: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:def 9;
U3=Lower_Arc(P) /\ P by A1,JORDAN6:61,XBOOLE_1:28;
then
A9: U3 is closed by A6,JORDAN6:2,11;
A10: Upper_Arc(P) /\ Lower_Arc(P)={W-min(P),E-max(P)} by A1,JORDAN6:def 9;
then
A11: E-max(P) in Upper_Arc(P) /\ Lower_Arc(P) by TARSKI:def 2;
A12: W-min(P) in Upper_Arc(P) /\ Lower_Arc(P) by A10,TARSKI:def 2;
consider f being Function of I[01], (TOP-REAL 2)|P1 such that
A13: f is being_homeomorphism and
A14: f.0 = W-min(P) and
A15: f.1 = E-max(P) by A2,TOPREAL1:def 1;
A16: f is one-to-one by A13,TOPS_2:def 5;
A17: dom f=[#](I[01]) by A13,TOPS_2:def 5;
A18: rng f=[#]((TOP-REAL 2)|P1) by A13,TOPS_2:def 5
.=P1 by PRE_TOPC:def 5;
A19: f is continuous by A13,TOPS_2:def 5;
now
per cases;
case
A20: for r being Real st 0<r & r<1 holds f.r in Lower_Arc(P);
P1 c= Lower_Arc(P)
proof
let y be object;
assume y in P1;
then consider x being object such that
A21: x in dom f and
A22: y=f.x by A18,FUNCT_1:def 3;
reconsider r=x as Real by A21;
A23: r<=1 by A21,BORSUK_1:40,XXREAL_1:1;
now
per cases by A21,A23,BORSUK_1:40,XXREAL_0:1,XXREAL_1:1;
case
0<r & r<1;
hence thesis by A20,A22;
end;
case
r=0;
hence thesis by A12,A14,A22,XBOOLE_0:def 4;
end;
case
r=1;
hence thesis by A11,A15,A22,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
hence thesis by A2,A6,Th14;
end;
case
A24: ex r being Real st 0<r & r<1 & not f.r in Lower_Arc(P);
now
per cases;
case
A25: for r being Real st 0<r & r<1 holds f.r in Upper_Arc(P);
P1 c= Upper_Arc(P)
proof
let y be object;
assume y in P1;
then consider x being object such that
A26: x in dom f and
A27: y=f.x by A18,FUNCT_1:def 3;
reconsider r=x as Real by A26;
A28: r<=1 by A26,BORSUK_1:40,XXREAL_1:1;
now
per cases by A26,A28,BORSUK_1:40,XXREAL_0:1,XXREAL_1:1;
case
0<r & r<1;
hence thesis by A25,A27;
end;
case
r=0;
hence thesis by A12,A14,A27,XBOOLE_0:def 4;
end;
case
r=1;
hence thesis by A11,A15,A27,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
hence thesis by A2,A4,JORDAN6:46;
end;
case
ex r being Real st 0<r & r<1 & not f.r in Upper_Arc(P);
then consider r2 being Real such that
A29: 0<r2 and
A30: r2<1 and
A31: not f.r2 in Upper_Arc(P);
r2 in [.0,1.] by A29,A30,XXREAL_1:1;
then f.r2 in rng f by A17,BORSUK_1:40,FUNCT_1:def 3;
then
A32: f.r2 in Lower_Arc(P) by A3,A8,A18,A31,XBOOLE_0:def 3;
consider r1 being Real such that
A33: 0<r1 and
A34: r1<1 and
A35: not f.r1 in Lower_Arc(P) by A24;
r1 in [.0,1.] by A33,A34,XXREAL_1:1;
then
A36: f.r1 in rng f by A17,BORSUK_1:40,FUNCT_1:def 3;
then
A37: f.r1 in Upper_Arc(P) by A3,A8,A18,A35,XBOOLE_0:def 3;
now
per cases;
case
A38: r1<=r2;
now
per cases by A38,XXREAL_0:1;
case
r1=r2;
hence contradiction by A3,A8,A18,A31,A35,A36,XBOOLE_0:def 3;
end;
case
A39: r1<r2;
reconsider Q=P as non empty Subset of Euclid 2 by TOPREAL3:8;
A40: the carrier of (TOP-REAL 2)|P1=[#]((TOP-REAL 2)|P1)
.=P1 by PRE_TOPC:def 5;
the carrier of (TOP-REAL 2)|P=[#]((TOP-REAL 2)|P)
.=P by PRE_TOPC:def 5;
then rng f c= the carrier of (TOP-REAL 2)|P by A3,A40;
then reconsider
g=f as Function of I[01],(TOP-REAL 2)|P by A17,FUNCT_2:2;
P=P1 \/ P by A3,XBOOLE_1:12;
then
A41: (TOP-REAL 2)|P1 is SubSpace of (TOP-REAL 2)|P by TOPMETR:4;
U2 \/ U3 =the carrier of ((Euclid 2)|Q) & (TOP-REAL 2)|
P=TopSpaceMetr(( Euclid 2)|Q) by A8,EUCLID:63,TOPMETR:def 2;
then consider r0 being Real such that
A42: r1<=r0 and
A43: r0<=r2 and
A44: g.r0 in U2 /\ U3 by A19,A7,A9,A30,A33,A32,A37,A39,A41,Th13,
PRE_TOPC:26;
r0<1 by A30,A43,XXREAL_0:2;
then
A45: r0 in dom f by A17,A33,A42,BORSUK_1:40,XXREAL_1:1;
A46: 1 in dom f by A17,BORSUK_1:40,XXREAL_1:1;
A47: 0 in dom f by A17,BORSUK_1:40,XXREAL_1:1;
now
per cases by A10,A44,TARSKI:def 2;
case
g.r0=W-min(P);
hence contradiction by A14,A16,A33,A42,A45,A47,
FUNCT_1:def 4;
end;
case
g.r0=E-max(P);
hence contradiction by A15,A16,A30,A43,A45,A46,
FUNCT_1:def 4;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
case
A48: r1>r2;
reconsider Q=P as non empty Subset of Euclid 2 by TOPREAL3:8;
A49: the carrier of (TOP-REAL 2)|P1=[#]((TOP-REAL 2)|P1)
.=P1 by PRE_TOPC:def 5;
the carrier of (TOP-REAL 2)|P=[#]((TOP-REAL 2)|P)
.=P by PRE_TOPC:def 5;
then rng f c= the carrier of (TOP-REAL 2)|P by A3,A49;
then reconsider g=f as Function of I[01],(TOP-REAL 2)|P by A17,
FUNCT_2:2;
P=P1 \/ P by A3,XBOOLE_1:12;
then
A50: (TOP-REAL 2)|P1 is SubSpace of (TOP-REAL 2)|P by TOPMETR:4;
U2 \/ U3 =the carrier of ((Euclid 2)|Q) & (TOP-REAL 2)|P=
TopSpaceMetr(( Euclid 2)|Q) by A8,EUCLID:63,TOPMETR:def 2;
then consider r0 being Real such that
A51: r2<=r0 and
A52: r0<=r1 and
A53: g.r0 in U2 /\ U3 by A19,A7,A9,A29,A34,A32,A37,A48,A50,Th13,
PRE_TOPC:26;
r0<1 by A34,A52,XXREAL_0:2;
then
A54: r0 in dom f by A17,A29,A51,BORSUK_1:40,XXREAL_1:1;
A55: 1 in dom f by A17,BORSUK_1:40,XXREAL_1:1;
A56: 0 in dom f by A17,BORSUK_1:40,XXREAL_1:1;
now
per cases by A10,A53,TARSKI:def 2;
case
g.r0=W-min(P);
hence contradiction by A14,A16,A29,A51,A54,A56,FUNCT_1:def 4;
end;
case
g.r0=E-max(P);
hence contradiction by A15,A16,A34,A52,A54,A55,FUNCT_1:def 4;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;