:: Topological Spaces and Continuous Functions
:: by Beata Padlewska and Agata Darmochwa\l
::
:: Received April 14, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines TopSpace-like PRE_TOPC:def 1 :
theorem :: PRE_TOPC:1
canceled;
theorem :: PRE_TOPC:2
canceled;
theorem :: PRE_TOPC:3
canceled;
theorem :: PRE_TOPC:4
canceled;
theorem Th5: :: PRE_TOPC:5
theorem :: PRE_TOPC:6
canceled;
theorem :: PRE_TOPC:7
canceled;
theorem :: PRE_TOPC:8
canceled;
theorem :: PRE_TOPC:9
canceled;
theorem :: PRE_TOPC:10
canceled;
theorem :: PRE_TOPC:11
canceled;
theorem :: PRE_TOPC:12
canceled;
theorem :: PRE_TOPC:13
canceled;
theorem :: PRE_TOPC:14
canceled;
theorem :: PRE_TOPC:15
canceled;
theorem :: PRE_TOPC:16
canceled;
theorem :: PRE_TOPC:17
canceled;
theorem :: PRE_TOPC:18
theorem :: PRE_TOPC:19
canceled;
theorem :: PRE_TOPC:20
canceled;
theorem :: PRE_TOPC:21
canceled;
theorem Th22: :: PRE_TOPC:22
theorem Th23: :: PRE_TOPC:23
theorem :: PRE_TOPC:24
canceled;
theorem :: PRE_TOPC:25
theorem :: PRE_TOPC:26
canceled;
theorem :: PRE_TOPC:27
:: deftheorem PRE_TOPC:def 2 :
canceled;
:: deftheorem PRE_TOPC:def 3 :
canceled;
:: deftheorem PRE_TOPC:def 4 :
canceled;
:: deftheorem Def5 defines open PRE_TOPC:def 5 :
:: deftheorem Def6 defines closed PRE_TOPC:def 6 :
:: deftheorem PRE_TOPC:def 7 :
canceled;
:: deftheorem PRE_TOPC:def 8 :
canceled;
:: deftheorem Def9 defines SubSpace PRE_TOPC:def 9 :
Lm1:
for T being TopStruct holds TopStruct(# the carrier of T,the topology of T #) is SubSpace of T
:: deftheorem Def10 defines | PRE_TOPC:def 10 :
theorem :: PRE_TOPC:28
theorem Th29: :: PRE_TOPC:29
theorem :: PRE_TOPC:30
:: deftheorem PRE_TOPC:def 11 :
canceled;
:: deftheorem Def12 defines continuous PRE_TOPC:def 12 :
theorem :: PRE_TOPC:31
theorem :: PRE_TOPC:32
canceled;
theorem :: PRE_TOPC:33
canceled;
theorem :: PRE_TOPC:34
canceled;
theorem :: PRE_TOPC:35
canceled;
theorem :: PRE_TOPC:36
canceled;
theorem :: PRE_TOPC:37
canceled;
theorem :: PRE_TOPC:38
canceled;
theorem Th39: :: PRE_TOPC:39
theorem :: PRE_TOPC:40
canceled;
theorem :: PRE_TOPC:41
theorem :: PRE_TOPC:42
canceled;
theorem Th43: :: PRE_TOPC:43
theorem Th44: :: PRE_TOPC:44
:: deftheorem Def13 defines Cl PRE_TOPC:def 13 :
theorem Th45: :: PRE_TOPC:45
theorem Th46: :: PRE_TOPC:46
theorem :: PRE_TOPC:47
theorem Th48: :: PRE_TOPC:48
theorem Th49: :: PRE_TOPC:49
theorem :: PRE_TOPC:50
theorem :: PRE_TOPC:51
theorem Th52: :: PRE_TOPC:52
theorem :: PRE_TOPC:53
theorem :: PRE_TOPC:54
theorem :: PRE_TOPC:55
theorem :: PRE_TOPC:56
theorem :: PRE_TOPC:57
:: deftheorem defines T_0 PRE_TOPC:def 14 :
:: deftheorem Def15 defines T_1 PRE_TOPC:def 15 :
:: deftheorem Def16 defines T_2 PRE_TOPC:def 16 :
:: deftheorem defines regular PRE_TOPC:def 17 :
:: deftheorem defines normal PRE_TOPC:def 18 :
:: deftheorem Def19 defines T_3 PRE_TOPC:def 19 :
:: deftheorem Def20 defines T_4 PRE_TOPC:def 20 :