:: by Alicia de la Cruz

::

:: Received September 30, 1991

:: Copyright (c) 1991-2018 Association of Mizar Users

theorem Th1: :: TBSP_1:1

for L being Real st 0 < L & L < 1 holds

for n, m being Nat st n <= m holds

L to_power m <= L to_power n

for n, m being Nat st n <= m holds

L to_power m <= L to_power n

proof end;

theorem Th2: :: TBSP_1:2

for L being Real st 0 < L & L < 1 holds

for k being Nat holds

( L to_power k <= 1 & 0 < L to_power k )

for k being Nat holds

( L to_power k <= 1 & 0 < L to_power k )

proof end;

theorem Th3: :: TBSP_1:3

for L being Real st 0 < L & L < 1 holds

for s being Real st 0 < s holds

ex n being Nat st L to_power n < s

for s being Real st 0 < s holds

ex n being Nat st L to_power n < s

proof end;

:: deftheorem defines totally_bounded TBSP_1:def 1 :

for N being non empty MetrStruct holds

( N is totally_bounded iff for r being Real st r > 0 holds

ex G being Subset-Family of N st

( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds

ex w being Element of N st C = Ball (w,r) ) ) );

for N being non empty MetrStruct holds

( N is totally_bounded iff for r being Real st r > 0 holds

ex G being Subset-Family of N st

( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds

ex w being Element of N st C = Ball (w,r) ) ) );

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 ) ) )

proof end;

theorem :: TBSP_1:4

for N being non empty MetrStruct

for f being Function holds

( f is sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) )

for f being Function holds

( f is sequence of N iff ( dom f = NAT & ( for n being Nat holds f . n is Element of N ) ) )

proof end;

:: deftheorem defines convergent TBSP_1:def 2 :

for N being non empty MetrStruct

for S2 being sequence of N holds

( S2 is convergent iff ex x being Element of N st

for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S2 . m),x) < r );

for N being non empty MetrStruct

for S2 being sequence of N holds

( S2 is convergent iff ex x being Element of N st

for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

dist ((S2 . m),x) < r );

definition

let M be non empty MetrSpace;

let S1 be sequence of M;

assume A1: S1 is convergent ;

ex b_{1} being Element of M st

for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),b_{1}) < r
by A1;

uniqueness

for b_{1}, b_{2} being Element of M st ( for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),b_{1}) < r ) & ( for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),b_{2}) < r ) holds

b_{1} = b_{2}

end;
let S1 be sequence of M;

assume A1: S1 is convergent ;

func lim S1 -> Element of M means :: TBSP_1:def 3

for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),it) < r;

existence for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),it) < r;

ex b

for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),b

uniqueness

for b

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),b

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),b

b

proof end;

:: deftheorem defines lim TBSP_1:def 3 :

for M being non empty MetrSpace

for S1 being sequence of M st S1 is convergent holds

for b_{3} being Element of M holds

( b_{3} = lim S1 iff for r being Real st r > 0 holds

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),b_{3}) < r );

for M being non empty MetrSpace

for S1 being sequence of M st S1 is convergent holds

for b

( b

ex n being Nat st

for m being Nat st m >= n holds

dist ((S1 . m),b

:: deftheorem defines Cauchy TBSP_1:def 4 :

for N being non empty MetrStruct

for S2 being sequence of N holds

( S2 is Cauchy iff for r being Real st r > 0 holds

ex p being Nat st

for n, m being Nat st p <= n & p <= m holds

dist ((S2 . n),(S2 . m)) < r );

for N being non empty MetrStruct

for S2 being sequence of N holds

( S2 is Cauchy iff for r being Real st r > 0 holds

ex p being Nat st

for n, m being Nat st p <= n & p <= m holds

dist ((S2 . n),(S2 . m)) < r );

definition

let N be non empty MetrStruct ;

end;
attr N is complete means :: TBSP_1:def 5

for S2 being sequence of N st S2 is Cauchy holds

S2 is convergent ;

for S2 being sequence of N st S2 is Cauchy holds

S2 is convergent ;

:: deftheorem defines complete TBSP_1:def 5 :

for N being non empty MetrStruct holds

( N is complete iff for S2 being sequence of N st S2 is Cauchy holds

S2 is convergent );

for N being non empty MetrStruct holds

( N is complete iff for S2 being sequence of N st S2 is Cauchy holds

S2 is convergent );

theorem Th5: :: TBSP_1:5

for N being non empty MetrStruct

for S2 being sequence of N st N is triangle & N is symmetric & S2 is convergent holds

S2 is Cauchy

for S2 being sequence of N st N is triangle & N is symmetric & S2 is convergent holds

S2 is Cauchy

proof end;

registration

let M be non empty symmetric triangle MetrStruct ;

coherence

for b_{1} being sequence of M st b_{1} is convergent holds

b_{1} is Cauchy
by Th5;

end;
coherence

for b

b

theorem Th6: :: TBSP_1:6

for N being non empty symmetric MetrStruct

for S2 being sequence of N holds

( S2 is Cauchy iff for r being Real st r > 0 holds

ex p being Nat st

for n, k being Nat st p <= n holds

dist ((S2 . (n + k)),(S2 . n)) < r )

for S2 being sequence of N holds

( S2 is Cauchy iff for r being Real st r > 0 holds

ex p being Nat st

for n, k being Nat st p <= n holds

dist ((S2 . (n + k)),(S2 . n)) < r )

proof end;

theorem :: TBSP_1:7

for M being non empty MetrSpace

for f being Contraction of M st M is complete holds

ex c being Element of M st

( f . c = c & ( for y being Element of M st f . y = y holds

y = c ) )

for f being Contraction of M st M is complete holds

ex c being Element of M st

( f . c = c & ( for y being Element of M st f . y = y holds

y = c ) )

proof end;

theorem :: TBSP_1:8

for T being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr T is compact holds

T is complete

T is complete

proof end;

theorem :: TBSP_1:9

for N being non empty MetrStruct st N is Reflexive & N is triangle & TopSpaceMetr N is compact holds

N is totally_bounded

N is totally_bounded

proof end;

definition

let N be non empty MetrStruct ;

end;
attr N is bounded means :: TBSP_1:def 6

ex r being Real st

( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) );

let C be Subset of N;ex r being Real st

( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) );

:: deftheorem defines bounded TBSP_1:def 6 :

for N being non empty MetrStruct holds

( N is bounded iff ex r being Real st

( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) ) );

for N being non empty MetrStruct holds

( N is bounded iff ex r being Real st

( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) ) );

:: deftheorem defines bounded TBSP_1:def 7 :

for N being non empty MetrStruct

for C being Subset of N holds

( C is bounded iff ex r being Real st

( 0 < r & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r ) ) );

for N being non empty MetrStruct

for C being Subset of N holds

( C is bounded iff ex r being Real st

( 0 < r & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r ) ) );

registration

let N be non empty MetrStruct ;

coherence

for b_{1} being Subset of N st b_{1} is empty holds

b_{1} is bounded

end;
coherence

for b

b

proof end;

registration
end;

theorem Th10: :: TBSP_1:10

for N being non empty MetrStruct

for C being Subset of N holds

( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st

( 0 < r & w in C & ( for z being Point of N st z in C holds

dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st

( 0 < r & ( for z being Point of N st z in C holds

dist (w,z) <= r ) ) implies C is bounded ) )

for C being Subset of N holds

( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st

( 0 < r & w in C & ( for z being Point of N st z in C holds

dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st

( 0 < r & ( for z being Point of N st z in C holds

dist (w,z) <= r ) ) implies C is bounded ) )

proof end;

theorem Th11: :: TBSP_1:11

for N being non empty MetrStruct

for w being Element of N

for r being Real st N is Reflexive & 0 < r holds

w in Ball (w,r)

for w being Element of N

for r being Real st N is Reflexive & 0 < r holds

w in Ball (w,r)

proof end;

theorem Th12: :: TBSP_1:12

for T being non empty Reflexive symmetric triangle MetrStruct

for t1 being Element of T

for r being Real st r <= 0 holds

Ball (t1,r) = {}

for t1 being Element of T

for r being Real st r <= 0 holds

Ball (t1,r) = {}

proof end;

Lm2: for T being non empty Reflexive symmetric triangle MetrStruct

for t1 being Element of T

for r being Real st 0 < r holds

Ball (t1,r) is bounded

proof end;

registration

let T be non empty Reflexive symmetric triangle MetrStruct ;

let t1 be Element of T;

let r be Real;

coherence

Ball (t1,r) is bounded

end;
let t1 be Element of T;

let r be Real;

coherence

Ball (t1,r) is bounded

proof end;

theorem Th13: :: TBSP_1:13

for T being non empty Reflexive symmetric triangle MetrStruct

for P, Q being Subset of T st P is bounded & Q is bounded holds

P \/ Q is bounded

for P, Q being Subset of T st P is bounded & Q is bounded holds

P \/ Q is bounded

proof end;

theorem Th14: :: TBSP_1:14

for N being non empty MetrStruct

for C, D being Subset of N st C is bounded & D c= C holds

D is bounded

for C, D being Subset of N st C is bounded & D c= C holds

D is bounded

proof end;

theorem Th15: :: TBSP_1:15

for T being non empty Reflexive symmetric triangle MetrStruct

for t1 being Element of T

for P being Subset of T st P = {t1} holds

P is bounded

for t1 being Element of T

for P being Subset of T st P = {t1} holds

P is bounded

proof end;

theorem Th16: :: TBSP_1:16

for T being non empty Reflexive symmetric triangle MetrStruct

for P being Subset of T st P is finite holds

P is bounded

for P being Subset of T st P is finite holds

P is bounded

proof end;

registration

let T be non empty Reflexive symmetric triangle MetrStruct ;

coherence

for b_{1} being Subset of T st b_{1} is finite holds

b_{1} is bounded
by Th16;

end;
coherence

for b

b

registration

let T be non empty Reflexive symmetric triangle MetrStruct ;

existence

ex b_{1} being Subset of T st

( b_{1} is finite & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

theorem Th17: :: TBSP_1:17

for T being non empty Reflexive symmetric triangle MetrStruct

for Y being Subset-Family of T st Y is finite & ( for P being Subset of T st P in Y holds

P is bounded ) holds

union Y is bounded

for Y being Subset-Family of T st Y is finite & ( for P being Subset of T st P in Y holds

P is bounded ) holds

union Y is bounded

proof end;

theorem :: TBSP_1:19

for T being non empty Reflexive symmetric triangle MetrStruct st T is totally_bounded holds

T is bounded

T is bounded

proof end;

definition

let N be non empty Reflexive MetrStruct ;

let C be Subset of N;

assume A1: C is bounded ;

for b_{1} being Real holds verum
;

existence

( ( C <> {} implies ex b_{1} being Real st

( ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= b_{1} ) & ( 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

b_{1} <= s ) ) ) & ( not C <> {} implies ex b_{1} being Real st b_{1} = 0 ) )

for b_{1}, b_{2} being Real holds

( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= b_{1} ) & ( 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

b_{1} <= s ) & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= b_{2} ) & ( 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

b_{2} <= s ) implies b_{1} = b_{2} ) & ( not C <> {} & b_{1} = 0 & b_{2} = 0 implies b_{1} = b_{2} ) )

end;
let C be Subset of N;

assume A1: C is bounded ;

func diameter C -> Real means :Def8: :: TBSP_1:def 8

( ( 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 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 ;

for b

existence

( ( C <> {} implies ex b

( ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= b

dist (x,y) <= s ) holds

b

proof end;

uniqueness for b

( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= b

dist (x,y) <= s ) holds

b

dist (x,y) <= b

dist (x,y) <= s ) holds

b

proof end;

:: deftheorem Def8 defines diameter TBSP_1:def 8 :

for N being non empty Reflexive MetrStruct

for C being Subset of N st C is bounded holds

for b_{3} being Real holds

( ( C <> {} implies ( b_{3} = diameter C iff ( ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= b_{3} ) & ( 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

b_{3} <= s ) ) ) ) & ( not C <> {} implies ( b_{3} = diameter C iff b_{3} = 0 ) ) );

for N being non empty Reflexive MetrStruct

for C being Subset of N st C is bounded holds

for b

( ( C <> {} implies ( b

dist (x,y) <= b

dist (x,y) <= s ) holds

b

theorem :: TBSP_1:20

for T being non empty Reflexive symmetric triangle MetrStruct

for x being set

for P being Subset of T st P = {x} holds

diameter P = 0

for x being set

for P being Subset of T st P = {x} holds

diameter P = 0

proof end;

theorem Th21: :: TBSP_1:21

for R being non empty Reflexive MetrStruct

for S being Subset of R st S is bounded holds

0 <= diameter S

for S being Subset of R st S is bounded holds

0 <= diameter S

proof end;

theorem :: TBSP_1:22

for M being non empty MetrSpace

for A being Subset of M st A <> {} & A is bounded & diameter A = 0 holds

ex g being Point of M st A = {g}

for A being Subset of M st A <> {} & A is bounded & diameter A = 0 holds

ex g being Point of M st A = {g}

proof end;

theorem :: TBSP_1:23

for T being non empty Reflexive symmetric triangle MetrStruct

for t1 being Element of T

for r being Real st 0 < r holds

diameter (Ball (t1,r)) <= 2 * r

for t1 being Element of T

for r being Real st 0 < r holds

diameter (Ball (t1,r)) <= 2 * r

proof end;

theorem :: TBSP_1:24

for R being non empty Reflexive MetrStruct

for S, V being Subset of R st S is bounded & V c= S holds

diameter V <= diameter S

for S, V being Subset of R st S is bounded & V c= S holds

diameter V <= diameter S

proof end;

theorem :: TBSP_1:25

for T being non empty Reflexive symmetric triangle MetrStruct

for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds

diameter (P \/ Q) <= (diameter P) + (diameter Q)

for P, Q being Subset of T st P is bounded & Q is bounded & P meets Q holds

diameter (P \/ Q) <= (diameter P) + (diameter Q)

proof end;

theorem :: TBSP_1:26

for T being non empty Reflexive symmetric triangle MetrStruct

for S1 being sequence of T st S1 is Cauchy holds

rng S1 is bounded

for S1 being sequence of T st S1 is Cauchy holds

rng S1 is bounded

proof end;