:: Maximal Anti-Discrete Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received July 26, 1994
:: Copyright (c) 1994 Association of Mizar Users
theorem Th1: :: TEX_4:1
theorem Th2: :: TEX_4:2
theorem :: TEX_4:3
canceled;
theorem :: TEX_4:4
:: deftheorem Def1 defines anti-discrete TEX_4:def 1 :
:: deftheorem Def2 defines anti-discrete TEX_4:def 2 :
:: deftheorem Def3 defines anti-discrete TEX_4:def 3 :
:: deftheorem Def4 defines anti-discrete TEX_4:def 4 :
theorem :: TEX_4:5
canceled;
theorem Th6: :: TEX_4:6
theorem Th7: :: TEX_4:7
theorem Th8: :: TEX_4:8
theorem Th9: :: TEX_4:9
:: deftheorem Def5 defines anti-discrete-set-family TEX_4:def 5 :
theorem Th10: :: TEX_4:10
theorem :: TEX_4:11
:: deftheorem defines MaxADSF TEX_4:def 6 :
theorem Th12: :: TEX_4:12
theorem Th13: :: TEX_4:13
theorem Th14: :: TEX_4:14
theorem Th15: :: TEX_4:15
:: deftheorem Def7 defines maximal_anti-discrete TEX_4:def 7 :
theorem :: TEX_4:16
theorem Th17: :: TEX_4:17
theorem Th18: :: TEX_4:18
theorem Th19: :: TEX_4:19
:: deftheorem defines MaxADSet TEX_4:def 8 :
theorem :: TEX_4:20
theorem Th21: :: TEX_4:21
theorem Th22: :: TEX_4:22
theorem Th23: :: TEX_4:23
theorem Th24: :: TEX_4:24
theorem Th25: :: TEX_4:25
theorem Th26: :: TEX_4:26
theorem :: TEX_4:27
theorem :: TEX_4:28
:: deftheorem Def9 defines maximal_anti-discrete TEX_4:def 9 :
theorem Th29: :: TEX_4:29
:: deftheorem defines maximal_anti-discrete TEX_4:def 10 :
:: deftheorem defines MaxADSet TEX_4:def 11 :
theorem Th30: :: TEX_4:30
theorem Th31: :: TEX_4:31
theorem Th32: :: TEX_4:32
theorem Th33: :: TEX_4:33
theorem Th34: :: TEX_4:34
theorem Th35: :: TEX_4:35
theorem Th36: :: TEX_4:36
theorem Th37: :: TEX_4:37
theorem :: TEX_4:38
theorem Th39: :: TEX_4:39
theorem Th40: :: TEX_4:40
theorem Th41: :: TEX_4:41
theorem Th42: :: TEX_4:42
theorem Th43: :: TEX_4:43
:: deftheorem Def12 defines anti-discrete TEX_4:def 12 :
:: deftheorem defines anti-discrete TEX_4:def 13 :
:: deftheorem Def14 defines anti-discrete TEX_4:def 14 :
theorem :: TEX_4:44
theorem :: TEX_4:45
theorem :: TEX_4:46
theorem Th47: :: TEX_4:47
theorem Th48: :: TEX_4:48
theorem Th49: :: TEX_4:49
theorem Th50: :: TEX_4:50
Lm1:
for X being non empty TopSpace
for x, y being Point of X st MaxADSet x = MaxADSet y holds
Cl {x} = Cl {y}
theorem Th51: :: TEX_4:51
theorem :: TEX_4:52
:: deftheorem defines MaxADSet TEX_4:def 15 :
theorem Th53: :: TEX_4:53
theorem :: TEX_4:54
theorem Th55: :: TEX_4:55
theorem :: TEX_4:56
theorem Th57: :: TEX_4:57
theorem Th58: :: TEX_4:58
theorem :: TEX_4:59
theorem Th60: :: TEX_4:60
theorem Th61: :: TEX_4:61
theorem Th62: :: TEX_4:62
theorem :: TEX_4:63
theorem :: TEX_4:64
theorem :: TEX_4:65
theorem :: TEX_4:66
theorem :: TEX_4:67
theorem Th68: :: TEX_4:68
theorem Th69: :: TEX_4:69
theorem :: TEX_4:70
theorem :: TEX_4:71
theorem :: TEX_4:72
theorem :: TEX_4:73
:: deftheorem Def16 defines maximal_anti-discrete TEX_4:def 16 :
theorem Th74: :: TEX_4:74
:: deftheorem Def17 defines MaxADSspace TEX_4:def 17 :
Lm2:
for Y being non empty TopStruct
for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds
X1 is SubSpace of X2
theorem :: TEX_4:75
theorem :: TEX_4:76
theorem :: TEX_4:77
theorem :: TEX_4:78
theorem :: TEX_4:79
theorem :: TEX_4:80
Lm3:
for Y being TopStruct
for A being Subset of Y holds the carrier of (Y | A) = A
theorem :: TEX_4:81
theorem :: TEX_4:82
:: deftheorem Def19 defines MaxADSspace TEX_4:def 18 :
theorem :: TEX_4:83
theorem :: TEX_4:84
theorem :: TEX_4:85
theorem :: TEX_4:86
theorem :: TEX_4:87
theorem :: TEX_4:88
theorem :: TEX_4:89
theorem :: TEX_4:90
theorem :: TEX_4:91