:: Totally Bounded Metric Spaces :: by Alicia de la Cruz :: :: Received September 30, 1991 :: Copyright (c) 1991-2012 Association of Mizar Users begin theorem Th1: :: TBSP_1:1 for L being Real st 0 < L & L < 1 holds for n, m being Element of NAT st n <= m holds L to_power m <= L to_power n proofend; theorem Th2: :: TBSP_1:2 for L being Real st 0 < L & L < 1 holds for k being Element of NAT holds ( L to_power k <= 1 & 0 < L to_power k ) proofend; 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 Element of NAT st L to_power n < s proofend; definition let N be non empty MetrStruct ; attrN is totally_bounded means :Def1: :: TBSP_1:def 1 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) ) ); end; :: deftheorem Def1 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) ) ) ); 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 ) ) ) proofend; 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 Element of NAT holds f . n is Element of N ) ) ) proofend; definition let N be non empty MetrStruct ; let S2 be sequence of N; attrS2 is convergent means :Def2: :: TBSP_1:def 2 ex x being Element of N st for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds dist ((S2 . m),x) < r; end; :: deftheorem Def2 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 Element of NAT st for m being Element of 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 ; func lim S1 -> Element of M means :: TBSP_1:def 3 for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),it) < r; existence ex b1 being Element of M st for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),b1) < r by A1, Def2; uniqueness for b1, b2 being Element of M st ( for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),b1) < r ) & ( for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),b2) < r ) holds b1 = b2 proofend; 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 b3 being Element of M holds ( b3 = lim S1 iff for r being Real st r > 0 holds ex n being Element of NAT st for m being Element of NAT st m >= n holds dist ((S1 . m),b3) < r ); definition let N be non empty MetrStruct ; let S2 be sequence of N; attrS2 is Cauchy means :Def4: :: TBSP_1:def 4 for r being Real st r > 0 holds ex p being Element of NAT st for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r; end; :: deftheorem Def4 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 Element of NAT st for n, m being Element of NAT st p <= n & p <= m holds dist ((S2 . n),(S2 . m)) < r ); definition let N be non empty MetrStruct ; attrN is complete means :Def5: :: TBSP_1:def 5 for S2 being sequence of N st S2 is Cauchy holds S2 is convergent ; end; :: deftheorem Def5 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 ); definition let N be non empty MetrStruct ; let S2 be sequence of N; let n be Element of NAT ; :: original:. redefine funcS2 . n -> Element of N; coherence S2 . n is Element of N proofend; end; 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 proofend; registration let M be non empty symmetric triangle MetrStruct ; cluster Function-like V33( NAT , the carrier of M) convergent -> Cauchy for Element of K10(K11(NAT, the carrier of M)); coherence for b1 being sequence of M st b1 is convergent holds b1 is Cauchy by Th5; end; 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 Element of NAT st for n, k being Element of NAT st p <= n holds dist ((S2 . (n + k)),(S2 . n)) < r ) proofend; 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 ) ) proofend; theorem :: TBSP_1:8 for T being non empty Reflexive symmetric triangle MetrStruct st TopSpaceMetr T is compact holds T is complete proofend; 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 proofend; definition let N be non empty MetrStruct ; attrN is bounded means :Def6: :: 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; attrC is bounded means :Def7: :: TBSP_1:def 7 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 ) ); end; :: deftheorem Def6 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 ) ) ); :: deftheorem Def7 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 ) ) ); registration let A be non empty set ; cluster DiscreteSpace A -> bounded ; coherence DiscreteSpace A is bounded proofend; end; registration cluster non empty Reflexive discerning symmetric triangle Discerning bounded for MetrStruct ; existence ex b1 being non empty MetrSpace st b1 is bounded proofend; end; registration let N be non empty MetrStruct ; cluster empty -> bounded for Element of K10( the carrier of N); coherence for b1 being Subset of N st b1 is empty holds b1 is bounded proofend; end; registration let N be non empty MetrStruct ; cluster bounded for Element of K10( the carrier of N); existence ex b1 being Subset of N st b1 is bounded proofend; 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 ) ) proofend; theorem Th11: :: TBSP_1:11 for N being non empty MetrStruct for w being Element of N for r being real number st N is Reflexive & 0 < r holds w in Ball (w,r) proofend; theorem Th12: :: TBSP_1:12 for T being non empty Reflexive symmetric triangle MetrStruct for t1 being Element of T for r being real number st r <= 0 holds Ball (t1,r) = {} proofend; 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 proofend; registration let T be non empty Reflexive symmetric triangle MetrStruct ; let t1 be Element of T; let r be real number ; cluster Ball (t1,r) -> bounded ; coherence Ball (t1,r) is bounded proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; registration let T be non empty Reflexive symmetric triangle MetrStruct ; cluster finite -> bounded for Element of K10( the carrier of T); coherence for b1 being Subset of T st b1 is finite holds b1 is bounded by Th16; end; registration let T be non empty Reflexive symmetric triangle MetrStruct ; cluster non empty finite for Element of K10( the carrier of T); existence ex b1 being Subset of T st ( b1 is finite & not b1 is empty ) proofend; 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 proofend; theorem Th18: :: TBSP_1:18 for N being non empty MetrStruct holds ( N is bounded iff [#] N is bounded ) proofend; registration let N be non empty bounded MetrStruct ; cluster [#] N -> bounded ; coherence [#] N is bounded by Th18; end; theorem :: TBSP_1:19 for T being non empty Reflexive symmetric triangle MetrStruct st T is totally_bounded holds T is bounded proofend; definition let N be non empty Reflexive MetrStruct ; 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 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 ) ) proofend; 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 ) ) proofend; 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 b3 being Real holds ( ( C <> {} implies ( b3 = diameter C iff ( ( for x, y being Point of N st x in C & y in C holds dist (x,y) <= b3 ) & ( 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 b3 <= s ) ) ) ) & ( not C <> {} implies ( b3 = diameter C iff b3 = 0 ) ) ); 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 proofend; 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 proofend; 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} proofend; 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 proofend; 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 proofend; 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) proofend; 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 proofend;