:: Maximal Discrete Subspaces of Almost Discrete Topological Spaces
:: by Zbigniew Karno
::
:: Received November 5, 1993
:: Copyright (c) 1993 Association of Mizar Users
:: deftheorem Def1 defines trivial TEX_2:def 1 :
theorem Th1: :: TEX_2:1
theorem :: TEX_2:2
theorem :: TEX_2:3
canceled;
theorem :: TEX_2:4
theorem :: TEX_2:5
canceled;
theorem :: TEX_2:6
theorem :: TEX_2:7
theorem :: TEX_2:8
theorem :: TEX_2:9
theorem :: TEX_2:10
canceled;
theorem :: TEX_2:11
canceled;
theorem :: TEX_2:12
:: deftheorem TEX_2:def 2 :
canceled;
:: deftheorem Def3 defines proper TEX_2:def 3 :
theorem Th13: :: TEX_2:13
theorem :: TEX_2:14
theorem Th15: :: TEX_2:15
theorem :: TEX_2:16
theorem Th17: :: TEX_2:17
theorem :: TEX_2:18
theorem :: TEX_2:19
:: deftheorem Def4 defines Sspace TEX_2:def 4 :
theorem :: TEX_2:20
theorem :: TEX_2:21
theorem :: TEX_2:22
canceled;
theorem :: TEX_2:23
theorem :: TEX_2:24
:: deftheorem Def5 defines discrete TEX_2:def 5 :
:: deftheorem Def6 defines discrete TEX_2:def 6 :
theorem Th25: :: TEX_2:25
theorem Th26: :: TEX_2:26
theorem Th27: :: TEX_2:27
theorem Th28: :: TEX_2:28
theorem :: TEX_2:29
theorem Th30: :: TEX_2:30
theorem Th31: :: TEX_2:31
theorem Th32: :: TEX_2:32
theorem :: TEX_2:33
theorem Th34: :: TEX_2:34
theorem Th35: :: TEX_2:35
theorem Th36: :: TEX_2:36
theorem Th37: :: TEX_2:37
theorem :: TEX_2:38
theorem :: TEX_2:39
Lm3:
for P, Q being set st P c= Q & P <> Q holds
Q \ P <> {}
theorem :: TEX_2:40
theorem Th41: :: TEX_2:41
theorem Th42: :: TEX_2:42
theorem :: TEX_2:43
theorem Th44: :: TEX_2:44
:: deftheorem Def7 defines maximal_discrete TEX_2:def 7 :
theorem :: TEX_2:45
theorem Th46: :: TEX_2:46
theorem Th47: :: TEX_2:47
theorem :: TEX_2:48
theorem Th49: :: TEX_2:49
theorem Th50: :: TEX_2:50
:: deftheorem Def8 defines maximal_discrete TEX_2:def 8 :
theorem Th51: :: TEX_2:51
theorem :: TEX_2:52
theorem Th53: :: TEX_2:53
theorem Th54: :: TEX_2:54
theorem Th55: :: TEX_2:55
theorem Th56: :: TEX_2:56
theorem Th57: :: TEX_2:57
theorem Th58: :: TEX_2:58
theorem :: TEX_2:59
theorem Th60: :: TEX_2:60
theorem :: TEX_2:61
theorem Th62: :: TEX_2:62
theorem Th63: :: TEX_2:63
theorem Th64: :: TEX_2:64
theorem Th65: :: TEX_2:65
theorem Th66: :: TEX_2:66
theorem Th67: :: TEX_2:67
theorem Th68: :: TEX_2:68
theorem :: TEX_2:69
theorem :: TEX_2:70
theorem :: TEX_2:71
theorem Th72: :: TEX_2:72
theorem :: TEX_2:73
theorem Th74: :: TEX_2:74
theorem :: TEX_2:75
Lm4:
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}
theorem Th76: :: TEX_2:76
theorem :: TEX_2:77
theorem Th78: :: TEX_2:78
theorem :: TEX_2:79