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


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 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 ) by SEQ_4:131;

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

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

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