begin
theorem Th1:
theorem Th2:
theorem Th3:
:: 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 ) ) )
theorem
canceled;
theorem
:: 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
canceled;
theorem Th7:
theorem Th8:
theorem
theorem
theorem
canceled;
theorem
:: deftheorem TBSP_1:def 7 :
canceled;
:: deftheorem Def8 defines bounded TBSP_1:def 8 :
:: deftheorem Def9 defines bounded TBSP_1:def 9 :
theorem
canceled;
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
Lm2:
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of
for r being real number st 0 < r holds
Ball t1,r is bounded
theorem
canceled;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
definition
let N be non
empty Reflexive MetrStruct ;
let C be
Subset of ;
assume A1:
C is
bounded
;
func diameter C -> Real means :
Def10:
( ( for
x,
y being
Point of st
x in C &
y in C holds
dist x,
y <= it ) & ( for
s being
Real st ( for
x,
y being
Point of 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 st x in C & y in C holds
dist x,y <= b1 ) & ( for s being Real st ( for x, y being Point of 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 st x in C & y in C holds
dist x,y <= b1 ) & ( for s being Real st ( for x, y being Point of st x in C & y in C holds
dist x,y <= s ) holds
b1 <= s ) & ( for x, y being Point of st x in C & y in C holds
dist x,y <= b2 ) & ( for s being Real st ( for x, y being Point of 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
canceled;
theorem
theorem Th29:
theorem
theorem
theorem
theorem
theorem