environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, ORDINAL1, XBOOLE_0, FINSET_1;
theorems METRIC_1, SUBSET_1, FUNCT_1, PCOMPS_1, PRE_TOPC, MEMBERED, TOPS_2, TARSKI, COMPTS_1, NAT_1, SEQ_2, ZFMISC_1, POWER, SERIES_1, ABSVALUE, FUNCT_2, SETFAM_1, FINSEQ_1, ALI2, RELSET_1, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_1, FINSET_1, XREAL_1, XXREAL_0, ORDINAL1, RELAT_1;
schemes DOMAIN_1, SUBSET_1, NAT_1, SEQ_1, FINSET_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;
constructors HIDDEN, 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;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0;
expansions TARSKI, XBOOLE_0;
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 ) ) )
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
definition
let N be non
empty Reflexive MetrStruct ;
let C be
Subset of
N;
assume A1:
C is
bounded
;
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 ) )
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 ) )
end;