:: Complex Spaces
:: by Czes{\l}aw Byli\'nski and Andrzej Trybulec
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users


theorem :: COMPLSP1:1
canceled;

theorem :: COMPLSP1:2
canceled;

theorem :: COMPLSP1:3
0c is_a_unity_wrt addcomplex by BINOP_2:1, SETWISEO:22;

theorem :: COMPLSP1:4
canceled;

theorem :: COMPLSP1:5
canceled;

theorem Th6: :: COMPLSP1:6
compcomplex is_an_inverseOp_wrt addcomplex
proof end;

theorem Th7: :: COMPLSP1:7
addcomplex is having_an_inverseOp by Th6, FINSEQOP:def 2;

theorem Th8: :: COMPLSP1:8
the_inverseOp_wrt addcomplex = compcomplex by Th6, Th7, FINSEQOP:def 3;

definition
canceled;
canceled;
redefine func diffcomplex equals :: COMPLSP1:def 3
addcomplex * (id COMPLEX ),compcomplex ;
compatibility
for b1 being Relation of [:COMPLEX ,COMPLEX :], COMPLEX holds
( b1 = diffcomplex iff b1 = addcomplex * (id COMPLEX ),compcomplex )
proof end;
end;

:: deftheorem COMPLSP1:def 1 :
canceled;

:: deftheorem COMPLSP1:def 2 :
canceled;

:: deftheorem defines diffcomplex COMPLSP1:def 3 :
diffcomplex = addcomplex * (id COMPLEX ),compcomplex ;

theorem :: COMPLSP1:9
canceled;

theorem :: COMPLSP1:10
canceled;

theorem :: COMPLSP1:11
canceled;

theorem :: COMPLSP1:12
1r is_a_unity_wrt multcomplex by BINOP_2:6, SETWISEO:22;

theorem :: COMPLSP1:13
canceled;

theorem :: COMPLSP1:14
canceled;

theorem Th15: :: COMPLSP1:15
multcomplex is_distributive_wrt addcomplex
proof end;

definition
let c be complex number ;
canceled;
func c multcomplex -> UnOp of COMPLEX equals :: COMPLSP1:def 5
multcomplex [;] c,(id COMPLEX );
coherence
multcomplex [;] c,(id COMPLEX ) is UnOp of COMPLEX
proof end;
end;

:: deftheorem COMPLSP1:def 4 :
canceled;

:: deftheorem defines multcomplex COMPLSP1:def 5 :
for c being complex number holds c multcomplex = multcomplex [;] c,(id COMPLEX );

Lm1: for c, c' being Element of COMPLEX holds (multcomplex [;] c,(id COMPLEX )) . c' = c * c'
proof end;

theorem :: COMPLSP1:16
for c, c' being Element of COMPLEX holds (c multcomplex ) . c' = c * c' by Lm1;

theorem :: COMPLSP1:17
for c being Element of COMPLEX holds c multcomplex is_distributive_wrt addcomplex by Th15, FINSEQOP:55;

definition
func abscomplex -> Function of COMPLEX , REAL means :Def6: :: COMPLSP1:def 6
for c being Element of COMPLEX holds it . c = |.c.|;
existence
ex b1 being Function of COMPLEX , REAL st
for c being Element of COMPLEX holds b1 . c = |.c.| from FUNCT_2:sch 4();
uniqueness
for b1, b2 being Function of COMPLEX , REAL st ( for c being Element of COMPLEX holds b1 . c = |.c.| ) & ( for c being Element of COMPLEX holds b2 . c = |.c.| ) holds
b1 = b2 from BINOP_2:sch 1();
end;

:: deftheorem Def6 defines abscomplex COMPLSP1:def 6 :
for b1 being Function of COMPLEX , REAL holds
( b1 = abscomplex iff for c being Element of COMPLEX holds b1 . c = |.c.| );

definition
let z1, z2 be FinSequence of COMPLEX ;
:: original: +
redefine func z1 + z2 -> FinSequence of COMPLEX equals :: COMPLSP1:def 7
addcomplex .: z1,z2;
coherence
z1 + z2 is FinSequence of COMPLEX
proof end;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = z1 + z2 iff b1 = addcomplex .: z1,z2 )
proof end;
:: original: -
redefine func z1 - z2 -> FinSequence of COMPLEX equals :: COMPLSP1:def 8
diffcomplex .: z1,z2;
coherence
z1 - z2 is FinSequence of COMPLEX
proof end;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = z1 - z2 iff b1 = diffcomplex .: z1,z2 )
proof end;
end;

:: deftheorem defines + COMPLSP1:def 7 :
for z1, z2 being FinSequence of COMPLEX holds z1 + z2 = addcomplex .: z1,z2;

:: deftheorem defines - COMPLSP1:def 8 :
for z1, z2 being FinSequence of COMPLEX holds z1 - z2 = diffcomplex .: z1,z2;

definition
let z be FinSequence of COMPLEX ;
:: original: -
redefine func - z -> FinSequence of COMPLEX equals :: COMPLSP1:def 9
compcomplex * z;
coherence
- z is FinSequence of COMPLEX
proof end;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = - z iff b1 = compcomplex * z )
proof end;
end;

:: deftheorem defines - COMPLSP1:def 9 :
for z being FinSequence of COMPLEX holds - z = compcomplex * z;

notation
let z be FinSequence of COMPLEX ;
let c be complex number ;
synonym c * z for c (#) z;
end;

definition
let z be FinSequence of COMPLEX ;
let c be complex number ;
:: original: *
redefine func c * z -> FinSequence of COMPLEX equals :: COMPLSP1:def 10
(c multcomplex ) * z;
coherence
c * z is FinSequence of COMPLEX
proof end;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = c * z iff b1 = (c multcomplex ) * z )
proof end;
end;

:: deftheorem defines * COMPLSP1:def 10 :
for z being FinSequence of COMPLEX
for c being complex number holds c * z = (c multcomplex ) * z;

definition
let z be FinSequence of COMPLEX ;
:: original: |.
redefine func abs z -> FinSequence of REAL equals :: COMPLSP1:def 11
abscomplex * z;
coherence
|.z.| is FinSequence of REAL
proof end;
compatibility
for b1 being FinSequence of REAL holds
( b1 = |.z.| iff b1 = abscomplex * z )
proof end;
end;

:: deftheorem defines abs COMPLSP1:def 11 :
for z being FinSequence of COMPLEX holds abs z = abscomplex * z;

definition
let n be Element of NAT ;
func COMPLEX n -> FinSequence-DOMAIN of COMPLEX equals :: COMPLSP1:def 12
n -tuples_on COMPLEX ;
correctness
coherence
n -tuples_on COMPLEX is FinSequence-DOMAIN of COMPLEX ;
;
end;

:: deftheorem defines COMPLEX COMPLSP1:def 12 :
for n being Element of NAT holds COMPLEX n = n -tuples_on COMPLEX ;

registration
let n be Element of NAT ;
cluster COMPLEX n -> ;
coherence
not COMPLEX n is empty ;
end;

Lm2: for n being Element of NAT
for z being Element of COMPLEX n holds dom z = Seg n
proof end;

theorem :: COMPLSP1:18
canceled;

theorem :: COMPLSP1:19
canceled;

theorem :: COMPLSP1:20
canceled;

theorem Th21: :: COMPLSP1:21
for k, n being Element of NAT
for z being Element of COMPLEX n st k in Seg n holds
z . k in COMPLEX
proof end;

definition
let n be Element of NAT ;
let z1, z2 be Element of COMPLEX n;
:: original: +
redefine func z1 + z2 -> Element of COMPLEX n;
coherence
z1 + z2 is Element of COMPLEX n by FINSEQ_2:140;
end;

theorem :: COMPLSP1:22
canceled;

theorem :: COMPLSP1:23
canceled;

theorem Th24: :: COMPLSP1:24
for k, n being Element of NAT
for c1, c2 being Element of COMPLEX
for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds
(z1 + z2) . k = c1 + c2
proof end;

definition
let n be Element of NAT ;
func 0c n -> FinSequence of COMPLEX equals :: COMPLSP1:def 13
n |-> 0c ;
correctness
coherence
n |-> 0c is FinSequence of COMPLEX ;
;
end;

:: deftheorem defines 0c COMPLSP1:def 13 :
for n being Element of NAT holds 0c n = n |-> 0c ;

definition
let n be Element of NAT ;
:: original: 0c
redefine func 0c n -> Element of COMPLEX n;
coherence
0c n is Element of COMPLEX n ;
end;

theorem :: COMPLSP1:25
canceled;

theorem :: COMPLSP1:26
canceled;

theorem :: COMPLSP1:27
canceled;

theorem :: COMPLSP1:28
for n being Element of NAT
for z being Element of COMPLEX n holds
( z + (0c n) = z & z = (0c n) + z ) by BINOP_2:1, FINSEQOP:57;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
:: original: -
redefine func - z -> Element of COMPLEX n;
coherence
- z is Element of COMPLEX n by FINSEQ_2:133;
end;

theorem Th29: :: COMPLSP1:29
for k, n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(- z) . k = - c
proof end;

Lm3: for n being Element of NAT holds - (0c n) = 0c n
proof end;

theorem :: COMPLSP1:30
for n being Element of NAT
for z being Element of COMPLEX n holds
( z + (- z) = 0c n & (- z) + z = 0c n ) by Th7, Th8, BINOP_2:1, FINSEQOP:77;

theorem :: COMPLSP1:31
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 + z2 = 0c n holds
( z1 = - z2 & z2 = - z1 ) by Th7, Th8, BINOP_2:1, FINSEQOP:78;

theorem :: COMPLSP1:32
for n being Element of NAT
for z being Element of COMPLEX n holds - (- z) = z ;

theorem :: COMPLSP1:33
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st - z1 = - z2 holds
z1 = z2
proof end;

Lm4: for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
proof end;

theorem :: COMPLSP1:34
for n being Element of NAT
for z1, z, z2 being Element of COMPLEX n st ( z1 + z = z2 + z or z1 + z = z + z2 ) holds
z1 = z2 by Lm4;

theorem Th35: :: COMPLSP1:35
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2)
proof end;

definition
let n be Element of NAT ;
let z1, z2 be Element of COMPLEX n;
:: original: -
redefine func z1 - z2 -> Element of COMPLEX n;
coherence
z1 - z2 is Element of COMPLEX n by FINSEQ_2:140;
end;

theorem :: COMPLSP1:36
for k, n being Element of NAT
for c1, c2 being Element of COMPLEX
for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds
(z1 - z2) . k = c1 - c2
proof end;

theorem :: COMPLSP1:37
canceled;

theorem :: COMPLSP1:38
for n being Element of NAT
for z being Element of COMPLEX n holds z - (0c n) = z
proof end;

theorem :: COMPLSP1:39
for n being Element of NAT
for z being Element of COMPLEX n holds (0c n) - z = - z
proof end;

theorem :: COMPLSP1:40
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds z1 - (- z2) = z1 + z2 ;

theorem Th41: :: COMPLSP1:41
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = z2 - z1
proof end;

theorem Th42: :: COMPLSP1:42
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = (- z1) + z2
proof end;

theorem Th43: :: COMPLSP1:43
for n being Element of NAT
for z being Element of COMPLEX n holds z - z = 0c n
proof end;

theorem Th44: :: COMPLSP1:44
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 - z2 = 0c n holds
z1 = z2
proof end;

theorem Th45: :: COMPLSP1:45
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) - z3 = z1 - (z2 + z3)
proof end;

theorem Th46: :: COMPLSP1:46
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 - z3) = (z1 + z2) - z3
proof end;

theorem :: COMPLSP1:47
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds z1 - (z2 - z3) = (z1 - z2) + z3
proof end;

theorem :: COMPLSP1:48
for n being Element of NAT
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) + z3 = (z1 + z3) - z2 by Th46;

theorem Th49: :: COMPLSP1:49
for n being Element of NAT
for z1, z being Element of COMPLEX n holds z1 = (z1 + z) - z
proof end;

theorem Th50: :: COMPLSP1:50
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds z1 + (z2 - z1) = z2
proof end;

theorem Th51: :: COMPLSP1:51
for n being Element of NAT
for z1, z being Element of COMPLEX n holds z1 = (z1 - z) + z
proof end;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
let c be Element of COMPLEX ;
:: original: *
redefine func c * z -> Element of COMPLEX n;
coherence
c * z is Element of COMPLEX n by FINSEQ_2:133;
end;

theorem Th52: :: COMPLSP1:52
for k, n being Element of NAT
for c', c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c' = z . k holds
(c * z) . k = c * c'
proof end;

theorem :: COMPLSP1:53
for n being Element of NAT
for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z
proof end;

theorem :: COMPLSP1:54
for n being Element of NAT
for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)
proof end;

theorem :: COMPLSP1:55
for n being Element of NAT
for c being Element of COMPLEX
for z1, z2 being Element of COMPLEX n holds c * (z1 + z2) = (c * z1) + (c * z2) by Th15, FINSEQOP:52, FINSEQOP:55;

theorem :: COMPLSP1:56
for n being Element of NAT
for z being Element of COMPLEX n holds 1r * z = z
proof end;

theorem :: COMPLSP1:57
for n being Element of NAT
for z being Element of COMPLEX n holds 0c * z = 0c n
proof end;

theorem :: COMPLSP1:58
for n being Element of NAT
for z being Element of COMPLEX n holds (- 1r ) * z = - z ;

definition
let n be Element of NAT ;
let z be Element of COMPLEX n;
:: original: |.
redefine func abs z -> Element of n -tuples_on REAL ;
correctness
coherence
|.z.| is Element of n -tuples_on REAL ;
by FINSEQ_2:133;
end;

theorem Th59: :: COMPLSP1:59
for k, n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n st k in Seg n & c = z . k holds
(abs z) . k = |.c.|
proof end;

theorem Th60: :: COMPLSP1:60
for n being Element of NAT holds abs (0c n) = n |-> 0
proof end;

theorem Th61: :: COMPLSP1:61
for n being Element of NAT
for z being Element of COMPLEX n holds abs (- z) = abs z
proof end;

theorem Th62: :: COMPLSP1:62
for n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)
proof end;

definition
let z be FinSequence of COMPLEX ;
func |.z.| -> Real equals :: COMPLSP1:def 14
 sqrt (Sum (sqr (abs z)));
correctness
coherence
sqrt (Sum (sqr (abs z))) is Real;
;
end;

:: deftheorem defines |. COMPLSP1:def 14 :
for z being FinSequence of COMPLEX holds |.z.| = sqrt (Sum (sqr (abs z)));

theorem Th63: :: COMPLSP1:63
for n being Element of NAT holds |.(0c n).| = 0
proof end;

theorem Th64: :: COMPLSP1:64
for n being Element of NAT
for z being Element of COMPLEX n st |.z.| = 0 holds
z = 0c n
proof end;

theorem Th65: :: COMPLSP1:65
for n being Element of NAT
for z being Element of COMPLEX n holds 0 <= |.z.|
proof end;

theorem :: COMPLSP1:66
for n being Element of NAT
for z being Element of COMPLEX n holds |.(- z).| = |.z.| by Th61;

theorem :: COMPLSP1:67
for n being Element of NAT
for c being Element of COMPLEX
for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|
proof end;

Lm5: for i, j being Element of NAT
for t being Element of i -tuples_on REAL st j in Seg i holds
t . j is Real
proof end;

theorem Th68: :: COMPLSP1:68
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 + z2).| <= |.z1.| + |.z2.|
proof end;

theorem Th69: :: COMPLSP1:69
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.|
proof end;

theorem :: COMPLSP1:70
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 + z2).|
proof end;

theorem :: COMPLSP1:71
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 - z2).|
proof end;

theorem Th72: :: COMPLSP1:72
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
proof end;

theorem Th73: :: COMPLSP1:73
for n being Element of NAT
for z1, z2 being Element of COMPLEX n st z1 <> z2 holds
0 < |.(z1 - z2).|
proof end;

theorem Th74: :: COMPLSP1:74
for n being Element of NAT
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| = |.(z2 - z1).|
proof end;

theorem Th75: :: COMPLSP1:75
for n being Element of NAT
for z1, z2, z being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
proof end;

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
attr A is open means :Def15: :: COMPLSP1:def 15
for x being Element of COMPLEX n st x in A holds
ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) );
end;

:: deftheorem Def15 defines open COMPLSP1:def 15 :
for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is open iff for x being Element of COMPLEX n st x in A holds
ex r being Real st
( 0 < r & ( for z being Element of COMPLEX n st |.z.| < r holds
x + z in A ) ) );

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
attr A is closed means :: COMPLSP1:def 16
for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A;
end;

:: deftheorem defines closed COMPLSP1:def 16 :
for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is closed iff for x being Element of COMPLEX n st ( for r being Real st r > 0 holds
ex z being Element of COMPLEX n st
( |.z.| < r & x + z in A ) ) holds
x in A );

theorem :: COMPLSP1:76
for n being Element of NAT
for A being Subset of (COMPLEX n) st A = {} holds
A is open
proof end;

theorem Th77: :: COMPLSP1:77
for n being Element of NAT
for A being Subset of (COMPLEX n) st A = COMPLEX n holds
A is open
proof end;

theorem Th78: :: COMPLSP1:78
for n being Element of NAT
for AA being Subset-Family of (COMPLEX n) st ( for A being Subset of (COMPLEX n) st A in AA holds
A is open ) holds
for A being Subset of (COMPLEX n) st A = union AA holds
A is open
proof end;

theorem Th79: :: COMPLSP1:79
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A is open & B is open holds
for C being Subset of (COMPLEX n) st C = A /\ B holds
C is open
proof end;

definition
let n be Element of NAT ;
let x be Element of COMPLEX n;
let r be Real;
func Ball x,r -> Subset of (COMPLEX n) equals :: COMPLSP1:def 17
{ z where z is Element of COMPLEX n : |.(z - x).| < r } ;
coherence
{ z where z is Element of COMPLEX n : |.(z - x).| < r } is Subset of (COMPLEX n)
proof end;
end;

:: deftheorem defines Ball COMPLSP1:def 17 :
for n being Element of NAT
for x being Element of COMPLEX n
for r being Real holds Ball x,r = { z where z is Element of COMPLEX n : |.(z - x).| < r } ;

theorem Th80: :: COMPLSP1:80
for n being Element of NAT
for r being Real
for z, x being Element of COMPLEX n holds
( z in Ball x,r iff |.(x - z).| < r )
proof end;

theorem Th81: :: COMPLSP1:81
for n being Element of NAT
for r being Real
for x being Element of COMPLEX n st 0 < r holds
x in Ball x,r
proof end;

theorem Th82: :: COMPLSP1:82
for n being Element of NAT
for r1 being Real
for z1 being Element of COMPLEX n holds Ball z1,r1 is open
proof end;

scheme :: COMPLSP1:sch 1
SubsetFD{ F1() -> non empty set , F2() -> non empty set , F3( set ) -> Element of F2(), P1[ set ] } :
{ F3(x) where x is Element of F1() : P1[x] } is Subset of F2()
proof end;

scheme :: COMPLSP1:sch 2
SubsetFD2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F3(), P1[ set , set ] } :
{ F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y] } is Subset of F3()
proof end;

definition
let n be Element of NAT ;
let x be Element of COMPLEX n;
let A be Subset of (COMPLEX n);
func dist x,A -> Real means :Def18: :: COMPLSP1:def 18
for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
it = lower_bound X;
existence
ex b1 being Real st
for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
b1 = lower_bound X
proof end;
uniqueness
for b1, b2 being Real st ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
b1 = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
b2 = lower_bound X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines dist COMPLSP1:def 18 :
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n)
for b4 being Real holds
( b4 = dist x,A iff for X being Subset of REAL st X = { |.(x - z).| where z is Element of COMPLEX n : z in A } holds
b4 = lower_bound X );

definition
let n be Element of NAT ;
let A be Subset of (COMPLEX n);
let r be Real;
func Ball A,r -> Subset of (COMPLEX n) equals :: COMPLSP1:def 19
{ z where z is Element of COMPLEX n : dist z,A < r } ;
coherence
{ z where z is Element of COMPLEX n : dist z,A < r } is Subset of (COMPLEX n)
proof end;
end;

:: deftheorem defines Ball COMPLSP1:def 19 :
for n being Element of NAT
for A being Subset of (COMPLEX n)
for r being Real holds Ball A,r = { z where z is Element of COMPLEX n : dist z,A < r } ;

theorem :: COMPLSP1:83
canceled;

theorem Th84: :: COMPLSP1:84
for X being Subset of REAL
for r being Real st X <> {} & ( for r' being Real st r' in X holds
r <= r' ) holds
lower_bound X >= r
proof end;

theorem Th85: :: COMPLSP1:85
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist x,A >= 0
proof end;

theorem Th86: :: COMPLSP1:86
for n being Element of NAT
for x, z being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
dist (x + z),A <= (dist x,A) + |.z.|
proof end;

theorem Th87: :: COMPLSP1:87
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st x in A holds
dist x,A = 0
proof end;

theorem Th88: :: COMPLSP1:88
for n being Element of NAT
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st not x in A & A <> {} & A is closed holds
dist x,A > 0
proof end;

theorem Th89: :: COMPLSP1:89
for n being Element of NAT
for z1, x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st A <> {} holds
|.(z1 - x).| + (dist x,A) >= dist z1,A
proof end;

theorem Th90: :: COMPLSP1:90
for n being Element of NAT
for r being Real
for z being Element of COMPLEX n
for A being Subset of (COMPLEX n) holds
( z in Ball A,r iff dist z,A < r )
proof end;

theorem Th91: :: COMPLSP1:91
for n being Element of NAT
for r being Real
for x being Element of COMPLEX n
for A being Subset of (COMPLEX n) st 0 < r & x in A holds
x in Ball A,r
proof end;

theorem Th92: :: COMPLSP1:92
for n being Element of NAT
for r being Real
for A being Subset of (COMPLEX n) st 0 < r holds
A c= Ball A,r
proof end;

theorem Th93: :: COMPLSP1:93
for n being Element of NAT
for r1 being Real
for A being Subset of (COMPLEX n) st A <> {} holds
Ball A,r1 is open
proof end;

definition
let n be Element of NAT ;
let A, B be Subset of (COMPLEX n);
func dist A,B -> Real means :Def20: :: COMPLSP1:def 20
for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
it = lower_bound X;
existence
ex b1 being Real st
for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
b1 = lower_bound X
proof end;
uniqueness
for b1, b2 being Real st ( for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
b1 = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
b2 = lower_bound X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines dist COMPLSP1:def 20 :
for n being Element of NAT
for A, B being Subset of (COMPLEX n)
for b4 being Real holds
( b4 = dist A,B iff for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
b4 = lower_bound X );

definition
let X, Y be Subset of REAL ;
func X + Y -> Subset of REAL equals :: COMPLSP1:def 21
{ (r + r1) where r, r1 is Real : ( r in X & r1 in Y ) } ;
coherence
{ (r + r1) where r, r1 is Real : ( r in X & r1 in Y ) } is Subset of REAL
proof end;
end;

:: deftheorem defines + COMPLSP1:def 21 :
for X, Y being Subset of REAL holds X + Y = { (r + r1) where r, r1 is Real : ( r in X & r1 in Y ) } ;

theorem Th94: :: COMPLSP1:94
for X, Y being Subset of REAL st X <> {} & Y <> {} holds
X + Y <> {}
proof end;

theorem Th95: :: COMPLSP1:95
for X, Y being Subset of REAL st X is bounded_below & Y is bounded_below holds
X + Y is bounded_below
proof end;

theorem Th96: :: COMPLSP1:96
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 end;

theorem Th97: :: COMPLSP1:97
for X, Y being Subset of REAL st Y is bounded_below & X <> {} & ( for r being Real st r in X holds
ex r1 being Real st
( r1 in Y & r1 <= r ) ) holds
lower_bound X >= lower_bound Y
proof end;

theorem Th98: :: COMPLSP1:98
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
dist A,B >= 0
proof end;

theorem :: COMPLSP1:99
for n being Element of NAT
for A, B being Subset of (COMPLEX n) holds dist A,B = dist B,A
proof end;

theorem Th100: :: COMPLSP1:100
for n being Element of NAT
for x being Element of COMPLEX n
for A, B being Subset of (COMPLEX n) st A <> {} & B <> {} holds
(dist x,A) + (dist x,B) >= dist A,B
proof end;

theorem :: COMPLSP1:101
for n being Element of NAT
for A, B being Subset of (COMPLEX n) st A meets B holds
dist A,B = 0
proof end;

definition
let n be Element of NAT ;
func ComplexOpenSets n -> Subset-Family of (COMPLEX n) equals :: COMPLSP1:def 22
{ A where A is Subset of (COMPLEX n) : A is open } ;
coherence
{ A where A is Subset of (COMPLEX n) : A is open } is Subset-Family of (COMPLEX n)
proof end;
end;

:: deftheorem defines ComplexOpenSets COMPLSP1:def 22 :
for n being Element of NAT holds ComplexOpenSets n = { A where A is Subset of (COMPLEX n) : A is open } ;

theorem Th102: :: COMPLSP1:102
for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A in ComplexOpenSets n iff A is open )
proof end;

registration
let A be non empty set ;
let t be Subset-Family of A;
cluster TopStruct(# A,t #) -> non empty ;
coherence
not TopStruct(# A,t #) is empty
proof end;
end;

definition
let n be Element of NAT ;
func the_Complex_Space n -> strict TopSpace equals :: COMPLSP1:def 23
 TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);
coherence
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is strict TopSpace
proof end;
end;

:: deftheorem defines the_Complex_Space COMPLSP1:def 23 :
for n being Element of NAT holds the_Complex_Space n = TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);

registration
let n be Element of NAT ;
cluster the_Complex_Space n -> non empty strict ;
coherence
not the_Complex_Space n is empty ;
end;

theorem :: COMPLSP1:103
for n being Element of NAT holds the topology of (the_Complex_Space n) = ComplexOpenSets n ;

theorem :: COMPLSP1:104
for n being Element of NAT holds the carrier of (the_Complex_Space n) = COMPLEX n ;

theorem :: COMPLSP1:105
for n being Element of NAT
for p being Point of (the_Complex_Space n) holds p is Element of COMPLEX n ;

theorem :: COMPLSP1:106
canceled;

theorem :: COMPLSP1:107
canceled;

theorem Th108: :: COMPLSP1:108
for n being Element of NAT
for V being Subset of (the_Complex_Space n)
for A being Subset of (COMPLEX n) st A = V holds
( A is open iff V is open )
proof end;

theorem Th109: :: COMPLSP1:109
for n being Element of NAT
for A being Subset of (COMPLEX n) holds
( A is closed iff A ` is open )
proof end;

theorem Th110: :: COMPLSP1:110
for n being Element of NAT
for V being Subset of (the_Complex_Space n)
for A being Subset of (COMPLEX n) st A = V holds
( A is closed iff V is closed )
proof end;

theorem :: COMPLSP1:111
for n being Element of NAT holds the_Complex_Space n is T_2
proof end;

theorem :: COMPLSP1:112
for n being Element of NAT holds the_Complex_Space n is regular
proof end;