:: Lower Tolerance. {P}reliminaries to {W}roclaw Taxonomy
:: by Mariusz Giero and Roman Matuszewski
::
:: Received December 5, 2000
:: Copyright (c) 2000-2026 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, 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 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;
constructors NAT_1, PARTIT1, FINSEQ_5, REWRITE1, TBSP_1, LANG1, XXREAL_2,
RELSET_1, BINOP_1, BINOP_2, VALUED_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, FINSEQ_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, SETFAM_1, RELAT_2;
equalities BINOP_1, EQREL_1, STRUCT_0, RELAT_1;
expansions 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;
begin :: Preliminaries
reserve A,X for non empty set;
reserve f for PartFunc of [:X,X:],REAL;
reserve a for Real;
registration
cluster non negative for Real;
existence
proof
take 0;
thus thesis;
end;
end;
theorem Th1:
for p being FinSequence, k being Nat
st k+1 in dom p & not k in dom p holds k = 0
proof
let p be FinSequence, k be Nat such that
A1: k+1 in dom p and
A2: not k in dom p;
assume k <> 0;
then
A3: k >= 1 by NAT_1:14;
k <= k+1 & k+1 <= len p by A1,FINSEQ_3:25,NAT_1:12;
then k <= len p by XXREAL_0:2;
hence thesis by A2,A3,FINSEQ_3:25;
end;
theorem Th2:
for p being FinSequence, i,j being Nat st i in dom p & j in dom p
& for k be Nat st k in dom p & k + 1 in dom p holds p.k = p.(k + 1)
holds p.i = p.j
proof
let p be FinSequence, i,j be Nat such that
A1: i in dom p & j in dom p and
A2: for k be Nat st k in dom p & k + 1 in dom p holds p.k = p.(k + 1);
defpred P[Nat] means for j being Nat st $1 in dom p & j in dom p holds p.$1
= p.j;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A4: P[k];
let j be Nat such that
A5: k+1 in dom p and
A6: j in dom p;
per cases;
suppose
A7: k in dom p;
hence p.(k+1) = p.k by A2,A5
.= p.j by A4,A6,A7;
end;
suppose
A8: not k in dom p;
defpred R[Nat] means $1 in dom p implies p.$1 = p.1;
A9: for w being Nat st R[w] holds R[w+1]
proof
let w be Nat such that
A10: R[w];
assume
A11: w+1 in dom p;
per cases;
suppose
w in dom p;
hence thesis by A2,A10,A11;
end;
suppose
not w in dom p;
then w = 0 by A11,Th1;
hence thesis;
end;
end;
A12: R[0] by FINSEQ_3:24;
A13: for k being Nat holds R[k] from NAT_1:sch 2(A12,A9);
k = 0 by A5,A8,Th1;
hence thesis by A6,A13;
end;
end;
A14: P[0] by FINSEQ_3:24;
for k being Nat holds P[k] from NAT_1:sch 2(A14,A3);
hence thesis by A1;
end;
theorem Th3:
for X being set, R being Relation of X st R is_reflexive_in X holds dom R = X
proof
let X be set, R be Relation of X such that
A1: R is_reflexive_in X;
for x be object st x in X ex y be object st [x,y] in R
proof
let x be object such that
A2: x in X;
take x;
thus thesis by A1,A2,RELAT_2:def 1;
end;
hence thesis by RELSET_1:9;
end;
theorem
for X being set, R being Relation of X st R is_reflexive_in X holds rng R = X
proof
let X be set, R be Relation of X such that
A1: R is_reflexive_in X;
for x be object st x in X ex y be object st [y,x] in R
proof
let x be object such that
A2: x in X;
take x;
thus thesis by A1,A2,RELAT_2:def 1;
end;
hence thesis by RELSET_1:10;
end;
theorem Th5:
for X being set, R being Relation of X st X c= field R
holds R[*] is_reflexive_in X
proof
let X be set, R be Relation of X such that
A1: X c= field R;
let x be object;
assume
A2: x in X;
set p = <*x*>;
A3: len p = 1 by FINSEQ_1:40;
then
A4: p.(len p) = x;
for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R
by FINSEQ_1:40;
hence [x,x] in R[*] by A1,A2,A3,A4,FINSEQ_1:def 17;
end;
theorem Th6:
for X being set,x,y be object
for R be Relation of X st X c= field R
holds R reduces x,y & x in X implies [x,y] in R[*]
proof
let X be set,x,y be object;
let R be Relation of X such that
A1: X c= field R;
assume that
A2: R reduces x,y and
A3: x in X;
per cases by A2,REWRITE1:20;
suppose
[x,y] in R[*];
hence thesis;
end;
suppose
A4: x = y;
R[*] is_reflexive_in X by A1,Th5;
hence thesis by A3,A4,RELAT_2:def 1;
end;
end;
theorem Th7:
for X being set, R being Relation of X st R is_symmetric_in X
holds R[*] is_symmetric_in X
proof
let X be set, R be Relation of X such that
A1: R is_symmetric_in X;
now
let x,y be object;
assume that
x in X and
y in X and
A2: [x,y] in R[*];
A3: x in field R & y in field R by A2,FINSEQ_1:def 17;
consider p being FinSequence such that
A4: len p >= 1 and
A5: p.1 = x and
A6: p.len p = y and
A7: for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R by A2,
FINSEQ_1:def 17;
consider r being FinSequence such that
A8: r = Rev p;
A9: now
let j be Nat such that
A10: j >= 1 and
A11: j < len r;
A12: len p - 0 > len p - j by A10,XREAL_1:10;
j <= len p by A8,A11,FINSEQ_5:def 3;
then j in Seg len p by A10,FINSEQ_1:1;
then j in dom p by FINSEQ_1:def 3;
then
A13: r.j = p.(len p - j + 1) by A8,FINSEQ_5:58;
A14: j < len p by A8,A11,FINSEQ_5:def 3;
then
A15: len p >= j + 1 by NAT_1:13;
j + 1 >= 1 by NAT_1:11;
then j + 1 in Seg len p by A15,FINSEQ_1:1;
then
A16: j + 1 in dom p by FINSEQ_1:def 3;
len p - j is Nat by A14,NAT_1:21;
then len p - j in NAT by ORDINAL1:def 12;
then consider j1 being Element of NAT such that
A17: j1 = len p - j;
j1 >= 1 by A15,A17,XREAL_1:19;
then
A18: [p.(len p - j),p.((len p - j) + 1)] in R by A7,A17,A12;
then p.(len p - j) in X & p.(len p - j + 1) in X by ZFMISC_1:87;
then [p.(len p - j + 1),p.(len p - (j+1) + 1)] in R by A1,A18,
RELAT_2:def 3;
hence [r.j,r.(j+1)] in R by A8,A16,A13,FINSEQ_5:58;
end;
A19: r.len r = r. len p by A8,FINSEQ_5:def 3
.= x by A5,A8,FINSEQ_5:62;
len r >= 1 & r.1 = y by A4,A6,A8,FINSEQ_5:62,def 3;
hence [y,x] in R[*] by A3,A19,A9,FINSEQ_1:def 17;
end;
hence thesis by RELAT_2:def 3;
end;
theorem Th8:
for X being set, R being Relation of X st X c= field R
holds R[*] is_transitive_in X
proof
let X be set, R be Relation of X such that
A1: X c= field R;
now
let x,y,z be object;
assume that
A2: x in X and
y in X and
z in X and
A3: [x,y] in R[*] & [y,z] in R[*];
R reduces x,y & R reduces y,z by A3,REWRITE1:20;
hence [x,z] in R[*] by A1,A2,Th6,REWRITE1:16;
end;
hence thesis by RELAT_2:def 8;
end;
theorem Th9:
for X being non empty set, R being Relation of X st
X c= field R & R is_symmetric_in X holds R[*] is Equivalence_Relation of X
proof
let X be non empty set, R be Relation of X such that
A1: X c= field R and
A2: R is_symmetric_in X;
R[*] is_reflexive_in X by A1,Th5;
then
A3: dom(R[*]) = X & field(R[*]) = X by ORDERS_1:13;
R[*] is_symmetric_in X & R[*] is_transitive_in X by A1,A2,Th7,Th8;
hence thesis by A3,PARTFUN1:def 2,RELAT_2:def 11,def 16;
end;
theorem Th10:
for R1,R2 being Relation of X holds R1 c= R2 implies R1[*] c= R2[*]
proof
let R1,R2 be Relation of X;
assume
A1: R1 c= R2;
A2: field R1 c= field R2 by A1,RELAT_1:16;
let p be object such that
A3: p in R1[*];
consider x,y being object such that
A4: p = [x,y] by A3,RELAT_1:def 1;
consider r being FinSequence such that
A5: len r >= 1 & r.1 = x & r.(len r) = y and
A6: for i being Nat st i >= 1 & i < len r holds [r.i, r.(i+1)] in R1
by A3,A4,FINSEQ_1:def 17;
A7: for i being Nat st i >= 1 & i < len r holds [r.i, r.(i+1)] in R2 by A1,A6;
x in field R1 & y in field R1 by A3,A4,FINSEQ_1:def 17;
hence p in R2[*] by A4,A5,A2,A7,FINSEQ_1:def 17;
end;
Lm1: now
let A;
let X,Y be a_partition of A;
assume that
A1: X in {{A}} and
A2: Y in {{A}};
X = {A} by A1,TARSKI:def 1;
hence X is_finer_than Y or Y is_finer_than X by A2,TARSKI:def 1;
end;
theorem Th11:
SmallestPartition A is_finer_than {A}
proof
let X be set;
assume
A1: X in SmallestPartition A;
take A;
thus thesis by A1,TARSKI:def 1;
end;
begin :: The notion of classification
definition
let A be non empty set;
mode Classification of A -> Subset of PARTITIONS(A) means
:Def1:
for X,Y being a_partition of A st X in it & Y in it holds
X is_finer_than Y or Y is_finer_than X;
existence
proof
{A} is a_partition of A by EQREL_1:39;
then {A} in PARTITIONS(A) by PARTIT1:def 3;
then reconsider S = {{A}} as Subset of PARTITIONS(A) by ZFMISC_1:31;
take S;
thus thesis by Lm1;
end;
end;
theorem
{{A}} is Classification of A
proof
{A} is a_partition of A by EQREL_1:39;
then {A} in PARTITIONS(A) by PARTIT1:def 3;
then reconsider S = {{A}} as Subset of PARTITIONS(A) by ZFMISC_1:31;
S is Classification of A
proof
let X be a_partition of A;
thus thesis by Lm1;
end;
hence thesis;
end;
theorem
{SmallestPartition A} is Classification of A
proof
SmallestPartition A in PARTITIONS(A) by PARTIT1:def 3;
then reconsider S = {SmallestPartition A} as Subset of PARTITIONS(A) by
ZFMISC_1:31;
S is Classification of A
proof
let X,Y be a_partition of A;
assume that
A1: X in S and
A2: Y in S;
X = SmallestPartition A by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
hence thesis;
end;
theorem Th14:
for S being Subset of PARTITIONS(A) st S = {{A},SmallestPartition A} holds
S is Classification of A
proof
let S be Subset of PARTITIONS(A);
assume
A1: S = {{A},SmallestPartition A};
let X,Y be a_partition of A such that
A2: X in S and
A3: Y in S;
per cases by A1,A2,TARSKI:def 2;
suppose
A4: X = {A};
per cases by A1,A3,TARSKI:def 2;
suppose
Y = {A};
hence thesis by A4;
end;
suppose
Y = SmallestPartition A;
hence thesis by A4,Th11;
end;
end;
suppose
A5: X = SmallestPartition A;
per cases by A1,A3,TARSKI:def 2;
suppose
Y = SmallestPartition A;
hence thesis by A5;
end;
suppose
Y = {A};
hence thesis by A5,Th11;
end;
end;
end;
definition
let A be non empty set;
mode Strong_Classification of A -> Subset of PARTITIONS(A) means
:Def2:
it is Classification of A & {A} in it & SmallestPartition A in it;
existence
proof
{A} is a_partition of A by EQREL_1:39;
then
A1: {A} in PARTITIONS(A) by PARTIT1:def 3;
SmallestPartition A in PARTITIONS(A) by PARTIT1:def 3;
then reconsider
S = {{A},SmallestPartition A} as Subset of PARTITIONS(A) by A1,ZFMISC_1:32;
take S;
thus thesis by Th14,TARSKI:def 2;
end;
end;
theorem
for S being Subset of PARTITIONS(A) st S = {{A},SmallestPartition A}
holds S is Strong_Classification of A
proof
let S be Subset of PARTITIONS(A) such that
A1: S = {{A},SmallestPartition A};
A2: SmallestPartition A in S by A1,TARSKI:def 2;
S is Classification of A & {A} in S by A1,Th14,TARSKI:def 2;
hence thesis by A2,Def2;
end;
begin :: The tolerance on a non empty set
definition
let X be non empty set, f be PartFunc of [:X,X:], REAL, a be Real;
func low_toler(f,a) -> Relation of X means
:Def3:
for x,y being Element of X holds [x,y] in it iff f.(x,y) <= a;
existence
proof
defpred X[Element of X,Element of X] means f.($1,$2) <= a;
consider R being Relation of X,X such that
A1: for x, y being Element of X holds [x,y] in R iff X[x,y] from
RELSET_1:sch 2;
take R;
thus thesis by A1;
end;
uniqueness
proof
let R1, R2 be Relation of X such that
A2: for x,y being Element of X holds [x,y] in R1 iff f.(x,y) <= a and
A3: for x,y being Element of X holds [x,y] in R2 iff f.(x,y) <= a;
A4: for c,d be object holds [c,d] in R2 implies [c,d] in R1
proof
let c,d be object;
assume
A5: [c,d] in R2;
then reconsider c1 = c, d1 = d as Element of X by ZFMISC_1:87;
f.(c1,d1) <= a by A3,A5;
hence thesis by A2;
end;
for c,d be object holds [c,d] in R1 implies [c,d] in R2
proof
let c,d be object;
assume
A6: [c,d] in R1;
then reconsider c1 = c, d1 = d as Element of X by ZFMISC_1:87;
f.(c1,d1) <= a by A2,A6;
hence thesis by A3;
end;
hence thesis by A4,RELAT_1:def 2;
end;
end;
theorem Th16:
f is Reflexive & a >= 0 implies low_toler(f,a) is_reflexive_in X
proof
assume
A1: f is Reflexive & a >= 0;
now
let x be object;
assume x in X;
then reconsider x1 = x as Element of X;
f.(x1,x1) <= a by A1,METRIC_1:def 2;
hence [x,x] in low_toler(f,a) by Def3;
end;
hence thesis by RELAT_2:def 1;
end;
theorem Th17:
f is symmetric implies low_toler(f,a) is_symmetric_in X
proof
assume
A1: f is symmetric;
now
let x,y be object such that
A2: x in X & y in X and
A3: [x,y] in low_toler(f,a);
reconsider x1 = x, y1 = y as Element of X by A2;
f.(x1,y1) <= a by A3,Def3;
then f.(y1,x1) <= a by A1,METRIC_1:def 4;
hence [y,x] in low_toler(f,a) by Def3;
end;
hence thesis by RELAT_2:def 3;
end;
theorem Th18:
a >= 0 & f is Reflexive symmetric implies low_toler(f,a) is Tolerance of X
proof
set T = low_toler(f,a);
assume that
A1: a >= 0 and
A2: f is Reflexive symmetric;
A3: low_toler(f,a) is_reflexive_in X by A1,A2,Th16;
A4: dom T = X by A1,A2,Th3,Th16;
then
A5: field T = X \/ (rng low_toler(f,a))
.= X by XBOOLE_1:12;
then T is_symmetric_in field T by A2,Th17;
hence thesis by A3,A4,A5,PARTFUN1:def 2,RELAT_2:def 9,def 11;
end;
theorem Th19:
for X being non empty set, f being PartFunc of [:X,X:], REAL,
a1,a2 being Real st a1 <= a2 holds low_toler(f,a1) c= low_toler(f,a2)
proof
let X be non empty set, f be PartFunc of [:X,X:], REAL, a1,a2 be Real
such that
A1: a1 <= a2;
let p be object such that
A2: p in low_toler(f,a1);
consider x,y being object such that
A3: x in X & y in X and
A4: p = [x,y] by A2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of X by A3;
f.(x1,y1) <= a1 by A2,A4,Def3;
then f.(x1,y1) <= a2 by A1,XXREAL_0:2;
hence p in low_toler(f,a2) by A4,Def3;
end;
definition
let X be set;
let f be PartFunc of [:X,X:], REAL;
attr f is nonnegative means
for x,y being Element of X holds f.(x,y) >= 0;
end;
theorem Th20:
for X being non empty set, f being PartFunc of [:X,X:],REAL,
x,y being object
st f is nonnegative Reflexive discerning holds [x,y] in low_toler(f,0)
implies x = y
proof
let X be non empty set, f be PartFunc of [:X,X:],REAL,
x,y be object such that
A1: f is nonnegative Reflexive discerning;
assume
A2: [x,y] in low_toler(f,0);
then reconsider x1 = x, y1 = y as Element of X by ZFMISC_1:87;
f.(x1,y1) <= 0 by A2,Def3;
then f.(x1,y1) = 0 by A1;
hence thesis by A1,METRIC_1:def 3;
end;
theorem Th21:
for X being non empty set, f being PartFunc of [:X,X:],REAL,
x being Element of X st f is Reflexive discerning holds
[x,x] in low_toler(f,0)
proof
let X be non empty set, f be PartFunc of [:X,X:],REAL, x be Element of X;
assume f is Reflexive discerning;
then f.(x,x) = 0 by METRIC_1:def 2;
hence thesis by Def3;
end;
theorem Th22:
for X being non empty set, f being PartFunc of [:X,X:],REAL,
a being Real st low_toler(f,a) is_reflexive_in X & f is symmetric holds
low_toler(f,a)[*] is Equivalence_Relation of X
proof
let X be non empty set, f be PartFunc of [:X,X:],REAL, a be Real such
that
A1: low_toler(f,a) is_reflexive_in X and
A2: f is symmetric;
dom low_toler(f,a) = X by A1,Th3;
then
AA: X c= field low_toler(f,a) by XBOOLE_1:7;
now
let x,y be object such that
A3: x in X & y in X and
A4: [x,y] in low_toler(f,a);
reconsider x1 = x, y1 = y as Element of X by A3;
f.(x1,y1) <= a by A4,Def3;
then f.(y1,x1) <= a by A2,METRIC_1:def 4;
hence [y,x] in low_toler(f,a) by Def3;
end;
then low_toler(f,a) is_symmetric_in X by RELAT_2:def 3;
hence thesis by AA,Th9;
end;
Lm2: for x be object, X being non empty set, a1,a2 being non negative Real
st a1 <= a2 for f being PartFunc of [:X,X:],REAL, 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)
proof
let x be object, X be non empty set, a1,a2 be non negative Real such
that
A1: a1 <= a2;
let f be PartFunc of [:X,X:],REAL, R1,R2 being Equivalence_Relation of X
such that
A2: R1 = low_toler(f,a1)[*] & R2 = low_toler(f,a2)[*];
let z1 be object;
assume z1 in Class(R1,x);
then
A3: [z1,x] in R1 by EQREL_1:19;
R1 c= R2 by A1,A2,Th10,Th19;
hence z1 in Class(R2,x) by A3,EQREL_1:19;
end;
begin :: The partitions defined by lower tolerance
theorem Th23:
for X being non empty set, f being PartFunc of [:X,X:],REAL st
f is nonnegative Reflexive discerning holds
low_toler(f,0)[*] = low_toler(f,0)
proof
let X be non empty set, f be PartFunc of [:X,X:],REAL such that
A1: f is nonnegative Reflexive discerning;
now
let p be object such that
A2: p in low_toler(f,0)[*];
consider x,y being object such that
A3: p = [x,y] by A2,RELAT_1:def 1;
low_toler(f,0) reduces x,y by A2,A3,REWRITE1:20;
then consider r being RedSequence of low_toler(f,0) such that
A4: r.1 = x & r.len r = y by REWRITE1:def 3;
A5: now
let i be Nat;
assume i in dom r & i+1 in dom r;
then [r.i,r.(i+1)] in low_toler(f,0) by REWRITE1:def 2;
hence r.i = r.(i+1) by A1,Th20;
end;
A6: x is Element of X by A2,A3,ZFMISC_1:87;
0 < len r by REWRITE1:def 2;
then 0+1 <= len r by NAT_1:13;
then 1 in dom r & len r in dom r by FINSEQ_3:25;
then r.1 = r. len r by A5,Th2;
hence p in low_toler(f,0) by A1,A3,A4,A6,Th21;
end;
then
low_toler(f,0) c= low_toler(f,0)[*] & low_toler(f,0)[*] c= low_toler(f,
0) by LANG1:18;
hence thesis by XBOOLE_0:def 10;
end;
theorem Th24:
for X being non empty set, f being PartFunc of [:X,X:],REAL,
R being Equivalence_Relation of X st R = low_toler(f,0)[*] &
f is nonnegative Reflexive discerning holds R = id X
proof
let X be non empty set, f be PartFunc of [:X,X:],REAL, R be
Equivalence_Relation of X such that
A1: R = low_toler(f,0)[*] and
A2: f is nonnegative Reflexive discerning;
A3: for x,y being object st x in X & x = y holds [x,y] in low_toler(f,0)[*]
proof
let x,y be object;
assume x in X & x = y;
then [x,y] in low_toler(f,0) by A2,Th21;
hence thesis by A2,Th23;
end;
for x,y being object st [x,y] in low_toler(f,0)[*] holds x in X & x = y
proof
let x,y be object;
assume [x,y] in low_toler(f,0)[*];
then [x,y] in low_toler(f,0) by A2,Th23;
hence thesis by A2,Th20,ZFMISC_1:87;
end;
hence thesis by A1,A3,RELAT_1:def 10;
end;
theorem
for X being non empty set, f being PartFunc of [:X,X:],REAL,
R being Equivalence_Relation of X st R = low_toler(f,0)[*] &
f is nonnegative Reflexive discerning holds Class R = SmallestPartition X
by Th24;
theorem Th26:
for X being finite non empty Subset of REAL, f being Function of
[:X,X:],REAL, z being finite non empty Subset of REAL, A being Real st z
= rng f & A >= max z holds for x,y being Element of X holds f.(x,y) <= A
proof
let X be finite non empty Subset of REAL, f be Function of [:X,X:],REAL, z
be finite non empty Subset of REAL, A be Real such that
A1: z = rng f and
A2: A >= max z;
now
let x,y be Element of X;
reconsider c = f.[x,y] as Real;
dom f = [:X,X:] by FUNCT_2:def 1;
then [x,y] in dom f by ZFMISC_1:def 2;
then c in z by A1,FUNCT_1:def 3;
then f.(x,y) <= max z by XXREAL_2:def 8;
hence f.(x,y) <= A by A2,XXREAL_0:2;
end;
hence thesis;
end;
theorem Th27:
for X being finite non empty Subset of REAL, f being Function of
[:X,X:],REAL, z being finite non empty Subset of REAL, A being Real st z
= rng f & A >= max z holds for R being Equivalence_Relation of X st R =
low_toler(f,A)[*] holds Class R = {X}
proof
let X be finite non empty Subset of REAL, f be Function of [:X,X:],REAL, z
be finite non empty Subset of REAL, A be Real such that
A1: z = rng f & A >= max z;
now
let R be Equivalence_Relation of X such that
A2: R = low_toler(f,A)[*];
A3: for x being set st x in X holds X = Class(R,x)
proof
let x be set;
assume x in X;
then reconsider x9 = x as Element of X;
now
let x1 be object;
assume x1 in X;
then reconsider x19 = x1 as Element of X;
f.(x19,x9) <= A by A1,Th26;
then
A4: [x1,x] in low_toler(f,A) by Def3;
low_toler(f,A) c= low_toler(f,A)[*] by LANG1:18;
hence x1 in Class(R,x) by A2,A4,EQREL_1:19;
end;
then X c= Class(R,x);
hence thesis by XBOOLE_0:def 10;
end;
now
let a be object;
assume a in {X};
then
A5: a = X by TARSKI:def 1;
consider x be object such that
A6: x in X by XBOOLE_0:def 1;
X = Class(R,x) by A3,A6;
hence a in Class R by A5,A6,EQREL_1:def 3;
end;
then
A7: {X} c= Class R;
now
let a be object;
assume a in Class R;
then ex x being object st x in X & a = Class(R,x) by EQREL_1:def 3;
then a = X by A3;
hence a in {X} by TARSKI:def 1;
end;
then Class R c= {X};
hence Class R = {X} by A7,XBOOLE_0:def 10;
end;
hence thesis;
end;
theorem
for X being finite non empty Subset of REAL, f being Function of [:X,X
:],REAL, z being finite non empty Subset of REAL, A being Real st z =
rng f & A >= max z holds low_toler(f,A)[*] = low_toler(f,A)
proof
let X be finite non empty Subset of REAL, f be Function of [:X,X:],REAL, z
be finite non empty Subset of REAL, A be Real such that
A1: z = rng f & A >= max z;
now
let p be object;
assume p in low_toler(f,A)[*];
then consider x,y being object such that
A2: x in X & y in X and
A3: p = [x,y] by ZFMISC_1:def 2;
reconsider x9 = x, y9 = y as Element of X by A2;
f.(x9,y9) <= A by A1,Th26;
hence p in low_toler(f,A) by A3,Def3;
end;
then
low_toler(f,A) c= low_toler(f,A)[*] & low_toler(f,A)[*] c= low_toler(f,A
) by LANG1:18;
hence thesis by XBOOLE_0:def 10;
end;
begin :: The classification on a non empty set
definition
let X be non empty set, f being PartFunc of [:X,X:],REAL;
func fam_class(f) -> Subset of PARTITIONS(X) means
:Def5:
for x being object holds x in it iff
ex a being non negative Real,R being Equivalence_Relation of X st
R = low_toler(f,a)[*] & Class(R) = x;
existence
proof
defpred X[object] means ex a being non negative Real, R being
Equivalence_Relation of X st R = low_toler(f,a)[*] & Class(R) = $1;
consider A be set such that
A1: for x being object holds x in A iff x in PARTITIONS(X) & X[x] from
XBOOLE_0:sch 1;
A c= PARTITIONS(X)
by A1;
then reconsider A1 = A as Subset of PARTITIONS(X);
take A1;
let x be object;
thus x in A1 implies ex a being non negative Real,R be
Equivalence_Relation of X st R = low_toler(f,a)[*] & Class(R) = x by A1;
given a being non negative Real, R be Equivalence_Relation of X
such that
A2: R = low_toler(f,a)[*] & Class(R) = x;
Class(R) in PARTITIONS(X) by PARTIT1:def 3;
hence thesis by A1,A2;
end;
uniqueness
proof
defpred X[object] means ex a being non negative Real,R be
Equivalence_Relation of X st R = low_toler(f,a)[*] & Class(R) = $1;
A3: for X1,X2 being Subset of PARTITIONS X st
(for x being object holds x in
X1 iff X[x]) &
(for x being object holds x in X2 iff X[x]) holds X1 = X2
from
LMOD_7:sch 1;
let X1,X2 be Subset of PARTITIONS X;
assume (for x being object holds x in X1 iff ex a being non negative Real
,R be Equivalence_Relation of X st R = low_toler(f,a)[*] & Class(R) = x)
& (for x being object holds x in X2 iff ex a being non negative Real,R be
Equivalence_Relation of X st R = low_toler(f,a)[*] & Class(R) = x);
hence thesis by A3;
end;
end;
theorem
for X being non empty set, f being PartFunc of [:X,X:],REAL, a being
non negative Real st low_toler(f,a) is_reflexive_in X & f is symmetric
holds fam_class(f) is non empty
proof
let X be non empty set, f be PartFunc of [:X,X:],REAL, a be non negative
Real;
assume low_toler(f,a) is_reflexive_in X & f is symmetric;
then reconsider R = low_toler(f,a)[*] as Equivalence_Relation of X by Th22;
reconsider x = Class(R) as set;
x in fam_class(f) by Def5;
hence thesis;
end;
theorem Th30:
for X being finite non empty Subset of REAL, f being Function of
[:X,X:],REAL st f is symmetric nonnegative holds {X} in fam_class(f)
proof
let X be finite non empty Subset of REAL, f be Function of [:X,X:],REAL such
that
A1: f is symmetric nonnegative;
dom f = [:X,X:] by FUNCT_2:def 1;
then reconsider rn = rng f as finite non empty Subset of REAL by RELAT_1:42;
reconsider A1 = max rn as Real;
now
set x = the Element of X;
assume
A2: A1 is negative;
f.(x,x) <= A1 by Th26;
hence contradiction by A1,A2;
end;
then reconsider A19 = A1 as non negative Real;
now
let x be object;
assume x in X;
then reconsider x1 = x as Element of X;
f.(x1,x1) <= A1 by Th26;
hence [x,x] in low_toler(f,A1) by Def3;
end;
then low_toler(f,A19) is_reflexive_in X by RELAT_2:def 1;
then reconsider R = low_toler(f,A19)[*] as Equivalence_Relation of X by A1
,Th22;
Class R in fam_class(f) by Def5;
hence thesis by Th27;
end;
theorem Th31:
for X being non empty set, f being PartFunc of [:X,X:],REAL
holds fam_class(f) is Classification of X
proof
let X be non empty set,f be PartFunc of [:X,X:],REAL;
for A,B being a_partition of X st A in fam_class(f) & B in fam_class(f)
holds A is_finer_than B or B is_finer_than A
proof
let A,B be a_partition of X;
assume that
A1: A in fam_class(f) and
A2: B in fam_class(f);
consider a1 being non negative Real, R1 being
Equivalence_Relation of X such that
A3: R1 = low_toler(f,a1)[*] and
A4: Class R1 = A by A1,Def5;
consider a2 being non negative Real, R2 being
Equivalence_Relation of X such that
A5: R2 = low_toler(f,a2)[*] and
A6: Class R2 = B by A2,Def5;
now
per cases;
suppose
A7: a1 <= a2;
now
let x be set;
assume x in A;
then consider c being object such that
A8: c in X and
A9: x = Class(R1,c) by A4,EQREL_1:def 3;
consider y being set such that
A10: y = Class(R2,c);
take y;
thus y in B by A6,A8,A10,EQREL_1:def 3;
thus x c= y by A3,A5,A7,A9,A10,Lm2;
end;
hence thesis;
end;
suppose
A11: a1 > a2;
now
let y be set;
assume y in B;
then consider c being object such that
A12: c in X and
A13: y = Class(R2,c) by A6,EQREL_1:def 3;
consider x being set such that
A14: x = Class(R1,c);
take x;
thus x in A by A4,A12,A14,EQREL_1:def 3;
thus y c= x by A3,A5,A11,A13,A14,Lm2;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by Def1;
end;
theorem
for X being finite non empty Subset of REAL, f being Function of [:X,X
:],REAL st (SmallestPartition X) in fam_class(f) & f is symmetric nonnegative
holds fam_class(f) is Strong_Classification of X
proof
let X be finite non empty Subset of REAL, f be Function of [:X,X:],REAL such
that
A1: (SmallestPartition X) in fam_class(f) and
A2: f is symmetric nonnegative;
A3: fam_class(f) is Classification of X by Th31;
{X} in fam_class(f) by A2,Th30;
hence thesis by A1,A3,Def2;
end;
begin :: The classification on a metric space
definition
let M be MetrStruct, a be Real, x,y be Element of M;
pred x,y are_in_tolerance_wrt a means
dist(x,y) <= a;
end;
definition
let M be non empty MetrStruct, a be Real;
func dist_toler(M,a) -> Relation of M means
:Def7:
for x,y being Element of M holds [x,y] in it iff x,y are_in_tolerance_wrt a;
existence
proof
defpred X[Element of M,Element of M] means $1,$2 are_in_tolerance_wrt a;
consider R being Relation of the carrier of M, the carrier of M such that
A1: for x, y being Element of M holds [x,y] in R iff X[x,y] from
RELSET_1:sch 2;
reconsider R as Relation of M;
take R;
thus thesis by A1;
end;
uniqueness
proof
let A, B be Relation of M such that
A2: for x,y being Element of M holds [x,y] in A iff x,y
are_in_tolerance_wrt a and
A3: for x,y being Element of M holds [x,y] in B iff x,y are_in_tolerance_wrt a;
A4: for c,d be object holds [c,d] in B implies [c,d] in A
proof
let c,d be object;
assume
A5: [c,d] in B;
then reconsider c1 = c, d1 = d as Element of M by ZFMISC_1:87;
c1,d1 are_in_tolerance_wrt a by A3,A5;
hence thesis by A2;
end;
for c,d be object holds [c,d] in A implies [c,d] in B
proof
let c,d be object;
assume
A6: [c,d] in A;
then reconsider c1 = c, d1 = d as Element of M by ZFMISC_1:87;
c1,d1 are_in_tolerance_wrt a by A2,A6;
hence thesis by A3;
end;
hence thesis by A4,RELAT_1:def 2;
end;
end;
theorem Th33:
for M being non empty MetrStruct, a being Real holds
dist_toler(M,a) = low_toler(the distance of M,a)
proof
let M be non empty MetrStruct, a be Real;
now
let z be object such that
A1: z in low_toler(the distance of M,a);
consider x,y being object such that
A2: x in the carrier of M & y in the carrier of M and
A3: z = [x,y] by A1,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of M by A2;
dist(x1,y1) = (the distance of M).(x1,y1) by METRIC_1:def 1;
then dist(x1,y1) <= a by A1,A3,Def3;
then x1,y1 are_in_tolerance_wrt a;
hence z in dist_toler(M,a) by A3,Def7;
end;
then
A4: low_toler(the distance of M,a) c= dist_toler(M,a);
now
let z be object such that
A5: z in dist_toler(M,a);
consider x,y being object such that
A6: x in the carrier of M & y in the carrier of M and
A7: z = [x,y] by A5,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Element of M by A6;
(the distance of M).(x1,y1) = dist(x1,y1) & x1,y1 are_in_tolerance_wrt
a by A5,A7,Def7,METRIC_1:def 1;
then (the distance of M).(x1,y1) <= a;
hence z in low_toler(the distance of M,a) by A7,Def3;
end;
then dist_toler(M,a) c= low_toler(the distance of M,a);
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem
for M being non empty Reflexive symmetric MetrStruct, a being Real,
T being Relation of the carrier of M,the carrier of M st
T = dist_toler(M,a) & a >= 0 holds T is Tolerance of the carrier of M
proof
let M be non empty Reflexive symmetric MetrStruct, a be Real, T be
Relation of the carrier of M,the carrier of M such that
A1: T = dist_toler(M,a) and
A2: a >= 0;
A3: the distance of M is symmetric & the distance of M is Reflexive by
METRIC_1:def 6,def 8;
T = low_toler(the distance of M,a) by A1,Th33;
hence thesis by A2,A3,Th18;
end;
definition
let M be Reflexive symmetric non empty MetrStruct;
func fam_class_metr(M) -> Subset of PARTITIONS(the carrier of M) means
:Def8:
for x being object holds x in it iff
ex a being non negative Real,R be Equivalence_Relation of M st
R = dist_toler(M,a)[*] & Class(R) = x;
existence
proof
defpred X[object] means ex a being non negative Real, R being
Equivalence_Relation of M st R = dist_toler(M,a)[*] & Class(R) = $1;
consider X be set such that
A1: for x being object holds x in X iff x in PARTITIONS the carrier of M
& X[x] from XBOOLE_0:sch 1;
X c= PARTITIONS the carrier of M
by A1;
then reconsider X1 = X as Subset of PARTITIONS the carrier of M;
take X1;
let x be object;
thus x in X1 implies ex a being non negative Real,R be
Equivalence_Relation of M st R = dist_toler(M,a)[*] & Class(R) = x by A1;
given a being non negative Real, R be Equivalence_Relation of M
such that
A2: R = dist_toler(M,a)[*] & Class(R) = x;
Class(R) in PARTITIONS(the carrier of M) by PARTIT1:def 3;
hence thesis by A1,A2;
end;
uniqueness
proof
defpred X[object] means ex a being non negative Real,R be
Equivalence_Relation of M st R = dist_toler(M,a)[*] & Class(R) = $1;
A3: for X1,X2 being Subset of PARTITIONS the carrier of M st
(for x being object holds x in X1 iff X[x]) &
(for x being object holds x in X2 iff X[x]) holds X1
= X2 from LMOD_7:sch 1;
let X1,X2 be Subset of PARTITIONS the carrier of M;
assume (for x being object holds x in X1 iff
ex a being non negative Real
,R be Equivalence_Relation of M st R = dist_toler(M,a)[*] & Class(R) = x
) & (for x being object holds x in X2 iff
ex a being non negative Real,R
be Equivalence_Relation of M st R = dist_toler(M,a)[*] & Class(R) = x);
hence thesis by A3;
end;
end;
theorem Th35:
for M being Reflexive symmetric non empty MetrStruct holds
fam_class_metr(M) = fam_class(the distance of M)
proof
let M be Reflexive symmetric non empty MetrStruct;
now
let z be object;
assume z in fam_class(the distance of M);
then consider
a being non negative Real, R be Equivalence_Relation of
the carrier of M such that
A1: R = low_toler(the distance of M,a)[*] and
A2: Class(R) = z by Def5;
reconsider R1 = R as Equivalence_Relation of M;
R1 = dist_toler(M,a)[*] by A1,Th33;
hence z in fam_class_metr(M) by A2,Def8;
end;
then
A3: fam_class(the distance of M) c= fam_class_metr(M);
now
let z be object;
assume z in fam_class_metr(M);
then consider
a being non negative Real, R be Equivalence_Relation of
M such that
A4: R = dist_toler(M,a)[*] and
A5: Class(R) = z by Def8;
R = low_toler(the distance of M,a)[*] by A4,Th33;
hence z in fam_class(the distance of M) by A5,Def5;
end;
then fam_class_metr(M) c= fam_class(the distance of M);
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th36:
for M being non empty MetrSpace for R being Equivalence_Relation of M st
R = dist_toler(M,0)[*] holds Class R = SmallestPartition the carrier of M
proof
let M be non empty MetrSpace;
now
let x,y be Element of M;
dist(x,y) >= 0 by METRIC_1:5;
hence (the distance of M).(x,y) >= 0 by METRIC_1:def 1;
end;
then
A1: the distance of M is nonnegative;
let R be Equivalence_Relation of M;
assume R = dist_toler(M,0)[*];
then
the distance of M is Reflexive discerning & low_toler(the distance of M,
0) [*] = R by Th33,METRIC_1:def 6,def 7;
hence thesis by A1,Th24;
end;
theorem Th37:
for M being Reflexive symmetric bounded non empty MetrStruct
st a >= diameter [#]M holds dist_toler(M,a) = nabla the carrier of M
proof
let M be Reflexive symmetric bounded non empty MetrStruct such that
A1: a >= diameter [#]M;
now
let z be object;
assume z in nabla the carrier of M;
then consider x,y being object such that
A2: x in the carrier of M & y in the carrier of M and
A3: z = [x,y] by ZFMISC_1:def 2;
reconsider x1=x, y1=y as Element of M by A2;
dist(x1,y1) <= diameter [#]M by TBSP_1:def 8;
then dist(x1,y1) <= a by A1,XXREAL_0:2;
then x1, y1 are_in_tolerance_wrt a;
hence z in dist_toler(M,a) by A3,Def7;
end;
then nabla the carrier of M c= dist_toler(M,a);
hence thesis by XBOOLE_0:def 10;
end;
theorem Th38:
for M being Reflexive symmetric bounded non empty MetrStruct
st a >= diameter [#]M holds dist_toler(M,a) = dist_toler(M,a)[*]
proof
let M be Reflexive symmetric bounded non empty MetrStruct such that
A1: a >= diameter [#]M;
dist_toler(M,a)[*] c= nabla the carrier of M;
then
dist_toler(M,a) c= dist_toler(M,a)[*] & dist_toler(M,a)[*] c= dist_toler
(M,a ) by A1,Th37,LANG1:18;
hence thesis by XBOOLE_0:def 10;
end;
theorem Th39:
for M being Reflexive symmetric bounded non empty MetrStruct
st a >= diameter [#]M holds dist_toler(M,a)[*] = nabla the carrier of M
proof
let M be Reflexive symmetric bounded non empty MetrStruct such that
A1: a >= diameter [#]M;
dist_toler(M,a) = dist_toler(M,a)[*] by A1,Th38;
hence thesis by A1,Th37;
end;
theorem Th40:
for M being Reflexive symmetric bounded non empty MetrStruct,
R being Equivalence_Relation of M, a being non negative Real st
a >= diameter [#]M & R = dist_toler(M,a)[*] holds
Class R = {the carrier of M}
proof
let M be Reflexive symmetric bounded non empty MetrStruct, R be
Equivalence_Relation of M, a be non negative Real;
Class(nabla the carrier of M) = {the carrier of M} by MSUALG_9:4;
hence thesis by Th39;
end;
registration
let M be Reflexive symmetric triangle non empty MetrStruct, C be non empty
bounded Subset of M;
cluster diameter C -> non negative;
coherence by TBSP_1:21;
end;
theorem Th41:
for M being bounded non empty MetrSpace holds
{the carrier of M} in fam_class_metr(M)
proof
let M be bounded non empty MetrSpace;
set a = diameter [#]M;
the distance of M is symmetric by METRIC_1:def 8;
then low_toler(the distance of M,a) is_symmetric_in the carrier of M by Th17;
then
A1: dist_toler(M,a) is_symmetric_in the carrier of M by Th33;
the distance of M is Reflexive by METRIC_1:def 6;
then low_toler(the distance of M,a) is_reflexive_in the carrier of M by Th16;
then dist_toler(M,a) is_reflexive_in the carrier of M by Th33;
then dom dist_toler(M,a) = the carrier of M by Th3;
then the carrier of M c= field dist_toler(M,a) by XBOOLE_1:7;
then reconsider R = dist_toler(M,a)[*] as Equivalence_Relation of M
by A1,Th9;
Class R = {the carrier of M} by Th40;
hence thesis by Def8;
end;
theorem Th42:
for M being Reflexive symmetric non empty MetrStruct holds
fam_class_metr(M) is Classification of the carrier of M
proof
let M be Reflexive symmetric non empty MetrStruct;
fam_class_metr(M) = fam_class(the distance of M) by Th35;
hence thesis by Th31;
end;
theorem
for M being bounded non empty MetrSpace holds
fam_class_metr(M) is Strong_Classification of the carrier of M
proof
reconsider a = 0 as non negative Real;
let M be bounded non empty MetrSpace;
the distance of M is symmetric by METRIC_1:def 8;
then low_toler(the distance of M,a) is_symmetric_in the carrier of M by Th17;
then
A1: dist_toler(M,a) is_symmetric_in the carrier of M by Th33;
the distance of M is Reflexive by METRIC_1:def 6;
then low_toler(the distance of M,a) is_reflexive_in the carrier of M by Th16;
then dist_toler(M,a) is_reflexive_in the carrier of M by Th33;
then dom dist_toler(M,a) = the carrier of M by Th3;
then the carrier of M c= field dist_toler(M,a) by XBOOLE_1:7;
then reconsider R = dist_toler(M,a)[*] as Equivalence_Relation of M
by A1,Th9;
Class R in fam_class_metr(M) by Def8;
then
A2: SmallestPartition (the carrier of M) in fam_class_metr(M) by Th36;
fam_class_metr(M) is Classification of the carrier of M & {the carrier
of M} in fam_class_metr(M) by Th41,Th42;
hence thesis by A2,Def2;
end;