environ
vocabularies HIDDEN, XBOOLE_0, METRIC_1, PCOMPS_1, PRE_TOPC, XXREAL_0, CARD_1, FUNCT_1, SUBSET_1, RELAT_1, STRUCT_0, WEIERSTR, NUMBERS, SEQ_4, ARYTM_3, RCOMP_1, TOPMETR, ORDINAL2, XXREAL_2, ARYTM_1, REAL_1, TARSKI, TBSP_1, EUCLID, HAUSDORF;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, BINOP_1, XXREAL_2, STRUCT_0, PRE_TOPC, COMPTS_1, TBSP_1, TOPMETR, METRIC_1, SEQ_4, PCOMPS_1, EUCLID, WEIERSTR;
definitions XBOOLE_0, TARSKI, XXREAL_2;
theorems METRIC_1, TOPMETR, GOBOARD6, PRE_TOPC, FUNCT_2, XBOOLE_0, FUNCT_1, TARSKI, WEIERSTR, SEQ_4, TBSP_1, JORDAN1K, COMPTS_1, PCOMPS_1, XREAL_1, XXREAL_0, EUCLID;
schemes ;
registrations SUBSET_1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, PCOMPS_1, EUCLID, TOPMETR, BORSUK_2, WAYBEL_2, TBSP_1, VALUED_0;
constructors HIDDEN, REAL_1, SQUARE_1, SEQ_4, CONNSP_1, COMPTS_1, TBSP_1, WEIERSTR, FUNCSDOM, BINOP_2, PSCOMP_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0, STRUCT_0;
expansions XXREAL_2;
Lm1:
for M being non empty MetrSpace
for P being non empty Subset of (TopSpaceMetr M)
for x being Point of M
for X being Subset of REAL st X = (dist x) .: P & P is compact holds
X is bounded_above
definition
let M be non
empty MetrSpace;
let P,
Q be
Subset of
(TopSpaceMetr M);
coherence
max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) is Real
;
commutativity
for b1 being Real
for P, Q being Subset of (TopSpaceMetr M) st b1 = max ((max_dist_min (P,Q)),(max_dist_min (Q,P))) holds
b1 = max ((max_dist_min (Q,P)),(max_dist_min (P,Q)))
;
end;
definition
let n be
Element of
NAT ;
let P,
Q be
Subset of
(TOP-REAL n);
existence
ex b1 being Real ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b1 = HausDist (P9,Q9) )
uniqueness
for b1, b2 being Real st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b1 = HausDist (P9,Q9) ) & ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b2 = HausDist (P9,Q9) ) holds
b1 = b2
;
commutativity
for b1 being Real
for P, Q being Subset of (TOP-REAL n) st ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( P = P9 & Q = Q9 & b1 = HausDist (P9,Q9) ) holds
ex P9, Q9 being Subset of (TopSpaceMetr (Euclid n)) st
( Q = P9 & P = Q9 & b1 = HausDist (P9,Q9) )
;
end;