convergent for Complex_Sequence;
end;
canceled;
theorem
s is convergent implies lim(s*') = (lim s)*';
begin
registration
let s1,s2 be convergent Complex_Sequence;
cluster s1 + s2 -> convergent for Complex_Sequence;
end;
canceled;
theorem
for s,s9 being convergent Complex_Sequence
holds lim (s + s9)=(lim s)+ (lim s9);
canceled;
theorem
for s,s9 being convergent Complex_Sequence
holds lim (s + s9)*' = (lim s)*' + (lim s9)*';
registration
let s be convergent Complex_Sequence, c be complex number;
cluster c(#)s -> convergent for Complex_Sequence;
end;
canceled;
theorem
for s being convergent Complex_Sequence, r being complex number
holds lim(r(#)s)=r*(lim s);
canceled;
theorem
for s being convergent Complex_Sequence
holds lim (r(#)s)*' = (r*')*(lim s)*';
registration
let s be convergent Complex_Sequence;
cluster -s -> convergent for Complex_Sequence;
end;
canceled;
theorem
for s being convergent Complex_Sequence
holds lim(-s)=-(lim s);
canceled;
theorem
for s being convergent Complex_Sequence
holds lim (-s)*' = -(lim s)*';
registration
let s1,s2 be convergent Complex_Sequence;
cluster s1 - s2 -> convergent for Complex_Sequence;
end;
canceled;
theorem
for s,s9 being convergent Complex_Sequence
holds lim(s - s9)=(lim s)-( lim s9);
canceled;
theorem
for s,s9 being convergent Complex_Sequence
holds lim (s - s9)*' = (lim s)*' - (lim s9)*';
registration
cluster convergent -> bounded for Complex_Sequence;
end;
registration
cluster non bounded -> non convergent for Complex_Sequence;
end;
registration
let s1,s2 be convergent Complex_Sequence;
cluster s1 (#) s2 -> convergent for Complex_Sequence;
end;
canceled;
theorem
for s,s9 being convergent Complex_Sequence
holds lim(s(#)s9)=(lim s)*(lim s9);
canceled;
theorem
for s,s9 being convergent Complex_Sequence
holds lim (s(#)s9)*' = (lim s)*' * (lim s9)*';
theorem
for s being convergent Complex_Sequence st lim s <> 0c
ex n st for m st n <=m holds |.(lim s).|/2<|.s.m.|;
theorem
for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero
holds s" is convergent;
theorem
s is convergent & (lim s)<>0c & s is non-zero implies lim s"=( lim s)";
canceled;
theorem
s is convergent & (lim s)<>0c & s is non-zero implies lim (s")*' = ((
lim s)*')";
theorem
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies s9/"s is convergent;
theorem
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies lim(s9/"s)=(lim s9)/(lim s);
canceled;
theorem
s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero
implies lim (s9/"s)*' = ((lim s9)*')/((lim s)*');
theorem
s is convergent & s1 is bounded & (lim s)=0c implies s(#)s1 is convergent;
theorem
s is convergent & s1 is bounded & (lim s)=0c implies lim(s(#)s1) =0c;
canceled;
theorem
s is convergent & s1 is bounded & (lim s)=0c implies lim (s(#)s1)*' = 0c;
begin
reserve n,n1,n2,m for Element of NAT,
r,r1,r2,p,g1,g2,g for real number,
seq,seq9,seq1 for Real_Sequence,
y for set;
theorem
-g

Real;
end;
registration
cluster constant -> convergent for Real_Sequence;
end;
registration
cluster constant for Real_Sequence;
end;
theorem
seq is convergent & seq9 is convergent implies seq + seq9 is convergent;
registration
let seq1,seq2 be convergent Real_Sequence;
cluster seq1 + seq2 -> convergent for Real_Sequence;
end;
theorem
seq is convergent & seq9 is convergent implies
lim (seq + seq9)=(lim seq)+(lim seq9);
theorem
seq is convergent implies r(#)seq is convergent;
registration
let r be real number;
let seq be convergent Real_Sequence;
cluster r(#)seq -> convergent for Real_Sequence;
end;
theorem
seq is convergent implies lim(r(#)seq)=r*(lim seq);
theorem
seq is convergent implies -seq is convergent;
registration
let seq be convergent Real_Sequence;
cluster -seq -> convergent for Real_Sequence;
end;
theorem
seq is convergent implies lim(-seq) = -(lim seq);
theorem
seq is convergent & seq9 is convergent implies seq - seq9 is convergent;
registration
let seq1,seq2 be convergent Real_Sequence;
cluster seq1 - seq2 -> convergent for Real_Sequence;
end;
theorem
seq is convergent & seq9 is convergent implies
lim(seq - seq9)=(lim seq)-(lim seq9);
theorem
seq is convergent implies seq is bounded;
registration
cluster convergent -> bounded for Real_Sequence;
end;
theorem
seq is convergent & seq9 is convergent implies seq (#) seq9 is convergent;
registration
let seq1,seq2 be convergent Real_Sequence;
cluster seq1 (#) seq2 -> convergent for Real_Sequence;
end;
theorem
seq is convergent & seq9 is convergent implies
lim(seq(#)seq9)=(lim seq)*(lim seq9);
theorem
seq is convergent implies (lim seq<>0 implies
ex n st for m st n<=m holds abs(lim seq)/2~~1 iff ex m st n=m+1 & m>0;
theorem
for f being FinSequence,n,m,k st len f = m+1 & n in dom f & k in
Seg m holds Del(f,n).k = f.k or Del(f,n).k = f.(k+1);
definition
let f be FinSequence;
redefine attr f is constant means
for n,m st n in dom f & m in dom f holds f.n=f.m;
end;
registration
cluster -> real-valued for FinSequence of REAL;
end;
registration
cluster non empty increasing for FinSequence of REAL;
end;
registration
cluster constant for FinSequence of REAL;
end;
theorem
v<>{} & rng v c= Seg n & v.(len v) = n & (for k st 1<=k & k<=len
v - 1 holds for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s) & i in
Seg n & i+1 in Seg n & m in dom v & v.m = i & (for k st k in dom v & v.k = i
holds k<=m) implies m+1 in dom v & v.(m+1)=i+1;
theorem
v<>{} & rng v c= Seg n & v.1 = 1 & v.(len v) = n & (for k st 1<=k & k
<=len v - 1 holds for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s)
implies (for i st i in Seg n ex k st k in dom v & v.k = i) & for m,k,i,r st m
in dom v & v.m = i & (for j st j in dom v & v.j = i holds j<=m) & m~~* Subset of REAL;
end;
theorem
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
(for r st r in X holds r<=it) & for s st 0 real number means
(for r st r in X holds it<=r) & for s st 0 Real;
redefine func lower_bound X -> Real;
end;
theorem
lower_bound {r} = r & upper_bound {r} = r;
theorem
lower_bound {r} = upper_bound {r};
theorem
X is real-bounded non empty implies lower_bound X <= upper_bound X;
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);
theorem
seq is convergent implies abs seq is convergent;
registration
let seq be convergent Real_Sequence;
cluster abs seq -> convergent for Real_Sequence;
end;
theorem
seq is convergent implies lim abs seq = abs lim seq;
theorem
abs seq is convergent & lim abs seq=0 implies seq is convergent & lim seq=0;
theorem
seq1 is subsequence of seq & seq is convergent implies seq1 is convergent;
theorem
seq1 is subsequence of seq & seq is convergent implies lim seq1= lim seq;
theorem
seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n)
implies seq1 is convergent;
theorem
seq is convergent & (ex k st for n st k<=n holds seq1.n=seq.n) implies
lim seq=lim seq1;
registration
cluster constant -> convergent for Real_Sequence;
end;
registration
cluster constant for Real_Sequence;
end;
registration
let seq be convergent Real_Sequence;
let k;
cluster seq ^\ k -> convergent for Real_Sequence;
end;
theorem
seq is convergent implies lim (seq^\k)=lim seq;
theorem
seq^\k is convergent implies seq is convergent;
theorem
seq^\k is convergent implies lim seq = lim (seq^\k);
theorem
seq is convergent & lim seq<>0 implies ex k st (seq ^\k) is non-zero;
theorem
seq is convergent & lim seq<>0 implies ex seq1 st seq1 is subsequence
of seq & seq1 is non-zero;
theorem
seq is constant & (r in rng seq or ex n st seq.n=r ) implies lim seq=r;
theorem
seq is constant implies for n holds lim seq=seq.n;
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)";
theorem
0<=r & (for n holds seq.n=1/(n+r)) implies seq is convergent;
theorem
0<=r & (for n holds seq.n=1/(n+r)) implies lim seq=0;
theorem
(for n holds seq.n=1/(n+1)) implies seq is convergent & lim seq=0;
theorem
0<=r & (for n holds seq.n=g/(n+r)) implies seq is convergent & lim seq =0;
theorem
0<=r & (for n holds seq.n=1/(n*n+r)) implies seq is convergent;
theorem
0<=r & (for n holds seq.n=1/(n*n+r)) implies lim seq=0;
theorem
(for n holds seq.n=1/(n*n+1)) implies seq is convergent & lim seq=0;
theorem
0<=r & (for n holds seq.n=g/(n*n+r)) implies seq is convergent & lim seq=0;
registration
cluster non-decreasing bounded_above -> convergent for Real_Sequence;
end;
registration
cluster non-increasing bounded_below -> convergent for Real_Sequence;
end;
registration
cluster monotone bounded -> convergent for Real_Sequence;
end;
theorem
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;
theorem
seq is bounded_below & seq is non-increasing implies for n holds lim
seq <= seq.n;
theorem
for seq ex Nseq st seq*Nseq is monotone;
theorem
seq is bounded implies ex seq1 st seq1 is subsequence of seq &
seq1 is convergent;
theorem
seq is convergent iff for s st 0= t holds lower_bound X >= t;
theorem
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
;
theorem
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;
theorem
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;
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;
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;
definition
let A be non empty natural-membered set;
redefine func min A -> Element of NAT;
end;
begin
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;
theorem
compcomplex is_an_inverseOp_wrt addcomplex;
theorem
addcomplex is having_an_inverseOp;
theorem
the_inverseOp_wrt addcomplex = compcomplex;
definition
redefine func diffcomplex equals
addcomplex*(id COMPLEX,compcomplex);
end;
theorem
1r is_a_unity_wrt multcomplex;
theorem
multcomplex is_distributive_wrt addcomplex;
definition let c be complex number;
func c multcomplex -> UnOp of COMPLEX equals
multcomplex[;](c,id COMPLEX);
end;
theorem
(c multcomplex).c9 = c*c9;
theorem
c multcomplex is_distributive_wrt addcomplex;
definition
func abscomplex -> Function of COMPLEX,REAL means
for c holds it.c = |.c.|;
end;
reserve z,z1,z2 for FinSequence of COMPLEX;
definition let z1,z2;
redefine func z1 + z2 -> FinSequence of COMPLEX equals
addcomplex.:(z1,z2);
redefine func z1 - z2 -> FinSequence of COMPLEX equals
diffcomplex.:(z1,z2);
end;
definition let z;
redefine func -z -> FinSequence of COMPLEX equals
compcomplex*z;
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;
end;
definition let z;
redefine func abs z -> FinSequence of REAL equals
abscomplex*z;
end;
definition let n;
func COMPLEX n -> FinSequenceSet of COMPLEX equals
n-tuples_on COMPLEX;
end;
registration let n;
cluster COMPLEX n -> non empty;
end;
reserve x,z,z1,z2,z3 for Element of COMPLEX n,
A,B for Subset of COMPLEX n;
theorem
k in Seg n implies z.k in COMPLEX;
definition let n,z1,z2;
redefine func z1 + z2 -> Element of COMPLEX n;
end;
theorem
k in Seg n & c1 = z1.k & c2 = z2.k implies (z1 + z2).k = c1 + c2;
definition let n;
func 0c n -> FinSequence of COMPLEX equals
n |-> 0c;
end;
definition let n;
redefine func 0c n -> Element of COMPLEX n;
end;
theorem
z + 0c n = z & z = 0c n + z;
definition let n,z;
redefine func -z -> Element of COMPLEX n;
end;
theorem
k in Seg n & c = z.k implies (-z).k = -c;
theorem
z + -z = 0c n & -z + z = 0c n;
theorem
z1 + z2 = 0c n implies z1 = -z2 & z2 = -z1
;
canceled;
theorem
-z1 = -z2 implies z1 = z2;
theorem
z1 + z = z2 + z or z1 + z = z + z2 implies z1 = z2;
theorem
-(z1 + z2) = -z1 + -z2;
definition let n,z1,z2;
redefine func z1 - z2 -> Element of COMPLEX n;
end;
theorem
k in Seg n implies (z1 - z2).k = z1.k - z2.k;
theorem
z - 0c n = z;
theorem
0c n - z = -z;
theorem
z1 - -z2 = z1 + z2;
theorem
-(z1 - z2) = z2 - z1;
theorem
-(z1 - z2) = -z1 + z2;
theorem
z - z = 0c n;
theorem
z1 - z2 = 0c n implies z1 = z2;
theorem
z1 - z2 - z3 = z1 - (z2 + z3);
theorem
z1 + (z2 - z3) = z1 + z2 - z3;
theorem
z1 - (z2 - z3) = z1 - z2 + z3;
theorem
z1 - z2 + z3 = z1 + z3 - z2;
theorem
z1 = z1 + z - z;
theorem
z1 + (z2 - z1) = z2;
theorem
z1 = z1 - z + z;
definition let n,z,c;
redefine func c*z -> Element of COMPLEX n;
end;
theorem
k in Seg n & c9 = z.k implies (c*z).k = c*c9;
theorem
c1*(c2*z) = (c1*c2)*z;
theorem
(c1 + c2)*z = c1*z + c2*z;
theorem
c*(z1+z2) = c*z1 + c*z2;
theorem
1r*z = z;
theorem
0c*z = 0c n;
theorem
(-1r)*z = -z;
definition let n,z;
redefine func abs z -> Element of n-tuples_on REAL;
end;
theorem
k in Seg n & c = z.k implies (abs z).k = |.c.|;
theorem
abs 0c n = n |-> 0;
theorem
abs -z = abs z;
theorem
abs(c*z) = |.c.|*(abs z);
definition
let z be FinSequence of COMPLEX;
func |.z.| -> Real equals
sqrt Sum sqr abs z;
end;
theorem
|.0c n.| = 0;
theorem
|.z.| = 0 implies z = 0c n;
theorem
0 <= |.z.|;
theorem
|.-z.| = |.z.|;
theorem
|.c*z.| = |.c.|*|.z.|;
theorem
|.z1 + z2.| <= |.z1.| + |.z2.|;
theorem
|.z1 - z2.| <= |.z1.| + |.z2.|;
theorem
|.z1.| - |.z2.| <= |.z1 + z2.|;
theorem
|.z1.| - |.z2.| <= |.z1 - z2.|;
theorem
|.z1 - z2.| = 0 iff z1 = z2;
theorem
z1 <> z2 implies 0 < |.z1 - z2.|;
theorem
|.z1 - z2.| = |.z2 - z1.|;
theorem
|.z1 - z2.| <= |.z1 - z.| + |.z - z2.|;
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;
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;
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;
definition
let n,x,r;
func Ball(x,r) -> Subset of COMPLEX n equals
{ z : |.z - x.| < r };
end;
theorem
z in Ball(x,r) iff |.x - z.| < r;
theorem
0 < r implies x in Ball(x,r);
theorem
Ball(z1,r1) is open;
definition let n,x,A;
func dist(x,A) -> Real means
for X being Subset of REAL st X = {|.x
- z.| : z in A} holds it = lower_bound X;
end;
definition let n,A,r;
func Ball(A,r) -> Subset of COMPLEX n equals
{ z : dist(z,A) < r };
end;
theorem
for X being Subset of REAL, r st X <> {} & for r9 st r9 in X
holds r <= r9 holds lower_bound X >= r;
theorem
A <> {} implies dist(x,A) >= 0;
theorem
A <> {} implies dist(x + z,A) <= dist(x,A) + |.z.|;
theorem
x in A implies dist(x,A) = 0;
theorem
not x in A & A <> {} & A is closed implies dist(x,A) > 0;
theorem
A <> {} implies |.z1 - x.| + dist(x,A) >= dist(z1,A);
theorem
z in Ball(A,r) iff dist(z,A) < r;
theorem
0 < r & x in A implies x in Ball(A,r);
theorem
0 < r implies A c= Ball(A,r);
theorem
A <> {} implies Ball(A,r1) is open;
definition
let n,A,B;
func dist(A,B) -> Real means
for X being Subset of REAL st X = {|.x
- z.| : x in A & z in B} holds it = lower_bound X;
end;
theorem
for X,Y being Subset of REAL holds X <> {} & Y <> {} implies X ++ Y <> {};
theorem
for X,Y being Subset of REAL holds X is bounded_below &
Y is bounded_below implies X++Y is bounded_below;
theorem
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;
theorem
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;
theorem
A <> {} & B <> {} implies dist(A,B) >= 0;
theorem
dist(A,B) = dist(B,A);
theorem
A <> {} & B <> {} implies dist(x,A) + dist(x,B) >= dist(A,B);
theorem
A meets B implies dist(A,B) = 0;
definition
let n;
func ComplexOpenSets(n) -> Subset-Family of COMPLEX n equals
{A where A is
Subset of COMPLEX n: A is open};
end;
theorem
for A being Subset of COMPLEX n holds A in ComplexOpenSets n iff A is open;
theorem
for A being Subset of COMPLEX n holds A is closed iff A` is open;
begin
reserve
v,v1,v2 for FinSequence of REAL,
n,m,k for Element of NAT,
x for set;
theorem
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;
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;
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;
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;
theorem
v is increasing implies for n,m st n in dom v & m in dom v & n<=m
holds v.n <= v.m;
theorem
v is increasing implies for n,m st n in dom v & m in dom v & n<>
m holds v.n<>v.m;
theorem
v is increasing & v1 = v|Seg n implies v1 is increasing;
theorem
for v holds ex v1 st rng v1 = rng v & len v1 = card rng v & v1 is
increasing;
theorem
for v1,v2 st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2
is increasing holds v1 = v2;
definition
let v;
func Incr(v) ->increasing FinSequence of REAL means
rng it = rng v & len it = card rng v;
end;
registration
let v be non empty FinSequence of REAL;
cluster Incr v -> non empty;
end;
registration
cluster non empty bounded_above bounded_below for Subset of REAL;
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);
theorem
for A,B being non empty bounded_above Subset of REAL holds upper_bound(A
\/ B) = max(upper_bound A,upper_bound B);
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;
begin
reserve n,n1,m,k for Element of NAT;
reserve x,y for set;
reserve s,g,g1,g2,r,p,q,t for real number;
reserve s1,s2,s3 for Real_Sequence;
reserve Nseq for increasing sequence of NAT;
reserve X for Subset of REAL;
definition
let g,s be real number;
redefine func [. g,s .] -> Subset of REAL equals
{r where r is Real: g<=r &
r<=s };
end;
definition
let g,s be ext-real number;
redefine func ]. g,s .[ -> Subset of REAL equals
{r where r is Real : g*