:: Totally Bounded Metric Spaces
:: by Alicia de la Cruz
::
:: Received September 30, 1991
:: Copyright (c) 1991-2017 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