:: Injective Spaces
:: by Jaros{\l}aw Gryko
::
:: Received April 17, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: WAYBEL18:1
canceled;
theorem Th2: :: WAYBEL18:2
theorem Th3: :: WAYBEL18:3
:: deftheorem Def1 defines TopSpace-yielding WAYBEL18:def 1 :
:: deftheorem Def2 defines product_prebasis WAYBEL18:def 2 :
theorem Th4: :: WAYBEL18:4
:: deftheorem Def3 defines product WAYBEL18:def 3 :
:: deftheorem defines proj WAYBEL18:def 4 :
theorem Th5: :: WAYBEL18:5
theorem Th6: :: WAYBEL18:6
theorem Th7: :: WAYBEL18:7
:: deftheorem Def5 defines injective WAYBEL18:def 5 :
theorem Th8: :: WAYBEL18:8
theorem :: WAYBEL18:9
:: deftheorem defines Image WAYBEL18:def 6 :
theorem Th10: :: WAYBEL18:10
:: deftheorem defines corestr WAYBEL18:def 7 :
theorem Th11: :: WAYBEL18:11
:: deftheorem defines is_Retract_of WAYBEL18:def 8 :
theorem Th12: :: WAYBEL18:12
definition
func Sierpinski_Space -> strict TopStruct means :
Def9:
:: WAYBEL18:def 9
( 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 :: WAYBEL18:13
theorem Th14: :: WAYBEL18:14
theorem Th15: :: WAYBEL18:15
theorem Th16: :: WAYBEL18:16
theorem Th17: :: WAYBEL18:17
theorem :: WAYBEL18:18
theorem Th19: :: WAYBEL18:19
theorem :: WAYBEL18:20