:: COMPLSP1 semantic presentation

theorem :: COMPLSP1:1

canceled;

theorem :: COMPLSP1:2

canceled;

theorem Th3: :: COMPLSP1:3

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

Lm1: the_unity_wrt addcomplex = 0c
by BINOP_2:1;

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 has_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 :Def3: :: COMPLSP1:def 3
addcomplex * (id COMPLEX ),compcomplex ;
compatibility

proof end;

end;

:: deftheorem COMPLSP1:def 1 :

:: deftheorem COMPLSP1:def 2 :

:: deftheorem Def3 defines diffcomplex COMPLSP1:def 3 :

Lm2: for c1, c2 being Element of COMPLEX holds diffcomplex . c1,c2 = c1 - c2
by BINOP_2:def 4;

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, COMPLEX1:def 7, SETWISEO:22;

theorem Th13: :: COMPLSP1:13

the_unity_wrt multcomplex = 1r by BINOP_2:6, COMPLEX1:def 7;

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

proof end;

end;

:: deftheorem COMPLSP1:def 4 :

:: deftheorem defines multcomplex COMPLSP1:def 5 :

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

proof end;

theorem Th16: :: COMPLSP1:16

for c, c' being Element of COMPLEX holds (c multcomplex ) . c' = c * c' by Lm3;

theorem Th17: :: 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 from FUNCT_2:sch 4( COMPLEX REAL );
uniqueness from BINOP_2:sch 1( COMPLEX REAL );

end;

:: deftheorem Def6 defines abscomplex COMPLSP1:def 6 :

definition

let z1, z2 be FinSequence of COMPLEX ;
func z1 + z2 -> FinSequence of COMPLEX equals :: COMPLSP1:def 7
addcomplex .: z1,z2;
correctness ;
func z1 - z2 -> FinSequence of COMPLEX equals :: COMPLSP1:def 8
diffcomplex .: z1,z2;
correctness ;

end;

:: deftheorem defines + COMPLSP1:def 7 :

:: deftheorem defines - COMPLSP1:def 8 :

definition

let z be FinSequence of COMPLEX ;
func - z -> FinSequence of COMPLEX equals :: COMPLSP1:def 9
compcomplex * z;
correctness ;

end;

:: deftheorem defines - COMPLSP1:def 9 :

definition

let c be complex number ;
let z be FinSequence of COMPLEX ;
func c * z -> FinSequence of COMPLEX equals :: COMPLSP1:def 10
(c multcomplex ) * z;
correctness ;

end;

:: deftheorem defines * COMPLSP1:def 10 :

definition

let z be FinSequence of COMPLEX ;
func abs z -> FinSequence of REAL equals :: COMPLSP1:def 11
abscomplex * z;
correctness ;

end;

:: deftheorem defines abs COMPLSP1:def 11 :

definition

let n be Nat;
func COMPLEX n -> FinSequence-DOMAIN of COMPLEX equals :: COMPLSP1:def 12
n -tuples_on COMPLEX ;
correctness ;

end;

:: deftheorem defines COMPLEX COMPLSP1:def 12 :

registration

let n be Nat;
cluster COMPLEX n -> ;
coherence ;

end;

theorem Th18: :: COMPLSP1:18

for n being Nat
for z being Element of COMPLEX n holds len z = n by FINSEQ_2:109;

Lm4: for n being Nat
for z being Element of COMPLEX n holds dom z = Seg n

proof end;

theorem :: COMPLSP1:19

for z being Element of COMPLEX 0 holds z = <*> COMPLEX by FINSEQ_2:113;

theorem :: COMPLSP1:20

<*> COMPLEX is Element of COMPLEX 0 by FINSEQ_2:114;

theorem Th21: :: COMPLSP1:21

for k, n being Nat
for z being Element of COMPLEX n st k in Seg n holds
z . k in COMPLEX

proof end;

theorem :: COMPLSP1:22

canceled;

theorem Th23: :: COMPLSP1:23

for n being Nat
for z1, z2 being Element of COMPLEX n st ( for k being Nat st k in Seg n holds
z1 . k = z2 . k ) holds
z1 = z2 by FINSEQ_2:139;

definition

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

end;

theorem Th24: :: COMPLSP1:24

for k, n being 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 Th25: :: COMPLSP1:25

for n being Nat
for z1, z2 being Element of COMPLEX n holds z1 + z2 = z2 + z1 by FINSEQOP:34;

theorem Th26: :: COMPLSP1:26

for n being Nat
for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 + z3) = (z1 + z2) + z3 by FINSEQOP:29;

definition

let n be Nat;
func 0c n -> FinSequence of COMPLEX equals :: COMPLSP1:def 13
n |-> 0c ;
correctness ;

end;

:: deftheorem defines 0c COMPLSP1:def 13 :

definition

let n be Nat;
:: original: 0c
redefine func 0c n -> Element of COMPLEX n;
coherence ;

end;

theorem :: COMPLSP1:27

for k, n being Nat st k in Seg n holds
(0c n) . k = 0c by FINSEQ_2:70;

Lm5: for n being Nat
for z being Element of COMPLEX n holds z + (0c n) = z
by Lm1, FINSEQOP:57;

theorem Th28: :: COMPLSP1:28

for n being Nat
for z being Element of COMPLEX n holds
( z + (0c n) = z & z = (0c n) + z )

proof end;

definition

let n be Nat;
let z be Element of COMPLEX n;
:: original: -
redefine func - z -> Element of COMPLEX n;
coherence by FINSEQ_2:133;

end;

theorem Th29: :: COMPLSP1:29

for k, n being 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;

Lm6: for n being Nat
for z being Element of COMPLEX n holds z + (- z) = 0c n
by Lm1, Th7, Th8, FINSEQOP:77;

Lm7: for n being Nat holds - (0c n) = 0c n

proof end;

theorem Th30: :: COMPLSP1:30

for n being Nat
for z being Element of COMPLEX n holds
( z + (- z) = 0c n & (- z) + z = 0c n )

proof end;

theorem Th31: :: COMPLSP1:31

for n being Nat
for z1, z2 being Element of COMPLEX n st z1 + z2 = 0c n holds
( z1 = - z2 & z2 = - z1 ) by Lm1, Th7, Th8, FINSEQOP:78;

theorem Th32: :: COMPLSP1:32

for n being Nat
for z being Element of COMPLEX n holds - (- z) = z

proof end;

theorem :: COMPLSP1:33

for n being Nat
for z1, z2 being Element of COMPLEX n st - z1 = - z2 holds
z1 = z2

proof end;

Lm8: for n being 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 Nat
for z1, z, z2 being Element of COMPLEX n st ( z1 + z = z2 + z or z1 + z = z + z2 ) holds
z1 = z2

proof end;

theorem Th35: :: COMPLSP1:35

for n being Nat
for z1, z2 being Element of COMPLEX n holds - (z1 + z2) = (- z1) + (- z2)

proof end;

definition

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

end;

theorem :: COMPLSP1:36

for k, n being 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 Th37: :: COMPLSP1:37

for n being Nat
for z1, z2 being Element of COMPLEX n holds z1 - z2 = z1 + (- z2) by Def3, FINSEQOP:89;

theorem :: COMPLSP1:38

for n being Nat
for z being Element of COMPLEX n holds z - (0c n) = z

proof end;

theorem :: COMPLSP1:39

for n being Nat
for z being Element of COMPLEX n holds (0c n) - z = - z

proof end;

theorem :: COMPLSP1:40

for n being Nat
for z1, z2 being Element of COMPLEX n holds z1 - (- z2) = z1 + z2

proof end;

theorem Th41: :: COMPLSP1:41

for n being Nat
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = z2 - z1

proof end;

theorem Th42: :: COMPLSP1:42

for n being Nat
for z1, z2 being Element of COMPLEX n holds - (z1 - z2) = (- z1) + z2

proof end;

theorem Th43: :: COMPLSP1:43

for n being Nat
for z being Element of COMPLEX n holds z - z = 0c n

proof end;

theorem Th44: :: COMPLSP1:44

for n being 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 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 Nat
for z1, z2, z3 being Element of COMPLEX n holds z1 + (z2 - z3) = (z1 + z2) - z3

proof end;

theorem Th47: :: COMPLSP1:47

for n being Nat
for z1, z2, z3 being Element of COMPLEX n holds z1 - (z2 - z3) = (z1 - z2) + z3

proof end;

theorem Th48: :: COMPLSP1:48

for n being Nat
for z1, z2, z3 being Element of COMPLEX n holds (z1 - z2) + z3 = (z1 + z3) - z2

proof end;

theorem Th49: :: COMPLSP1:49

for n being Nat
for z1, z being Element of COMPLEX n holds z1 = (z1 + z) - z

proof end;

theorem Th50: :: COMPLSP1:50

for n being Nat
for z1, z2 being Element of COMPLEX n holds z1 + (z2 - z1) = z2

proof end;

theorem Th51: :: COMPLSP1:51

for n being Nat
for z1, z being Element of COMPLEX n holds z1 = (z1 - z) + z

proof end;

definition

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

end;

theorem Th52: :: COMPLSP1:52

for k, n being 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 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 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 Nat
for c being Element of COMPLEX
for z1, z2 being Element of COMPLEX n holds c * (z1 + z2) = (c * z1) + (c * z2)

proof end;

theorem :: COMPLSP1:56

for n being Nat
for z being Element of COMPLEX n holds 1r * z = z

proof end;

theorem :: COMPLSP1:57

for n being Nat
for z being Element of COMPLEX n holds 0c * z = 0c n

proof end;

theorem :: COMPLSP1:58

for n being Nat
for z being Element of COMPLEX n holds (- 1r ) * z = - z

proof end;

definition

let n be Nat;
let z be Element of COMPLEX n;
:: original: abs
redefine func abs z -> Element of n -tuples_on REAL ;
correctness by FINSEQ_2:133;

end;

theorem Th59: :: COMPLSP1:59

for k, n being 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 Nat holds abs (0c n) = n |-> 0

proof end;

theorem Th61: :: COMPLSP1:61

for n being Nat
for z being Element of COMPLEX n holds abs (- z) = abs z

proof end;

theorem Th62: :: COMPLSP1:62

for n being 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 ;

end;

:: deftheorem defines |. COMPLSP1:def 14 :

theorem Th63: :: COMPLSP1:63

for n being Nat holds |.(0c n).| = 0

proof end;

theorem Th64: :: COMPLSP1:64

for n being Nat
for z being Element of COMPLEX n st |.z.| = 0 holds
z = 0c n

proof end;

theorem Th65: :: COMPLSP1:65

for n being Nat
for z being Element of COMPLEX n holds 0 <= |.z.|

proof end;

theorem Th66: :: COMPLSP1:66

for n being Nat
for z being Element of COMPLEX n holds |.(- z).| = |.z.| by Th61;

theorem :: COMPLSP1:67

for n being Nat
for c being Element of COMPLEX
for z being Element of COMPLEX n holds |.(c * z).| = |.c.| * |.z.|

proof end;

Lm9: for i, j being 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 Nat
for z1, z2 being Element of COMPLEX n holds |.(z1 + z2).| <= |.z1.| + |.z2.|

proof end;

theorem Th69: :: COMPLSP1:69

for n being Nat
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.|

proof end;

theorem :: COMPLSP1:70

for n being Nat
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 + z2).|

proof end;

theorem :: COMPLSP1:71

for n being Nat
for z1, z2 being Element of COMPLEX n holds |.z1.| - |.z2.| <= |.(z1 - z2).|

proof end;

theorem Th72: :: COMPLSP1:72

for n being 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 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 Nat
for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| = |.(z2 - z1).|

proof end;

theorem Th75: :: COMPLSP1:75

for n being Nat
for z1, z2, z being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|

proof end;

definition

let n be 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 :

definition

let n be 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 :

theorem :: COMPLSP1:76

for n being Nat
for A being Subset of (COMPLEX n) st A = {} holds
A is open

proof end;

theorem Th77: :: COMPLSP1:77

for n being 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 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 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 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

proof end;

end;

:: deftheorem defines Ball COMPLSP1:def 17 :

theorem Th80: :: COMPLSP1:80

for n being 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 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 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{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> Element of F₂(), P₁[ set ] } :

{ F₃(x) where x is Element of F₁() : P₁[x] } is Subset of F₂()

proof end;

scheme :: COMPLSP1:sch 2
SubsetFD2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set , set ) -> Element of F₃(), P₁[ set , set ] } :

{ F₄(x,y) where x is Element of F₁(), y is Element of F₂() : P₁[x,y] } is Subset of F₃()

proof end;

definition

let n be 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines dist COMPLSP1:def 18 :

definition

let n be 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

proof end;

end;

:: deftheorem defines Ball COMPLSP1:def 19 :

Lm10: for r, r1 being Real st ( for r' being real number st r' > 0 holds
r + r' >= r1 ) holds
r >= r1
by XREAL_1:43;

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 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 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 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 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 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 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 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 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 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines dist COMPLSP1:def 20 :

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

proof end;

end;

:: deftheorem defines + COMPLSP1:def 21 :

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 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 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 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 Nat
for A, B being Subset of (COMPLEX n) st A meets B holds
dist A,B = 0

proof end;

definition

let n be 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

proof end;

end;

:: deftheorem defines ComplexOpenSets COMPLSP1:def 22 :

theorem Th102: :: COMPLSP1:102

for n being 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

proof end;

end;

definition

let n be Nat;
func the_Complex_Space n -> strict TopSpace equals :: COMPLSP1:def 23
TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);
coherence

proof end;

end;

:: deftheorem defines the_Complex_Space COMPLSP1:def 23 :

registration

let n be Nat;
cluster the_Complex_Space n -> non empty strict ;
coherence ;

end;

theorem :: COMPLSP1:103

for n being Nat holds the topology of (the_Complex_Space n) = ComplexOpenSets n ;

theorem :: COMPLSP1:104

for n being Nat holds the carrier of (the_Complex_Space n) = COMPLEX n ;

theorem :: COMPLSP1:105

for n being 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 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 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 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 Nat holds the_Complex_Space n is_T2

proof end;

theorem :: COMPLSP1:112

for n being Nat holds the_Complex_Space n is_T3

proof end;