:: Subsets of Topological Spaces
:: by Miros{\l}aw Wysocki and Agata Darmochwa\l
::
:: Received April 28, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: TOPS_1:1
canceled;
theorem :: TOPS_1:2
canceled;
theorem :: TOPS_1:3
canceled;
theorem :: TOPS_1:4
canceled;
theorem :: TOPS_1:5
canceled;
theorem :: TOPS_1:6
canceled;
theorem :: TOPS_1:7
canceled;
theorem :: TOPS_1:8
canceled;
theorem :: TOPS_1:9
canceled;
theorem :: TOPS_1:10
canceled;
theorem :: TOPS_1:11
canceled;
theorem :: TOPS_1:12
canceled;
theorem :: TOPS_1:13
canceled;
theorem :: TOPS_1:14
canceled;
theorem :: TOPS_1:15
canceled;
theorem :: TOPS_1:16
canceled;
theorem :: TOPS_1:17
canceled;
theorem :: TOPS_1:18
canceled;
theorem :: TOPS_1:19
canceled;
theorem :: TOPS_1:20
canceled;
theorem :: TOPS_1:21
theorem :: TOPS_1:22
theorem :: TOPS_1:23
canceled;
theorem :: TOPS_1:24
canceled;
theorem :: TOPS_1:25
canceled;
theorem :: TOPS_1:26
canceled;
theorem Th27: :: TOPS_1:27
theorem :: TOPS_1:28
canceled;
theorem Th29: :: TOPS_1:29
theorem Th30: :: TOPS_1:30
theorem :: TOPS_1:31
theorem Th32: :: TOPS_1:32
theorem :: TOPS_1:33
canceled;
theorem Th34: :: TOPS_1:34
theorem Th35: :: TOPS_1:35
theorem Th36: :: TOPS_1:36
theorem :: TOPS_1:37
theorem Th38: :: TOPS_1:38
Lm2:
for GX being non empty 1-sorted
for R being Subset of GX
for p being Element of GX holds
( p in R ` iff not p in R )
by XBOOLE_0:def 5;
theorem Th39: :: TOPS_1:39
theorem Th40: :: TOPS_1:40
theorem :: TOPS_1:41
:: deftheorem defines Int TOPS_1:def 1 :
theorem :: TOPS_1:42
canceled;
theorem Th43: :: TOPS_1:43
theorem Th44: :: TOPS_1:44
theorem :: TOPS_1:45
theorem Th46: :: TOPS_1:46
theorem Th47: :: TOPS_1:47
theorem Th48: :: TOPS_1:48
theorem Th49: :: TOPS_1:49
theorem :: TOPS_1:50
theorem :: TOPS_1:51
theorem Th52: :: TOPS_1:52
theorem Th53: :: TOPS_1:53
theorem Th54: :: TOPS_1:54
theorem Th55: :: TOPS_1:55
theorem :: TOPS_1:56
theorem :: TOPS_1:57
theorem Th58: :: TOPS_1:58
theorem :: TOPS_1:59
:: deftheorem defines Fr TOPS_1:def 2 :
theorem :: TOPS_1:60
theorem Th61: :: TOPS_1:61
theorem :: TOPS_1:62
theorem :: TOPS_1:63
canceled;
theorem :: TOPS_1:64
theorem Th65: :: TOPS_1:65
theorem Th66: :: TOPS_1:66
theorem Th67: :: TOPS_1:67
theorem Th68: :: TOPS_1:68
theorem :: TOPS_1:69
Lm3:
for TS being TopSpace
for K, L being Subset of TS holds Fr K c= ((Fr (K \/ L)) \/ (Fr (K /\ L))) \/ ((Fr K) /\ (Fr L))
theorem :: TOPS_1:70
theorem :: TOPS_1:71
theorem :: TOPS_1:72
theorem Th73: :: TOPS_1:73
theorem Th74: :: TOPS_1:74
Lm4:
for GX being TopStruct
for T being Subset of GX holds Fr T = (Cl T) \ (Int T)
Lm5:
for TS being TopSpace
for K being Subset of TS holds Cl (Fr K) = Fr K
Lm6:
for TS being TopSpace
for K being Subset of TS holds Int (Fr (Fr K)) = {}
theorem :: TOPS_1:75
Lm7:
for X, Y, Z being set st X c= Z & Y = Z \ X holds
X c= Z \ Y
theorem Th76: :: TOPS_1:76
theorem Th77: :: TOPS_1:77
:: deftheorem Def3 defines dense TOPS_1:def 3 :
theorem :: TOPS_1:78
canceled;
theorem :: TOPS_1:79
theorem Th80: :: TOPS_1:80
theorem Th81: :: TOPS_1:81
theorem :: TOPS_1:82
:: deftheorem Def4 defines boundary TOPS_1:def 4 :
theorem :: TOPS_1:83
canceled;
theorem Th84: :: TOPS_1:84
theorem Th85: :: TOPS_1:85
theorem :: TOPS_1:86
theorem :: TOPS_1:87
theorem :: TOPS_1:88
:: deftheorem Def5 defines nowhere_dense TOPS_1:def 5 :
theorem :: TOPS_1:89
canceled;
theorem :: TOPS_1:90
theorem Th91: :: TOPS_1:91
theorem Th92: :: TOPS_1:92
theorem Th93: :: TOPS_1:93
theorem :: TOPS_1:94
theorem Th95: :: TOPS_1:95
theorem Th96: :: TOPS_1:96
theorem Th97: :: TOPS_1:97
:: deftheorem Def6 defines condensed TOPS_1:def 6 :
:: deftheorem Def7 defines closed_condensed TOPS_1:def 7 :
:: deftheorem Def8 defines open_condensed TOPS_1:def 8 :
theorem :: TOPS_1:98
canceled;
theorem :: TOPS_1:99
canceled;
theorem :: TOPS_1:100
canceled;
theorem Th101: :: TOPS_1:101
theorem Th102: :: TOPS_1:102
theorem :: TOPS_1:103
theorem Th104: :: TOPS_1:104
theorem :: TOPS_1:105
theorem Th106: :: TOPS_1:106
theorem :: TOPS_1:107
theorem Th108: :: TOPS_1:108
theorem :: TOPS_1:109
theorem :: TOPS_1:110
theorem :: TOPS_1:111