environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, METRIC_1, PROB_1, REWRITE1, TARSKI, RELAT_1, STRUCT_0, SUBSET_1, FUNCT_1, PCOMPS_1, REAL_1, PRE_TOPC, CARD_1, ARYTM_3, NEWTON, XXREAL_0, NAT_1, SEQ_1, ZFMISC_1, MCART_1, ARYTM_1, BHSP_3, SEQ_2, ORDINAL2, NORMSP_1, RELAT_2, ORDINAL1, METRIC_6, RCOMP_1, COMPTS_1, WAYBEL_3, YELLOW_8, FRECHET, CONNSP_2, PARTFUN1, FCONT_1, TMAP_1, CFCONT_1, RLTOPSP1, SUPINF_2, ALGSTR_0, RLVECT_1, SETFAM_1, COMPLEX1, RLVECT_3, CARD_3, NORMSP_2, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, COMPLEX1, REAL_1, NAT_1, STRUCT_0, ALGSTR_0, PRE_TOPC, FRECHET, NEWTON, FRECHET2, YELLOW_8, DOMAIN_1, WAYBEL_3, RLVECT_1, CONVEX1, COMPTS_1, TBSP_1, TMAP_1, CONNSP_2, CARD_3, METRIC_1, METRIC_6, PCOMPS_1, RUSUB_4, RLTOPSP1, NFCONT_1, SEQ_1, KURATO_2, NORMSP_0, NORMSP_1;
definitions TARSKI, RLVECT_1, RLTOPSP1, ALGSTR_0, PRE_TOPC;
theorems TARSKI, XBOOLE_1, RLVECT_1, FRECHET, FRECHET2, YELLOW_8, WAYBEL12, ZFMISC_1, TMAP_1, CONNSP_2, FUNCT_2, XBOOLE_0, XREAL_1, COMPLEX1, XCMPLX_1, NORMSP_1, METRIC_1, METRIC_6, PCOMPS_1, SUBSET_1, PRE_TOPC, BINOP_1, TOPS_1, NFCONT_1, NEWTON, XXREAL_0, FUNCT_1, TBSP_1, NAT_1, ORDINAL1, TOPREAL6, PREPOWER, PARTFUN1, RELSET_1, TOPS_2, XREAL_0;
schemes BINOP_1, RECDEF_1, NAT_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, STRUCT_0, TOPS_1, METRIC_1, PCOMPS_1, HAUSDORF, KURATO_2, RLTOPSP1, FRECHET, NEWTON, NAT_1, XTUPLE_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, REAL_1, SQUARE_1, NEWTON, CONNSP_2, TBSP_1, RUSUB_4, CONVEX1, TMAP_1, METRIC_6, WAYBEL_3, YELLOW_8, FRECHET, FRECHET2, NFCONT_1, RLTOPSP1, RELSET_1, TOPS_2, BINOP_1, VFUNCT_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RLVECT_1, METRIC_1, PCOMPS_1, CONVEX1, RUSUB_4, SUBSET_1, STRUCT_0, ALGSTR_0;
expansions TARSKI, RLVECT_1, METRIC_1, PRE_TOPC;
definition
let X be
RealNormSpace;
existence
ex b1 being Function of [: the carrier of X, the carrier of X:],REAL st
for x, y being Point of X holds b1 . (x,y) = ||.(x - y).||
uniqueness
for b1, b2 being Function of [: the carrier of X, the carrier of X:],REAL st ( for x, y being Point of X holds b1 . (x,y) = ||.(x - y).|| ) & ( for x, y being Point of X holds b2 . (x,y) = ||.(x - y).|| ) holds
b1 = b2
end;
Lm1:
for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is Reflexive
Lm2:
for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is discerning
Lm3:
for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is symmetric
Lm4:
for X being RealNormSpace holds the distance of MetrStruct(# the carrier of X,(distance_by_norm_of X) #) is triangle
Lm5:
for X being RealNormSpace
for r being Real
for x being Point of X holds { y where y is Point of X : ||.(x - y).|| < r } = { y where y is Point of X : ||.(y - x).|| < r }