:: Complex Spaces
:: by Czes{\l}aw Byli\'nski and Andrzej Trybulec
::
:: Received September 27, 1990
:: Copyright (c) 1990-2012 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
proofend;
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 )
proofend;

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 )
proofend;

theorem :: COMPLSP1:6
for n being Element of NAT holds the_Complex_Space n is T_2
proofend;

theorem :: COMPLSP1:7
for n being Element of NAT holds the_Complex_Space n is regular
proofend;