:: Compactness of the Bounded Closed Subsets of TOP-REAL 2
:: by Artur Korni{\l}owicz
::
:: Received February 19, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: TOPREAL6:1
canceled;
theorem :: TOPREAL6:2
canceled;
theorem :: TOPREAL6:3
canceled;
theorem :: TOPREAL6:4
canceled;
theorem :: TOPREAL6:5
canceled;
theorem Th6: :: TOPREAL6:6
theorem Th7: :: TOPREAL6:7
theorem Th8: :: TOPREAL6:8
theorem :: TOPREAL6:9
theorem Th10: :: TOPREAL6:10
theorem :: TOPREAL6:11
theorem Th12: :: TOPREAL6:12
theorem Th13: :: TOPREAL6:13
theorem Th14: :: TOPREAL6:14
theorem :: TOPREAL6:15
theorem Th16: :: TOPREAL6:16
theorem Th17: :: TOPREAL6:17
theorem :: TOPREAL6:18
theorem :: TOPREAL6:19
theorem Th20: :: TOPREAL6:20
theorem :: TOPREAL6:21
theorem Th22: :: TOPREAL6:22
theorem :: TOPREAL6:23
canceled;
theorem Th24: :: TOPREAL6:24
theorem Th25: :: TOPREAL6:25
theorem :: TOPREAL6:26
theorem :: TOPREAL6:27
canceled;
theorem :: TOPREAL6:28
canceled;
theorem Th29: :: TOPREAL6:29
theorem Th30: :: TOPREAL6:30
theorem :: TOPREAL6:31
theorem Th32: :: TOPREAL6:32
theorem :: TOPREAL6:33
theorem Th34: :: TOPREAL6:34
theorem Th35: :: TOPREAL6:35
theorem Th36: :: TOPREAL6:36
theorem :: TOPREAL6:37
theorem :: TOPREAL6:38
theorem :: TOPREAL6:39
theorem :: TOPREAL6:40
theorem :: TOPREAL6:41
theorem :: TOPREAL6:42
theorem :: TOPREAL6:43
theorem :: TOPREAL6:44
theorem :: TOPREAL6:45
theorem :: TOPREAL6:46
theorem Th47: :: TOPREAL6:47
theorem Th48: :: TOPREAL6:48
theorem Th49: :: TOPREAL6:49
theorem Th50: :: TOPREAL6:50
theorem Th51: :: TOPREAL6:51
theorem Th52: :: TOPREAL6:52
theorem :: TOPREAL6:53
theorem :: TOPREAL6:54
theorem :: TOPREAL6:55
theorem :: TOPREAL6:56
theorem :: TOPREAL6:57
theorem :: TOPREAL6:58
theorem :: TOPREAL6:59
theorem :: TOPREAL6:60
theorem Th61: :: TOPREAL6:61
theorem :: TOPREAL6:62
theorem :: TOPREAL6:63
theorem :: TOPREAL6:64
Lm1:
for M being non empty MetrSpace
for z being Point of M
for r being real number
for A being Subset of (TopSpaceMetr M) st A = cl_Ball z,r holds
A ` is open
theorem Th65: :: TOPREAL6:65
theorem :: TOPREAL6:66
theorem Th67: :: TOPREAL6:67
theorem Th68: :: TOPREAL6:68
theorem :: TOPREAL6:69
theorem :: TOPREAL6:70
theorem Th71: :: TOPREAL6:71
theorem :: TOPREAL6:72
theorem Th73: :: TOPREAL6:73
theorem :: TOPREAL6:74
theorem :: TOPREAL6:75
canceled;
theorem Th76: :: TOPREAL6:76
theorem Th77: :: TOPREAL6:77
theorem Th78: :: TOPREAL6:78
Lm2:
R^1 = TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #)
by PCOMPS_1:def 6, TOPMETR:def 7;
theorem Th79: :: TOPREAL6:79
theorem :: TOPREAL6:80
theorem Th81: :: TOPREAL6:81
theorem :: TOPREAL6:82
theorem Th83: :: TOPREAL6:83
theorem Th84: :: TOPREAL6:84
theorem Th85: :: TOPREAL6:85
theorem :: TOPREAL6:86
theorem Th87: :: TOPREAL6:87
theorem Th88: :: TOPREAL6:88
theorem Th89: :: TOPREAL6:89
theorem Th90: :: TOPREAL6:90
theorem Th91: :: TOPREAL6:91
theorem Th92: :: TOPREAL6:92
theorem Th93: :: TOPREAL6:93
theorem :: TOPREAL6:94
theorem :: TOPREAL6:95
theorem :: TOPREAL6:96
theorem :: TOPREAL6:97
theorem Th98: :: TOPREAL6:98
theorem :: TOPREAL6:99
definition
let n be
Element of
NAT ;
let a,
b be
Point of
(TOP-REAL n);
func dist a,
b -> Real means :
Def1:
:: TOPREAL6:def 1
ex
p,
q being
Point of
(Euclid n) st
(
p = a &
q = b &
it = dist p,
q );
existence
ex b1 being Real ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist p,q )
uniqueness
for b1, b2 being Real st ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist p,q ) & ex p, q being Point of (Euclid n) st
( p = a & q = b & b2 = dist p,q ) holds
b1 = b2
;
commutativity
for b1 being Real
for a, b being Point of (TOP-REAL n) st ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist p,q ) holds
ex p, q being Point of (Euclid n) st
( p = b & q = a & b1 = dist p,q )
;
end;
:: deftheorem Def1 defines dist TOPREAL6:def 1 :
theorem Th100: :: TOPREAL6:100
theorem Th101: :: TOPREAL6:101
theorem :: TOPREAL6:102
theorem :: TOPREAL6:103
theorem :: TOPREAL6:104