:: Alexandroff One Point Compactification
:: by Czeslaw Bylinski
::
:: Received August 13, 2007
:: Copyright (c) 2007 Association of Mizar Users
:: deftheorem Def1 defines compact COMPACT1:def 1 :
:: deftheorem Def2 defines relatively-compact COMPACT1:def 2 :
:: deftheorem Def3 defines liminally-compact COMPACT1:def 3 :
:: deftheorem Def4 defines locally-relatively-compact COMPACT1:def 4 :
:: deftheorem Def5 defines locally-closed/compact COMPACT1:def 5 :
:: deftheorem Def6 defines locally-compact COMPACT1:def 6 :
theorem :: COMPACT1:1
theorem Th2: :: COMPACT1:2
:: deftheorem defines embedding COMPACT1:def 7 :
theorem Th3: :: COMPACT1:3
:: deftheorem Def8 defines compactification COMPACT1:def 8 :
:: deftheorem Def9 defines One-Point_Compactification COMPACT1:def 9 :
theorem Th4: :: COMPACT1:4
theorem Th5: :: COMPACT1:5
theorem :: COMPACT1:6
theorem Th7: :: COMPACT1:7
theorem :: COMPACT1:8