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

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, COMPLEX1, ARYTM_3, ARYTM_1, TARSKI, XBOOLE_0, CARD_1, RCOMP_1, SETFAM_1, METRIC_1, PRE_TOPC, STRUCT_0, CARD_5, COMPLSP1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SETFAM_1, REAL_1, COMPLEX1, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC, FINSEQ_1, VALUED_1, RVSUM_1, FINSEQ_2, SEQ_4;
definitions PRE_TOPC, COMPTS_1, XBOOLE_0;
theorems SUBSET_1, ZFMISC_1, XBOOLE_0, XREAL_1, SEQ_4;
schemes ;
registrations NUMBERS, XREAL_0, MEMBERED, FINSEQ_2, PRE_TOPC;
constructors HIDDEN, SETFAM_1, PARTFUN1, BINOP_1, SETWISEO, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, SEQ_4, FINSEQOP, RVSUM_1, COMPTS_1, XXREAL_2, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities SEQ_4, STRUCT_0, SUBSET_1;
expansions PRE_TOPC;


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;