:: On Discrete and Almost Discrete Topological Spaces
:: by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem Th1: :: TEX_1:1
theorem :: TEX_1:2
theorem Th3: :: TEX_1:3
theorem Th4: :: TEX_1:4
theorem Th5: :: TEX_1:5
theorem Th6: :: TEX_1:6
theorem Th7: :: TEX_1:7
Lm1:
for X, Y being set holds
( X c= Y iff X is Subset of Y )
;
:: deftheorem Def1 defines trivial TEX_1:def 1 :
theorem :: TEX_1:8
:: deftheorem defines cobool TEX_1:def 2 :
:: deftheorem defines ADTS TEX_1:def 3 :
theorem :: TEX_1:9
canceled;
theorem :: TEX_1:10
canceled;
theorem Th11: :: TEX_1:11
theorem Th12: :: TEX_1:12
theorem Th13: :: TEX_1:13
theorem Th14: :: TEX_1:14
theorem :: TEX_1:15
theorem :: TEX_1:16
theorem :: TEX_1:17
theorem :: TEX_1:18
canceled;
theorem :: TEX_1:19
canceled;
theorem :: TEX_1:20
theorem :: TEX_1:21
theorem :: TEX_1:22
theorem Th23: :: TEX_1:23
:: deftheorem TEX_1:def 4 :
canceled;
:: deftheorem defines STS TEX_1:def 5 :
theorem Th24: :: TEX_1:24
theorem Th25: :: TEX_1:25
theorem Th26: :: TEX_1:26
theorem :: TEX_1:27
theorem Th28: :: TEX_1:28
theorem Th29: :: TEX_1:29
theorem :: TEX_1:30
theorem :: TEX_1:31
theorem :: TEX_1:32
theorem :: TEX_1:33
theorem :: TEX_1:34
:: deftheorem Def6 defines discrete TEX_1:def 6 :
theorem :: TEX_1:35
:: deftheorem Def7 defines almost_discrete TEX_1:def 7 :
theorem Th36: :: TEX_1:36
theorem Th37: :: TEX_1:37
theorem :: TEX_1:38
theorem Th39: :: TEX_1:39
theorem :: TEX_1:40
theorem :: TEX_1:41