:: Separated and Weakly Separated Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received January 8, 1992
:: Copyright (c) 1992 Association of Mizar Users
Lm1:
for A being set
for B, C, D being Subset of A st B \ C = {} holds
B misses D \ C
Lm2:
for A, B, C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
theorem Th1: :: TSEP_1:1
theorem Th2: :: TSEP_1:2
theorem :: TSEP_1:3
theorem Th4: :: TSEP_1:4
Lm3:
for X being TopStruct
for X0 being SubSpace of X holds TopStruct(# the carrier of X0,the topology of X0 #) is strict SubSpace of X
theorem Th5: :: TSEP_1:5
theorem :: TSEP_1:6
theorem Th7: :: TSEP_1:7
theorem Th8: :: TSEP_1:8
theorem Th9: :: TSEP_1:9
theorem Th10: :: TSEP_1:10
theorem Th11: :: TSEP_1:11
theorem :: TSEP_1:12
theorem :: TSEP_1:13
theorem :: TSEP_1:14
theorem Th15: :: TSEP_1:15
:: deftheorem Def1 defines open TSEP_1:def 1 :
Lm4:
for T being TopStruct holds TopStruct(# the carrier of T,the topology of T #) is SubSpace of T
theorem Th16: :: TSEP_1:16
theorem :: TSEP_1:17
theorem :: TSEP_1:18
theorem :: TSEP_1:19
theorem Th20: :: TSEP_1:20
:: deftheorem Def2 defines union TSEP_1:def 2 :
theorem :: TSEP_1:21
theorem Th22: :: TSEP_1:22
theorem :: TSEP_1:23
theorem :: TSEP_1:24
theorem :: TSEP_1:25
:: deftheorem Def3 defines misses TSEP_1:def 3 :
:: deftheorem TSEP_1:def 4 :
canceled;
:: deftheorem Def5 defines meet TSEP_1:def 5 :
theorem :: TSEP_1:26
canceled;
theorem :: TSEP_1:27
canceled;
theorem :: TSEP_1:28
canceled;
theorem Th29: :: TSEP_1:29
theorem Th30: :: TSEP_1:30
theorem :: TSEP_1:31
theorem :: TSEP_1:32
theorem :: TSEP_1:33
theorem :: TSEP_1:34
theorem :: TSEP_1:35
theorem :: TSEP_1:36
theorem :: TSEP_1:37
canceled;
theorem Th38: :: TSEP_1:38
theorem Th39: :: TSEP_1:39
theorem Th40: :: TSEP_1:40
theorem Th41: :: TSEP_1:41
theorem Th42: :: TSEP_1:42
theorem Th43: :: TSEP_1:43
theorem Th44: :: TSEP_1:44
theorem Th45: :: TSEP_1:45
theorem Th46: :: TSEP_1:46
theorem Th47: :: TSEP_1:47
theorem Th48: :: TSEP_1:48
theorem Th49: :: TSEP_1:49
:: deftheorem TSEP_1:def 6 :
canceled;
:: deftheorem Def7 defines are_weakly_separated TSEP_1:def 7 :
theorem :: TSEP_1:50
canceled;
theorem Th51: :: TSEP_1:51
theorem Th52: :: TSEP_1:52
theorem Th53: :: TSEP_1:53
theorem Th54: :: TSEP_1:54
theorem Th55: :: TSEP_1:55
theorem Th56: :: TSEP_1:56
theorem Th57: :: TSEP_1:57
theorem Th58: :: TSEP_1:58
theorem Th59: :: TSEP_1:59
theorem Th60: :: TSEP_1:60
theorem Th61: :: TSEP_1:61
theorem Th62: :: TSEP_1:62
theorem Th63: :: TSEP_1:63
theorem Th64: :: TSEP_1:64
theorem Th65: :: TSEP_1:65
theorem Th66: :: TSEP_1:66
theorem Th67: :: TSEP_1:67
:: deftheorem Def8 defines are_separated TSEP_1:def 8 :
theorem :: TSEP_1:68
theorem :: TSEP_1:69
canceled;
theorem :: TSEP_1:70
theorem :: TSEP_1:71
theorem :: TSEP_1:72
theorem :: TSEP_1:73
theorem :: TSEP_1:74
theorem :: TSEP_1:75
theorem :: TSEP_1:76
theorem Th77: :: TSEP_1:77
theorem :: TSEP_1:78
theorem :: TSEP_1:79
theorem :: TSEP_1:80
theorem :: TSEP_1:81
theorem :: TSEP_1:82
theorem Th83: :: TSEP_1:83
:: deftheorem Def9 defines are_weakly_separated TSEP_1:def 9 :
theorem :: TSEP_1:84
canceled;
theorem Th85: :: TSEP_1:85
theorem Th86: :: TSEP_1:86
theorem Th87: :: TSEP_1:87
theorem Th88: :: TSEP_1:88
theorem :: TSEP_1:89
theorem :: TSEP_1:90
theorem :: TSEP_1:91
theorem :: TSEP_1:92
theorem :: TSEP_1:93
theorem :: TSEP_1:94
theorem :: TSEP_1:95
theorem :: TSEP_1:96
theorem :: TSEP_1:97
theorem :: TSEP_1:98
theorem :: TSEP_1:99
theorem :: TSEP_1:100