:: COMPLSP1 semantic presentation

begin


definition
let n be Element of NAT ;
func the_Complex_Space n ->  strict TopSpace equals :: COMPLSP1:def 1
 TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);
coherence
 TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is strict TopSpace
proof
set T = TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);
 TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is TopSpace-like
proof
reconsider z = COMPLEX n as Subset of (COMPLEX n) by ZFMISC_1:def_1;
 z is open by SEQ_4:107;
hence  the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of K10(K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #))) holds
( not b1 c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or union b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ) & ( for b1, b2 being Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) holds
( not b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or b1 /\ b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ) )
thus  for A being Subset-Family of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) st A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) holds
union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ::_thesis: for b1, b2 being Element of K10( the carrier of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)) holds
( not b1 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or b1 /\ b2 in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) )
proof
let A be Subset-Family of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); ::_thesis: ( A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) implies union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) )
assume  A c= the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; ::_thesis: union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)
then A1: for B being Subset of (COMPLEX n) st B in A holds
B is open by SEQ_4:131;
reconsider z = union A as Subset of (COMPLEX n) ;
 z is open by A1, SEQ_4:108;
hence  union A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; ::_thesis: verum
end;
let A, B be Subset of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #); ::_thesis: ( not A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or not B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) or A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) )
reconsider z1 = A, z2 = B as Subset of (COMPLEX n) ;
reconsider z = A /\ B as Subset of (COMPLEX n) ;
assume  ( A in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) & B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ) ; ::_thesis: A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #)
then  ( z1 is open & z2 is open ) by SEQ_4:131;
then  z is open by SEQ_4:109;
hence  A /\ B in the topology of TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) ; ::_thesis: verum
end;
hence  TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is strict TopSpace ; ::_thesis: verum
end;
end;

:: deftheorem  defines the_Complex_Space COMPLSP1:def_1_:_
 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:1
for n being Element of NAT holds the topology of (the_Complex_Space n) = ComplexOpenSets n ;

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


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

theorem Th4: :: COMPLSP1:4
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
let n be Element of NAT ; ::_thesis: 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 )
let V be Subset of (the_Complex_Space n); ::_thesis: for A being Subset of (COMPLEX n) st A = V holds
( A is open iff V is open )
let A be Subset of (COMPLEX n); ::_thesis: ( A = V implies ( A is open iff V is open ) )
assume  A = V ; ::_thesis: ( A is open iff V is open )
then  ( A in ComplexOpenSets n iff V in the topology of (the_Complex_Space n) ) ;
hence  ( A is open iff V is open ) by PRE_TOPC:def_2, SEQ_4:131; ::_thesis: verum
end;

theorem Th5: :: COMPLSP1:5
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
let n be Element of NAT ; ::_thesis: 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 )
let V be Subset of (the_Complex_Space n); ::_thesis: for A being Subset of (COMPLEX n) st A = V holds
( A is closed iff V is closed )
let A be Subset of (COMPLEX n); ::_thesis: ( A = V implies ( A is closed iff V is closed ) )
assume  A = V ; ::_thesis: ( A is closed iff V is closed )
then  ( ([#] (the_Complex_Space n)) \ V is open iff A ` is open ) by Th4;
hence  ( A is closed iff V is closed ) by PRE_TOPC:def_3, SEQ_4:132; ::_thesis: verum
end;

theorem :: COMPLSP1:6
for n being Element of NAT holds the_Complex_Space n is T_2
proof
let n be Element of NAT ; ::_thesis: the_Complex_Space n is T_2
let p be Point of (the_Complex_Space n); :: according to PRE_TOPC:def_10 ::_thesis: for b1 being Element of the carrier of (the_Complex_Space n) holds
( p = b1 or ex b2, b3 being Element of K10( the carrier of (the_Complex_Space n)) st
( b2 is open & b3 is open & p in b2 & b1 in b3 & b2 misses b3 ) )
let q be Point of (the_Complex_Space n); ::_thesis: ( p = q or ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A1: p <> q ; ::_thesis: ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
reconsider z1 = p, z2 = q as Element of COMPLEX n ;
set d = |.(z1 - z2).| / 2;
reconsider K1 = Ball (z1,(|.(z1 - z2).| / 2)), K2 = Ball (z2,(|.(z1 - z2).| / 2)) as Subset of (the_Complex_Space n) ;
take  K1 ; ::_thesis: ex b1 being Element of K10( the carrier of (the_Complex_Space n)) st
( K1 is open & b1 is open & p in K1 & q in b1 & K1 misses b1 )
take  K2 ; ::_thesis: ( K1 is open & K2 is open & p in K1 & q in K2 & K1 misses K2 )
 ( Ball (z1,(|.(z1 - z2).| / 2)) is open & Ball (z2,(|.(z1 - z2).| / 2)) is open ) by SEQ_4:112;
hence  ( K1 is open & K2 is open ) by Th4; ::_thesis: ( p in K1 & q in K2 & K1 misses K2 )
 0 < |.(z1 - z2).| by A1, SEQ_4:103;
hence  ( p in K1 & q in K2 ) by SEQ_4:111, XREAL_1:215; ::_thesis: K1 misses K2
assume  K1 /\ K2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being Element of COMPLEX n such that
A2: x in (Ball (z1,(|.(z1 - z2).| / 2))) /\ (Ball (z2,(|.(z1 - z2).| / 2))) by SUBSET_1:4;
 x in K2 by A2, XBOOLE_0:def_4;
then A3: |.(z2 - x).| < |.(z1 - z2).| / 2 by SEQ_4:110;
 x in K1 by A2, XBOOLE_0:def_4;
then  |.(z1 - x).| < |.(z1 - z2).| / 2 by SEQ_4:110;
then  |.(z1 - x).| + |.(z2 - x).| < (|.(z1 - z2).| / 2) + (|.(z1 - z2).| / 2) by A3, XREAL_1:8;
then  |.(z1 - x).| + |.(x - z2).| < |.(z1 - z2).| by SEQ_4:104;
hence  contradiction by SEQ_4:105; ::_thesis: verum
end;

theorem :: COMPLSP1:7
for n being Element of NAT holds the_Complex_Space n is regular
proof
let n be Element of NAT ; ::_thesis: the_Complex_Space n is regular
let p be Point of (the_Complex_Space n); :: according to COMPTS_1:def_2 ::_thesis: for b1 being Element of K10( the carrier of (the_Complex_Space n)) holds
( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of K10( the carrier of (the_Complex_Space n)) st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )
let P be Subset of (the_Complex_Space n); ::_thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )
assume that
A1: P <> {} and
A2: ( P is closed & p in P ` ) ; ::_thesis: ex b1, b2 being Element of K10( the carrier of (the_Complex_Space n)) st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )
reconsider A = P as Subset of (COMPLEX n) ;
reconsider z1 = p as Element of COMPLEX n ;
set d = (dist (z1,A)) / 2;
reconsider K1 = Ball (z1,((dist (z1,A)) / 2)), K2 = Ball (A,((dist (z1,A)) / 2)) as Subset of (the_Complex_Space n) ;
take  K1 ; ::_thesis: ex b1 being Element of K10( the carrier of (the_Complex_Space n)) st
( K1 is open & b1 is open & p in K1 & P c= b1 & K1 misses b1 )
take  K2 ; ::_thesis: ( K1 is open & K2 is open & p in K1 & P c= K2 & K1 misses K2 )
A3: Ball (z1,((dist (z1,A)) / 2)) is open by SEQ_4:112;
 Ball (A,((dist (z1,A)) / 2)) is open by A1, SEQ_4:122;
hence  ( K1 is open & K2 is open ) by A3, Th4; ::_thesis: ( p in K1 & P c= K2 & K1 misses K2 )
 ( A is closed & not p in P ) by A2, Th5, XBOOLE_0:def_5;
then  0 < (dist (z1,A)) / 2 by A1, SEQ_4:117, XREAL_1:215;
hence  ( p in K1 & P c= K2 ) by SEQ_4:111, SEQ_4:121; ::_thesis: K1 misses K2
assume  K1 /\ K2 <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider x being Element of COMPLEX n such that
A4: x in (Ball (z1,((dist (z1,A)) / 2))) /\ (Ball (A,((dist (z1,A)) / 2))) by SUBSET_1:4;
 x in K2 by A4, XBOOLE_0:def_4;
then A5: dist (x,A) < (dist (z1,A)) / 2 by SEQ_4:119;
 x in K1 by A4, XBOOLE_0:def_4;
then  |.(z1 - x).| < (dist (z1,A)) / 2 by SEQ_4:110;
then  |.(z1 - x).| + (dist (x,A)) < ((dist (z1,A)) / 2) + ((dist (z1,A)) / 2) by A5, XREAL_1:8;
hence  contradiction by A1, SEQ_4:118; ::_thesis: verum
end;