environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, TARSKI, RELAT_1, ZFMISC_1, MCART_1, XBOOLE_0, SETFAM_1, EQREL_1, CARD_3, PRE_TOPC, STRUCT_0, ORDINAL2, CONNSP_2, TOPS_1, RCOMP_1, FINSET_1, PCOMPS_1, METRIC_1, XXREAL_1, CARD_1, XXREAL_0, REAL_1, BORSUK_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, FINSET_1, RELAT_1, FUNCT_1, XTUPLE_0, MCART_1, DOMAIN_1, RCOMP_1, SETFAM_1, EQREL_1, FUNCT_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, METRIC_1, PCOMPS_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2;
definitions TARSKI, PRE_TOPC, TOPS_2, CONNSP_2, EQREL_1, STRUCT_0, XBOOLE_0, RELAT_1, SETFAM_1;
theorems TARSKI, ZFMISC_1, DOMAIN_1, PRE_TOPC, FUNCT_1, FUNCT_2, TOPS_1, EQREL_1, FUNCT_3, SUBSET_1, TOPS_2, CONNSP_2, COMPTS_1, SETFAM_1, PCOMPS_1, METRIC_1, RCOMP_1, MCART_1, RELAT_1, XBOOLE_0, XBOOLE_1, XXREAL_1, XTUPLE_0;
schemes CLASSES1, DOMAIN_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSET_1, XREAL_0, MEMBERED, EQREL_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, RELSET_1, ZFMISC_1, XTUPLE_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, FUNCT_3, FINSET_1, MEMBERED, EQREL_1, RCOMP_1, TOPS_1, TOPS_2, COMPTS_1, CONNSP_2, PCOMPS_1, RELSET_1, XTUPLE_0, BINOP_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities STRUCT_0, BINOP_1;
expansions TARSKI, PRE_TOPC, TOPS_2, XBOOLE_0, RELAT_1;
definition
let X,
Y be
TopSpace;
existence
ex b1 being strict TopSpace st
( the carrier of b1 = [: the carrier of X, the carrier of Y:] & the topology of b1 = { (union A) where A is Subset-Family of b1 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } )
uniqueness
for b1, b2 being strict TopSpace st the carrier of b1 = [: the carrier of X, the carrier of Y:] & the topology of b1 = { (union A) where A is Subset-Family of b1 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } & the carrier of b2 = [: the carrier of X, the carrier of Y:] & the topology of b2 = { (union A) where A is Subset-Family of b2 : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } holds
b1 = b2
;
end;
Lm1:
for X being non empty TopSpace
for A being Subset of X
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )
Lm2:
for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
Lm3:
TopSpaceMetr RealSpace = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)
by PCOMPS_1:def 5;