:: Totally Bounded Metric Spaces
:: by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991 Association of Mizar Users
theorem Th1: :: TBSP_1:1
theorem Th2: :: TBSP_1:2
theorem Th3: :: TBSP_1:3
:: deftheorem Def1 defines totally_bounded TBSP_1:def 1 :
Lm1:
for N being non empty MetrStruct
for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) )
theorem :: TBSP_1:4
canceled;
theorem :: TBSP_1:5
:: deftheorem TBSP_1:def 2 :
canceled;
:: deftheorem Def3 defines convergent TBSP_1:def 3 :
:: deftheorem defines lim TBSP_1:def 4 :
:: deftheorem Def5 defines Cauchy TBSP_1:def 5 :
:: deftheorem Def6 defines complete TBSP_1:def 6 :
theorem :: TBSP_1:6
canceled;
theorem Th7: :: TBSP_1:7
theorem Th8: :: TBSP_1:8
theorem :: TBSP_1:9
theorem :: TBSP_1:10
theorem :: TBSP_1:11
canceled;
theorem :: TBSP_1:12
:: deftheorem TBSP_1:def 7 :
canceled;
:: deftheorem Def8 defines bounded TBSP_1:def 8 :
:: deftheorem Def9 defines bounded TBSP_1:def 9 :
theorem :: TBSP_1:13
canceled;
theorem Th14: :: TBSP_1:14
theorem Th15: :: TBSP_1:15
theorem Th16: :: TBSP_1:16
theorem Th17: :: TBSP_1:17
Lm2:
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being real number st 0 < r holds
Ball t1,r is bounded
theorem :: TBSP_1:18
canceled;
theorem Th19: :: TBSP_1:19
theorem Th20: :: TBSP_1:20
theorem Th21: :: TBSP_1:21
theorem Th22: :: TBSP_1:22
theorem Th23: :: TBSP_1:23
theorem Th24: :: TBSP_1:24
theorem Th25: :: TBSP_1:25
theorem :: TBSP_1:26
definition
let N be non
empty Reflexive MetrStruct ;
let C be
Subset of
N;
assume A1:
C is
bounded
;
func diameter C -> Real means :
Def10:
:: TBSP_1:def 10
( ( for
x,
y being
Point of
N st
x in C &
y in C holds
dist x,
y <= it ) & ( for
s being
Real st ( for
x,
y being
Point of
N st
x in C &
y in C holds
dist x,
y <= s ) holds
it <= s ) )
if C <> {} otherwise it = 0 ;
consistency
for b1 being Real holds verum
;
existence
( ( C <> {} implies ex b1 being Real st
( ( for x, y being Point of N st x in C & y in C holds
dist x,y <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist x,y <= s ) holds
b1 <= s ) ) ) & ( not C <> {} implies ex b1 being Real st b1 = 0 ) )
uniqueness
for b1, b2 being Real holds
( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist x,y <= s ) holds
b1 <= s ) & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= b2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist x,y <= s ) holds
b2 <= s ) implies b1 = b2 ) & ( not C <> {} & b1 = 0 & b2 = 0 implies b1 = b2 ) )
end;
:: deftheorem Def10 defines diameter TBSP_1:def 10 :
theorem :: TBSP_1:27
canceled;
theorem :: TBSP_1:28
theorem Th29: :: TBSP_1:29
theorem :: TBSP_1:30
theorem :: TBSP_1:31
theorem :: TBSP_1:32
theorem :: TBSP_1:33
theorem :: TBSP_1:34