:: Remarks on Special Subsets of Topological Spaces
:: by Zbigniew Karno
::
:: Received April 6, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem Th1: :: TOPS_3:1
theorem Th2: :: TOPS_3:2
theorem Th3: :: TOPS_3:3
theorem Th4: :: TOPS_3:4
theorem Th5: :: TOPS_3:5
theorem Th6: :: TOPS_3:6
theorem Th7: :: TOPS_3:7
theorem :: TOPS_3:8
:: deftheorem Def1 defines boundary TOPS_3:def 1 :
theorem :: TOPS_3:9
theorem Th10: :: TOPS_3:10
theorem Th11: :: TOPS_3:11
theorem :: TOPS_3:12
theorem :: TOPS_3:13
theorem :: TOPS_3:14
theorem :: TOPS_3:15
:: deftheorem Def2 defines dense TOPS_3:def 2 :
theorem :: TOPS_3:16
theorem Th17: :: TOPS_3:17
theorem Th18: :: TOPS_3:18
theorem :: TOPS_3:19
theorem :: TOPS_3:20
theorem :: TOPS_3:21
:: deftheorem Def3 defines nowhere_dense TOPS_3:def 3 :
theorem :: TOPS_3:22
theorem :: TOPS_3:23
theorem :: TOPS_3:24
theorem :: TOPS_3:25
theorem Th26: :: TOPS_3:26
theorem Th27: :: TOPS_3:27
theorem Th28: :: TOPS_3:28
theorem :: TOPS_3:29
theorem Th30: :: TOPS_3:30
:: deftheorem Def4 defines everywhere_dense TOPS_3:def 4 :
:: deftheorem defines everywhere_dense TOPS_3:def 5 :
theorem :: TOPS_3:31
theorem Th32: :: TOPS_3:32
theorem Th33: :: TOPS_3:33
theorem :: TOPS_3:34
theorem Th35: :: TOPS_3:35
theorem Th36: :: TOPS_3:36
theorem :: TOPS_3:37
theorem Th38: :: TOPS_3:38
theorem Th39: :: TOPS_3:39
theorem Th40: :: TOPS_3:40
theorem Th41: :: TOPS_3:41
theorem :: TOPS_3:42
theorem :: TOPS_3:43
theorem Th44: :: TOPS_3:44
theorem Th45: :: TOPS_3:45
theorem :: TOPS_3:46
theorem :: TOPS_3:47
theorem :: TOPS_3:48
theorem :: TOPS_3:49
theorem :: TOPS_3:50
theorem :: TOPS_3:51
theorem :: TOPS_3:52
theorem Th53: :: TOPS_3:53
theorem Th54: :: TOPS_3:54
theorem :: TOPS_3:55
theorem Th56: :: TOPS_3:56
theorem Th57: :: TOPS_3:57
theorem :: TOPS_3:58
theorem Th59: :: TOPS_3:59
theorem Th60: :: TOPS_3:60
theorem Th61: :: TOPS_3:61
theorem Th62: :: TOPS_3:62
theorem :: TOPS_3:63
theorem :: TOPS_3:64
theorem Th65: :: TOPS_3:65
theorem Th66: :: TOPS_3:66
theorem :: TOPS_3:67
theorem Th68: :: TOPS_3:68
Lm1:
for X being non empty TopSpace
for X0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C is open & C = the carrier of X0 & A c= C & A = B & A is nowhere_dense holds
B is nowhere_dense
theorem Th69: :: TOPS_3:69
theorem :: TOPS_3:70
theorem :: TOPS_3:71
theorem Th72: :: TOPS_3:72
theorem Th73: :: TOPS_3:73
theorem :: TOPS_3:74
theorem :: TOPS_3:75
theorem Th76: :: TOPS_3:76
theorem Th77: :: TOPS_3:77
theorem Th78: :: TOPS_3:78
theorem Th79: :: TOPS_3:79
theorem Th80: :: TOPS_3:80
theorem Th81: :: TOPS_3:81
theorem Th82: :: TOPS_3:82
theorem Th83: :: TOPS_3:83
theorem :: TOPS_3:84
theorem :: TOPS_3:85