begin
theorem
canceled;
theorem Th2:
theorem Th3:
:: deftheorem Def1 defines TopSpace-yielding WAYBEL18:def 1 :
for F being Relation holds
( F is TopSpace-yielding iff for x being set st x in rng F holds
x is TopStruct );
:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :
for I being set
for J being TopSpace-yielding ManySortedSet of I
for b3 being Subset-Family of (product (Carrier J)) holds
( b3 = product_prebasis J iff for x being Subset of (product (Carrier J)) holds
( x in b3 iff ex i being set ex T being TopStruct ex V being Subset of T st
( i in I & V is open & T = J . i & x = product ((Carrier J) +* (i,V)) ) ) );
theorem Th4:
:: deftheorem Def3 defines product WAYBEL18:def 3 :
for I being set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for b3 being strict TopSpace holds
( b3 = product J iff ( the carrier of b3 = product (Carrier J) & product_prebasis J is prebasis of b3 ) );
:: deftheorem defines proj WAYBEL18:def 4 :
for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I holds proj (J,i) = proj ((Carrier J),i);
theorem Th5:
theorem Th6:
theorem Th7:
begin
:: deftheorem Def5 defines injective WAYBEL18:def 5 :
for Z being TopStruct holds
( Z is injective iff for X being non empty TopSpace
for f being Function of X,Z st f is continuous holds
for Y being non empty TopSpace st X is SubSpace of Y holds
ex g being Function of Y,Z st
( g is continuous & g | the carrier of X = f ) );
theorem Th8:
theorem
:: deftheorem defines Image WAYBEL18:def 6 :
for X being 1-sorted
for Y being TopStruct
for f being Function of X,Y holds Image f = Y | (rng f);
theorem Th10:
:: deftheorem defines corestr WAYBEL18:def 7 :
for X being 1-sorted
for Y being non empty TopStruct
for f being Function of X,Y holds corestr f = f;
theorem Th11:
:: deftheorem defines is_Retract_of WAYBEL18:def 8 :
for X, Y being TopStruct holds
( X is_Retract_of Y iff ex f being Function of Y,Y st
( f is continuous & f * f = f & Image f,X are_homeomorphic ) );
theorem Th12:
definition
func Sierpinski_Space -> strict TopStruct means :
Def9:
( the
carrier of
it = {0,1} & the
topology of
it = {{},{1},{0,1}} );
existence
ex b1 being strict TopStruct st
( the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} )
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} & the carrier of b2 = {0,1} & the topology of b2 = {{},{1},{0,1}} holds
b1 = b2
;
end;
:: deftheorem Def9 defines Sierpinski_Space WAYBEL18:def 9 :
for b1 being strict TopStruct holds
( b1 = Sierpinski_Space iff ( the carrier of b1 = {0,1} & the topology of b1 = {{},{1},{0,1}} ) );
Lm1:
Sierpinski_Space is T_0
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem