begin
theorem
canceled;
theorem Th2:
theorem Th3:
:: deftheorem Def1 defines TopSpace-yielding WAYBEL18:def 1 :
:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :
theorem Th4:
:: deftheorem Def3 defines product WAYBEL18:def 3 :
:: deftheorem defines proj WAYBEL18:def 4 :
theorem Th5:
theorem Th6:
theorem Th7:
begin
:: deftheorem Def5 defines injective WAYBEL18:def 5 :
theorem Th8:
theorem
:: deftheorem defines Image WAYBEL18:def 6 :
theorem Th10:
:: deftheorem defines corestr WAYBEL18:def 7 :
theorem Th11:
:: deftheorem defines is_Retract_of WAYBEL18:def 8 :
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 :
Lm1:
Sierpinski_Space is T_0
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem Th19:
theorem