:: On Nowhere and Everywhere Dense Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received November 9, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem Th1: :: TEX_3:1
Lm1:
for X being non empty TopSpace
for A, B being Subset of X st A is everywhere_dense & B is everywhere_dense holds
A meets B
Lm2:
for X being non empty TopSpace
for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B
theorem Th2: :: TEX_3:2
theorem :: TEX_3:3
theorem Th4: :: TEX_3:4
theorem :: TEX_3:5
theorem Th6: :: TEX_3:6
theorem :: TEX_3:7
theorem Th8: :: TEX_3:8
:: deftheorem Def1 defines dense TEX_3:def 1 :
theorem Th9: :: TEX_3:9
theorem Th10: :: TEX_3:10
theorem :: TEX_3:11
theorem :: TEX_3:12
theorem :: TEX_3:13
theorem :: TEX_3:14
theorem :: TEX_3:15
:: deftheorem Def2 defines everywhere_dense TEX_3:def 2 :
theorem Th16: :: TEX_3:16
theorem Th17: :: TEX_3:17
theorem :: TEX_3:18
theorem :: TEX_3:19
theorem :: TEX_3:20
theorem :: TEX_3:21
theorem :: TEX_3:22
theorem Th23: :: TEX_3:23
theorem :: TEX_3:24
theorem :: TEX_3:25
theorem :: TEX_3:26
theorem :: TEX_3:27
theorem :: TEX_3:28
:: deftheorem Def3 defines boundary TEX_3:def 3 :
theorem Th29: :: TEX_3:29
theorem Th30: :: TEX_3:30
theorem Th31: :: TEX_3:31
theorem :: TEX_3:32
theorem Th33: :: TEX_3:33
theorem Th34: :: TEX_3:34
:: deftheorem Def4 defines nowhere_dense TEX_3:def 4 :
theorem Th35: :: TEX_3:35
theorem :: TEX_3:36
theorem Th37: :: TEX_3:37
theorem :: TEX_3:38
theorem Th39: :: TEX_3:39
theorem Th40: :: TEX_3:40
theorem Th41: :: TEX_3:41
theorem :: TEX_3:42
theorem :: TEX_3:43
theorem :: TEX_3:44
theorem :: TEX_3:45
theorem :: TEX_3:46
theorem :: TEX_3:47
theorem :: TEX_3:48
theorem :: TEX_3:49
theorem :: TEX_3:50
theorem :: TEX_3:51
theorem :: TEX_3:52
theorem :: TEX_3:53
theorem :: TEX_3:54
theorem :: TEX_3:55
theorem :: TEX_3:56
theorem :: TEX_3:57
theorem :: TEX_3:58
theorem :: TEX_3:59
theorem :: TEX_3:60
theorem :: TEX_3:61
theorem Th62: :: TEX_3:62
theorem :: TEX_3:63
theorem :: TEX_3:64
theorem :: TEX_3:65
theorem :: TEX_3:66
theorem Th67: :: TEX_3:67
theorem :: TEX_3:68
theorem :: TEX_3:69
theorem :: TEX_3:70
theorem :: TEX_3:71
theorem :: TEX_3:72
theorem :: TEX_3:73
theorem :: TEX_3:74
theorem :: TEX_3:75