:: Bases and Refinements of Topologies
:: by Grzegorz Bancerek
::
:: Received March 9, 1998
:: Copyright (c) 1998 Association of Mizar Users
theorem :: YELLOW_9:1
theorem Th2: :: YELLOW_9:2
theorem Th3: :: YELLOW_9:3
theorem Th4: :: YELLOW_9:4
theorem :: YELLOW_9:5
Lm1:
for tau being Subset-Family of {0 }
for r being Relation of {0 } st tau = {{} ,{0 }} & r = {[0 ,0 ]} holds
( TopRelStr(# {0 },r,tau #) is trivial & TopRelStr(# {0 },r,tau #) is reflexive & not TopRelStr(# {0 },r,tau #) is empty & TopRelStr(# {0 },r,tau #) is discrete & TopRelStr(# {0 },r,tau #) is finite )
:: deftheorem Def1 defines incl YELLOW_9:def 1 :
:: deftheorem defines +id YELLOW_9:def 2 :
:: deftheorem defines opp+id YELLOW_9:def 3 :
theorem :: YELLOW_9:6
theorem :: YELLOW_9:7
theorem Th8: :: YELLOW_9:8
theorem Th9: :: YELLOW_9:9
theorem :: YELLOW_9:10
theorem Th11: :: YELLOW_9:11
theorem :: YELLOW_9:12
theorem :: YELLOW_9:13
theorem Th14: :: YELLOW_9:14
theorem Th15: :: YELLOW_9:15
theorem Th16: :: YELLOW_9:16
theorem Th17: :: YELLOW_9:17
theorem Th18: :: YELLOW_9:18
theorem Th19: :: YELLOW_9:19
theorem Th20: :: YELLOW_9:20
theorem Th21: :: YELLOW_9:21
theorem Th22: :: YELLOW_9:22
theorem Th23: :: YELLOW_9:23
theorem Th24: :: YELLOW_9:24
theorem Th25: :: YELLOW_9:25
theorem Th26: :: YELLOW_9:26
theorem :: YELLOW_9:27
theorem :: YELLOW_9:28
theorem Th29: :: YELLOW_9:29
theorem :: YELLOW_9:30
theorem Th31: :: YELLOW_9:31
theorem Th32: :: YELLOW_9:32
theorem Th33: :: YELLOW_9:33
theorem :: YELLOW_9:34
theorem Th35: :: YELLOW_9:35
theorem :: YELLOW_9:36
theorem Th37: :: YELLOW_9:37
theorem Th38: :: YELLOW_9:38
theorem :: YELLOW_9:39
theorem Th40: :: YELLOW_9:40
theorem Th41: :: YELLOW_9:41
theorem :: YELLOW_9:42
theorem :: YELLOW_9:43
:: deftheorem Def4 defines TopAugmentation YELLOW_9:def 4 :
theorem :: YELLOW_9:44
theorem :: YELLOW_9:45
theorem :: YELLOW_9:46
theorem Th47: :: YELLOW_9:47
theorem Th48: :: YELLOW_9:48
theorem Th49: :: YELLOW_9:49
theorem Th50: :: YELLOW_9:50
theorem Th51: :: YELLOW_9:51
theorem :: YELLOW_9:52
Lm2:
for S being TopStruct ex T being strict TopSpace st
( the carrier of T = the carrier of S & the topology of S is prebasis of T )
:: deftheorem Def5 defines TopExtension YELLOW_9:def 5 :
theorem Th53: :: YELLOW_9:53
:: deftheorem Def6 defines Refinement YELLOW_9:def 6 :
theorem :: YELLOW_9:54
theorem :: YELLOW_9:55
theorem :: YELLOW_9:56
theorem :: YELLOW_9:57
theorem :: YELLOW_9:58
theorem Th59: :: YELLOW_9:59
theorem Th60: :: YELLOW_9:60
theorem :: YELLOW_9:61