:: Families of Subsets, Subspaces and Mappings in Topological Spaces
:: by Agata Darmochwa{\l}
::
:: Received June 21, 1989
:: Copyright (c) 1990 Association of Mizar Users
theorem :: TOPS_2:1
theorem :: TOPS_2:2
canceled;
theorem Th3: :: TOPS_2:3
theorem :: TOPS_2:4
canceled;
theorem :: TOPS_2:5
theorem :: TOPS_2:6
theorem :: TOPS_2:7
canceled;
theorem :: TOPS_2:8
canceled;
theorem :: TOPS_2:9
canceled;
theorem :: TOPS_2:10
theorem Th11: :: TOPS_2:11
theorem Th12: :: TOPS_2:12
Lm1:
for T being 1-sorted
for F being Subset-Family of T st COMPLEMENT F is finite holds
F is finite
theorem Th13: :: TOPS_2:13
:: deftheorem Def1 defines open TOPS_2:def 1 :
:: deftheorem Def2 defines closed TOPS_2:def 2 :
theorem :: TOPS_2:14
canceled;
theorem :: TOPS_2:15
canceled;
theorem Th16: :: TOPS_2:16
theorem :: TOPS_2:17
theorem :: TOPS_2:18
theorem :: TOPS_2:19
theorem :: TOPS_2:20
theorem :: TOPS_2:21
theorem :: TOPS_2:22
theorem :: TOPS_2:23
theorem :: TOPS_2:24
theorem :: TOPS_2:25
theorem Th26: :: TOPS_2:26
theorem Th27: :: TOPS_2:27
theorem :: TOPS_2:28
theorem :: TOPS_2:29
theorem :: TOPS_2:30
canceled;
theorem :: TOPS_2:31
theorem Th32: :: TOPS_2:32
theorem Th33: :: TOPS_2:33
theorem Th34: :: TOPS_2:34
theorem :: TOPS_2:35
theorem :: TOPS_2:36
theorem :: TOPS_2:37
canceled;
theorem Th38: :: TOPS_2:38
:: deftheorem Def3 defines | TOPS_2:def 3 :
theorem :: TOPS_2:39
canceled;
theorem :: TOPS_2:40
theorem Th41: :: TOPS_2:41
theorem :: TOPS_2:42
theorem :: TOPS_2:43
theorem Th44: :: TOPS_2:44
theorem :: TOPS_2:45
theorem :: TOPS_2:46
theorem :: TOPS_2:47
theorem :: TOPS_2:48
theorem :: TOPS_2:49
theorem :: TOPS_2:50
theorem :: TOPS_2:51
canceled;
theorem Th52: :: TOPS_2:52
theorem :: TOPS_2:53
canceled;
theorem :: TOPS_2:54
theorem Th55: :: TOPS_2:55
theorem Th56: :: TOPS_2:56
theorem Th57: :: TOPS_2:57
theorem Th58: :: TOPS_2:58
theorem :: TOPS_2:59
theorem :: TOPS_2:60
:: deftheorem Def4 defines /" TOPS_2:def 4 :
theorem :: TOPS_2:61
canceled;
theorem Th62: :: TOPS_2:62
theorem Th63: :: TOPS_2:63
theorem Th64: :: TOPS_2:64
theorem :: TOPS_2:65
theorem Th66: :: TOPS_2:66
theorem Th67: :: TOPS_2:67
theorem Th68: :: TOPS_2:68
:: deftheorem Def5 defines being_homeomorphism TOPS_2:def 5 :
theorem :: TOPS_2:69
canceled;
theorem Th70: :: TOPS_2:70
theorem :: TOPS_2:71
theorem :: TOPS_2:72
theorem :: TOPS_2:73
theorem :: TOPS_2:74
theorem Th75: :: TOPS_2:75
theorem :: TOPS_2:76
theorem :: TOPS_2:77