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

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 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 :: COMPLSP1:4

canceled;

theorem :: COMPLSP1:5

canceled;

theorem Th6: :: COMPLSP1:6

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 Th7: :: COMPLSP1:7

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

for n being Element of NAT holds the_Complex_Space n is T_2

proof end;

theorem :: COMPLSP1:9

for n being Element of NAT holds the_Complex_Space n is regular

proof end;