environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PARTFUN1, ZFMISC_1, XXREAL_0, CARD_1, FINSEQ_1, NAT_1, ARYTM_3, RELAT_1, FUNCT_1, RELAT_2, TARSKI, REWRITE1, FINSEQ_5, ARYTM_1, SUBSET_1, EQREL_1, SETFAM_1, PARTIT1, METRIC_1, SUPINF_2, FINSET_1, STRUCT_0, XXREAL_2, MEASURE5, TAXONOM1, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, PARTFUN1, STRUCT_0, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, PARTIT1, METRIC_1, TBSP_1, FINSET_1, EQREL_1, ALG_1, REWRITE1, FINSEQ_1, XXREAL_2, NAT_1, LANG1, FINSEQ_5;
definitions TARSKI, SETFAM_1;
theorems EQREL_1, ZFMISC_1, PARTIT1, TARSKI, RELAT_2, METRIC_1, RELAT_1, REWRITE1, FINSEQ_1, LANG1, FINSEQ_5, RELSET_1, NAT_1, FUNCT_1, FUNCT_2, FINSEQ_3, TBSP_1, MSUALG_9, XBOOLE_0, XBOOLE_1, PARTFUN1, ORDERS_1, XREAL_1, XXREAL_0, ORDINAL1, XXREAL_2;
schemes RELSET_1, LMOD_7, NAT_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, EQREL_1, STRUCT_0, TBSP_1, XXREAL_2, BINOP_2, VALUED_0, ORDINAL1;
constructors HIDDEN, NAT_1, PARTIT1, FINSEQ_5, REWRITE1, TBSP_1, LANG1, XXREAL_2, RELSET_1, BINOP_1, BINOP_2, VALUED_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities BINOP_1, EQREL_1, STRUCT_0;
expansions TARSKI, SETFAM_1;
definition
let X be non
empty set ;
let f be
PartFunc of
[:X,X:],
REAL;
let a be
Real;
existence
ex b1 being Relation of X st
for x, y being Element of X holds
( [x,y] in b1 iff f . (x,y) <= a )
uniqueness
for b1, b2 being Relation of X st ( for x, y being Element of X holds
( [x,y] in b1 iff f . (x,y) <= a ) ) & ( for x, y being Element of X holds
( [x,y] in b2 iff f . (x,y) <= a ) ) holds
b1 = b2
end;
Lm2:
for x being object
for X being non empty set
for a1, a2 being non negative Real st a1 <= a2 holds
for f being PartFunc of [:X,X:],REAL
for R1, R2 being Equivalence_Relation of X st R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] holds
Class (R1,x) c= Class (R2,x)
definition
let M be non
empty MetrStruct ;
let a be
Real;
existence
ex b1 being Relation of M st
for x, y being Element of M holds
( [x,y] in b1 iff x,y are_in_tolerance_wrt a )
uniqueness
for b1, b2 being Relation of M st ( for x, y being Element of M holds
( [x,y] in b1 iff x,y are_in_tolerance_wrt a ) ) & ( for x, y being Element of M holds
( [x,y] in b2 iff x,y are_in_tolerance_wrt a ) ) holds
b1 = b2
end;