:: Totally Bounded Metric Spaces :: by Alicia de la Cruz :: :: Received September 30, 1991 :: Copyright (c) 1991-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, METRIC_1, SUBSET_1, SETFAM_1, RELAT_2, FUNCT_1, REAL_1, CARD_1, ARYTM_3, XXREAL_0, POWER, RELAT_1, SEQ_1, SEQ_2, ORDINAL2, COMPLEX1, ARYTM_1, FINSET_1, STRUCT_0, TARSKI, NAT_1, BHSP_3, REWRITE1, ALI2, PRE_TOPC, PCOMPS_1, RCOMP_1, ZFMISC_1, ORDINAL1, XXREAL_2, MEASURE5, FINSEQ_1, TBSP_1, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1, FINSEQ_1, DOMAIN_1, SETFAM_1, FUNCT_2, BINOP_1, FINSET_1, NAT_1, STRUCT_0, PRE_TOPC, TOPS_2, SEQ_1, SEQ_2, COMPTS_1, METRIC_1, POWER, PCOMPS_1, ALI2, XXREAL_0; constructors SETFAM_1, DOMAIN_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1, FINSEQ_1, SEQ_2, POWER, TOPS_2, COMPTS_1, PCOMPS_1, ALI2, VALUED_1, RELSET_1, COMSEQ_2, BINOP_1; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, METRIC_1, PCOMPS_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve M for non empty MetrSpace, c,g1,g2 for Element of M; reserve N for non empty MetrStruct, w for Element of N, G for Subset-Family of N, C for Subset of N; reserve R for Reflexive non empty MetrStruct; reserve T for Reflexive symmetric triangle non empty MetrStruct, t1 for Element of T, Y for Subset-Family of T, P for Subset of T; reserve f for Function, n,m,p,n1,n2,k for Nat, r,s,L for Real, x,y for set; theorem :: TBSP_1:1 for L st 00 ex G st G is finite & the carrier of N = union G & for C st C in G ex w st C = Ball(w,r); end; reserve S1 for sequence of M, S2 for sequence of N; theorem :: TBSP_1:4 f is sequence of N iff dom f = NAT & for n holds f.n is Element of N; definition let N,S2; attr S2 is convergent means :: TBSP_1:def 2 ex x being Element of N st for r st r>0 ex n st for m st n<=m holds dist(S2.m,x) Element of M means :: TBSP_1:def 3 for r st r>0 ex n st for m st m>=n holds dist(S1.m,it)0 ex p st for n,m st p<=n & p<=m holds dist(S2.n,S2.m) Cauchy for sequence of M; end; theorem :: TBSP_1:6 for N being symmetric non empty MetrStruct, S2 being sequence of N holds S2 is Cauchy iff for r st r>0 ex p st for n,k st p<=n holds dist(S2.(n+k),S2.n) bounded; end; registration cluster bounded for non empty MetrSpace; end; registration let N; cluster empty -> bounded for Subset of N; end; registration let N; cluster bounded for Subset of N; end; theorem :: TBSP_1:10 for C being Subset of N holds ( C <> {} & C is bounded implies ex r,w st 0 bounded; end; theorem :: TBSP_1:13 for P, Q being Subset of T holds P is bounded & Q is bounded implies P \/ Q is bounded; theorem :: TBSP_1:14 for C, D being Subset of N holds C is bounded & D c= C implies D is bounded; theorem :: TBSP_1:15 for P being Subset of T holds P = {t1} implies P is bounded; theorem :: TBSP_1:16 for P being Subset of T holds P is finite implies P is bounded; registration let T; cluster finite -> bounded for Subset of T; end; registration let T; cluster finite non empty for Subset of T; end; theorem :: TBSP_1:17 Y is finite & (for P being Subset of T st P in Y holds P is bounded) implies union Y is bounded; theorem :: TBSP_1:18 N is bounded iff [#]N is bounded; registration let N be bounded non empty MetrStruct; cluster [#]N -> bounded; end; theorem :: TBSP_1:19 T is totally_bounded implies T is bounded; definition let N be Reflexive non empty MetrStruct, C be Subset of N; assume C is bounded; func diameter C -> Real means :: 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 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; end; theorem :: TBSP_1:20 for P being Subset of T holds P = {x} implies diameter P = 0; theorem :: TBSP_1:21 for S being Subset of R st S is bounded holds 0 <= diameter S; theorem :: TBSP_1:22 for A being Subset of M holds A <> {} & A is bounded & diameter A = 0 implies ex g being Point of M st A = {g}; theorem :: TBSP_1:23 0