:: Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 1989
:: Copyright (c) 1990-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, SUBSET_1, SEQ_1, ORDINAL2, NAT_1, ARYTM_3, XXREAL_0,
REAL_1, CARD_1, ARYTM_1, MEMBERED, XXREAL_2, COMPLEX1, TARSKI, XBOOLE_0,
SEQ_2, FUNCT_1, VALUED_0, RELAT_1, FUNCOP_1, VALUED_1, SQUARE_1, SEQM_3,
SEQ_4, BINOP_1, BINOP_2, FINSEQOP, XCMPLX_0, COMPLSP1, FINSEQ_1,
ZFMISC_1, FINSEQ_2, CARD_3, RVSUM_1, RCOMP_1, SETFAM_1, METRIC_1,
FINSET_1, ORDINAL4, PARTFUN1, GOBOARD2, MEMBER_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, CARD_1, FINSET_1,
MEMBERED, ORDINAL1, NUMBERS, XXREAL_2, XCMPLX_0, XXREAL_0, XREAL_0,
SETFAM_1, REAL_1, SQUARE_1, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, SEQ_1,
COMSEQ_2, SEQ_2, SEQM_3, FUNCT_2, BINOP_1, BINOP_2, FINSEQ_1, FUNCOP_1,
NAT_1, VALUED_0, VALUED_1, MEMBER_1, RVSUM_1, FINSEQ_2, RECDEF_1,
FINSEQOP;
constructors FUNCOP_1, REAL_1, NAT_1, COMPLEX1, PARTFUN1, SEQ_2, SEQM_3,
SQUARE_1, VALUED_1, RECDEF_1, XXREAL_2, FINSET_1, RELSET_1, BINOP_1,
BINOP_2, SETWISEO, FINSEQOP, ZFMISC_1, RVSUM_1, MEMBER_1, COMSEQ_2,
NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FUNCOP_1, SEQ_2,
FINSET_1, BINOP_2, FUNCT_1, FINSEQ_2, SUBSET_1, NAT_1, RELAT_1, FINSEQ_1,
CARD_1, MEMBER_1, SQUARE_1, RVSUM_1, XCMPLX_0, SEQ_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions XBOOLE_0, TARSKI, SEQ_2, FINSEQ_1, XXREAL_2, FINSEQOP;
equalities COMPLEX1, FINSEQ_1, SQUARE_1, SUBSET_1, VALUED_1, XCMPLX_0;
expansions XBOOLE_0, TARSKI, SEQ_2, XXREAL_2, FINSEQOP, VALUED_1;
theorems NAT_1, SEQ_1, SEQ_2, SEQM_3, AXIOMS, FUNCT_1, FUNCT_2, ABSVALUE,
TARSKI, RELAT_1, RELSET_1, XREAL_0, XBOOLE_1, SUBSET_1, XCMPLX_0,
MEMBERED, XREAL_1, FUNCOP_1, COMPLEX1, XXREAL_0, ORDINAL1, SQUARE_1,
XXREAL_2, VALUED_0, BINOP_2, SETWISEO, FINSEQOP, BINOP_1, ZFMISC_1,
VALUED_1, FINSEQ_1, FINSEQ_2, RVSUM_1, XBOOLE_0, FINSEQ_3, CARD_1,
CARD_2, FINSEQ_4, MEMBER_1, NUMBERS;
schemes NAT_1, RECDEF_1, SEQ_1, SUBSET_1, FUNCT_2, FRAENKEL, BINOP_2,
DOMAIN_1;
begin
reserve n,k,k1,m,m1,n1,n2,l for Nat;
reserve r,r1,r2,p,p1,g,g1,g2,s,s1,s2,t for Real;
reserve seq,seq1,seq2 for Real_Sequence;
reserve Nseq for increasing sequence of NAT;
reserve x for set;
reserve X,Y for Subset of REAL;
theorem Th1:
for X,Y st for r,p st r in X & p in Y holds r<p ex g st for r,p
st r in X & p in Y holds r<=g & g<=p
proof
let X,Y;
assume for r,p st r in X & p in Y holds r<p;
then for r,p st r in X & p in Y holds r<=p;
then consider g such that
A1: for r,p st r in X & p in Y holds r <= g & g <= p by AXIOMS:1;
reconsider g as Real;
take g;
thus thesis by A1;
end;
theorem Th2:
0<p & (ex r st r in X) & (for r st r in X holds r+p in X) implies
for g ex r st r in X & g<r
proof
assume that
A1: 0<p and
A2: ex r st r in X and
A3: for r st r in X holds r+p in X and
A4: ex g st for r st r in X holds not g<r;
defpred X[Real] means for r st r in X holds not $1<r;
consider Y such that
A5: for p1 being Element of REAL holds p1 in Y iff X[p1] from SUBSET_1:sch 3;
now
let r,p1 such that
A6: r in X and
A7: p1 in Y;
r+p in X by A3,A6;
then
A8: r+p<=p1 by A5,A7;
r+(0 qua Nat)<r+p by A1,XREAL_1:8;
hence r<p1 by A8,XXREAL_0:2;
end;
then consider g2 such that
A9: for r,p1 st r in X & p1 in Y holds r<=g2 & g2<=p1 by Th1;
consider g1 such that
A10: for r st r in X holds not g1<r by A4;
g1 in REAL by XREAL_0:def 1;
then
A11: g1 in Y by A10,A5;
reconsider g2p = g2-p as Element of REAL by XREAL_0:def 1;
A12: now
assume not g2-p in Y;
then not X[g2p] by A5;
then consider r1 being Real such that
A13: r1 in X & g2p<r1;
g2-p+p<r1+p & r1+p in X by A3,A13,XREAL_1:6;
hence contradiction by A11,A9;
end;
-p<-(0 qua Nat) by A1;
then g2+-p<g2+(0 qua Nat) by XREAL_1:6;
hence contradiction by A2,A9,A12;
end;
theorem Th3:
for r ex n st r<n
proof
let r;
for r st r in NAT holds r+1 in NAT by AXIOMS:2;
then consider p such that
A1: p in NAT and
A2: r<p by Th2, NUMBERS:19;
consider n1 such that
A3: n1=p by A1;
take n1;
thus thesis by A2,A3;
end;
theorem
X is real-bounded iff ex s st 0<s & for r st r in X holds |.r.|<s
proof
thus X is real-bounded implies ex s st 0<s & for r st r in X holds |.r.|<s
proof
assume
A1: X is real-bounded;
then consider s1 such that
A2: s1 is UpperBound of X by XXREAL_2:def 10;
A3: for r st r in X holds r<=s1 by A2,XXREAL_2:def 1;
consider s2 such that
A4: s2 is LowerBound of X by A1,XXREAL_2:def 9;
A5: for r st r in X holds s2<=r by A4,XXREAL_2:def 2;
take s=|.s1.|+|.s2.|+1;
A6: 0<=|.s1.| by COMPLEX1:46;
A7: 0<=|.s2.| by COMPLEX1:46;
hence 0<s by A6;
let r such that
A8: r in X;
s1<=|.s1.| & r<=s1 by A3,A8,ABSVALUE:4;
then r<=|.s1.| by XXREAL_0:2;
then r+(0 qua Nat)<=|.s1.|+|.s2.| by A7,XREAL_1:7;
then
A9: r<s by XREAL_1:8;
-|.s2.|<=s2 & s2<=r by A5,A8,ABSVALUE:4;
then -|.s2.|<=r by XXREAL_0:2;
then -|.s1.|+-|.s2.|<=(0 qua Nat)+r by A6,XREAL_1:7;
then
A10: -|.s1.|-|.s2.|+-1<r+(0 qua Nat) by XREAL_1:8;
-|.s1.|-|.s2.|-1=-(|.s1.|+|.s2.|+1);
hence thesis by A9,A10,SEQ_2:1;
end;
given s such that
0<s and
A11: for r st r in X holds |.r.|<s;
thus X is bounded_below
proof
take -s;
let r be ExtReal;
assume
A12: r in X;
then reconsider r as Real;
|.r.|<s by A11,A12;
then
A13: -s<-|.r.| by XREAL_1:24;
-|.r.|<=r by ABSVALUE:4;
hence thesis by A13,XXREAL_0:2;
end;
take s;
let r be ExtReal;
assume
A14: r in X;
then reconsider r as Real;
r<=|.r.| by ABSVALUE:4;
hence thesis by A11,A14,XXREAL_0:2;
end;
definition
let r;
redefine func {r} -> Subset of REAL; :: redefines { (TARSKI, definition)
coherence
proof
{r} c= REAL
by XREAL_0:def 1;
hence thesis;
end;
end;
theorem Th5:
for X being real-membered set holds X is non empty bounded_above
implies ex g st (for r st r in X holds r<=g) & for s st 0<s ex r st r in X & g-
s<r
proof
let X be real-membered set;
assume that
A1: X is non empty and
A2: X is bounded_above;
consider p1 such that
A3: p1 is UpperBound of X by A2;
A4: for r st r in X holds r<=p1 by A3,XXREAL_2:def 1;
defpred X[Real] means for r st r in X holds r<=$1;
consider Y such that
A5: for p be Element of REAL holds p in Y iff X[p] from SUBSET_1:sch 3;
X is Subset of REAL & for r,p st r in X & p in Y holds r<=p by A5,MEMBERED:3;
then consider g1 such that
A6: for r,p st r in X & p in Y holds r<=g1 & g1<=p by AXIOMS:1;
reconsider g1 as Real;
take g=g1;
A7: ex r1 being Real st r1 in X by A1;
A8: now
given s1 such that
A9: 0<s1 and
A10: for r st r in X holds not g-s1<r;
reconsider gs1 = g-s1 as Element of REAL by XREAL_0:def 1;
gs1 in Y by A5,A10;
then g<=g-s1 by A7,A6;
then g-(g-s1)<=g-s1-(g-s1) by XREAL_1:9;
hence contradiction by A9;
end;
p1 in REAL by XREAL_0:def 1;
then p1 in Y by A4,A5;
hence thesis by A6,A8;
end;
theorem Th6:
for X being real-membered set holds (for r st r in X holds r<=g1
) & (for s st 0<s ex r st (r in X & g1-s<r)) & (for r st r in X holds r<=g2) &
(for s st 0<s ex r st (r in X & g2-s<r)) implies g1=g2
proof
let X be real-membered set;
assume that
A1: for r st r in X holds r<=g1 and
A2: for s st 0<s ex r st r in X & g1-s<r and
A3: for r st r in X holds r<=g2 and
A4: for s st 0<s ex r st r in X & g2-s<r;
A5: now
assume g2<g1;
then ex r1 st r1 in X & g1-(g1-g2)<r1 by A2,XREAL_1:50;
hence contradiction by A3;
end;
now
assume g1<g2;
then ex r1 st r1 in X & g2-(g2-g1)<r1 by A4,XREAL_1:50;
hence contradiction by A1;
end;
hence thesis by A5,XXREAL_0:1;
end;
theorem Th7:
for X being real-membered set holds X is non empty bounded_below
implies ex g st (for r st r in X holds g<=r) & for s st 0<s ex r st r in X & r<
g+s
proof
let X be real-membered set;
assume that
A1: X is non empty and
A2: X is bounded_below;
A3: ex r1 being Real st r1 in X by A1;
consider p1 such that
A4: p1 is LowerBound of X by A2;
A5: for r st r in X holds p1<=r by A4,XXREAL_2:def 2;
reconsider X as Subset of REAL by MEMBERED:3;
defpred X[Real] means for r st r in X holds $1<=r;
consider Y such that
A6: for p be Element of REAL holds p in Y iff X[p] from SUBSET_1:sch 3;
for p,r st p in Y & r in X holds p<=r by A6;
then consider g1 such that
A7: for p,r st p in Y & r in X holds p<=g1 & g1<=r by AXIOMS:1;
reconsider g1 as Real;
take g=g1;
A8: now
given s1 such that
A9: 0<s1 and
A10: for r st r in X holds not r<g+s1;
reconsider gs1 = g+s1 as Element of REAL by XREAL_0:def 1;
gs1 in Y by A6,A10;
then g+s1<=g by A3,A7;
then g+s1-g<=g-g by XREAL_1:9;
hence contradiction by A9;
end;
p1 in REAL by XREAL_0:def 1;
then p1 in Y by A5,A6;
hence thesis by A7,A8;
end;
theorem Th8:
for X being real-membered set holds (for r st r in X holds g1<=r
) & (for s st 0<s ex r st (r in X & r<g1+s)) & (for r st r in X holds g2<=r) &
(for s st 0<s ex r st (r in X & r<g2+s)) implies g1=g2
proof
let X be real-membered set;
assume that
A1: for r st r in X holds g1<=r and
A2: for s st 0<s ex r st r in X & r<g1+s and
A3: for r st r in X holds g2<=r and
A4: for s st 0<s ex r st r in X & r<g2+s;
A5: now
assume g2<g1;
then ex r1 st r1 in X & r1<g2+(g1-g2) by A4,XREAL_1:50;
hence contradiction by A1;
end;
now
assume g1<g2;
then ex r1 st r1 in X & r1<g1+(g2-g1) by A2,XREAL_1:50;
hence contradiction by A3;
end;
hence thesis by A5,XXREAL_0:1;
end;
definition
let X be real-membered set;
assume
A1: X is non empty bounded_above;
func upper_bound X -> Real means
:Def1:
(for r st r in X holds r<=it) & for s st 0<s ex r st r in X & it-s<r;
existence by A1,Th5;
uniqueness by Th6;
end;
definition
let X be real-membered set;
assume
A1: X is non empty bounded_below;
func lower_bound X -> Real means
:Def2:
(for r st r in X holds it<=r) & for s st 0<s ex r st r in X & r<it+s;
existence by A1,Th7;
uniqueness by Th8;
end;
Lm1: for X being non empty real-membered set st (for s st s in X holds s >= r)
& for t st for s st s in X holds s >= t holds r >= t holds r = lower_bound X
proof
let X be non empty real-membered set;
assume that
A1: for s st s in X holds s >= r and
A2: for t st for s st s in X holds s >= t holds r >= t;
A3: for s being Real st 0 < s holds
not for t be Real st t in X holds t >= r+s by A2,XREAL_1:29;
X is bounded_below
proof
take r;
let s be ExtReal;
assume s in X;
hence thesis by A1;
end;
hence thesis by A1,A3,Def2;
end;
Lm2: for X being non empty real-membered set, r st (for s st s in X holds s <=
r) & for t st for s st s in X holds s <= t holds r <= t holds r = upper_bound X
proof
let X be non empty real-membered set, r;
assume that
A1: for s st s in X holds s <= r and
A2: for t st for s st s in X holds s <= t holds r <= t;
A3: now
let s be Real such that
A4: 0 < s;
assume for t be Real st t in X holds r-s >= t;
then r <= r-s by A2;
then r+s <= r by XREAL_1:19;
hence contradiction by A4,XREAL_1:29;
end;
X is bounded_above
proof
take r;
let s be ExtReal;
assume s in X;
hence thesis by A1;
end;
hence thesis by A1,A3,Def1;
end;
registration
let X be non empty bounded_below real-membered set;
identify lower_bound X with inf X;
compatibility
proof
A1: now
let t;
assume for s st s in X holds s >= t;
then for x being ExtReal st x in X holds t <= x;
then t is LowerBound of X by XXREAL_2:def 2;
hence inf X >= t by XXREAL_2:def 4;
end;
for s st s in X holds s >= inf X by XXREAL_2:3;
hence thesis by A1,Lm1;
end;
end;
registration
let X be non empty bounded_above real-membered set;
identify upper_bound X with sup X;
compatibility
proof
A1: now
let t;
assume for s st s in X holds t >= s;
then for x being ExtReal st x in X holds x <= t;
then t is UpperBound of X by XXREAL_2:def 1;
hence t >= sup X by XXREAL_2:def 3;
end;
for s st s in X holds s <= sup X by XXREAL_2:4;
hence thesis by A1,Lm2;
end;
end;
theorem Th9:
lower_bound {r} = r & upper_bound {r} = r by XXREAL_2:11,13;
theorem Th10:
lower_bound {r} = upper_bound {r}
proof
lower_bound {r}=r by XXREAL_2:13;
hence thesis by XXREAL_2:11;
end;
theorem
X is real-bounded non empty implies lower_bound X <= upper_bound X
proof
assume X is real-bounded non empty;
then reconsider X as real-bounded non empty real-membered set;
lower_bound X <= upper_bound X by XXREAL_2:40;
hence thesis;
end;
theorem
X is real-bounded non empty implies ((ex r,p st r in X & p in X & p<>r) iff
lower_bound X < upper_bound X)
proof
assume that
A1: X is real-bounded and
A2: X is non empty;
thus (ex r,p st r in X & p in X & p<>r) implies lower_bound X<upper_bound X
proof
given r,p such that
A3: r in X and
A4: p in X and
A5: p<>r;
A6: now
assume
A7: r<p;
lower_bound X<=r by A1,A3,Def2;
then
A8: lower_bound X<p by A7,XXREAL_0:2;
p<=upper_bound X by A1,A4,Def1;
hence thesis by A8,XXREAL_0:2;
end;
now
assume
A9: p<r;
lower_bound X<=p by A1,A4,Def2;
then
A10: lower_bound X<r by A9,XXREAL_0:2;
r<=upper_bound X by A1,A3,Def1;
hence thesis by A10,XXREAL_0:2;
end;
hence thesis by A5,A6,XXREAL_0:1;
end;
consider r being Element of REAL such that
A11: r in X by A2;
assume that
A12: lower_bound X<upper_bound X and
A13: for r,p st r in X & p in X holds p=r;
for x be object holds x in X iff x=r by A13,A11;
then X={r} by TARSKI:def 1;
hence contradiction by A12,Th10;
end;
::
:: Theorems about the Convergence and the Limit
::
theorem Th13:
seq is convergent implies abs seq is convergent
proof
assume seq is convergent;
then consider g1 such that
A1: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p;
reconsider g1 as Real;
take g=|.g1.|;
let p;
assume 0<p;
then consider n1 such that
A2: for m st n1<=m holds |.seq.m-g1.|<p by A1;
take n=n1;
let m;
|.g1-seq.m.|=|.-((seq.m)-g1).| .=|.seq.m-g1.| by COMPLEX1:52;
then g-|.seq.m.|<=|.seq.m-g1.| by COMPLEX1:59;
then |.seq.m.|-g<=|.seq.m-g1.| & -|.seq.m-g1.|<= -(g-|.seq.m.|) by
COMPLEX1:59,XREAL_1:24;
then |.|.seq.m.|-g.|<=|.seq.m-g1.| by ABSVALUE:5;
then
A3: |.((abs seq).m)-g.| <=|.seq.m-g1.| by SEQ_1:12;
assume n<=m;
then |.seq.m-g1.|<p by A2;
hence thesis by A3,XXREAL_0:2;
end;
registration
let seq be convergent Real_Sequence;
cluster abs seq -> convergent for Real_Sequence;
coherence by Th13;
end;
theorem
seq is convergent implies lim abs seq = |.lim seq.|
proof
assume
A1: seq is convergent;
now
let p;
assume 0<p;
then consider n1 such that
A2: for m st n1<=m holds |.(seq.m)-(lim seq).|<p by A1,SEQ_2:def 7;
take n=n1;
let m;
|.(lim seq)-seq.m.|=|.-((seq.m)-(lim seq)).|
.=|.(seq.m)-(lim seq).| by COMPLEX1:52;
then |.lim seq.|-|.seq.m.|<=|.seq.m-lim seq.| by COMPLEX1:59;
then |.seq.m.|-|.lim seq.|<=|.seq.m-lim seq.| & -|.(seq.m)-(lim
seq).|<=- (|.lim seq.|-|.seq.m.|) by COMPLEX1:59,XREAL_1:24;
then |.|.seq.m.|-|.lim seq.|.|<=|.seq.m-lim seq.| by ABSVALUE:5;
then
A3: |.((abs seq).m)-|.lim seq.|.| <=|.seq.m-lim seq.| by SEQ_1:12;
assume n<=m;
then |.seq.m-lim seq.|<p by A2;
hence |.((abs seq).m)-|.lim seq.|.|<p by A3,XXREAL_0:2;
end;
hence thesis by A1,SEQ_2:def 7;
end;
theorem
abs seq is convergent & lim abs seq=0 implies seq is convergent & lim seq=0
proof
assume that
A1: abs seq is convergent and
A2: lim abs seq=0;
A3: now
let n;
-|.seq.n.|<=seq.n by ABSVALUE:4;
then
A4: -((abs seq).n)<=seq.n by SEQ_1:12;
seq.n<=|.seq.n.| by ABSVALUE:4;
hence (-abs seq).n<=seq.n & seq.n<=(abs seq).n by A4,SEQ_1:10,12;
end;
A5: -abs seq is convergent & lim(-abs seq)=-lim abs seq by A1,SEQ_2:10;
hence seq is convergent by A1,A2,A3,SEQ_2:19;
thus thesis by A1,A2,A5,A3,SEQ_2:20;
end;
theorem Th16:
seq1 is subsequence of seq & seq is convergent implies seq1 is convergent
proof
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent;
consider g1 such that
A3: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p by A2;
take g1;
let p;
assume 0<p;
then consider n1 such that
A4: for m st n1<=m holds |.seq.m-g1.|<p by A3;
take n=n1;
let m such that
A5: n<=m;
consider Nseq such that
A6: seq1=seq*Nseq by A1,VALUED_0:def 17;
m<=Nseq.m by SEQM_3:14;
then
A7: n<=Nseq.m by A5,XXREAL_0:2;
m in NAT by ORDINAL1:def 12;
then seq1.m=seq.(Nseq.m) by A6,FUNCT_2:15;
hence thesis by A4,A7;
end;
theorem Th17:
seq1 is subsequence of seq & seq is convergent implies lim seq1= lim seq
proof
assume that
A1: seq1 is subsequence of seq and
A2: seq is convergent;
consider Nseq such that
A3: seq1=seq*Nseq by A1,VALUED_0:def 17;
A4: now
let p;
assume 0<p;
then consider n1 such that
A5: for m st n1<=m holds |.seq.m-lim seq.|<p by A2,SEQ_2:def 7;
take n=n1;
let m such that
A6: n<=m;
m<=Nseq.m by SEQM_3:14;
then
A7: n<=Nseq.m by A6,XXREAL_0:2;
m in NAT by ORDINAL1:def 12;
then seq1.m=seq.(Nseq.m) by A3,FUNCT_2:15;
hence |.(seq1.m)-(lim seq).|<p by A5,A7;
end;
seq1 is convergent by A1,A2,Th16;
hence thesis by A4,SEQ_2:def 7;
end;
theorem Th18:
seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n)
implies seq1 is convergent
proof
assume that
A1: seq is convergent and
A2: ex k st for n st k<=n holds seq1.n=seq.n;
consider g1 such that
A3: for p st 0<p ex n st for m st n<=m holds |.seq.m-g1.|<p by A1;
consider k such that
A4: for n st k<=n holds seq1.n=seq.n by A2;
take g=g1;
let p;
assume 0<p;
then consider n1 such that
A5: for m st n1<=m holds |.seq.m-g1.|<p by A3;
A6: now
assume
A7: n1<=k;
take n=k;
let m;
assume
A8: n<=m;
then n1<=m by A7,XXREAL_0:2;
then |.seq.m-g1.|<p by A5;
hence |.seq1.m-g.|<p by A4,A8;
end;
now
assume
A9: k<=n1;
take n=n1;
let m;
assume
A10: n<=m;
then seq1.m=seq.m by A4,A9,XXREAL_0:2;
hence |.seq1.m-g.|<p by A5,A10;
end;
hence thesis by A6;
end;
theorem
seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n) implies
lim seq=lim seq1
proof
assume that
A1: seq is convergent;
given k such that
A2: for n st k<=n holds seq1.n=seq.n;
A3: now
let p;
assume 0<p;
then consider n1 such that
A4: for m st n1<=m holds |.seq.m-lim seq.|<p by A1,SEQ_2:def 7;
A5: now
assume
A6: n1<=k;
take n=k;
let m;
assume
A7: n<=m;
then n1<=m by A6,XXREAL_0:2;
then |.seq.m-lim seq.|<p by A4;
hence |.(seq1.m)-(lim seq).|<p by A2,A7;
end;
now
assume
A8: k<=n1;
take n=n1;
let m;
assume
A9: n<=m;
then seq1.m=seq.m by A2,A8,XXREAL_0:2;
hence |.(seq1.m)-(lim seq).|<p by A4,A9;
end;
hence ex n st for m st n<=m holds |.seq1.m-lim seq.|<p by A5;
end;
seq1 is convergent by A1,A2,Th18;
hence thesis by A3,SEQ_2:def 7;
end;
registration
let seq be convergent Real_Sequence;
let k;
cluster seq ^\ k -> convergent for Real_Sequence;
coherence by Th16;
end;
theorem
seq is convergent implies lim (seq^\k)=lim seq by Th17;
theorem Th21:
seq^\k is convergent implies seq is convergent
proof
assume seq^\k is convergent;
then consider g1 such that
A1: for p st 0<p ex n st for m st n<=m holds |.(seq^\k).m-g1.|<p;
take g1;
let p;
assume 0<p;
then consider n1 such that
A2: for m st n1<=m holds |.(seq^\k).m-g1.|<p by A1;
take n=n1+k;
let m;
assume
A3: n<=m;
then consider l be Nat such that
A4: m=n1+k+l by NAT_1:10;
reconsider l as Element of NAT by ORDINAL1:def 12;
m-k=n1+l+k+-k by A4;
then consider m1 be Element of NAT such that
A5: m1=m-k;
now
assume not n1<=m1;
then m1+k<n1+k by XREAL_1:6;
hence contradiction by A3,A5;
end;
then
A6: |.(seq^\k).m1-g1.|<p by A2;
m1+k=m by A5;
hence thesis by A6,NAT_1:def 3;
end;
theorem
seq^\k is convergent implies lim seq = lim (seq^\k)
proof
assume
A1: seq^\k is convergent;
A2: now
let p;
assume 0<p;
then consider n1 such that
A3: for m st n1<=m holds |.(seq^\k).m-(lim (seq^\k)).|<p by A1,SEQ_2:def 7;
take n=n1+k;
let m;
assume
A4: n<=m;
then consider l be Nat such that
A5: m=n1+k+l by NAT_1:10;
reconsider l as Element of NAT by ORDINAL1:def 12;
m-k=n1+l+k+-k by A5;
then consider m1 such that
A6: m1=m-k;
now
assume not n1<=m1;
then m1+k<n1+k by XREAL_1:6;
hence contradiction by A4,A6;
end;
then
A7: |.(seq^\k).m1-(lim(seq^\k)).|<p by A3;
m1+k=m by A6;
hence |.seq.m-(lim(seq^\k)).|<p by A7,NAT_1:def 3;
end;
seq is convergent by A1,Th21;
hence thesis by A2,SEQ_2:def 7;
end;
theorem Th23:
seq is convergent & lim seq<>0 implies ex k st (seq ^\k) is non-zero
proof
assume that
A1: seq is convergent and
A2: lim seq<>0;
consider n1 such that
A3: for m st n1<=m holds |.lim seq.|/2<|.seq.m.| by A1,A2,SEQ_2:16;
take k=n1;
now
let n;
(0 qua Nat)+k<=n+k by XREAL_1:7;
then |.lim seq.|/2<|.(seq.(n+k)).| by A3;
then
A4: |.lim seq.|/2<|.((seq ^\k).n).| by NAT_1:def 3;
0<|.lim seq.| by A2,COMPLEX1:47;
then 0/2<|.lim seq.|/2;
hence (seq ^\k).n<>0 by A4,ABSVALUE:2;
end;
hence thesis by SEQ_1:5;
end;
theorem
seq is convergent & lim seq<>0 implies ex seq1 st seq1 is subsequence
of seq & seq1 is non-zero
proof
assume seq is convergent & lim seq <>0;
then consider k such that
A1: seq ^\k is non-zero by Th23;
take seq ^\k;
thus thesis by A1;
end;
theorem Th25:
seq is constant & (r in rng seq or ex n st seq.n=r ) implies lim seq=r
proof
assume
A1: seq is constant;
then consider r1 being Element of REAL such that
A2: rng seq={r1} by FUNCT_2:111;
A3: now
assume that
A4: r in rng seq;
consider r2 being Element of REAL such that
A5: for n being Nat holds seq.n=r2 by A1,VALUED_0:def 18;
A6: r=r1 by A4,A2,TARSKI:def 1;
reconsider zz=0 as Nat;
now
let p such that
A7: 0<p;
take n=zz;
let m such that
n<=m;
m in NAT by ORDINAL1:def 12;
then m in dom seq by FUNCT_2:def 1;
then seq.m in rng seq by FUNCT_1:def 3;
then r2 in rng seq by A5;
then r2=r by A2,A6,TARSKI:def 1;
then seq.m=r by A5;
hence |.(seq.m)-r.|<p by A7,ABSVALUE:2;
end;
hence thesis by A1,SEQ_2:def 7;
end;
A8: now
assume that
A9: ex n st seq.n=r;
consider n such that
A10: seq.n=r by A9;
n in NAT by ORDINAL1:def 12;
then n in dom seq by FUNCT_2:def 1;
hence thesis by A3,A10,FUNCT_1:def 3;
end;
assume r in rng seq or ex n st seq.n=r;
hence thesis by A3,A8;
end;
theorem
seq is constant implies for n holds lim seq=seq.n by Th25;
theorem
seq is convergent & lim seq<>0 implies
for seq1 st seq1 is subsequence of seq & seq1 is non-zero
holds lim (seq1")=(lim seq)"
proof
assume that
A1: seq is convergent and
A2: lim seq<>0;
let seq1 such that
A3: seq1 is subsequence of seq and
A4: seq1 is non-zero;
lim seq1=lim seq by A1,A3,Th17;
hence thesis by A1,A2,A3,A4,Th16,SEQ_2:22;
end;
::$CT 3
LmTh28:
(for n holds seq.n = 1/(n+r)) implies
for p st 0<p ex n st for m st n<=m holds |.seq.m-0.| < p
proof
assume
A0: for n holds seq.n = 1/(n+r);
let p such that
A1: 0 < p;
consider n such that
A3: n > (1/p)-r by Th3;
take n;
let m such that
A2: n <= m;
B0: seq.m = 1/(m+r) by A0;
(1/p)-r < m by A3,A2,XXREAL_0:2;
then
A4: (1/p)-r+r < m+r by XREAL_1:8;
then p" " > (m+r)" by A1,XREAL_1:88;
then
B1: 1/(m+r) < p;
B2: -p < -0 by A1;
0 <= m+r by A1,A4;
then -p < 1/(m+r) by B2;
hence thesis by B0,B1,SEQ_2:1;
end;
Th28:
(for n holds seq.n = 1/(n+r)) implies seq is convergent
proof
assume
A0: for n holds seq.n = 1/(n+r);
take 0;
let p;
assume 0<p;
then consider n such that
A2: for m st n<=m holds |.seq.m-0.| < p by A0,LmTh28;
take n;
thus thesis by A2;
end;
Th29:
(for n holds seq.n = 1/(n+r)) implies lim seq = 0
proof
assume
A1: for n holds seq.n=1/(n+r);
then
A2: seq is convergent by Th28;
for p st 0<p ex n st for m st n<=m holds |.seq.m-0.|<p by A1,LmTh28;
hence thesis by A2,SEQ_2:def 7;
end;
theorem
(for n holds seq.n=g/(n+r)) implies seq is convergent & lim seq =0
proof
assume
A2: for n holds seq.n=g/(n+r);
reconsider r1 = r as Real;
deffunc U(Nat) = 1/($1+r1);
consider seq1 such that
A3: for n holds seq1.n=U(n) from SEQ_1:sch 1;
A4: now
let n be Element of NAT;
thus (g(#)seq1).n=g*(seq1.n) by SEQ_1:9
.=g*(1/(n+r)) by A3
.=g*(1*(n+r)")
.=g/(n+r)
.=seq.n by A2;
end;
A5: g(#)seq1 is convergent by A3,Th28,SEQ_2:7;
lim (g(#)seq1)=g*(lim seq1) by A3,Th28,SEQ_2:8
.=g*(0 qua Nat) by A3,Th29
.=0;
hence thesis by A5,A4,FUNCT_2:63;
end;
::$CT 3
LmTh32:
0<=r & (for n holds seq.n=1/(n*n+r)) implies
for p st 0<p ex n st for m st n<=m holds |.seq.m-0.|<p
proof
assume that
A1: 0<=r and
A2: for n holds seq.n=1/(n*n+r);
let p;
consider k1 such that
A3: p"<k1 by Th3;
assume
A4: 0<p;
then
A5: k1>0 by A3;
then k1>=1+(0 qua Nat) by NAT_1:13;
then k1<=k1*k1 by XREAL_1:151;
then
A6: k1+r<=k1*k1+r by XREAL_1:6;
take n=k1;
let m such that
A7: n<=m;
n*n<=m*m by A7,XREAL_1:66;
then
A8: n*n+r<=m*m+r by XREAL_1:6;
p"+(0 qua Nat)<k1+r by A1,A3,XREAL_1:8;
then p"+(0 qua Nat)<k1*k1+r by A6,XXREAL_0:2;
then 1/(k1*k1+r)<1/p" by A4,XREAL_1:76;
then
A9: 1/(k1*k1+r)<1*p" ";
0<n^2 by A5;
then 1/(m*m+r)<=1/(n*n+r) by A1,A8,XREAL_1:118;
then
A10: 1/(m*m+r)<p by A9,XXREAL_0:2;
seq.m=1/(m*m+r) by A2;
hence thesis by A1,A10,ABSVALUE:def 1;
end;
Th32:
0<=r & (for n holds seq.n=1/(n*n+r)) implies seq is convergent
proof
assume that
A1: 0<=r and
A2: for n holds seq.n=1/(n*n+r);
take 0;
let p;
assume 0<p;
then consider n such that
A3: for m st n<=m holds |.seq.m-0.| < p by A1,A2,LmTh32;
take n;
thus thesis by A3;
end;
Th33:
0<=r & (for n holds seq.n=1/(n*n+r)) implies lim seq=0
proof
assume that
A1: 0<=r and
A2: for n holds seq.n=1/(n*n+r);
A3: seq is convergent by A1,A2,Th32;
for p st 0<p ex n st for m st n<=m holds |.seq.m-0.|<p by A1,A2,LmTh32;
hence thesis by A3,SEQ_2:def 7;
end;
theorem
0<=r & (for n holds seq.n=g/(n*n+r)) implies seq is convergent & lim seq=0
proof
assume that
A1: 0<=r and
A2: for n holds seq.n=g/(n*n+r);
reconsider r1 = r as Real;
deffunc U(Nat) = 1/($1*$1+r1);
consider seq1 such that
A3: for n holds seq1.n=U(n) from SEQ_1:sch 1;
A4: now
let n be Element of NAT;
thus (g(#)seq1).n=g*(seq1.n) by SEQ_1:9
.=g*(1/(n*n+r)) by A3
.=g*(1*(n*n+r)")
.=g/(n*n+r)
.=seq.n by A2;
end;
A5: g(#)seq1 is convergent by A1,A3,Th32,SEQ_2:7;
lim (g(#)seq1)=g*(lim seq1) by A1,A3,Th32,SEQ_2:8
.=g*(0 qua Nat) by A1,A3,Th33
.=0;
hence thesis by A5,A4,FUNCT_2:63;
end;
registration
cluster non-decreasing bounded_above -> convergent for Real_Sequence;
coherence
proof
let seq be Real_Sequence;
assume that
A1: seq is non-decreasing and
A2: seq is bounded_above;
consider r2 such that
A3: for n holds seq.n<r2 by A2;
defpred X[Real] means ex n st $1=seq.n;
consider X such that
A4: for p be Element of REAL holds p in X iff X[p] from SUBSET_1:sch 3;
A5: now
take r=r2;
let p;
assume p in X;
then ex n1 st p=seq.n1 by A4;
hence p<=r by A3;
end;
A6: (ex r st for p being Real st p in X holds p<=r)
implies X is bounded_above
proof
given r such that
A7: for p being Real st p in X holds p<=r;
take r; let p be ExtReal;
thus thesis by A7;
end;
take g=upper_bound X;
let s;
assume
A8: 0<s;
seq.0 in X by A4;
then consider p1 such that
A9: p1 in X and
A10: upper_bound X-s<p1 by A6,A8,Def1;
consider n1 such that
A11: p1=seq.n1 by A4,A9;
take n=n1;
let m;
assume n<=m;
then seq.n<=seq.m by A1,SEQM_3:6;
then g+ -s<seq.m by A10,A11,XXREAL_0:2;
then
A12: -s<seq.m -g by XREAL_1:20;
seq.m in X by A4;
then seq.m<=g by A6,A5,Def1;
then seq.m +(0 qua Nat)<g+s by A8,XREAL_1:8;
then seq.m -g<s by XREAL_1:19;
hence thesis by A12,SEQ_2:1;
end;
end;
registration
cluster non-increasing bounded_below -> convergent for Real_Sequence;
coherence
proof
let seq be Real_Sequence;
assume that
A1: seq is non-increasing and
A2: seq is bounded_below;
defpred X[Real] means ex n st $1=seq.n;
consider X such that
A3: for p be Element of REAL holds p in X iff X[p] from SUBSET_1:sch 3;
take g=lower_bound X;
let s;
assume
A4: 0<s;
A5: (ex r st for p being Real st p in X holds r<=p)
implies X is bounded_below
proof
given r such that
A6: for p being Real st p in X holds r<=p;
take r; let p be ExtReal;
thus thesis by A6;
end;
seq.0 in X by A3;
then consider p1 such that
A7: p1 in X and
A8: p1<lower_bound X+s by A5,A4,Def2;
consider n1 such that
A9: p1=seq.n1 by A3,A7;
take n=n1;
let m;
consider r1 such that
A10: for n holds r1< seq.n by A2;
A11: now
take r=r1;
let p;
assume p in X;
then ex n1 st p=seq.n1 by A3;
hence r<=p by A10;
end;
seq.m in X by A3;
then (0 qua Nat)+g<=seq.m by A5,A11,Def2;
then
A12: 0<=seq.m-g by XREAL_1:19;
assume n<=m;
then seq.m<=seq.n by A1,SEQM_3:8;
then seq.m <g+s by A8,A9,XXREAL_0:2;
then
A13: seq.m -g<s by XREAL_1:19;
-s<-(0 qua Nat) by A4;
hence thesis by A13,A12,SEQ_2:1;
end;
end;
registration
cluster monotone bounded -> convergent for Real_Sequence;
coherence
proof
let seq be Real_Sequence;
assume that
A1: seq is monotone and
A2: seq is bounded;
A3: seq is non-increasing implies thesis by A2;
seq is non-decreasing implies thesis by A2;
hence thesis by A1,A3,SEQM_3:def 5;
end;
end;
theorem Th36:
seq is monotone & seq is bounded implies seq is convergent;
theorem
seq is bounded_above & seq is non-decreasing implies for n holds seq.n
<=lim seq
proof
assume that
A1: seq is bounded_above and
A2: seq is non-decreasing;
let m;
set seq1 = NAT --> seq.m;
deffunc U(Nat) = seq.($1+m);
consider seq2 such that
A3: for n holds seq2.n=U(n) from SEQ_1:sch 1;
A4: now
let n;
n in NAT by ORDINAL1:def 12;
then seq1.n=seq.m & seq2.n=seq.(m+n) by A3,FUNCOP_1:7;
hence seq1.n<=seq2.n by A2,SEQM_3:5;
end;
seq1.0=seq.m;
then
A5: lim seq1=seq.m by Th25;
for n being Nat holds seq2.n=U(n) by A3;
then
A6: seq2=seq^\m by NAT_1:def 3;
then lim seq2=lim seq by A1,A2,Th17;
hence thesis by A1,A2,A5,A6,A4,SEQ_2:18;
end;
theorem
seq is bounded_below & seq is non-increasing implies for n holds lim
seq <= seq.n
proof
assume that
A1: seq is bounded_below and
A2: seq is non-increasing;
let m;
set seq1 = NAT --> seq.m;
deffunc U(Nat) = seq.($1+m);
consider seq2 such that
A3: for n holds seq2.n=U(n) from SEQ_1:sch 1;
A4: now
let n;
n in NAT by ORDINAL1:def 12;
then seq1.n=seq.m & seq2.n=seq.(m+n) by A3,FUNCOP_1:7;
hence seq2.n<=seq1.n by A2,SEQM_3:7;
end;
seq1.0=seq.m;
then
A5: lim seq1=seq.m by Th25;
for n being Nat holds seq2.n=U(n) by A3;
then
A6: seq2=seq^\m by NAT_1:def 3;
then lim seq2=lim seq by A1,A2,Th17;
hence thesis by A1,A2,A5,A6,A4,SEQ_2:18;
end;
theorem Th39:
for seq ex Nseq st seq*Nseq is monotone
proof
let seq;
defpred X[Nat] means for m st $1<m holds seq.$1<seq.m;
consider XN being Subset of NAT such that
A1: for n being Element of NAT holds n in XN iff X[n] from SUBSET_1:sch 3;
A2: now
given k1 such that
A3: for n st n in XN holds n<=k1;
set seq1=seq ^\(1+k1);
defpred P[set,set,set] means for k,l st k=$2 & l=$3 holds k<l & seq1.l<=
seq1.k & for m st k<m & seq1.m<=seq1.k holds l<=m;
A4: now
let k;
A5: k in NAT by ORDINAL1:def 12;
assume k1<k;
then not k in XN by A3;
then consider m such that
A6: k<m and
A7: not seq.k<seq.m by A1,A5;
take n=m;
thus k<n by A6;
thus seq.n<=seq.k by A7;
end;
A8: now
let k;
(0 qua Nat)+k1<k+1+k1 by XREAL_1:8;
then consider n such that
A9: k+1+k1<n and
A10: seq.n<=seq.(k+1+k1) by A4;
consider m be Nat such that
A11: n=k+1+k1+m by A9,NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
n-(1+k1)=k+(0 qua Nat)+m by A11;
then consider n1 be Element of NAT such that
A12: n1=n-(1+k1);
seq.n<=seq.(k+(1+k1)) by A10;
then
A13: seq.n<=seq1.k by NAT_1:def 3;
take l=n1;
now
assume not k<l;
then n-(1+k1)+(1+k1)<=k+(1+k1) by A12,XREAL_1:6;
hence contradiction by A9;
end;
hence k<l;
n=l+(1+k1) by A12;
hence seq1.l<=seq1.k by A13,NAT_1:def 3;
end;
A14: for n being Nat for x being Element of NAT ex y being
Element of NAT st P[n,x,y]
proof
let n be Nat,x be Element of NAT;
defpred X[Nat] means x<$1 & seq1.$1<=seq1.x;
ex n be Element of NAT st X[n] by A8;
then
A15: ex n be Nat st X[n];
ex l be Nat st X[l] & for m be Nat st X[m] holds l <= m from NAT_1:
sch 5(A15);
then consider l be Nat such that
A16: x<l & seq1.l<=seq1.x & for m be Nat st x<m & seq1.m<=seq1.x holds l <= m;
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A16;
end;
consider f being sequence of NAT such that
f.0 = 0 and
A17: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:
sch 2 (A14);
A18: dom f =NAT by FUNCT_2:def 1;
rng f c= REAL;
then reconsider f as Real_Sequence by A18,RELSET_1:4;
for n holds f.n<f.(n+1) by A17;
then reconsider f as increasing sequence of NAT by SEQM_3:def 6;
consider Nseq such that
A19: seq1=seq*Nseq by VALUED_0:def 17;
reconsider Nseq1=Nseq*f as increasing sequence of NAT;
take Nseq1;
now
let n;
A20: n in NAT & n+1 in NAT by ORDINAL1:def 12;
seq1.(f.(n+1))<=seq1.(f.n) by A17;
then (seq1*f).(n+1)<=seq1.(f.n) by FUNCT_2:15;
then (seq*Nseq*f).(n+1)<=(seq1*f).n by A19,FUNCT_2:15,A20;
then (seq*Nseq1).(n+1)<=(seq*Nseq*f).n by A19,RELAT_1:36;
hence (seq*Nseq1).(n+1)<=(seq*Nseq1).n by RELAT_1:36;
end;
then seq*Nseq1 is non-increasing;
hence seq*Nseq1 is monotone by SEQM_3:def 5;
end;
now
defpred P[set,set,set] means for k,l being Element of NAT st k=$2 & l=$3
holds l in XN & k<l & for m st m in XN & k<m holds l<=m;
assume
A21: for l ex n st n in XN & not n<=l;
then consider n1 such that
A22: n1 in XN and
not n1<=0;
reconsider O9=n1 as Element of NAT by ORDINAL1:def 12;
A23: for n being Nat for x being Element of NAT ex y being
Element of NAT st P[n,x,y]
proof
let n be Nat,x be Element of NAT;
defpred X[Nat] means $1 in XN & x<$1;
ex n be Nat st X[n] by A21;
then ex n be Element of NAT st X[n];
then
A24: ex n be Nat st X[n];
ex l be Nat st X[l] & for m be Nat st X[m] holds l <= m from NAT_1:
sch 5(A24);
then consider l be Nat such that
A25: l in XN & x<l & for m be Nat st m in XN & x<m holds l <= m;
reconsider l as Element of NAT by ORDINAL1:def 12;
take l;
thus thesis by A25;
end;
consider f being sequence of NAT such that
A26: f.0 = O9 and
A27: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:
sch 2 (A23);
A28: dom f =NAT by FUNCT_2:def 1;
rng f c= REAL;
then reconsider f as Real_Sequence by A28,RELSET_1:4;
A29: for n holds n is Element of NAT & f.n is Element of NAT
by ORDINAL1:def 12;
A30: now
let n;
f.n is Element of NAT & f.(n+1) is Element of NAT by A29;
hence f.n<f.(n+1) by A27;
end;
A31: now
defpred X[Nat] means f.$1 in XN;
let n;
A32: now
let k such that
X[k];
f.k is Element of NAT & f.(k+1) is Element of NAT by A29;
hence X[k+1] by A27;
end;
A33: X[0] by A22,A26;
thus for n holds X[n] from NAT_1:sch 2(A33,A32);
end;
reconsider f as increasing sequence of NAT by A30,SEQM_3:def 6;
take Nseq=f;
now
let n;
A34: n in NAT by ORDINAL1:def 12;
Nseq.n in XN & Nseq.n<Nseq.(n+1) by A31,A30;
then seq.(Nseq.n)<seq.(Nseq.(n+1)) by A1;
then (seq*Nseq).n<seq.(Nseq.(n+1)) by FUNCT_2:15,A34;
hence (seq*Nseq).n<(seq*Nseq).(n+1) by FUNCT_2:15;
end;
then seq*Nseq is increasing;
hence seq*Nseq is monotone by SEQM_3:def 5;
end;
hence thesis by A2;
end;
::$N Bolzano-Weierstrass Theorem (1 dimension)
theorem Th40:
seq is bounded implies ex seq1 st seq1 is subsequence of seq &
seq1 is convergent
proof
assume
A1: seq is bounded;
consider Nseq such that
A2: seq*Nseq is monotone by Th39;
take seq1=seq*Nseq;
thus seq1 is subsequence of seq;
thus thesis by A1,A2,Th36,SEQM_3:29;
end;
::$N Cauchy sequence
theorem :: Cauchy Theorem
seq is convergent iff for s st 0<s ex n st for m st n<=m
holds |.seq.m -seq.n.|<s
proof
thus seq is convergent implies for s st 0<s ex n st for m st n<=m
holds |.seq.m -seq.n.|<s
proof
assume seq is convergent;
then consider g1 such that
A1: for s st 0<s ex n st for m st n<=m holds |.seq.m -g1.|<s;
let s;
assume 0<s;
then consider n1 such that
A2: for m st n1<=m holds |.seq.m -g1.|<s/2 by A1;
take n=n1;
let m;
assume n<=m;
then
A3: |.seq.m-g1.|<s/2 by A2;
A4: |.seq.m -g1+(g1-seq.n).|<=|.seq.m-g1.|+|.g1-seq.n.| by COMPLEX1:56;
|.seq.n -g1.|<s/2 by A2;
then |.-(g1-seq.n).|<s/2;
then |.g1-seq.n.|<s/2 by COMPLEX1:52;
then |.seq.m-g1.|+|.g1-seq.n.|<s/2+s/2 by A3,XREAL_1:8;
hence thesis by A4,XXREAL_0:2;
end;
assume
A5: for s st 0<s ex n st for m st n<=m holds |.seq.m -seq.n.|<s;
then consider n1 such that
A6: for m st n1<=m holds |.seq.m -seq.n1.|<1;
consider r1 such that
A7: 0<r1 and
A8: for m st m<=n1 holds |.seq.m.|<r1 by SEQ_2:4;
now
take r=r1+|.seq.n1.|+1;
(0 qua Nat)+(0 qua Nat)<r1+|.seq.n1.| by A7,COMPLEX1:46,XREAL_1:8;
hence 0<r;
let m;
A9: now
assume n1<=m;
then
A10: |.seq.m -seq.n1.|<1 by A6;
|.seq.m.|-|.seq.n1.|<=|.seq.m -seq.n1.| by COMPLEX1:59;
then |.seq.m.|-|.seq.n1.|<1 by A10,XXREAL_0:2;
then |.seq.m.|-|.seq.n1.|+|.seq.n1.|<1+|.seq.n1.| by XREAL_1:6;
then (0 qua Nat)+|.seq.m.|<r1+(|.seq.n1.|+1) by A7,XREAL_1:8;
hence |.seq.m.|<r;
end;
now
assume m<=n1;
then |.seq.m.|<r1 by A8;
then |.seq.m.|+(0 qua Nat)<r1+|.seq.n1.| by COMPLEX1:46,XREAL_1:8;
hence |.seq.m.|<r by XREAL_1:8;
end;
hence |.seq.m.|<r by A9;
end;
then seq is bounded by SEQ_2:3;
then consider seq1 such that
A11: seq1 is subsequence of seq and
A12: seq1 is convergent by Th40;
consider g1 such that
A13: for s st 0<s ex n st for m st n<=m holds |.seq1.m-g1.|<s by A12;
take g1;
let s;
assume
A14: 0<s;
then consider n1 such that
A15: for m st n1<=m holds |.seq1.m-g1.|<s/3 by A13;
consider n2 such that
A16: for m st n2<=m holds |.seq.m -seq.n2.|<s/3 by A5,A14;
take n=n1+n2;
let m such that
A17: n<=m;
consider Nseq such that
A18: seq1=seq*Nseq by A11,VALUED_0:def 17;
A19: m in NAT by ORDINAL1:def 12;
n1<=n by NAT_1:12;
then n1<=m by A17,XXREAL_0:2;
then |.(seq*Nseq).m -g1.|<s/3 by A18,A15;
then
A20: |.seq.(Nseq.m) -g1.|<s/3 by FUNCT_2:15,A19;
n2<=n by NAT_1:12; then
A21: n2<=m by A17,XXREAL_0:2;
m<=Nseq.m by SEQM_3:14;
then n2<=Nseq.m by A21,XXREAL_0:2;
then |.seq.(Nseq.m) -seq.n2.|<s/3 by A16;
then |.-(seq.n2-seq.(Nseq.m)).|<s/3;
then
A22: |.seq.n2-seq.(Nseq.m).|<s/3 by COMPLEX1:52;
|.seq.m -seq.n2.|<s/3 by A16,A21;
then
A23: |.seq.m -seq.n2.|+|.seq.n2-seq.(Nseq.m).|<s/3+s/3 by A22,XREAL_1:8;
|.seq.m -seq.n2+(seq.n2-seq.(Nseq.m)).|<=
|.seq.m -seq.n2.|+|.seq.n2-seq.(Nseq.m).| by COMPLEX1:56;
then |.seq.m -seq.(Nseq.m).|<s/3+s/3 by A23,XXREAL_0:2;
then
A24: |.seq.m -seq.(Nseq.m).|+|.seq.(Nseq.m) -g1.|<s/3+s/3+s/3 by A20,
XREAL_1:8;
|.seq.m -seq.(Nseq.m)+(seq.(Nseq.m) -g1).|<= |.seq.m -seq.(Nseq.m).|+
|.seq.(Nseq.m) -g1.| by COMPLEX1:56;
hence thesis by A24,XXREAL_0:2;
end;
theorem
seq is constant & seq1 is convergent implies lim (seq+seq1) =(seq.0) +
lim seq1 & lim (seq-seq1) =(seq.0) - lim seq1 & lim (seq1-seq) =(lim seq1) -seq
.0 & lim (seq(#)seq1) =(seq.0) * (lim seq1)
proof
assume that
A1: seq is constant and
A2: seq1 is convergent;
thus lim (seq+seq1)=(lim seq)+(lim seq1) by A1,A2,SEQ_2:6
.=(seq.0)+(lim seq1) by A1,Th25;
thus lim (seq-seq1)=(lim seq)-(lim seq1) by A1,A2,SEQ_2:12
.=(seq.0)-(lim seq1) by A1,Th25;
thus lim (seq1-seq)=(lim seq1)-(lim seq) by A1,A2,SEQ_2:12
.=(lim seq1)-(seq.0) by A1,Th25;
thus lim (seq(#)seq1)=(lim seq)*(lim seq1) by A1,A2,SEQ_2:15
.=(seq.0)*(lim seq1) by A1,Th25;
end;
begin :: Addenda
:: from PSCOMP_1
theorem Th43:
for X being non empty real-membered set for t st for s st s in X
holds s >= t holds lower_bound X >= t
proof
let X be non empty real-membered set;
set r = lower_bound X;
let t;
assume
A1: for s st s in X holds s >= t;
set s = t-r;
assume r < t; then
A2: s > 0 by XREAL_1:50;
X is bounded_below proof take t; let s be ExtReal;
thus thesis by A1;
end;
then ex t9 be Real st t9 in X & t9 < r+s by A2,Def2;
hence contradiction by A1;
end;
theorem Th44:
for X being non empty real-membered set st (for s st s in X holds s >=
r) & for t st for s st s in X holds s >= t holds r >= t holds r = lower_bound X
by Lm1;
theorem Th45:
for X being non empty real-membered set, r for t st for s st s
in X holds s <= t holds upper_bound X <= t
proof
let X be non empty real-membered set, r;
set r = upper_bound X;
let t;
assume
A1: for s st s in X holds s <= t;
set s = r-t;
assume r > t; then
A2: s > 0 by XREAL_1:50;
X is bounded_above proof take t;
let s be ExtReal;
thus thesis by A1;
end;
then ex t9 be Real st t9 in X & r-s < t9 by A2,Def1;
hence contradiction by A1;
end;
theorem Th46:
for X being non empty real-membered set, r st (for s st s in X holds s
<= r) & for t st for s st s in X holds s <= t holds r <= t holds r =
upper_bound X by Lm2;
theorem
for X being non empty real-membered set, Y being real-membered set st
X c= Y & Y is bounded_below holds lower_bound Y <= lower_bound X
proof
let X be non empty real-membered set, Y be real-membered set;
assume X c= Y & Y is bounded_below;
then t in X implies t >= lower_bound Y by Def2;
hence thesis by Th43;
end;
theorem
for X being non empty real-membered set, Y being real-membered set st
X c= Y & Y is bounded_above holds upper_bound X <= upper_bound Y
proof
let X be non empty real-membered set, Y be real-membered set;
assume X c= Y & Y is bounded_above;
then t in X implies t <= upper_bound Y by Def1;
hence thesis by Th45;
end;
:: from CQC_SIM1, 2007.03.15, A.T.
definition
let A be non empty natural-membered set;
redefine func min A -> Element of NAT; :: redefines min (XXREAL_2, redefinition) → min (XXREAL_2, synonym) → inf (XXREAL_2, definition)
coherence by ORDINAL1:def 12;
end;
begin :: moved from COMPLSP1, 2010.02.25
reserve k,n for Nat,
r,r9,r1,r2 for Real,
c,c9,c1,c2,c3 for Element of COMPLEX;
theorem
0c is_a_unity_wrt addcomplex by BINOP_2:1,SETWISEO:14;
theorem Th50:
compcomplex is_an_inverseOp_wrt addcomplex
proof
let c;
thus addcomplex.(c,compcomplex.c) = c+compcomplex.c by BINOP_2:def 3
.= c+-c by BINOP_2:def 1
.= the_unity_wrt addcomplex by BINOP_2:1;
thus addcomplex.(compcomplex.c,c) = compcomplex.c+c by BINOP_2:def 3
.= -c+c by BINOP_2:def 1
.= the_unity_wrt addcomplex by BINOP_2:1;
end;
theorem Th51:
addcomplex is having_an_inverseOp by Th50;
theorem Th52:
the_inverseOp_wrt addcomplex = compcomplex by Th50,Th51,FINSEQOP:def 3;
definition
redefine func diffcomplex equals :: redefines diffcomplex (BINOP_2, definition)
addcomplex*(id COMPLEX,compcomplex);
compatibility
proof
let b be BinOp of COMPLEX;
now
let c1,c2;
thus diffcomplex.(c1,c2) = c1 - c2 by BINOP_2:def 4
.= c1 + - c2
.= addcomplex.(c1,- c2) by BINOP_2:def 3
.= addcomplex.(c1,compcomplex.c2) by BINOP_2:def 1
.= (addcomplex*(id COMPLEX,compcomplex)).(c1,c2) by FINSEQOP:82;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem
1r is_a_unity_wrt multcomplex by BINOP_2:6,SETWISEO:14;
theorem Th54:
multcomplex is_distributive_wrt addcomplex
proof
now
let c1,c2,c3;
thus multcomplex.(c1,addcomplex.(c2,c3)) = multcomplex.(c1,c2+c3) by
BINOP_2:def 3
.= c1*(c2+c3) by BINOP_2:def 5
.= c1*c2+c1*c3
.= addcomplex.(c1*c2,c1*c3) by BINOP_2:def 3
.= addcomplex.(multcomplex.(c1,c2),c1*c3) by BINOP_2:def 5
.= addcomplex.(multcomplex.(c1,c2),multcomplex.(c1,c3)) by BINOP_2:def 5;
thus multcomplex.(addcomplex.(c1,c2),c3) = multcomplex.(c1+c2,c3) by
BINOP_2:def 3
.= (c1+c2)*c3 by BINOP_2:def 5
.= c1*c3+c2*c3
.= addcomplex.(c1*c3,c2*c3) by BINOP_2:def 3
.= addcomplex.(multcomplex.(c1,c3),c2*c3) by BINOP_2:def 5
.= addcomplex.(multcomplex.(c1,c3),multcomplex.(c2,c3)) by BINOP_2:def 5;
end;
hence thesis by BINOP_1:11;
end;
definition let c be Complex;
func c multcomplex -> UnOp of COMPLEX equals
multcomplex[;](c,id COMPLEX);
coherence
proof
reconsider c9 = c as Element of COMPLEX by XCMPLX_0:def 2;
multcomplex[;](c9,id COMPLEX) is UnOp of COMPLEX;
hence thesis;
end;
end;
Lm3:(multcomplex[;](c,id COMPLEX)).c9 = c*c9
proof
thus (multcomplex[;](c,id COMPLEX)).c9 = multcomplex.(c,(id COMPLEX).c9) by
FUNCOP_1:53
.= multcomplex.(c,c9)
.= c*c9 by BINOP_2:def 5;
end;
theorem
(c multcomplex).c9 = c*c9 by Lm3;
theorem
c multcomplex is_distributive_wrt addcomplex by Th54,FINSEQOP:54;
definition
func abscomplex -> Function of COMPLEX,REAL means :Def5:
for c holds it.c = |.c.|;
existence
proof
deffunc F(Element of COMPLEX) = In(|.$1.|,REAL);
consider F being Function of COMPLEX,REAL such that
A1: for c holds F.c = F(c) from FUNCT_2:sch 4;
take F;
let c;
thus F.c = F(c) by A1
.= |.c.|;
end;
uniqueness from BINOP_2:sch 1;
end;
reserve z,z1,z2 for FinSequence of COMPLEX;
definition let z1,z2;
redefine func z1 + z2 -> FinSequence of COMPLEX equals :: redefines + (VALUED_1, definition)
addcomplex.:(z1,z2);
coherence
proof
thus rng (z1+z2) c= COMPLEX;
end;
compatibility
proof
set g = addcomplex.:(z1,z2);
dom addcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1;
then [:rng z1, rng z2:] c= dom addcomplex by ZFMISC_1:96;
then
A1: dom(z1+z2) = dom z1 /\ dom z2 & dom g = dom z1 /\ dom z2 by FUNCOP_1:69
,VALUED_1:def 1;
now
let x be object;
assume
A2: x in dom (z1+z2);
hence (z1+z2).x = z1.x + z2.x by VALUED_1:def 1
.= addcomplex.(z1.x,z2.x) by BINOP_2:def 3
.= g.x by A1,A2,FUNCOP_1:22;
end;
hence thesis by A1,FUNCT_1:2;
end;
redefine func z1 - z2 -> FinSequence of COMPLEX equals :: redefines - (VALUED_1, definition)
diffcomplex.:(z1,z2);
coherence
proof
thus rng (z1-z2) c= COMPLEX;
end;
compatibility
proof
set g = diffcomplex.:(z1,z2);
dom diffcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1;
then [:rng z1, rng z2:] c= dom diffcomplex by ZFMISC_1:96;
then
A3: dom g = dom z1 /\ dom z2 by FUNCOP_1:69;
A4: dom(z1-z2) = dom z1 /\ dom z2 by VALUED_1:12;
now
let x be object;
assume
A5: x in dom (z1-z2);
hence (z1-z2).x = z1.x - z2.x by VALUED_1:13
.= diffcomplex.(z1.x,z2.x) by BINOP_2:def 4
.= g.x by A4,A3,A5,FUNCOP_1:22;
end;
hence thesis by A3,FUNCT_1:2,VALUED_1:12;
end;
end;
definition let z;
redefine func -z -> FinSequence of COMPLEX equals :: redefines - (VALUED_1, definition)
compcomplex*z;
coherence
proof
thus rng -z c= COMPLEX;
end;
compatibility
proof
set g = compcomplex*z;
dom compcomplex = COMPLEX by FUNCT_2:def 1;
then rng z c= dom compcomplex;
then
A1: dom g = dom z by RELAT_1:27;
A2: dom -z = dom z by VALUED_1:8;
now
let x be object;
assume
A3: x in dom -z;
thus (-z).x = -z.x by VALUED_1:8
.= compcomplex.(z.x) by BINOP_2:def 1
.= g.x by A2,A1,A3,FUNCT_1:12;
end;
hence thesis by A1,FUNCT_1:2,VALUED_1:8;
end;
end;
notation let z;
let c be Complex;
synonym c*z for c(#)z;
end;
definition let z;
let c be Complex;
redefine func c*z -> FinSequence of COMPLEX equals :: redefines * (SEQ_4, synonym) → (#) (VALUED_1, definition)
(c multcomplex)*z;
coherence
proof
thus rng (c(#)z) c= COMPLEX;
end;
compatibility
proof
set g = (c multcomplex)*z;
dom (c multcomplex) = COMPLEX by FUNCT_2:def 1;
then rng z c= dom (c multcomplex);
then
A1: dom (c(#)z) = dom z & dom g = dom z by RELAT_1:27,VALUED_1:def 5;
now
let x be object;
assume
A2: x in dom (c(#)z);
A3: c is Element of COMPLEX & z.x is Element of COMPLEX by XCMPLX_0:def 2;
thus (c(#)z).x = c*z.x by VALUED_1:6
.= (c multcomplex).(z.x) by A3,Lm3
.= g.x by A1,A2,FUNCT_1:12;
end;
hence thesis by A1,FUNCT_1:2;
end;
end;
definition let z;
redefine func abs z -> FinSequence of REAL equals :: redefines abs (VALUED_1, synonym) → |. (VALUED_1, definition)
abscomplex*z;
coherence
proof
thus rng abs z c= REAL;
end;
compatibility
proof
set g = abscomplex*z;
dom abscomplex = COMPLEX by FUNCT_2:def 1;
then rng z c= dom abscomplex;
then
A1: dom abs z = dom z & dom g = dom z by RELAT_1:27,VALUED_1:def 11;
now
let x be object;
assume
A2: x in dom abs z;
A3: z.x is Element of COMPLEX by XCMPLX_0:def 2;
thus (abs z).x = |.z.x.| by VALUED_1:18
.= abscomplex.(z.x) by A3,Def5
.= g.x by A1,A2,FUNCT_1:12;
end;
hence thesis by A1,FUNCT_1:2;
end;
end;
definition let n;
func COMPLEX n -> FinSequenceSet of COMPLEX equals
n-tuples_on COMPLEX;
correctness;
end;
registration let n;
cluster COMPLEX n -> non empty;
coherence;
end;
reserve x,z,z1,z2,z3 for Element of COMPLEX n,
A,B for Subset of COMPLEX n;
Lm4: dom z = Seg n
proof
len z = n by CARD_1:def 7;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th57:
k in Seg n implies z.k in COMPLEX
proof
len z = n by CARD_1:def 7;
then Seg n = dom z by FINSEQ_1:def 3;
hence thesis by FINSEQ_2:11;
end;
definition let n,z1,z2;
redefine func z1 + z2 -> Element of COMPLEX n; :: redefines + (VALUED_1, definition)
coherence by FINSEQ_2:120;
end;
theorem Th58:
k in Seg n & c1 = z1.k & c2 = z2.k implies (z1 + z2).k = c1 + c2
proof
assume that
A1: k in Seg n and
A2: c1 = z1.k & c2 = z2.k;
k in dom(z1+z2) by A1,Lm4;
hence (z1 + z2).k = addcomplex.(c1,c2) by A2,FUNCOP_1:22
.= c1 + c2 by BINOP_2:def 3;
end;
definition let n;
func 0c n -> FinSequence of COMPLEX equals
n |-> 0c;
correctness;
end;
definition let n;
redefine func 0c n -> Element of COMPLEX n; :: redefines 0c (SEQ_4, definition)
coherence;
end;
theorem
z + 0c n = z & z = 0c n + z by BINOP_2:1,FINSEQOP:56;
definition let n,z;
redefine func -z -> Element of COMPLEX n; :: redefines - (VALUED_1, definition)
coherence by FINSEQ_2:113;
end;
theorem Th60:
k in Seg n & c = z.k implies (-z).k = -c
proof
assume that
A1: k in Seg n and
A2: c = z.k;
k in dom(-z) by A1,Lm4;
hence (-z).k = compcomplex.c by A2,FUNCT_1:12
.= -c by BINOP_2:def 1;
end;
Lm5: -0c n = 0c n
proof
thus -0c n = n|->(compcomplex.0c) by FINSEQOP:16
.= n|->-(0c qua Complex) by BINOP_2:def 1
.= 0c n;
end;
theorem
z + -z = 0c n & -z + z = 0c n by Th51,Th52,BINOP_2:1,FINSEQOP:73;
theorem
z1 + z2 = 0c n implies z1 = -z2 & z2 = -z1 by Th51,Th52,BINOP_2:1,FINSEQOP:74
;
::$CT
theorem
-z1 = -z2 implies z1 = z2
proof
assume -z1 = -z2;
hence z1 = -(-z2) .= z2;
end;
Lm6: z1 + z = z2 + z implies z1 = z2
proof
assume z1 + z = z2 + z;
then z1 + (z + -z)= (z2 + z) + -z by FINSEQOP:28;
then
A1: z1 + (z + -z)= z2 + (z + -z) by FINSEQOP:28;
z + -z = 0c n by Th51,Th52,BINOP_2:1,FINSEQOP:73;
then z1 = z2 + 0c n by A1,BINOP_2:1,FINSEQOP:56;
hence thesis by BINOP_2:1,FINSEQOP:56;
end;
theorem
z1 + z = z2 + z or z1 + z = z + z2 implies z1 = z2 by Lm6;
theorem Th65:
-(z1 + z2) = -z1 + -z2
proof
(z1 + z2) + (-z1 + -z2) = z2 + z1 + -z1 + -z2 by FINSEQOP:28
.= z2 + (z1 + -z1) + -z2 by FINSEQOP:28
.= z2 + 0c n + -z2 by Th51,Th52,BINOP_2:1,FINSEQOP:73
.= z2 + -z2 by BINOP_2:1,FINSEQOP:56
.= 0c n by Th51,Th52,BINOP_2:1,FINSEQOP:73;
hence thesis by Th51,Th52,BINOP_2:1,FINSEQOP:74;
end;
definition let n,z1,z2;
redefine func z1 - z2 -> Element of COMPLEX n; :: redefines - (VALUED_1, definition)
coherence by FINSEQ_2:120;
end;
theorem
k in Seg n implies (z1 - z2).k = z1.k - z2.k
proof
assume that
A1: k in Seg n;
set c1 = z1.k, c2 = z2.k;
k in dom(z1 - z2) by A1,Lm4;
hence (z1 - z2).k = diffcomplex.(c1,c2) by FUNCOP_1:22
.= c1 - c2 by BINOP_2:def 4;
end;
theorem
z - 0c n = z
proof
thus z - 0c n = z + 0c n by Lm5
.= z by BINOP_2:1,FINSEQOP:56;
end;
theorem
0c n - z = -z
proof
thus 0c n - z = 0c n + -z .= -z by BINOP_2:1,FINSEQOP:56;
end;
theorem
z1 - -z2 = z1 + z2;
theorem Th70:
-(z1 - z2) = z2 - z1
proof
thus -(z1 - z2) = -z1 + -(-z2) by Th65
.= z2 - z1;
end;
theorem Th71:
-(z1 - z2) = -z1 + z2
proof
thus -(z1 - z2) = -z1 + -(-z2) by Th65
.= -z1 + z2;
end;
theorem Th72:
z - z = 0c n
proof
thus z - z = z + -z .= 0c n by Th51,Th52,BINOP_2:1,FINSEQOP:73;
end;
theorem Th73:
z1 - z2 = 0c n implies z1 = z2
proof
assume z1 - z2 = 0c n;
then z1 + - z2 = 0c n;
then z1 = -(-z2) by Th51,Th52,BINOP_2:1,FINSEQOP:74;
hence thesis;
end;
theorem Th74:
z1 - z2 - z3 = z1 - (z2 + z3)
proof
thus z1 - z2 - z3 = z1 + -z2 + -z3 .= z1 + (- z2 + -z3) by FINSEQOP:28
.= z1 - (z2 + z3) by Th65;
end;
theorem Th75:
z1 + (z2 - z3) = z1 + z2 - z3
proof
thus z1 + (z2 - z3) = z1 + (z2 + -z3) .= z1 + z2 + -z3 by FINSEQOP:28
.= z1 + z2 - z3;
end;
theorem
z1 - (z2 - z3) = z1 - z2 + z3
proof
thus z1 - (z2 - z3) = z1 + (-z2 + z3) by Th71
.= z1 + -z2 + z3 by FINSEQOP:28
.= z1 - z2 + z3;
end;
theorem
z1 - z2 + z3 = z1 + z3 - z2 by Th75;
theorem Th78:
z1 = z1 + z - z
proof
thus z1 = z1 + 0c n by BINOP_2:1,FINSEQOP:56
.= z1 + (z - z) by Th72
.= z1 + z - z by Th75;
end;
theorem Th79:
z1 + (z2 - z1) = z2
proof
thus z1 + (z2 - z1) = z2 + -z1 + z1 .= z2 + (-z1 + z1) by FINSEQOP:28
.= z2 + 0c n by Th51,Th52,BINOP_2:1,FINSEQOP:73
.= z2 by BINOP_2:1,FINSEQOP:56;
end;
theorem Th80:
z1 = z1 - z + z
proof
thus z1 = z1 + 0c n by BINOP_2:1,FINSEQOP:56
.= z1 + (-z + z) by Th51,Th52,BINOP_2:1,FINSEQOP:73
.= z1 + -z + z by FINSEQOP:28
.= z1 - z + z;
end;
definition let n,z,c;
redefine func c*z -> Element of COMPLEX n; :: redefines * (SEQ_4, synonym) → (#) (VALUED_1, definition)
coherence by FINSEQ_2:113;
end;
theorem Th81:
k in Seg n & c9 = z.k implies (c*z).k = c*c9
proof
assume that
A1: k in Seg n and
A2: c9 = z.k;
k in dom(c*z) by A1,Lm4;
hence (c*z).k = (c multcomplex).c9 by A2,FUNCT_1:12
.= c*c9 by Lm3;
end;
theorem
c1*(c2*z) = (c1*c2)*z
proof
thus (c1*c2)*z = multcomplex[;](multcomplex.(c1,c2),id COMPLEX)*z by
BINOP_2:def 5
.= multcomplex[;](c1,multcomplex[;](c2,id COMPLEX))*z by FUNCOP_1:62
.= (multcomplex[;](c1,id COMPLEX)*multcomplex[;](c2,id COMPLEX))*z by
FUNCOP_1:55
.= c1*(c2*z) by RELAT_1:36;
end;
theorem
(c1 + c2)*z = c1*z + c2*z
proof
set c1M = multcomplex[;](c1,id COMPLEX), c2M = multcomplex[;](c2,id COMPLEX);
thus (c1 + c2)*z = multcomplex[;](addcomplex.(c1,c2),id COMPLEX)*z by
BINOP_2:def 3
.= addcomplex.:(c1M,c2M)*z by Th54,FINSEQOP:35
.= c1*z + c2*z by FUNCOP_1:25;
end;
theorem
c*(z1+z2) = c*z1 + c*z2 by Th54,FINSEQOP:51,54;
theorem
1r*z = z
proof
A1: rng z c= COMPLEX;
thus 1r*z = (id COMPLEX)*z by BINOP_2:6,FINSEQOP:44
.= z by A1,RELAT_1:53;
end;
theorem
0c*z = 0c n
proof
A1: rng z c= COMPLEX;
thus 0c*z = multcomplex[;](0c,(id COMPLEX)*z) by FUNCOP_1:34
.= multcomplex[;](0c,z) by A1,RELAT_1:53
.= 0c n by Th51,Th54,BINOP_2:1,FINSEQOP:76;
end;
theorem
(-1r)*z = -z;
definition let n,z;
redefine func abs z -> Element of n-tuples_on REAL; :: redefines abs (VALUED_1, synonym) → |. (VALUED_1, definition)
correctness by FINSEQ_2:113;
end;
theorem Th88:
k in Seg n & c = z.k implies (abs z).k = |.c.|
proof
assume that
A1: k in Seg n and
A2: c = z.k;
len abs z = n by CARD_1:def 7;
then k in dom abs z by A1,FINSEQ_1:def 3;
hence (abs z).k = abscomplex.c by A2,FUNCT_1:12
.= |.c.| by Def5;
end;
theorem Th89:
abs 0c n = n |-> 0
proof
thus abs 0c n = n |-> abscomplex.0c by FINSEQOP:16
.= n |-> 0 by Def5,COMPLEX1:44;
end;
theorem Th90:
abs -z = abs z
proof
now
let j be Nat;
assume
A1: j in Seg n;
then reconsider c = z.j, c9 = (-z).j as Element of COMPLEX by Th57;
thus (abs -z).j = |.c9.| by A1,Th88
.= |.-c.| by A1,Th60
.= |.c.| by COMPLEX1:52
.= (abs z).j by A1,Th88;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th91:
abs(c*z) = |.c.|*(abs z)
proof
now
let j be Nat;
reconsider w = j as Element of NAT by ORDINAL1:def 12;
assume
A1: j in Seg n;
then reconsider c9 = z.j, cc = (c*z).j as Element of COMPLEX by Th57;
reconsider ac = (abs z).w as Real;
thus (abs(c*z)).j = |.cc.| by A1,Th88
.= |.c*c9.| by A1,Th81
.= |.c.|*|.c9.| by COMPLEX1:65
.= |.c.|*ac by A1,Th88
.= (|.c.|*(abs z)).j by RVSUM_1:45;
end;
hence thesis by FINSEQ_2:119;
end;
definition
let z be FinSequence of COMPLEX;
func |.z.| -> Real equals
sqrt Sum sqr abs z;
correctness;
end;
theorem Th92:
|.0c n.| = 0
proof
thus |.0c n .| = sqrt Sum sqr (n |-> (0 qua Real)) by Th89
.= sqrt Sum (n |-> (0 qua Real)^2) by RVSUM_1:56
.= sqrt (n*(0 qua Nat)) by RVSUM_1:80
.= 0;
end;
theorem Th93:
|.z.| = 0 implies z = 0c n
proof
assume
A1: |.z.| = 0;
now
let j be Nat;
assume
A2: j in Seg n;
then reconsider c = z.j as Element of COMPLEX by Th57;
0 <= Sum sqr abs z by RVSUM_1:86;
then (abs z).j = (n|->0).j by A1,RVSUM_1:91,SQUARE_1:24;
then |.c.| = (n|-> 0).j by A2,Th88;
then c = 0c by COMPLEX1:45;
hence z.j = (n|->0c).j;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th94:
0 <= |.z.|
proof
0 <= Sum sqr abs z by RVSUM_1:86;
hence thesis by SQUARE_1:def 2;
end;
theorem
|.-z.| = |.z.| by Th90;
theorem
|.c*z.| = |.c.|*|.z.|
proof
A1: 0 <= |.c.|^2 & 0 <= Sum sqr abs z by RVSUM_1:86,XREAL_1:63;
thus |.c*z.| = sqrt Sum sqr (|.c.|*abs z) by Th91
.= sqrt Sum (|.c.|^2 * sqr abs z) by RVSUM_1:58
.= sqrt (|.c.|^2 * Sum sqr abs z) by RVSUM_1:87
.= sqrt |.c.|^2 * sqrt Sum sqr abs z by A1,SQUARE_1:29
.= |.c.|*|.z.| by COMPLEX1:46,SQUARE_1:22;
end;
theorem Th97:
|.z1 + z2.| <= |.z1.| + |.z2.|
proof
A1: 0 <= Sum sqr abs (z1 + z2) by RVSUM_1:86;
A2: 0 <= Sum sqr abs z1 by RVSUM_1:86;
then
A3: 0 <= sqrt Sum sqr abs z1 by SQUARE_1:def 2;
A4: for k be Nat holds k in Seg n implies 0 <= (mlt(abs z1,abs z2)).k
proof
let k be Nat;
set r = (mlt(abs z1,abs z2)).k;
assume
A5: k in Seg n;
then reconsider c1 = z1.k, c2 = z2.k as Element of COMPLEX by Th57;
(abs z1).k = |.c1.| & (abs z2).k = |.c2.| by A5,Th88;
then
A6: r = |.c1.|*|.c2.| by RVSUM_1:60;
0 <= |.c1.| & 0 <= |.c2.| by COMPLEX1:46;
hence thesis by A6;
end;
0 <= (Sum mlt(abs z1,abs z2))^2 by XREAL_1:63;
then
A7: sqrt(Sum mlt(abs z1,abs z2))^2 <= sqrt((Sum sqr abs z1)*(Sum sqr abs z2
)) by RVSUM_1:92,SQUARE_1:26;
len mlt(abs z1,abs z2) = n by CARD_1:def 7;
then dom mlt(abs z1,abs z2) = Seg n by FINSEQ_1:def 3;
then Sum mlt(abs z1,abs z2) <= sqrt((Sum sqr abs z1)*(Sum sqr abs z2)) by A4
,A7,RVSUM_1:84,SQUARE_1:22;
then 2*Sum mlt(abs z1,abs z2) <= 2*sqrt((Sum sqr abs z1)*(Sum sqr abs z2))
by XREAL_1:64;
then
Sum sqr abs z1+(2*Sum mlt(abs z1,abs z2)) <= Sum sqr abs z1+2*sqrt((Sum
sqr abs z1)*(Sum sqr abs z2)) by XREAL_1:7;
then
A8: Sum sqr abs z1+(2*Sum mlt(abs z1,abs z2)) + Sum sqr abs z2 <= Sum sqr
abs z1+2*sqrt((Sum sqr abs z1)*(Sum sqr abs z2)) + Sum sqr abs z2 by
XREAL_1:7;
A9: for k be Nat holds k in Seg n implies (sqr abs (z1 + z2)).k <= (sqr (abs
z1 + abs z2)).k
proof
let k be Nat;
set r2 = (sqr (abs z1 + abs z2)).k;
len(abs z1 + abs z2) = n by CARD_1:def 7;
then
A10: dom (abs z1 + abs z2) = Seg n by FINSEQ_1:def 3;
assume
A11: k in Seg n;
then reconsider c12 = (z1 + z2).k as Element of COMPLEX by Th57;
reconsider abs912 = (abs (z1 + z2)).k as Real;
0 <= |.c12.| by COMPLEX1:46;
then
A12: 0 <= abs912 by A11,Th88;
reconsider abs1 = (abs z1).k, abs2 = (abs z2).k as Real;
reconsider c1 = z1.k, c2 = z2.k as Element of COMPLEX by A11,Th57;
reconsider abs12 = (abs z1 + abs z2).k as Real;
|.c1 + c2.| <= |.c1.| + |.c2.| by COMPLEX1:56;
then |.c12.| <= |.c1.| + |.c2.| by A11,Th58;
then |.c12.| <= |.c1.| + abs2 by A11,Th88;
then |.c12.| <= abs1 + abs2 by A11,Th88;
then |.c12.| <= abs12 by A11,A10,VALUED_1:def 1;
then abs912 <= abs12 by A11,Th88;
then (abs912)^2 <= (abs12)^2 by A12,SQUARE_1:15;
then (abs912)^2 <= r2 by VALUED_1:11;
hence thesis by VALUED_1:11;
end;
A13: 0 <= Sum sqr abs z2 by RVSUM_1:86;
then
A14: 0 <= sqrt Sum sqr abs z2 by SQUARE_1:def 2;
A15: Sum sqr abs z1 = (sqrt Sum sqr abs z1)^2 by A2,SQUARE_1:def 2;
A16: (sqrt Sum sqr abs z2)^2 = Sum sqr abs z2 by A13,SQUARE_1:def 2;
Sum sqr (abs z1 + abs z2) = Sum (sqr abs z1 + 2*mlt(abs z1,abs z2) + sqr
abs z2) by RVSUM_1:68
.= Sum(sqr abs z1 + 2*mlt(abs z1,abs z2)) + Sum sqr abs z2 by RVSUM_1:89
.= Sum sqr abs z1 + Sum(2*mlt(abs z1,abs z2)) + Sum sqr abs z2 by
RVSUM_1:89
.= Sum sqr abs z1 + (2*Sum mlt(abs z1,abs z2))+Sum sqr abs z2 by RVSUM_1:87
;
then Sum sqr abs (z1 + z2) <= Sum sqr abs z1 + (2*Sum mlt(abs z1,abs z2))+
Sum sqr abs z2 by A9,RVSUM_1:82;
then Sum sqr abs (z1 + z2) <= Sum sqr abs z1+2*sqrt((Sum sqr abs z1)*(Sum
sqr abs z2)) + Sum sqr abs z2 by A8,XXREAL_0:2;
then Sum sqr abs (z1 + z2) <= Sum sqr abs z1+2*((sqrt Sum sqr abs z1)*(sqrt
Sum sqr abs z2)) + Sum sqr abs z2 by A2,A13,SQUARE_1:29;
then sqrt Sum sqr abs (z1 + z2) <= sqrt(((sqrt Sum sqr abs z1) + (sqrt Sum
sqr abs z2))^2) by A15,A16,A1,SQUARE_1:26;
hence thesis by A3,A14,SQUARE_1:22;
end;
theorem Th98:
|.z1 - z2.| <= |.z1.| + |.z2.|
proof
|.z1 - z2.| <= |.z1.| + |.-z2.| by Th97;
hence thesis by Th90;
end;
theorem
|.z1.| - |.z2.| <= |.z1 + z2.|
proof
z1 = z1 + z2 - z2 by Th78;
then |.z1.| <= |.z1 + z2.| + |.z2.| by Th98;
hence thesis by XREAL_1:20;
end;
theorem
|.z1.| - |.z2.| <= |.z1 - z2.|
proof
z1 = z1 - z2 + z2 by Th80;
then |.z1.| <= |.z1 - z2.| + |.z2.| by Th97;
hence thesis by XREAL_1:20;
end;
theorem Th101:
|.z1 - z2.| = 0 iff z1 = z2
proof
thus |.z1 - z2.| = 0 implies z1 = z2
proof
assume |.z1 - z2.| = 0;
then z1 - z2 = 0c n by Th93;
hence thesis by Th73;
end;
assume z1 = z2;
then z1 - z2 = 0c n by Th72;
hence thesis by Th92;
end;
theorem
z1 <> z2 implies 0 < |.z1 - z2.|
proof
assume z1 <> z2;
then 0 <> |.z1 - z2.| by Th101;
hence thesis by Th94;
end;
theorem Th103:
|.z1 - z2.| = |.z2 - z1.|
proof
thus |.z1 - z2.| = |.-(z2 - z1).| by Th70
.= |.z2 - z1.| by Th90;
end;
theorem Th104:
|.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
proof
|.z1 - z2.| = |.z1 - z + z - z2.| by Th80
.= |.(z1 - z) + (z - z2).| by Th75;
hence thesis by Th97;
end;
definition
let n;
let A be Subset of COMPLEX n;
attr A is open means
for x st x in A ex r st 0 < r & for z st |.z.| < r holds x + z in A;
end;
definition let n;
let A be Subset of COMPLEX n;
attr A is closed means
for x st for r st r > 0 ex z st |.z.| < r & x + z in A holds x in A;
end;
theorem
for A being Subset of COMPLEX n st A = {} holds A is open;
theorem
for A being Subset of COMPLEX n st A = COMPLEX n holds A is open
proof
let A be Subset of COMPLEX n;
assume
A1: A = COMPLEX n;
let x such that
x in A;
reconsider j=1 as Element of REAL by NUMBERS:19;
take j;
thus 0 < j;
let z such that
|.z.| < j;
thus thesis by A1;
end;
theorem
for AA being Subset-Family of COMPLEX n st for A being Subset of
COMPLEX n st A in AA holds A is open for A being Subset of COMPLEX n st A =
union AA holds A is open
proof
let AA be Subset-Family of COMPLEX n such that
A1: for A being Subset of COMPLEX n st A in AA holds A is open;
let A be Subset of COMPLEX n such that
A2: A = union AA;
let x;
assume x in A;
then consider B being set such that
A3: x in B and
A4: B in AA by A2,TARSKI:def 4;
reconsider B as Subset of COMPLEX n by A4;
B is open by A1,A4;
then consider r such that
A5: 0 < r and
A6: for z st |.z.| < r holds x + z in B by A3;
take r;
thus 0 < r by A5;
let z;
assume |.z.| < r;
then x + z in B by A6;
hence thesis by A2,A4,TARSKI:def 4;
end;
theorem
for A,B being Subset of COMPLEX n st A is open & B is open for C
being Subset of COMPLEX n st C = A /\ B holds C is open
proof
let A,B be Subset of COMPLEX n such that
A1: A is open and
A2: B is open;
let C be Subset of COMPLEX n such that
A3: C = A /\ B;
let x;
assume
A4: x in C;
then x in A by A3,XBOOLE_0:def 4;
then consider r1 such that
A5: 0 < r1 and
A6: for z st |.z.| < r1 holds x + z in A by A1;
x in B by A3,A4,XBOOLE_0:def 4;
then consider r2 such that
A7: 0 < r2 and
A8: for z st |.z.| < r2 holds x + z in B by A2;
take min(r1,r2);
thus 0 < min(r1,r2) by A5,A7,XXREAL_0:15;
let z;
assume
A9: |.z.| < min(r1,r2);
min(r1,r2) <= r2 by XXREAL_0:17;
then |.z.| < r2 by A9,XXREAL_0:2;
then
A10: x + z in B by A8;
min(r1,r2) <= r1 by XXREAL_0:17;
then |.z.| < r1 by A9,XXREAL_0:2;
then x + z in A by A6;
hence thesis by A3,A10,XBOOLE_0:def 4;
end;
definition
let n,x,r;
func Ball(x,r) -> Subset of COMPLEX n equals
{ z : |.z - x.| < r };
coherence
proof
defpred P[FinSequence of COMPLEX] means |.$1 - x.| < r;
{ z : P[z] } c= COMPLEX n from FRAENKEL:sch 10;
hence thesis;
end;
end;
theorem Th109:
z in Ball(x,r) iff |.x - z.| < r
proof
A1: z in { z2 : |.z2 - x.| < r } iff ex z1 st z = z1 & |.z1 - x.| < r;
|.z - x.| = |.x - z.| by Th103;
hence thesis by A1;
end;
theorem
0 < r implies x in Ball(x,r)
proof
assume
A1: 0 < r;
|.x - x.| = 0 by Th101;
hence thesis by A1;
end;
theorem
Ball(z1,r1) is open
proof
let x;
assume x in Ball(z1,r1); then
A1: |.z1 - x.| < r1 by Th109;
take r = r1 - |.z1 - x.|;
thus 0 < r by A1,XREAL_1:50;
let z;
assume |.z.| < r; then
A2: |.z.| + |.z1 - x.| < r + |.z1 - x.| by XREAL_1:6;
z1 - x - z = z1 - (x + z) by Th74;
then |.z1 - (x + z).| <= |.z.| + |.z1 - x.| by Th98;
then |.z1 - (x + z).| < r + |.z1 - x.| by A2,XXREAL_0:2;
hence thesis by Th109;
end;
definition let n,x,A;
func dist(x,A) -> Real means
:Def17:
for X being Subset of REAL st X = {|.x
- z.| : z in A} holds it = lower_bound X;
existence
proof
deffunc f(Element of COMPLEX n) = In(|.x - $1.|,REAL);
deffunc g(Element of COMPLEX n) = |.x - $1.|;
defpred P[set] means $1 in A;
reconsider X = {f(z) where z is Element of COMPLEX n: P[z]}
as Subset of REAL from DOMAIN_1:sch 8;
A1: f(z) = g(z);
A2: {f(z1) where z1 is Element of COMPLEX n: P[z1]}
= {g(z2) where z2 is Element of COMPLEX n: P[z2]}
from FRAENKEL:sch 5(A1);
take L=lower_bound X;
thus thesis by A2;
end;
uniqueness
proof
let r1,r2 be Real such that
A3: for X being Subset of REAL st X = {|.x - z.| : z in A} holds r1 =
lower_bound X and
A4: for X being Subset of REAL st X = {|.x - z.| : z in A} holds r2 =
lower_bound X;
deffunc f(Element of COMPLEX n) = In(|.x - $1.|,REAL);
deffunc g(Element of COMPLEX n) = |.x - $1.|;
defpred P[set] means $1 in A;
reconsider X = {f(z) where z is Element of COMPLEX n: P[z]}
as Subset of REAL from DOMAIN_1:sch 8;
A1: f(z) = g(z);
A2: {f(z1) where z1 is Element of COMPLEX n: P[z1]}
= {g(z2) where z2 is Element of COMPLEX n: P[z2]}
from FRAENKEL:sch 5(A1);
r1 = lower_bound X by A3,A2;
hence thesis by A4,A2;
end;
end;
definition let n,A,r;
func Ball(A,r) -> Subset of COMPLEX n equals
{ z : dist(z,A) < r };
coherence
proof
defpred P[Element of COMPLEX n] means dist($1,A) < r;
{ z : P[z] } c= COMPLEX n from FRAENKEL:sch 10;
hence thesis;
end;
end;
theorem Th112:
for X being Subset of REAL, r st X <> {} & for r9 st r9 in X
holds r <= r9 holds lower_bound X >= r
proof
let X be Subset of REAL, r such that
A1: X <> {} and
A2: for r9 st r9 in X holds r <= r9;
for r9 be ExtReal st r9 in X holds r <= r9 by A2;
then r is LowerBound of X by XXREAL_2:def 2;
then
A3: X is bounded_below;
now
let r9 be Real;
assume r9 > 0;
then consider r1 be Real such that
A4: r1 in X and
A5: r1 < lower_bound X + r9 by A1,A3,Def2;
r <= r1 by A2,A4;
hence lower_bound X + r9 >= r by A5,XXREAL_0:2;
end;
hence thesis by XREAL_1:41;
end;
theorem Th113:
A <> {} implies dist(x,A) >= 0
proof
defpred P[set] means $1 in A;
deffunc f(Element of COMPLEX n) = In(|.x - $1.|,REAL);
deffunc g(Element of COMPLEX n) = |.x - $1.|;
reconsider X = {f(z) : P[z]} as Subset of REAL from DOMAIN_1:sch 8;
A1: f(z) = g(z);
A2: {f(z1) where z1 is Element of COMPLEX n: P[z1]}
= {g(z2) where z2 is Element of COMPLEX n: P[z2]}
from FRAENKEL:sch 5(A1);
assume A <> {};
then consider z1 such that
A3: z1 in A by SUBSET_1:4;
A4: |.x - z1.| in X by A3,A2;
A5: now
let r9;
assume r9 in X;
then ex z st r9 = f(z) & z in A;
hence r9>= 0 by Th94;
end;
dist(x,A) = lower_bound X by Def17,A2;
hence thesis by A4,A5,Th112;
end;
theorem Th114:
A <> {} implies dist(x + z,A) <= dist(x,A) + |.z.|
proof
defpred P[set] means $1 in A;
deffunc g(Element of COMPLEX n) = In(|.x + z - $1.|,REAL);
deffunc h(Element of COMPLEX n) = |.x + z - $1.|;
reconsider Y = {g(z1) : P[z1]} as Subset of REAL from DOMAIN_1:sch 8;
deffunc f(Element of COMPLEX n) = In(|.x - $1.|,REAL);
deffunc f1(Element of COMPLEX n) = |.x - $1.|;
A1: for z1 being Element of COMPLEX n holds h(z1) = g(z1);
A2: {h(z1): P[z1]}
= {g(z2) where z2 is Element of COMPLEX n: P[z2]}
from FRAENKEL:sch 5(A1);
A3: for z1 being Element of COMPLEX n holds f(z1) = f1(z1);
A4: {f(z1): P[z1]}
= {f1(z2) where z2 is Element of COMPLEX n: P[z2]}
from FRAENKEL:sch 5(A3);
A5: Y is bounded_below
proof
take 0;
let r be ExtReal;
assume r in Y;
then ex z1 st r = |.x + z - z1 .| & z1 in A by A2;
hence thesis by Th94;
end;
reconsider X = {f(z1) : P[z1]} as Subset of REAL from DOMAIN_1:sch 8;
assume A <> {};
then consider z2 such that
A6: z2 in A by SUBSET_1:4;
A7: dist(x+z,A) = lower_bound Y by Def17,A2;
A8: now let r9;
assume r9 in X;
then consider z3 such that
A9: r9 = |.x - z3.| and
A10: z3 in A by A4;
|.x + z - z3.| = |.x - z3 + z.| by Th75; then
A11: |.x + z - z3.| <= r9 + |.z.| by A9,Th97;
|.x + z - z3.| in Y by A10,A2;
then |.x + z - z3.| >= dist(x + z,A) by A7,A5,Def2;
then r9+ |.z.| >= dist(x + z,A) by A11,XXREAL_0:2;
hence r9 >= dist(x + z,A) - |.z.| by XREAL_1:20;
end;
A12: |.x - z2.| in X by A6,A4;
dist(x,A) = lower_bound X by Def17,A4;
then dist(x + z,A) - |.z.| <= dist(x,A) by A12,A8,Th112;
hence thesis by XREAL_1:20;
end;
theorem Th115:
x in A implies dist(x,A) = 0
proof
defpred P[set] means $1 in A;
deffunc f(Element of COMPLEX n) = In(|.x - $1.|,REAL);
deffunc g(Element of COMPLEX n) = |.x - $1.|;
reconsider X = {f(z): P[z]} as Subset of REAL from DOMAIN_1:sch 8;
A1: f(z) = g(z);
A2: {f(z1) where z1 is Element of COMPLEX n: P[z1]}
= {g(z2) where z2 is Element of COMPLEX n: P[z2]}
from FRAENKEL:sch 5(A1);
assume
A3: x in A;
then
A4: |.x - x.| in X by A2;
A5: now
reconsider r = |.x - x.| as Real;
let r1 be Real such that
A6: 0<r1;
take r;
thus r in X by A3,A2;
thus r<(0 qua Nat)+r1 by A6,Th101;
end;
A7: now
let r be Real;
assume r in X;
then ex z st r = |.x - z .| & z in A by A2;
hence 0<=r by Th94;
end;
A8: X is bounded_below
proof
take 0;
let x be ExtReal;
thus thesis by A7;
end;
thus dist(x,A) = lower_bound X by Def17,A2
.= 0 by A4,A7,A8,A5,Def2;
end;
theorem
not x in A & A <> {} & A is closed implies dist(x,A) > 0
proof
assume that
A1: not x in A and
A2: A <> {} and
A3: for x st for r st r > 0 ex z st |.z.| < r & x + z in A holds x in A and
A4: dist(x,A) <= 0;
A5: dist(x,A) = 0 by A2,A4,Th113;
now
deffunc f(Element of COMPLEX n) = In(|.x - $1.|,REAL);
deffunc g(Element of COMPLEX n) = |.x - $1.|;
defpred P[set] means $1 in A;
A6: f(z) = g(z);
A7: {f(z1) where z1 is Element of COMPLEX n: P[z1]}
= {g(z2) where z2 is Element of COMPLEX n: P[z2]}
from FRAENKEL:sch 5(A6);
reconsider X = {f(z) : P[z]} as Subset of REAL from DOMAIN_1:sch 8;
let r such that
A8: r > 0;
consider z such that
A9: z in A by A2,SUBSET_1:4;
A10: X is bounded_below
proof
take 0;
let r be ExtReal;
assume r in X;
then ex z st r = |.x - z .| & z in A by A7;
hence thesis by Th94;
end;
A11: |.x - z.| in X by A9,A7;
dist(x,A) = lower_bound X & (0 qua Nat)+r = r by Def17,A7;
then consider r9 be Real such that
A12: r9 in X and
A13: r9< r by A5,A8,A11,A10,Def2;
consider z1 such that
A14: r9 = |.x - z1.| & z1 in A by A12,A7;
take z = z1 - x;
thus |.z.| < r & x + z in A by A13,A14,Th79,Th103;
end;
hence contradiction by A1,A3;
end;
theorem
A <> {} implies |.z1 - x.| + dist(x,A) >= dist(z1,A)
proof
x + (z1 - x) = z1 by Th79;
hence thesis by Th114;
end;
theorem Th118:
z in Ball(A,r) iff dist(z,A) < r
proof
z in { z2 : dist(z2,A) < r } iff ex z1 st z = z1 & dist(z1,A) < r;
hence thesis;
end;
theorem Th119:
0 < r & x in A implies x in Ball(A,r)
proof
assume that
A1: 0 < r and
A2: x in A;
dist(x,A) = 0 by A2,Th115;
hence thesis by A1;
end;
theorem
0 < r implies A c= Ball(A,r)
by Th119;
theorem
A <> {} implies Ball(A,r1) is open
proof
assume
A1: A <> {};
let x;
assume x in Ball(A,r1); then
A2: dist(x,A) < r1 by Th118;
take r = r1 - dist(x,A);
thus 0 < r by A2,XREAL_1:50;
let z;
assume |.z.| < r; then
A3: |.z.| + dist(x,A) < r + dist(x,A) by XREAL_1:6;
dist(x + z,A) <= |.z.| + dist(x,A) by A1,Th114;
then dist(x + z,A) < r + dist(x,A) by A3,XXREAL_0:2;
hence thesis;
end;
definition
let n,A,B;
func dist(A,B) -> Real means
:Def19:
for X being Subset of REAL st X = {|.x
- z.| : x in A & z in B} holds it = lower_bound X;
existence
proof
deffunc f(Element of COMPLEX n,Element of COMPLEX n)
= In(|.$1 - $2.|,REAL);
deffunc g(Element of COMPLEX n,Element of COMPLEX n)
= |.$1 - $2.|;
defpred P[set,set] means $1 in A & $2 in B;
reconsider X = {f(x,z) : P[x,z]} as Subset of REAL from DOMAIN_1:sch 9;
A1: for z1,z2 being Element of COMPLEX n holds f(z1,z2) = g(z1,z2);
A2: {f(z1,z2) where z1,z2 is Element of COMPLEX n: P[z1,z2]}
= {g(z1,z2) where z1,z2 is Element of COMPLEX n: P[z1,z2]}
from FRAENKEL:sch 7(A1);
take L=lower_bound X;
thus thesis by A2;
end;
uniqueness
proof
let r1,r2 be Real such that
A3: for X being Subset of REAL st X = {|.x - z.| : x in A & z in B}
holds r1 = lower_bound X and
A4: for X being Subset of REAL st X = {|.x - z.| : x in A & z in B}
holds r2 = lower_bound X;
deffunc f(Element of COMPLEX n,Element of COMPLEX n)
= In(|.$1 - $2.|,REAL);
deffunc g(Element of COMPLEX n,Element of COMPLEX n)
= |.$1 - $2.|;
defpred P[set,set] means $1 in A & $2 in B;
reconsider X = {f(x,z) : P[x,z]} as Subset of REAL from DOMAIN_1:sch 9;
A1: for z1,z2 being Element of COMPLEX n holds f(z1,z2) = g(z1,z2);
A2: {f(z1,z2) where z1,z2 is Element of COMPLEX n: P[z1,z2]}
= {g(z1,z2) where z1,z2 is Element of COMPLEX n: P[z1,z2]}
from FRAENKEL:sch 7(A1);
r1 = lower_bound X by A3,A2;
hence thesis by A4,A2;
end;
end;
theorem
for X,Y being Subset of REAL holds X <> {} & Y <> {} implies X ++ Y <> {};
theorem Th123:
for X,Y being Subset of REAL holds X is bounded_below &
Y is bounded_below implies X++Y is bounded_below
proof
let X,Y be Subset of REAL;
assume X is bounded_below;
then consider r1 be Real such that
A1: r1 is LowerBound of X;
A2: for r be Real st r in X holds r1<=r by A1,XXREAL_2:def 2;
assume Y is bounded_below;
then consider r2 be Real such that
A3: r2 is LowerBound of Y;
A4: for r be Real st r in Y holds r2<=r by A3,XXREAL_2:def 2;
take r1 + r2;
let r be ExtReal;
assume r in X++Y; then
r in {r22+r12 where r22,r12 is Complex
: r22 in X & r12 in Y} by MEMBER_1:def 6;
then consider r22,r12 being Complex such that
A5: r = r22 + r12 and
A6: r22 in X and
A7: r12 in Y;
reconsider r9 = r22, r99 = r12 as Real by A6,A7;
A8: r2 <= r99 by A4,A7;
r1 <= r9 by A2,A6;
hence thesis by A5,A8,XREAL_1:7;
end;
theorem Th124:
for X,Y being Subset of REAL st
X <> {} & X is bounded_below & Y <> {} & Y is bounded_below holds
lower_bound (X ++ Y) = lower_bound X + lower_bound Y
proof
let X,Y be Subset of REAL such that
A1: X <> {} and
A2: X is bounded_below and
A3: Y <> {} and
A4: Y is bounded_below;
A5: now
let r9 be Real;
assume 0<r9;
then
A6: r9/2 > 0;
then consider r1 be Real such that
A7: r1 in X and
A8: r1<lower_bound X+r9/2 by A1,A2,Def2;
consider r2 be Real such that
A9: r2 in Y and
A10: r2<lower_bound Y+r9/2 by A3,A4,A6,Def2;
reconsider r = r1 + r2 as Real;
take r;
thus r in X++Y by A7,A9,MEMBER_1:46;
lower_bound X + r9/2 + (lower_bound Y + r9/2) = lower_bound X +
lower_bound Y + r9;
hence r<lower_bound X + lower_bound Y+r9 by A8,A10,XREAL_1:8;
end;
A11: now
let r be Real;
assume r in X++Y; then
r in {r22+r12 where r22,r12 is Complex
: r22 in X & r12 in Y} by MEMBER_1:def 6;
then consider r11,r22 being Complex such that
A12: r = r11 + r22 and
A13: r11 in X & r22 in Y;
reconsider r1 = r11, r2 = r22 as Real by A13;
r1 >= lower_bound X & r2 >= lower_bound Y by A2,A4,A13,Def2;
hence lower_bound X + lower_bound Y<=r by A12,XREAL_1:7;
end;
X ++ Y <> {} & X ++ Y is bounded_below by A1,A2,A3,A4,Th123;
hence thesis by A11,A5,Def2;
end;
theorem Th125:
for X,Y being Subset of REAL st Y is bounded_below & X <> {} &
for r st r in X ex r1 st r1 in Y & r1 <= r holds
lower_bound X >= lower_bound Y
proof
let X,Y be Subset of REAL such that
A1: Y is bounded_below and
A2: X <> {} and
A3: for r st r in X ex r1 st r1 in Y & r1 <= r;
now
let r1;
assume r1 in X;
then consider r2 such that
A4: r2 in Y and
A5: r2 <= r1 by A3;
lower_bound Y <= r2 by A1,A4,Def2;
hence r1 >= lower_bound Y by A5,XXREAL_0:2;
end;
hence thesis by A2,Th112;
end;
theorem Th126:
A <> {} & B <> {} implies dist(A,B) >= 0
proof
defpred P[set,set] means $1 in A & $2 in B;
deffunc f(Element of COMPLEX n,Element of COMPLEX n) = |.$1 - $2.|;
deffunc g(Element of COMPLEX n,Element of COMPLEX n) = In(|.$1 - $2.|,REAL);
A1: for z1,z2 being Element of COMPLEX n holds f(z1,z2) = g(z1,z2);
A2: {f(z1,z2) where z1,z2 is Element of COMPLEX n: P[z1,z2]}
= {g(z1,z2) where z1,z2 is Element of COMPLEX n: P[z1,z2]}
from FRAENKEL:sch 7(A1);
reconsider Z = {g(z1,z) where z1,z is Element of COMPLEX n:
P[z1,z]} as Subset of REAL from DOMAIN_1:sch 9;
assume that
A3: A <> {} and
A4: B <> {};
consider z1 such that
A5: z1 in A by A3,SUBSET_1:4;
A6: now
let r9;
assume r9 in Z;
then ex z1,z st r9 = |.z1 - z.| & z1 in A & z in B by A2;
hence r9>= 0 by Th94;
end;
consider z2 such that
A7: z2 in B by A4,SUBSET_1:4;
A8: dist(A,B) = lower_bound Z by Def19,A2;
|.z1 - z2.| in Z by A5,A7,A2;
hence thesis by A8,A6,Th112;
end;
theorem
dist(A,B) = dist(B,A)
proof
defpred R[set,set] means $1 in B & $2 in A;
deffunc f(Element of COMPLEX n,Element of COMPLEX n) = In(|.$1 - $2.|,REAL);
deffunc f1(Element of COMPLEX n,Element of COMPLEX n) = |.$1 - $2.|;
reconsider Y = {f(z,z1) where z,z1 is Element of COMPLEX n: R[z,z1]}
as Subset of REAL from DOMAIN_1:sch 9;
defpred P[set,set] means $1 in A & $2 in B;
reconsider X = {f(z1,z) where z1,z is Element of COMPLEX n: P[z1,z]}
as Subset of REAL from DOMAIN_1:sch 9;
A1: now
let r be Element of REAL;
A2: now
given z,z1 such that
A3: r =f(z,z1) & z in B & z1 in A;
take z1,z;
thus r =f(z1,z) & z1 in A & z in B by A3,Th103;
end;
now
given z1,z such that
A4: r =f(z1,z) & z1 in A & z in B;
take z,z1;
thus r =f(z,z1) & z in B & z1 in A by A4,Th103;
end;
hence r in X iff r in Y by A2;
end;
A5: f(z,z1) = f1(z,z1);
A6: {f(z,z1) where z,z1 is Element of COMPLEX n: R[z,z1]}
= {f1(z,z1) where z,z1 is Element of COMPLEX n: R[z,z1]}
from FRAENKEL:sch 7(A5);
{f(z1,z) where z1,z is Element of COMPLEX n: P[z1,z]}
= {f1(z1,z) where z1,z is Element of COMPLEX n: P[z1,z]}
from FRAENKEL:sch 7(A5);
then dist(A,B) = lower_bound X & dist(B,A) = lower_bound Y by Def19,A6;
hence thesis by A1,SUBSET_1:3;
end;
theorem Th128:
A <> {} & B <> {} implies dist(x,A) + dist(x,B) >= dist(A,B)
proof
defpred Y[set] means $1 in B;
deffunc g(Element of COMPLEX n) = |.x - $1.|;
deffunc g1(Element of COMPLEX n) = In(|.x - $1.|,REAL);
reconsider Y = {g1(z) : Y[z]} as Subset of REAL from DOMAIN_1:sch 8;
defpred P[set,set] means $1 in A & $2 in B;
defpred X[set] means $1 in A;
deffunc f(Element of COMPLEX n,Element of COMPLEX n) = In(|.$1 - $2.|,REAL);
deffunc f1(Element of COMPLEX n,Element of COMPLEX n) = |.$1 - $2.|;
reconsider X = {g1(z) : X[z]} as Subset of REAL from DOMAIN_1:sch 8;
assume that
A1: A <> {} and
A2: B <> {};
consider z2 such that
A3: z2 in B by A2,SUBSET_1:4;
A4: Y <> {} & Y is bounded_below
proof
g1(z2) in Y by A3;
hence Y <> {};
take 0;
let r be ExtReal;
assume r in Y;
then ex z1 st r = g1(z1) & z1 in B;
hence thesis by Th94;
end;
A5: g1(z) = g(z);
A6: {g1(z): Y[z]} ={g(z1): Y[z1]} from FRAENKEL:sch 5(A5);
{g1(z): X[z]} ={g(z1): X[z1]} from FRAENKEL:sch 5(A5);
then
A7: lower_bound X = dist(x,A) & lower_bound Y = dist(x,B) by Def17,A6;
A8: g1(z2) in Y by A3;
reconsider Z = {f(z1,z) where z1,z: P[z1,z]} as Subset of REAL
from DOMAIN_1:sch 9;
consider z1 such that
A9: z1 in A by A1,SUBSET_1:4;
X++Y c= REAL by MEMBERED:3;
then reconsider XY = X++Y as Subset of REAL;
A10: for r st r in XY ex r1 st r1 in Z & r1 <= r
proof
let r;
assume r in XY; then
r in {r2+r1 where r2,r1 is Complex
: r2 in X & r1 in Y} by MEMBER_1:def 6;
then consider r2,r1 being Complex such that
A11: r = r2 + r1 and
A12: r2 in X and
A13: r1 in Y;
consider z2 such that
A14: r1 = g1(z2) & z2 in B by A13;
consider z1 such that
A15: r2 = g1(z1) and
A16: z1 in A by A12;
take r3 = f(z1,z2);
r2 = |.z1 - x.| by A15,Th103;
hence r3 in Z & r3 <= r by A11,A16,A14,Th104;
end;
A17: Z is bounded_below
proof
take 0;
let r be ExtReal;
assume r in Z;
then ex z1,z st r = f(z1,z) & P[z1,z];
hence thesis by Th94;
end;
A18: X <> {} & X is bounded_below
proof
g1(z1) in X by A9;
hence X <> {};
take 0;
let r be ExtReal;
assume r in X;
then ex z st r = g1(z) & z in A;
hence thesis by Th94;
end;
A19: for z3,z holds f(z3,z) = f1(z3,z);
{f(z3,z) where z3,z is Element of COMPLEX n: P[z3,z]}
= {f1(z3,z) where z3,z is Element of COMPLEX n: P[z3,z]}
from FRAENKEL:sch 7(A19);
then
A20: lower_bound Z = dist(A,B) by Def19;
g1(z1) in X by A9;
then |.x - z1.| + |.x - z2 .| in X ++ Y by A8,MEMBER_1:46;
then XY <> {};
then lower_bound XY >= lower_bound Z by A17,A10,Th125;
hence thesis by A18,A4,A7,A20,Th124;
end;
theorem
A meets B implies dist(A,B) = 0
proof
assume A meets B;
then consider z being object such that
A1: z in A and
A2: z in B by XBOOLE_0:3;
reconsider z as Element of COMPLEX n by A1;
dist(z,A) = 0 & dist(z,B) = 0 by A1,A2,Th115;
then (0 qua Nat) + (0 qua Nat) >= dist(A,B) by A1,A2,Th128;
hence thesis by A1,A2,Th126;
end;
definition
let n;
func ComplexOpenSets(n) -> Subset-Family of COMPLEX n equals
{A where A is
Subset of COMPLEX n: A is open};
coherence
proof
set S = {A where A is Subset of COMPLEX n: A is open};
S c= bool COMPLEX n
proof
let x be object;
assume x in S;
then ex A being Subset of COMPLEX n st x = A & A is open;
hence thesis;
end;
hence thesis;
end;
end;
theorem
for A being Subset of COMPLEX n holds A in ComplexOpenSets n iff A is open
proof
let B be Subset of COMPLEX n;
B in {A where A is Subset of COMPLEX n: A is open} iff ex C being Subset
of COMPLEX n st B = C & C is open;
hence thesis;
end;
theorem
for A being Subset of COMPLEX n holds A is closed iff A` is open
proof
let A be Subset of COMPLEX n;
thus A is closed implies A` is open
proof
assume
A1: for x st for r st r > 0 ex z st |.z.| < r & x + z in A holds x in A;
let x;
assume x in A`;
then not x in A by XBOOLE_0:def 5;
then consider r such that
A2: r > 0 and
A3: for z st |.z.| < r holds not x + z in A by A1;
take r;
thus 0 < r by A2;
let z;
assume |.z.| < r;
hence thesis by A3,SUBSET_1:29;
end;
assume
A4: for x st x in A` ex r st 0 < r & for z st |.z.| < r holds x + z in A`;
let x such that
A5: for r st r > 0 ex z st |.z.| < r & x + z in A;
now
let r;
assume r > 0;
then consider z such that
A6: |.z.| < r & x + z in A by A5;
take z;
thus |.z.| < r & not x + z in A` by A6,XBOOLE_0:def 5;
end;
then not x in A` by A4;
hence thesis by SUBSET_1:29;
end;
begin :: moved from GOBOARD2, 2010.03.01, A.T.
reserve
v,v1,v2 for FinSequence of REAL,
n,m,k for Nat,
x for set;
defpred P[Nat] means for R being finite Subset of REAL st R <> {} & card R =
$1 holds R is bounded_above & upper_bound(R) in R & R is bounded_below &
lower_bound(R) in R;
Lm7: P[0];
Lm8: for n st P[n] holds P[n+1]
proof
let n such that
A1: P[n];
let R be finite Subset of REAL such that
A2: R <> {} and
A3: card R = n+1;
now
per cases;
suppose
A4: n=0;
thus R is bounded_above;
consider x being object such that
A5: R={x} by A3,A4,CARD_2:42;
x in R by A5,TARSKI:def 1;
then reconsider r=x as Real;
upper_bound R = r by A5,Th9;
hence upper_bound R in R by A5,TARSKI:def 1;
thus R is bounded_below;
lower_bound R = r by A5,Th9;
hence lower_bound R in R by A5,TARSKI:def 1;
end;
suppose
A6: n<>0;
set x = the Element of R;
reconsider x as Real;
reconsider X = R \ {x} as finite Subset of REAL;
set u = upper_bound X, m = max(x,u), l = lower_bound X, mi = min(x,l);
{x} c= R by A2,ZFMISC_1:31;
then card (R\{x}) = card R - card {x} by CARD_2:44;
then
A7: card X = n+1-1 by A3,CARD_1:30
.=n;
then
A8: upper_bound X in X by A1,A6,CARD_1:27;
A9: now
reconsider s = m as Real;
let r be Real such that
A10: 0<r;
take s;
now
per cases by XXREAL_0:16;
suppose
m=x;
hence s in R by A2;
thus m-r<s by A10,XREAL_1:44;
end;
suppose
m=u;
hence s in R by A8,XBOOLE_0:def 5;
thus m-r<s by A10,XREAL_1:44;
end;
end;
hence s in R & m-r<s;
end;
A11: lower_bound X in X by A1,A6,A7,CARD_1:27;
A12: now
reconsider s = mi as Real;
let r be Real such that
A13: 0<r;
take s;
now
per cases by XXREAL_0:15;
suppose
mi=x;
hence s in R by A2;
thus s<mi+r by A13,XREAL_1:29;
end;
suppose
mi=l;
hence s in R by A11,XBOOLE_0:def 5;
thus s<mi+r by A13,XREAL_1:29;
end;
end;
hence s in R & s<mi+r;
end;
thus R is bounded_above;
A14: u<=m by XXREAL_0:25;
A15: now
let s be Real such that
A16: s in R;
now
per cases;
suppose
s=x;
hence s<=m by XXREAL_0:25;
end;
suppose
s<>x;
then not s in {x} by TARSKI:def 1;
then s in X by A16,XBOOLE_0:def 5;
then s<=u by Def1;
hence s<=m by A14,XXREAL_0:2;
end;
end;
hence s<=m;
end;
now
per cases by XXREAL_0:16;
suppose
m=x;
hence m in R by A2;
end;
suppose
m=u;
hence m in R by A8,XBOOLE_0:def 5;
end;
end;
hence upper_bound R in R by A15,A9,Def1;
thus R is bounded_below;
A17: mi<=l by XXREAL_0:17;
A18: now
let s be Real such that
A19: s in R;
now
per cases;
suppose
s=x;
hence mi<=s by XXREAL_0:17;
end;
suppose
s<>x;
then not s in {x} by TARSKI:def 1;
then s in X by A19,XBOOLE_0:def 5;
then l<=s by Def2;
hence mi<=s by A17,XXREAL_0:2;
end;
end;
hence mi<=s;
end;
now
per cases by XXREAL_0:15;
suppose
mi=x;
hence mi in R by A2;
end;
suppose
mi=l;
hence mi in R by A11,XBOOLE_0:def 5;
end;
end;
hence lower_bound R in R by A18,A12,Def2;
end;
end;
hence thesis;
end;
Lm9: for n holds P[n] from NAT_1:sch 2(Lm7,Lm8);
theorem Th132:
for R being finite Subset of REAL holds R <> {} implies R is
bounded_above & upper_bound(R) in R & R is bounded_below & lower_bound(R) in R
proof
let R be finite Subset of REAL;
assume
A1: R <> {};
P[card R] by Lm9;
hence thesis by A1;
end;
theorem
for n being Nat for f being FinSequence holds 1 <= n & n+1 <= len
f iff n in dom f & n+1 in dom f
proof
let n be Nat;
let f be FinSequence;
thus 1<=n & n+1 <= len f implies n in dom f & n+1 in dom f
proof
assume that
A1: 1<=n and
A2: n+1 <= len f;
n<=n+1 by NAT_1:11;
then 1<=n+1 & n<=len f by A2,NAT_1:11,XXREAL_0:2;
hence thesis by A1,A2,FINSEQ_3:25;
end;
thus thesis by FINSEQ_3:25;
end;
theorem
for n being Nat for f being FinSequence holds 1 <= n & n+2 <= len f
iff n in dom f & n+1 in dom f & n+2 in dom f
proof
let n be Nat;
let f be FinSequence;
thus 1<=n & n+2 <= len f implies n in dom f & n+1 in dom f & n+2 in dom f
proof
assume that
A1: 1<=n and
A2: n+2 <= len f;
n+1<=n+1+1 by NAT_1:11;
then
A3: 1<=n+1 & n+1<=len f by A2,NAT_1:11,XXREAL_0:2;
n<=n+2 by NAT_1:11;
then 1<=n+2 & n<=len f by A1,A2,XXREAL_0:2;
hence thesis by A1,A2,A3,FINSEQ_3:25;
end;
assume that
A4: n in dom f and
n+1 in dom f and
A5: n+2 in dom f;
thus thesis by A4,A5,FINSEQ_3:25;
end;
theorem
for D being non empty set, f1,f2 being FinSequence of D, n st 1
<= n & n <= len f2 holds (f1^f2)/.(n + len f1) = f2/.n
proof
let D be non empty set, f1,f2 be FinSequence of D, n such that
A1: 1 <= n and
A2: n <= len f2;
A3: len f1 < n + len f1 by A1,NAT_1:19;
len(f1^f2) = len f1 + len f2 by FINSEQ_1:22;
then
A4: n + len f1 <= len(f1^f2) by A2,XREAL_1:6;
n + len f1 >= n by NAT_1:11;
then n + len f1 >= 1 by A1,XXREAL_0:2;
hence (f1^f2)/.(n + len f1) = (f1^f2).(n + len f1) by A4,FINSEQ_4:15
.= f2.(n + len f1 - len f1) by A3,A4,FINSEQ_1:24
.= f2/.n by A1,A2,FINSEQ_4:15;
end;
theorem
v is increasing implies for n,m st n in dom v & m in dom v & n<=m
holds v.n <= v.m
proof
assume
A1: v is increasing;
let n,m such that
A2: n in dom v & m in dom v and
A3: n<=m;
now
per cases;
suppose
n=m;
hence thesis;
end;
suppose
n<>m;
then n<m by A3,XXREAL_0:1;
hence thesis by A1,A2,SEQM_3:def 1;
end;
end;
hence thesis;
end;
theorem Th137:
v is increasing implies
for n,m st n in dom v & m in dom v & n <> m holds v.n <> v.m
proof
assume
A1: v is increasing;
let n,m;
assume that
A2: n in dom v & m in dom v and
A3: n<>m;
now
per cases by A3,XXREAL_0:1;
suppose
n<m;
hence thesis by A1,A2,SEQM_3:def 1;
end;
suppose
n>m;
hence thesis by A1,A2,SEQM_3:def 1;
end;
end;
hence thesis;
end;
theorem
v is increasing & v1 = v|Seg n implies v1 is increasing;
defpred P1[Nat] means
for v st card rng v = $1 holds ex v1 st rng
v1 = rng v & len v1 = card rng v & v1 is increasing;
Lm10: P1[0]
proof
let v;
assume card rng v = 0;
then
A1: rng v = {};
take v1 = v;
thus rng v1 = rng v;
thus len v1 = card rng v by A1,RELAT_1:41;
for n,m holds n in dom v1 & m in dom v1 & n<m implies v1.n < v1.m by A1,
RELAT_1:38,41;
hence thesis by SEQM_3:def 1;
end;
Lm11: for n st P1[n] holds P1[n+1]
proof
let n such that
A1: P1[n];
let v such that
A2: card rng v = n+1;
now
reconsider R = rng v as finite Subset of REAL;
set u = upper_bound(R), X = R \ {u};
set f = X|`v;
Seq f=f*Sgm(dom f) & rng Sgm(dom f)=dom f by FINSEQ_1:50;
then
A3: rng Seq f = rng f by RELAT_1:28
.= X by RELAT_1:89,XBOOLE_1:36;
then reconsider f1 = Seq f as FinSequence of REAL by FINSEQ_1:def 4;
reconsider X as finite set;
upper_bound(R) in R by A2,Th132,CARD_1:27;
then
A4: {u} c= R by ZFMISC_1:31;
then
A5: card X = card R - card {u} by CARD_2:44;
A6: card {u}=1 by CARD_1:30;
then consider v2 such that
A7: rng v2 = rng f1 and
A8: len v2 = card rng f1 and
A9: v2 is increasing by A1,A2,A3,A5;
reconsider uu=u as Element of REAL by XREAL_0:def 1;
take v1 = v2 ^ <* uu *>;
thus rng v1 = X \/ rng <*u*> by A3,A7,FINSEQ_1:31
.= (rng v \ {u}) \/ {u} by FINSEQ_1:39
.= rng v \/ {u} by XBOOLE_1:39
.= rng v by A4,XBOOLE_1:12;
thus
A10: len v1 = n+ len <*u*> by A2,A3,A5,A6,A8,FINSEQ_1:22
.= card rng v by A2,FINSEQ_1:39;
now
let k,m;
assume that
A11: k in dom v1 and
A12: m in dom v1 and
A13: k<m;
A14: 1<=m by A12,FINSEQ_3:25;
A15: m<=len v1 by A12,FINSEQ_3:25;
set r=v1.k, s=v1.m;
A16: 1<=k by A11,FINSEQ_3:25;
A17: k<=len v1 by A11,FINSEQ_3:25;
now
per cases;
suppose
A18: m=len v1;
k<len v1 by A13,A15,XXREAL_0:2;
then k<=len v2 by A2,A3,A5,A6,A8,A10,NAT_1:13;
then
A19: k in dom v2 by A16,FINSEQ_3:25;
then r=v2.k by FINSEQ_1:def 7;
then
A20: r in rng v2 by A19,FUNCT_1:def 3;
then r in R by A3,A7,XBOOLE_0:def 5;
then
A21: r<=u by Def1;
not r in {u} by A3,A7,A20,XBOOLE_0:def 5;
then
A22: r<>u by TARSKI:def 1;
s=u by A2,A3,A5,A6,A8,A10,A18,FINSEQ_1:42;
hence r<s by A21,A22,XXREAL_0:1;
end;
suppose
m <>len v1;
then m<len v1 by A15,XXREAL_0:1;
then m<=len v2 by A2,A3,A5,A6,A8,A10,NAT_1:13;
then
A23: m in dom v2 by A14,FINSEQ_3:25;
then
A24: s=v2.m by FINSEQ_1:def 7;
k<len v1 by A13,A17,A15,XXREAL_0:1;
then k<=len v2 by A2,A3,A5,A6,A8,A10,NAT_1:13;
then
A25: k in dom v2 by A16,FINSEQ_3:25;
then r=v2.k by FINSEQ_1:def 7;
hence r<s by A9,A13,A25,A23,A24,SEQM_3:def 1;
end;
end;
hence r<s;
end;
hence v1 is increasing by SEQM_3:def 1;
end;
hence thesis;
end;
Lm12: for n holds P1[n] from NAT_1:sch 2(Lm10,Lm11);
theorem
for v holds ex v1 st rng v1 = rng v & len v1 = card rng v & v1 is
increasing by Lm12;
defpred P3[Nat] means
for v1,v2 st len v1=$1 & len v2=$1 & rng v1=
rng v2 & v1 is increasing & v2 is increasing holds v1=v2;
Lm13: P3[0]
proof
let v1,v2;
assume that
A1: len v1=0 and
A2: len v2=0 and
rng v1=rng v2 and
v1 is increasing and
v2 is increasing;
v1={} by A1;
hence thesis by A2;
end;
Lm14: for n st P3[n] holds P3[n+1]
proof
let n such that
A1: P3[n];
let v1,v2 such that
A2: len v1=n+1 and
A3: len v2=n+1 and
A4: rng v1=rng v2 and
A5: v1 is increasing and
A6: v2 is increasing;
reconsider X = rng v1 as Subset of REAL;
set u = upper_bound(X);
X <> {} by A2,CARD_1:27,RELAT_1:41;
then
A7: upper_bound(X) in X by Th132;
then consider m being Nat such that
A8: m in dom v2 and
A9: v2.m=u by A4,FINSEQ_2:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
A10: m<=len v2 by A8,FINSEQ_3:25;
A11: n<=n+1 by NAT_1:11;
then Seg n c= Seg(n+1) by FINSEQ_1:5;
then
A12: Seg n = Seg(n+1) /\ Seg n by XBOOLE_1:28;
dom v2=Seg len v2 by FINSEQ_1:def 3;
then
A13: dom (v2|Seg n) =Seg n by A3,A12,RELAT_1:61;
dom v1 = Seg len v1 by FINSEQ_1:def 3;
then
A14: dom (v1|Seg n) = Seg n by A2,A12,RELAT_1:61;
then reconsider f1 = v1|Seg n, f2 = v2|Seg n as FinSequence by A13,
FINSEQ_1:def 2;
rng f2 c= rng v2 by RELAT_1:70; then
A15: rng f2 c= REAL by XBOOLE_1:1;
rng f1 c= rng v1 by RELAT_1:70;
then rng f1 c= REAL by XBOOLE_1:1;
then reconsider f1, f2 as FinSequence of REAL by A15,FINSEQ_1:def 4;
consider k being Nat such that
A16: k in dom v1 and
A17: v1.k=u by A7,FINSEQ_2:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
A18: k<=len v1 by A16,FINSEQ_3:25;
A19: 1<=k by A16,FINSEQ_3:25;
A20: now
assume k<>len v1;
then k<len v1 by A18,XXREAL_0:1;
then
A21: k+1<=len v1 by NAT_1:13;
reconsider s=v1.(k+1) as Real;
A22: k<k+1 by NAT_1:13;
1<=k+1 by A19,NAT_1:13;
then
A23: k+1 in dom v1 by A21,FINSEQ_3:25;
then v1.(k+1) in rng v1 by FUNCT_1:def 3;
then s<=u by Def1;
hence contradiction by A5,A16,A17,A23,A22,SEQM_3:def 1;
end;
A24: 1<=m by A8,FINSEQ_3:25;
A25: now
assume m<>len v2;
then m<len v2 by A10,XXREAL_0:1;
then
A26: m+1<=len v2 by NAT_1:13;
reconsider s=v2.(m+1) as Real;
A27: m<m+1 by NAT_1:13;
1<=m+1 by A24,NAT_1:13;
then
A28: m+1 in dom v2 by A26,FINSEQ_3:25;
then v2.(m+1) in rng v2 by FUNCT_1:def 3;
then s<=u by A4,Def1;
hence contradiction by A6,A8,A9,A28,A27,SEQM_3:def 1;
end;
n in NAT by ORDINAL1:def 12;
then
A29: len f1 = n by A14,FINSEQ_1:def 3;
then
A30: dom f1 c= dom v1 by A2,A11,FINSEQ_3:30;
A31: rng f1 = rng v1 \ {u}
proof
thus rng f1 c= rng v1 \ {u}
proof
let x be object;
assume x in rng f1;
then consider i being Nat such that
A32: i in dom f1 and
A33: f1.i=x by FINSEQ_2:10;
A34: x=v1.i by A32,A33,FUNCT_1:47;
A35: v1.i in rng v1 by A30,A32,FUNCT_1:def 3;
i<=n by A14,A32,FINSEQ_1:1;
then i<>n+1 by NAT_1:13;
then x<>u by A2,A5,A16,A17,A20,A30,A32,A34,Th137;
then not x in {u} by TARSKI:def 1;
hence thesis by A34,A35,XBOOLE_0:def 5;
end;
let x be object;
assume
A36: x in rng v1 \ {u};
then x in rng v1 by XBOOLE_0:def 5;
then consider i being Nat such that
A37: i in dom v1 and
A38: v1.i=x by FINSEQ_2:10;
A39: i<=len v1 by A37,FINSEQ_3:25;
not x in {u} by A36,XBOOLE_0:def 5;
then i <> len v1 by A17,A20,A38,TARSKI:def 1;
then i<len v1 by A39,XXREAL_0:1;
then
A40: i<=len f1 by A2,A29,NAT_1:13;
1<=i by A37,FINSEQ_3:25;
then
A41: i in dom f1 by A40,FINSEQ_3:25;
then f1.i in rng f1 by FUNCT_1:def 3;
hence thesis by A38,A41,FUNCT_1:47;
end;
A42: dom v1 = Seg len v1 by FINSEQ_1:def 3;
A43: now
let i be Nat;
assume
A44: i in dom v1;
then
A45: 1<=i by A42,FINSEQ_1:1;
A46: i<=len f1+1 by A2,A29,A42,A44,FINSEQ_1:1;
now
per cases;
suppose
i=len f1+1;
hence (f1^<*u*>).i=v1.i by A2,A17,A20,A29,FINSEQ_1:42;
end;
suppose
i<>len f1+1;
then i < len f1+1 by A46,XXREAL_0:1;
then i<=len f1 by NAT_1:13;
then
A47: i in dom f1 by A14,A29,A45;
hence (f1^<*u*>).i=f1.i by FINSEQ_1:def 7
.= v1.i by A47,FUNCT_1:47;
end;
end;
hence (f1^<*u*>).i=v1.i;
end;
len (f1^<*u*>) = n + len <*u*> by A29,FINSEQ_1:22
.= len v1 by A2,FINSEQ_1:39;
then
A48: v1=f1^<*u*> by A43,FINSEQ_2:9;
n in NAT by ORDINAL1:def 12;
then
A49: len f2 = n by A13,FINSEQ_1:def 3;
then
A50: len (f2^<*u*>) = n + len <*u*> by FINSEQ_1:22
.= len v2 by A3,FINSEQ_1:39;
A51: dom f2 c= dom v2 by A3,A11,A49,FINSEQ_3:30;
A52: rng f2 = rng v2 \ {u}
proof
thus rng f2 c= rng v2 \ {u}
proof
let x be object;
assume x in rng f2;
then consider i being Nat such that
A53: i in dom f2 and
A54: f2.i=x by FINSEQ_2:10;
A55: x=v2.i by A53,A54,FUNCT_1:47;
A56: v2.i in rng v2 by A51,A53,FUNCT_1:def 3;
i<=n by A13,A53,FINSEQ_1:1;
then i<>n+1 by NAT_1:13;
then x<>u by A3,A6,A8,A9,A25,A51,A53,A55,Th137;
then not x in {u} by TARSKI:def 1;
hence thesis by A55,A56,XBOOLE_0:def 5;
end;
let x be object;
assume
A57: x in rng v2 \ {u};
then x in rng v2 by XBOOLE_0:def 5;
then consider i being Nat such that
A58: i in dom v2 and
A59: v2.i=x by FINSEQ_2:10;
A60: i<=len v2 by A58,FINSEQ_3:25;
not x in {u} by A57,XBOOLE_0:def 5;
then i <> len v2 by A9,A25,A59,TARSKI:def 1;
then i<len v2 by A60,XXREAL_0:1;
then
A61: i<=len f2 by A3,A49,NAT_1:13;
1<=i by A58,FINSEQ_3:25;
then
A62: i in dom f2 by A61,FINSEQ_3:25;
then f2.i in rng f2 by FUNCT_1:def 3;
hence thesis by A59,A62,FUNCT_1:47;
end;
A63: dom v2 = Seg len v2 by FINSEQ_1:def 3;
A64: now
let i be Nat;
assume
A65: i in dom v2;
then
A66: 1<=i by A63,FINSEQ_1:1;
A67: i<=len f2+1 by A3,A49,A63,A65,FINSEQ_1:1;
now
per cases;
suppose
i=len f2+1;
hence (f2^<*u*>).i=v2.i by A3,A9,A25,A49,FINSEQ_1:42;
end;
suppose
i<>len f2+1;
then i < len f2+1 by A67,XXREAL_0:1;
then i<=len f2 by NAT_1:13;
then
A68: i in dom f2 by A13,A49,A66;
hence (f2^<*u*>).i=f2.i by FINSEQ_1:def 7
.= v2.i by A68,FUNCT_1:47;
end;
end;
hence (f2^<*u*>).i=v2.i;
end;
f1 is increasing & f2 is increasing by A5,A6;
then f1=f2 by A1,A4,A29,A49,A31,A52;
hence thesis by A48,A50,A64,FINSEQ_2:9;
end;
Lm15: for n holds P3[n] from NAT_1:sch 2(Lm13,Lm14);
theorem
for v1,v2 st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2
is increasing holds v1 = v2 by Lm15;
definition
let v;
func Incr(v) ->increasing FinSequence of REAL means
:Def21:
rng it = rng v & len it = card rng v;
existence
proof
consider v1 such that
A1: rng v1 = rng v & len v1 = card rng v and
A2: v1 is increasing by Lm12;
reconsider v1 as increasing FinSequence of REAL by A2;
take v1;
thus thesis by A1;
end;
uniqueness by Lm15;
end;
registration
let v be non empty FinSequence of REAL;
cluster Incr v -> non empty;
coherence
proof
A1: len Incr(v)=card rng v by Def21;
assume Incr(v) is empty;
then rng v = {} by A1;
hence contradiction;
end;
end;
:: from SPRECT_1, 2011.04.24, A.T
registration
cluster non empty bounded_above bounded_below for Subset of REAL;
existence
proof
reconsider A = {0} as Subset of REAL;
take A;
thus A is non empty;
thus A is bounded_above;
take 0;
let t be ExtReal;
assume t in A;
hence thesis;
end;
end;
theorem
for A,B being non empty bounded_below Subset of REAL holds lower_bound(A
\/ B) = min(lower_bound A,lower_bound B)
proof
let A,B be non empty bounded_below Subset of REAL;
set r = min(lower_bound A,lower_bound B);
A1: r <= lower_bound B by XXREAL_0:17;
A2: for r1 being Real st for t being Real st t in A \/ B holds
t >= r1 holds r >= r1
proof
let r1 be Real;
assume
A3: for t being Real st t in A \/ B holds t >= r1;
now
let t be Real;
assume t in B;
then t in A \/ B by XBOOLE_0:def 3;
hence t >= r1 by A3;
end;
then
A4: lower_bound B >= r1 by Th43;
now
let t be Real;
assume t in A;
then t in A \/ B by XBOOLE_0:def 3;
hence t >= r1 by A3;
end;
then lower_bound A >= r1 by Th43;
hence thesis by A4,XXREAL_0:20;
end;
A5: r <= lower_bound A by XXREAL_0:17;
for t being Real st t in A \/ B holds t >= r
proof
let t be Real;
assume t in A \/ B;
then t in A or t in B by XBOOLE_0:def 3;
then lower_bound A <= t or lower_bound B <= t by Def2;
hence thesis by A5,A1,XXREAL_0:2;
end;
hence thesis by A2,Th44;
end;
theorem
for A,B being non empty bounded_above Subset of REAL holds upper_bound(A
\/ B) = max(upper_bound A,upper_bound B)
proof
let A,B be non empty bounded_above Subset of REAL;
set r = max(upper_bound A,upper_bound B);
A1: r >= upper_bound B by XXREAL_0:25;
A2: for r1 being Real st for t being Real st t in A \/ B holds
t <= r1 holds r <= r1
proof
let r1 be Real;
assume
A3: for t being Real st t in A \/ B holds t <= r1;
now
let t be Real;
assume t in B;
then t in A \/ B by XBOOLE_0:def 3;
hence t <= r1 by A3;
end;
then
A4: upper_bound B <= r1 by Th45;
now
let t be Real;
assume t in A;
then t in A \/ B by XBOOLE_0:def 3;
hence t <= r1 by A3;
end;
then upper_bound A <= r1 by Th45;
hence thesis by A4,XXREAL_0:28;
end;
A5: r >= upper_bound A by XXREAL_0:25;
for t being Real st t in A \/ B holds t <= r
proof
let t be Real;
assume t in A \/ B;
then t in A or t in B by XBOOLE_0:def 3;
then upper_bound A >= t or upper_bound B >= t by Def1;
hence thesis by A5,A1,XXREAL_0:2;
end;
hence thesis by A2,Th46;
end;
:: from TOPMETR3, 2011.04.24, A.T
theorem
for R being non empty Subset of REAL,r0 being Real st for
r being Real st r in R holds r <= r0 holds upper_bound R <= r0
proof
let R be non empty Subset of REAL,r0 be Real;
assume
A1: for r being Real st r in R holds r<=r0;
then for r being ExtReal st r in R holds r<=r0;
then r0 is UpperBound of R by XXREAL_2:def 1;
then
A2: R is bounded_above;
now
set r1=(upper_bound R) -r0;
assume upper_bound R >r0;
then r1>0 by XREAL_1:50;
then ex r being Real st r in R & (upper_bound R)-r1<r
by A2,Def1;
hence contradiction by A1;
end;
hence thesis;
end;