:: by Czes{\l}aw Byli\'nski and Andrzej Trybulec

::

:: Received September 27, 1990

:: Copyright (c) 1990-2018 Association of Mizar Users

definition

let n be Element of NAT ;

TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is strict TopSpace

end;
func the_Complex_Space n -> strict TopSpace equals :: COMPLSP1:def 1

TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);

coherence TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);

TopStruct(# (COMPLEX n),(ComplexOpenSets n) #) is strict TopSpace

proof 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) #);

for n being Element of NAT holds the_Complex_Space n = TopStruct(# (COMPLEX n),(ComplexOpenSets n) #);

theorem :: COMPLSP1:1

theorem :: COMPLSP1:2

theorem :: COMPLSP1:3

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 )

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;