:: Convergent Real Sequences. Upper and Lower Bound of Sets of Real Numbers :: by Jaros{\l}aw Kotowicz :: :: Received November 23, 1989 :: Copyright (c) 1990-2012 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, XREAL_0, ORDINAL1, 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; 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, SEQ_1, RECDEF_1, XXREAL_2, FINSET_1, RELSET_1, BINOP_1, BINOP_2, SETWISEO, FINSEQOP, ZFMISC_1, RVSUM_1, MEMBER_1, COMSEQ_2; 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, SEQM_3, MEMBER_1, PBOOLE, COMSEQ_2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions XBOOLE_0, TARSKI, SEQ_2, COMPLEX1, FINSEQ_1, FINSEQ_2, SQUARE_1, XXREAL_2, VALUED_0, FINSEQOP, SUBSET_1, 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; 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 Element of NAT; reserve r,r1,r2,p,p1,g,g1,g2,s,s1,s2,t for real number; 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

Subset of REAL; coherence proof {r} c= REAL proof let x be set; assume x in {r}; hence thesis by XREAL_0:def 1; end; 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 real number means :Def1: (for r st r in X holds r<=it) & for s st 0 real number means :Def2: (for r st r in X holds it<=r) & for s st 0= 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: now let s be real number such that A4: 0 < s; assume for t be real number st t in X holds t >= r+s; then r >= r+s by A2; hence contradiction by A4,XREAL_1:29; end; X is bounded_below proof take r; let s be ext-real number; 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 number such that A4: 0 < s; assume for t be real number 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 ext-real number; 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 ext-real number 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 ext-real number 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; definition let X; redefine func upper_bound X -> Real; coherence by XREAL_0:def 1; redefine func lower_bound X -> Real; coherence by XREAL_0:def 1; 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 Xr; A6: now assume A7: r convergent for Real_Sequence; coherence by Th13; end; theorem seq is convergent implies lim abs seq = abs lim seq proof assume A1: seq is convergent; now let p; assume 0 convergent for Real_Sequence; coherence; end; registration cluster constant for Real_Sequence; existence proof take the constant Real_Sequence; thus thesis; end; 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

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 abs(lim seq)/20 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 Real such that A2: rng seq={r1} by FUNCT_2:111; A3: now assume that A4: r in rng seq; consider r2 being 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; now let p such that A7: 00 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; theorem Th28: 0<=r & (for n holds seq.n=1/(n+r)) implies seq is convergent proof assume that A1: 0<=r and A2: for n holds seq.n=1/(n+r); take 0; let p; assume A3: 00 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)0 by A4; then k1>=1+(0 qua Nat) by NAT_1:13; then k1<=k1*k1 by XREAL_1:151; then A7: k1+r<=k1*k1+r by XREAL_1:6; take n=k1; let m; assume n<=m; then n*n<=m*m by XREAL_1:66; then A8: n*n+r<=m*m+r by XREAL_1:6; p"+(0 qua Nat) 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 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 Real holds p in X iff X[p] from SUBSET_1:sch 3; take g=lower_bound X; let s; assume A4: 0 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; 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 by FUNCOP_1:7; then A5: lim seq1=seq.m by Th25; now let n be Nat; n in NAT by ORDINAL1:def 12; hence seq2.n=U(n) by A3; end; 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; 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 by FUNCOP_1:7; then A5: lim seq1=seq.m by Th25; now let n be Nat; n in NAT by ORDINAL1:def 12; hence seq2.n=U(n) by A3; end; 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[Element of NAT] means for m st $1= 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 ext-real number; thus thesis by A1; end; then ex t9 be real number 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 ext-real number; thus thesis by A1; end; then ex t9 be real number 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; coherence by ORDINAL1:def 12; end; begin :: moved from COMPLSP1, 2010.02.25 reserve k,n for Element of 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,FINSEQOP:def 2; theorem Th52: the_inverseOp_wrt addcomplex = compcomplex by Th50,Th51,FINSEQOP:def 3; definition redefine func diffcomplex equals 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 number; 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) by FUNCT_1:18 .= 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 from FUNCT_2:sch 4; 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 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 set; 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 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 set; 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 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 set; 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 number; synonym c*z for c(#)z; end; definition let z; let c be complex number; redefine func c*z -> FinSequence of COMPLEX equals (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 set; 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 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 set; assume A2: x in dom abs z; A3: z.x is Element of COMPLEX by XCMPLX_0:def 2; thus (abs z).x = abs(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; 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; 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; 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 number) 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 ; canceled; 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 Th66: -(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; 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 Th71: -(z1 - z2) = z2 - z1 proof thus -(z1 - z2) = -z1 + -(-z2) by Th66 .= z2 - z1; end; theorem Th72: -(z1 - z2) = -z1 + z2 proof thus -(z1 - z2) = -z1 + -(-z2) by Th66 .= -z1 + z2; end; theorem Th73: z - z = 0c n proof thus z - z = z + -z .= 0c n by Th51,Th52,BINOP_2:1,FINSEQOP:73; end; theorem Th74: 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 Th75: z1 - z2 - z3 = z1 - (z2 + z3) proof thus z1 - z2 - z3 = z1 + -z2 + -z3 .= z1 + (- z2 + -z3) by FINSEQOP:28 .= z1 - (z2 + z3) by Th66; end; theorem Th76: 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 Th72 .= z1 + -z2 + z3 by FINSEQOP:28 .= z1 - z2 + z3; end; theorem z1 - z2 + z3 = z1 + z3 - z2 by Th76; theorem Th79: z1 = z1 + z - z proof thus z1 = z1 + 0c n by BINOP_2:1,FINSEQOP:56 .= z1 + (z - z) by Th73 .= z1 + z - z by Th76; end; theorem Th80: 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 Th81: 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; coherence by FINSEQ_2:113; end; theorem Th82: 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; correctness by FINSEQ_2:113; end; theorem Th89: 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 Th90: abs 0c n = n |-> 0 proof thus abs 0c n = n |-> abscomplex.0c by FINSEQOP:16 .= n |-> 0 by Def5,COMPLEX1:44; end; theorem Th91: 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,Th89 .= |.-c.| by A1,Th60 .= |.c.| by COMPLEX1:52 .= (abs z).j by A1,Th89; end; hence thesis by FINSEQ_2:119; end; theorem Th92: 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,Th89 .= |.c*c9.| by A1,Th82 .= |.c.|*|.c9.| by COMPLEX1:65 .= |.c.|*ac by A1,Th89 .= (|.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 Th93: |.0c n.| = 0 proof thus |.0c n .| = sqrt Sum sqr (n |-> (0 qua Real)) by Th90 .= sqrt Sum (n |-> (0 qua Real)^2) by RVSUM_1:56 .= sqrt (n*(0 qua Nat)) by RVSUM_1:80 .= 0 by SQUARE_1:17; end; theorem Th94: |.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,Th89; then c = 0c by COMPLEX1:45; hence z.j = (n|->0c).j; end; hence thesis by FINSEQ_2:119; end; theorem Th95: 0 <= |.z.| proof 0 <= Sum sqr abs z by RVSUM_1:86; hence thesis by SQUARE_1:def 2; end; theorem |.-z.| = |.z.| by Th91; 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 Th92 .= 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 Th98: |.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,Th89; 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,Th89; 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,Th89; then |.c12.| <= abs1 + abs2 by A11,Th89; then |.c12.| <= abs12 by A11,A10,VALUED_1:def 1; then abs912 <= abs12 by A11,Th89; 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 Th99: |.z1 - z2.| <= |.z1.| + |.z2.| proof |.z1 - z2.| <= |.z1.| + |.-z2.| by Th98; hence thesis by Th91; end; theorem |.z1.| - |.z2.| <= |.z1 + z2.| proof z1 = z1 + z2 - z2 by Th79; then |.z1.| <= |.z1 + z2.| + |.z2.| by Th99; hence thesis by XREAL_1:20; end; theorem |.z1.| - |.z2.| <= |.z1 - z2.| proof z1 = z1 - z2 + z2 by Th81; then |.z1.| <= |.z1 - z2.| + |.z2.| by Th98; hence thesis by XREAL_1:20; end; theorem Th102: |.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 Th94; hence thesis by Th74; end; assume z1 = z2; then z1 - z2 = 0c n by Th73; hence thesis by Th93; end; theorem z1 <> z2 implies 0 < |.z1 - z2.| proof assume z1 <> z2; then 0 <> |.z1 - z2.| by Th102; hence thesis by Th95; end; theorem Th104: |.z1 - z2.| = |.z2 - z1.| proof thus |.z1 - z2.| = |.-(z2 - z1).| by Th71 .= |.z2 - z1.| by Th91; end; theorem Th105: |.z1 - z2.| <= |.z1 - z.| + |.z - z2.| proof |.z1 - z2.| = |.z1 - z + z - z2.| by Th81 .= |.(z1 - z) + (z - z2).| by Th76; hence thesis by Th98; end; definition let n; let A be Subset of COMPLEX n; attr A is open means :Def14: 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 proof let A be Subset of COMPLEX n; assume A1: A = {}; let x; thus thesis by A1; end; 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; take j=1; 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,Def14; 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,Def14; 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,Def14; 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 Th110: 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 Th104; hence thesis by A1; end; theorem 0 < r implies x in Ball(x,r) proof assume A1: 0 < r; |.x - x.| = 0 by Th102; 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 Th110; 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 Th75; then |.z1 - (x + z).| <= |.z.| + |.z1 - x.| by Th99; then |.z1 - (x + z).| < r + |.z1 - x.| by A2,XXREAL_0:2; hence thesis by Th110; 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) = |.x - $1.|; defpred P[set] means $1 in A; reconsider X = {f(z) : P[z]} as Subset of REAL from DOMAIN_1:sch 8; take lower_bound X; thus thesis; end; uniqueness proof deffunc f(Element of COMPLEX n) = |.x - $1.|; defpred P[set] means $1 in A; reconsider X = {f(z) : P[z]} as Subset of REAL from DOMAIN_1:sch 8; let r1,r2 be Real such that A1: for X being Subset of REAL st X = {|.x - z.| : z in A} holds r1 = lower_bound X and A2: for X being Subset of REAL st X = {|.x - z.| : z in A} holds r2 = lower_bound X; r1 = lower_bound X by A1; hence thesis by 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 Th113: 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 ext-real number 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 by XXREAL_2:def 9; now let r9 be real number; assume r9 > 0; then consider r1 be real number 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 Th114: A <> {} implies dist(x,A) >= 0 proof defpred P[set] means $1 in A; deffunc f(Element of COMPLEX n) = |.x - $1.|; reconsider X = {f(z) : P[z]} as Subset of REAL from DOMAIN_1:sch 8; assume A <> {}; then consider z1 such that A1: z1 in A by SUBSET_1:4; A2: |.x - z1.| in X by A1; A3: now let r9; assume r9 in X; then ex z st r9 = |.x - z.| & z in A; hence r9>= 0 by Th95; end; dist(x,A) = lower_bound X by Def17; hence thesis by A2,A3,Th113; end; theorem Th115: A <> {} implies dist(x + z,A) <= dist(x,A) + |.z.| proof defpred P[set] means $1 in A; deffunc g(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) = |.x - $1.|; A1: Y is bounded_below proof take 0; let r be ext-real number; assume r in Y; then ex z1 st r = |.x + z - z1 .| & z1 in A; hence thesis by Th95; end; reconsider X = {f(z1) : P[z1]} as Subset of REAL from DOMAIN_1:sch 8; assume A <> {}; then consider z2 such that A2: z2 in A by SUBSET_1:4; A3: dist(x+z,A) = lower_bound Y by Def17; A4: now let r9; assume r9 in X; then consider z3 such that A5: r9 = |.x - z3.| and A6: z3 in A; |.x + z - z3.| = |.x - z3 + z.| by Th76; then A7: |.x + z - z3.| <= r9 + |.z.| by A5,Th98; |.x + z - z3.| in Y by A6; then |.x + z - z3.| >= dist(x + z,A) by A3,A1,Def2; then r9+ |.z.| >= dist(x + z,A) by A7,XXREAL_0:2; hence r9 >= dist(x + z,A) - |.z.| by XREAL_1:20; end; A8: |.x - z2.| in X by A2; dist(x,A) = lower_bound X by Def17; then dist(x + z,A) - |.z.| <= dist(x,A) by A8,A4,Th113; hence thesis by XREAL_1:20; end; theorem Th116: x in A implies dist(x,A) = 0 proof defpred P[set] means $1 in A; deffunc f(Element of COMPLEX n) = |.x - $1.|; reconsider X = {f(z): P[z]} as Subset of REAL from DOMAIN_1:sch 8; assume A1: x in A; then A2: |.x - x.| in X; A3: now reconsider r = |.x - x.| as real number; let r1 be real number such that A4: 0 {} & 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,Th114; now deffunc f(Element of COMPLEX n) = |.x - $1.|; defpred P[set] means $1 in A; reconsider X = {f(z) : P[z]} as Subset of REAL from DOMAIN_1:sch 8; let r such that A6: r > 0; consider z such that A7: z in A by A2,SUBSET_1:4; A8: X is bounded_below proof take 0; let r be ext-real number; assume r in X; then ex z st r = |.x - z .| & z in A; hence thesis by Th95; end; A9: |.x - z.| in X by A7; dist(x,A) = lower_bound X & (0 qua Nat)+r = r by Def17; then consider r9 be real number such that A10: r9 in X and A11: r9< r by A5,A6,A9,A8,Def2; consider z1 such that A12: r9 = |.x - z1.| & z1 in A by A10; take z = z1 - x; thus |.z.| < r & x + z in A by A11,A12,Th80,Th104; end; hence contradiction by A1,A3; end; theorem A <> {} implies |.z1 - x.| + dist(x,A) >= dist(z1,A) proof x + (z1 - x) = z1 by Th80; hence thesis by Th115; end; theorem Th119: 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 Th120: 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,Th116; hence thesis by A1; end; theorem 0 < r implies A c= Ball(A,r) proof assume A1: r > 0; let x be set; assume x in A; hence thesis by A1,Th120; end; 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 Th119; 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,Th115; 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) = |.$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; take lower_bound X; thus thesis; end; uniqueness proof deffunc f(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; let r1,r2 be Real such that A1: for X being Subset of REAL st X = {|.x - z.| : x in A & z in B} holds r1 = lower_bound X and A2: for X being Subset of REAL st X = {|.x - z.| : x in A & z in B} holds r2 = lower_bound X; r1 = lower_bound X by A1; hence thesis by A2; end; end; theorem for X,Y being Subset of REAL holds X <> {} & Y <> {} implies X ++ Y <> {}; theorem Th124: 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 number such that A1: r1 is LowerBound of X by XXREAL_2:def 9; A2: for r be real number st r in X holds r1<=r by A1,XXREAL_2:def 2; assume Y is bounded_below; then consider r2 be real number such that A3: r2 is LowerBound of Y by XXREAL_2:def 9; A4: for r be real number st r in Y holds r2<=r by A3,XXREAL_2:def 2; take r1 + r2; let r be ext-real number; assume r in X++Y; then r in {r22+r12 where r22 is Element of COMPLEX, r12 is Element of COMPLEX : r22 in X & r12 in Y} by MEMBER_1:def 6; then consider r22,r12 being Element of COMPLEX such that A5: r = r22 + r12 and A6: r22 in X and A7: r12 in Y; reconsider r9 = r22, r99 = r12 as real number by A6,A7; A8: r2 <= r99 by A4,A7; r1 <= r9 by A2,A6; hence thesis by A5,A8,XREAL_1:7; end; theorem Th125: 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 number; assume 0 0 by XREAL_1:215; then consider r1 be real number such that A7: r1 in X and A8: 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,Th124; hence thesis by A11,A5,Def2; end; theorem Th126: 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,Th113; end; theorem Th127: 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.|; reconsider Z = {f(z1,z): P[z1,z]} as Subset of REAL from DOMAIN_1:sch 9; assume that A1: A <> {} and A2: B <> {}; consider z1 such that A3: z1 in A by A1,SUBSET_1:4; A4: now let r9; assume r9 in Z; then ex z1,z st r9 = |.z1 - z.| & z1 in A & z in B; hence r9>= 0 by Th95; end; consider z2 such that A5: z2 in B by A2,SUBSET_1:4; A6: dist(A,B) = lower_bound Z by Def19; |.z1 - z2.| in Z by A3,A5; hence thesis by A6,A4,Th113; 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) = |.$1 - $2.|; reconsider Y = {f(z,z1) : 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) : P[z1,z]} as Subset of REAL from DOMAIN_1:sch 9; A1: now let r; A2: now given z,z1 such that A3: r =|.z - z1.| & z in B & z1 in A; take z1,z; thus r =|.z1 - z.| & z1 in A & z in B by A3,Th104; end; now given z1,z such that A4: r =|.z1 - z.| & z1 in A & z in B; take z,z1; thus r =|.z - z1.| & z in B & z1 in A by A4,Th104; end; hence r in X iff r in Y by A2; end; dist(A,B) = lower_bound X & dist(B,A) = lower_bound Y by Def19; hence thesis by A1,SUBSET_1:3; end; theorem Th129: 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.|; reconsider Y = {g(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) = |.$1 - $2.|; reconsider X = {g(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 |.x - z2.| in Y by A3; hence Y <> {}; take 0; let r be ext-real number; assume r in Y; then ex z1 st r = |.x - z1 .| & z1 in B; hence thesis by Th95; end; A5: lower_bound X = dist(x,A) & lower_bound Y = dist(x,B) by Def17; A6: |.x - z2 .| in Y by A3; reconsider Z = {f(z1,z) : P[z1,z]} as Subset of REAL from DOMAIN_1:sch 9; consider z1 such that A7: z1 in A by A1,SUBSET_1:4; A8: now let r; assume r in X ++ Y; then r in {r2+r1 where r2 is Element of COMPLEX, r1 is Element of COMPLEX : r2 in X & r1 in Y} by MEMBER_1:def 6; then consider r2,r1 being Element of COMPLEX such that A9: r = r2 + r1 and A10: r2 in X and A11: r1 in Y; consider z2 such that A12: r1 = |.x - z2.| & z2 in B by A11; consider z1 such that A13: r2 = |.x - z1.| and A14: z1 in A by A10; take r3 = |.z1 - z2.|; r2 = |.z1 - x.| by A13,Th104; hence r3 in Z & r3 <= r by A9,A14,A12,Th105; end; A15: Z is bounded_below proof take 0; let r be ext-real number; assume r in Z; then ex z1,z st r = |.z1 - z .| & z1 in A & z in B; hence thesis by Th95; end; A16: X <> {} & X is bounded_below proof |.x - z1.| in X by A7; hence X <> {}; take 0; let r be ext-real number; assume r in X; then ex z st r = |.x - z .| & z in A; hence thesis by Th95; end; A17: lower_bound Z = dist(A,B) by Def19; A18: X++Y c= REAL by MEMBERED:3; |.x - z1.| in X by A7; then |.x - z1.| + |.x - z2 .| in X ++ Y by A6,MEMBER_1:46; then lower_bound (X ++ Y) >= lower_bound Z by A15,A8,Th126,A18; hence thesis by A16,A4,A5,A17,Th125; end; theorem A meets B implies dist(A,B) = 0 proof assume A meets B; then consider z being set 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,Th116; then (0 qua Nat) + (0 qua Nat) >= dist(A,B) by A1,A2,Th129; hence thesis by A1,A2,Th127; 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 set; 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 Element of 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 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 by A2,TARSKI:def 3; 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 number; let r be real number such that A10: 0x; 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 number 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 1(Lm7,Lm8); theorem Th133: 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 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 nm; hence thesis by A1,A2,SEQM_3:def 1; end; end; hence thesis; end; theorem Th139: v is increasing & v1 = v|Seg n implies v1 is increasing proof assume that A1: v is increasing and A2: v1 = v|Seg n; now per cases; suppose n<=len v; then Seg n c= Seg len v by FINSEQ_1:5; then A3: Seg n c= dom v by FINSEQ_1:def 3; then Seg n = dom v /\ Seg n by XBOOLE_1:28; then A4: dom v1 = Seg n by A2,RELAT_1:61; now let m,k such that A5: m in dom v1 & k in dom v1 and A6: m; 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: ku by TARSKI:def 1; s=u by A2,A3,A5,A6,A8,A10,A18,FINSEQ_1:42; hence rlen v1; then m {} by A2,CARD_1:27,RELAT_1:41; then A7: upper_bound(X) in X by Th133; 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 klen v2; then mn+1 by NAT_1:13; then x<>u by A2,A5,A16,A17,A20,A30,A32,A34,Th138; then not x in {u} by TARSKI:def 1; hence thesis by A34,A35,XBOOLE_0:def 5; end; let x; 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).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,FINSEQ_1:1; 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; 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; 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,Th138; then not x in {u} by TARSKI:def 1; hence thesis by A55,A56,XBOOLE_0:def 5; end; let x; 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).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,FINSEQ_1:1; 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,Th139; 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 1(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 ext-real number; 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 number st for t being real number st t in A \/ B holds t >= r1 holds r >= r1 proof let r1 be real number; assume A3: for t being real number st t in A \/ B holds t >= r1; now let t be real number; 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 number; 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 number st t in A \/ B holds t >= r proof let t be real number; 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 number st for t being real number st t in A \/ B holds t <= r1 holds r <= r1 proof let r1 be real number; assume A3: for t being real number st t in A \/ B holds t <= r1; now let t be real number; 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 number; 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 number st t in A \/ B holds t <= r proof let t be real number; 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 number st for r being real number st r in R holds r <= r0 holds upper_bound R <= r0 proof let R be non empty Subset of REAL,r0 be real number; assume A1: for r being real number st r in R holds r<=r0; then for r being ext-real number st r in R holds r<=r0; then r0 is UpperBound of R by XXREAL_2:def 1; then A2: R is bounded_above by XXREAL_2:def 10; now set r1=(upper_bound R) -r0; assume upper_bound R >r0; then r1>0 by XREAL_1:50; then ex r being real number st r in R & (upper_bound R)-r1