:: Complex Spaces
:: by Czes{\l}aw Byli\'nski and Andrzej Trybulec
::
:: 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(# (),() #);
coherence
TopStruct(# (),() #) 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(# (),() #);

registration
let n be Element of NAT ;
coherence
not the_Complex_Space n is empty
;
end;

theorem :: COMPLSP1:1
for n being Element of NAT holds the topology of = ComplexOpenSets n ;

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

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

theorem Th4: :: COMPLSP1:4
for n being Element of NAT
for V being Subset of
for A being Subset of () 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
for A being Subset of () 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;