:: $T_0$ Topological Spaces
:: by Mariusz \.Zynel and Adam Guzowski
::
:: Received May 6, 1994
:: Copyright (c) 1994 Association of Mizar Users
theorem :: T_0TOPSP:1
canceled;
theorem Th2: :: T_0TOPSP:2
:: deftheorem defines are_homeomorphic T_0TOPSP:def 1 :
:: deftheorem Def2 defines open T_0TOPSP:def 2 :
:: deftheorem Def3 defines Indiscernibility T_0TOPSP:def 3 :
:: deftheorem defines Indiscernible T_0TOPSP:def 4 :
:: deftheorem defines T_0-reflex T_0TOPSP:def 5 :
:: deftheorem defines T_0-canonical_map T_0TOPSP:def 6 :
theorem :: T_0TOPSP:3
canceled;
theorem :: T_0TOPSP:4
canceled;
theorem :: T_0TOPSP:5
canceled;
theorem Th6: :: T_0TOPSP:6
theorem Th7: :: T_0TOPSP:7
theorem Th8: :: T_0TOPSP:8
theorem Th9: :: T_0TOPSP:9
theorem Th10: :: T_0TOPSP:10
theorem Th11: :: T_0TOPSP:11
theorem Th12: :: T_0TOPSP:12
Lm1:
for T being non empty TopSpace
for x, y being Point of (T_0-reflex T) st x <> y holds
ex V being Subset of (T_0-reflex T) st
( V is open & ( ( x in V & not y in V ) or ( y in V & not x in V ) ) )
:: deftheorem Def7 defines T_0 T_0TOPSP:def 7 :
theorem :: T_0TOPSP:13
theorem :: T_0TOPSP:14
theorem Th15: :: T_0TOPSP:15
theorem Th16: :: T_0TOPSP:16
theorem :: T_0TOPSP:17