:: Lower Tolerance. {P}reliminaries to {W}roclaw Taxonomy
:: by Mariusz Giero and Roman Matuszewski
::
:: Received December 5, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

registration
clusterV11() ext-real non negative real for set ;
existence
 not for b1 being real number holds b1 is negative
proofend;
end;

theorem Th1: :: TAXONOM1:1
for p being FinSequence
for k being Nat st k + 1 in dom p & not k in dom p holds
k = 0
proofend;

theorem Th2: :: TAXONOM1:2
for p being FinSequence
for i, j being Nat st i in dom p & j in dom p & ( for k being Nat st k in dom p & k + 1 in dom p holds
p . k = p . (k + 1) ) holds
p . i = p . j
proofend;

theorem Th3: :: TAXONOM1:3
for X being set
for R being Relation of X st R is_reflexive_in X holds
dom R = X
proofend;

theorem :: TAXONOM1:4
for X being set
for R being Relation of X st R is_reflexive_in X holds
rng R = X
proofend;

theorem Th5: :: TAXONOM1:5
for X being set
for R being Relation of X st R is_reflexive_in X holds
R [*] is_reflexive_in X
proofend;

theorem Th6: :: TAXONOM1:6
for X, x, y being set
for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds
[x,y] in R [*]
proofend;

theorem Th7: :: TAXONOM1:7
for X being set
for R being Relation of X st R is_symmetric_in X holds
R [*] is_symmetric_in X
proofend;

theorem Th8: :: TAXONOM1:8
for X being set
for R being Relation of X st R is_reflexive_in X holds
R [*] is_transitive_in X
proofend;

theorem Th9: :: TAXONOM1:9
for X being non empty set
for R being Relation of X st R is_reflexive_in X & R is_symmetric_in X holds
R [*] is Equivalence_Relation of X
proofend;

theorem Th10: :: TAXONOM1:10
for X being non empty set
for R1, R2 being Relation of X st R1 c= R2 holds
R1 [*] c= R2 [*]
proofend;

Lm1: now__::_thesis:_for_A_being_non_empty_set_
for_X,_Y_being_a_partition_of_A_st_X_in_{{A}}_&_Y_in_{{A}}_&_not_X_is_finer_than_Y_holds_
Y_is_finer_than_X
let A be non empty set ; ::_thesis: for X, Y being a_partition of A st X in {{A}} & Y in {{A}} & not X is_finer_than Y holds
Y is_finer_than X
let X, Y be a_partition of A; ::_thesis: ( X in {{A}} & Y in {{A}} & not X is_finer_than Y implies Y is_finer_than X )
assume that
A1: X in {{A}} and
A2: Y in {{A}} ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X )
 X = {A} by A1, TARSKI:def_1;
hence  ( X is_finer_than Y or Y is_finer_than X ) by A2, TARSKI:def_1; ::_thesis: verum
end;

theorem Th11: :: TAXONOM1:11
for A being non empty set holds SmallestPartition A is_finer_than {A}
proofend;

begin

definition
let A be non empty set ;
mode Classification of A ->  Subset of (PARTITIONS A) means :Def1: :: TAXONOM1:def 1
 for X, Y being a_partition of A st X in it & Y in it & not X is_finer_than Y holds
Y is_finer_than X;
existence
 ex b1 being Subset of (PARTITIONS A) st
for X, Y being a_partition of A st X in b1 & Y in b1 & not X is_finer_than Y holds
Y is_finer_than X
proofend;
end;

:: deftheorem Def1 defines Classification TAXONOM1:def_1_:_
 for A being non empty set
for b2 being Subset of (PARTITIONS A) holds
( b2 is Classification of A iff for X, Y being a_partition of A st X in b2 & Y in b2 & not X is_finer_than Y holds
Y is_finer_than X );

theorem :: TAXONOM1:12
for A being non empty set holds {{A}} is Classification of A
proofend;

theorem :: TAXONOM1:13
for A being non empty set holds {(SmallestPartition A)} is Classification of A
proofend;

theorem Th14: :: TAXONOM1:14
for A being non empty set
for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds
S is Classification of A
proofend;

definition
let A be non empty set ;
mode Strong_Classification of A ->  Subset of (PARTITIONS A) means :Def2: :: TAXONOM1:def 2
( it is Classification of A & {A} in it & SmallestPartition A in it );
existence
 ex b1 being Subset of (PARTITIONS A) st
( b1 is Classification of A & {A} in b1 & SmallestPartition A in b1 )
proofend;
end;

:: deftheorem Def2 defines Strong_Classification TAXONOM1:def_2_:_
 for A being non empty set
for b2 being Subset of (PARTITIONS A) holds
( b2 is Strong_Classification of A iff ( b2 is Classification of A & {A} in b2 & SmallestPartition A in b2 ) );

theorem :: TAXONOM1:15
for A being non empty set
for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds
S is Strong_Classification of A
proofend;

begin

definition
let X be non empty set ;
let f be PartFunc of [:X,X:],REAL;
let a be real number ;
func low_toler (f,a) ->  Relation of X means :Def3: :: TAXONOM1:def 3
 for x, y being Element of X holds
( [x,y] in it iff f . (x,y) <= a );
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 )
proofend;
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 ) ) &amp; ( for x, y being Element of X holds
( [x,y] in b2 iff f . (x,y) <= a ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines low_toler TAXONOM1:def_3_:_
 for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number
for b4 being Relation of X holds
( b4 = low_toler (f,a) iff for x, y being Element of X holds
( [x,y] in b4 iff f . (x,y) <= a ) );

theorem Th16: :: TAXONOM1:16
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number st f is Reflexive &amp; a >= 0 holds
low_toler (f,a) is_reflexive_in X
proofend;

theorem Th17: :: TAXONOM1:17
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number st f is symmetric holds
low_toler (f,a) is_symmetric_in X
proofend;

theorem Th18: :: TAXONOM1:18
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number st a >= 0 &amp; f is Reflexive &amp; f is symmetric holds
low_toler (f,a) is Tolerance of X
proofend;

theorem Th19: :: TAXONOM1:19
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a1, a2 being real number st a1 <= a2 holds
low_toler (f,a1) c= low_toler (f,a2)
proofend;

definition
let X be set ;
let f be PartFunc of [:X,X:],REAL;
attrf is nonnegative  means :Def4: :: TAXONOM1:def 4
 for x, y being Element of X holds f . (x,y) >= 0 ;
end;

:: deftheorem Def4 defines nonnegative TAXONOM1:def_4_:_
 for X being set
for f being PartFunc of [:X,X:],REAL holds
( f is nonnegative iff for x, y being Element of X holds f . (x,y) >= 0 );

theorem Th20: :: TAXONOM1:20
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for x, y being set st f is nonnegative &amp; f is Reflexive &amp; f is discerning &amp; [x,y] in low_toler (f,0) holds
x = y
proofend;

theorem Th21: :: TAXONOM1:21
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for x being Element of X st f is Reflexive &amp; f is discerning holds
[x,x] in low_toler (f,0)
proofend;

theorem Th22: :: TAXONOM1:22
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being real number st low_toler (f,a) is_reflexive_in X &amp; f is symmetric holds
(low_toler (f,a)) [*] is Equivalence_Relation of X
proofend;

Lm2:  for x being set
for X being non empty set
for a1, a2 being non negative real number 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)) [*] &amp; R2 = (low_toler (f,a2)) [*] holds
Class (R1,x) c= Class (R2,x)
proofend;

begin

theorem Th23: :: TAXONOM1:23
for X being non empty set
for f being PartFunc of [:X,X:],REAL st f is nonnegative &amp; f is Reflexive &amp; f is discerning holds
(low_toler (f,0)) [*] = low_toler (f,0)
proofend;

theorem Th24: :: TAXONOM1:24
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for R being Equivalence_Relation of X st R = (low_toler (f,0)) [*] &amp; f is nonnegative &amp; f is Reflexive &amp; f is discerning holds
R = id X
proofend;

theorem :: TAXONOM1:25
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for R being Equivalence_Relation of X st R = (low_toler (f,0)) [*] &amp; f is nonnegative &amp; f is Reflexive &amp; f is discerning holds
Class R = SmallestPartition X by Th24;

theorem Th26: :: TAXONOM1:26
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f &amp; A >= max z holds
for x, y being Element of X holds f . (x,y) <= A
proofend;

theorem Th27: :: TAXONOM1:27
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f &amp; A >= max z holds
for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds
Class R = {X}
proofend;

theorem :: TAXONOM1:28
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL
for z being non empty finite Subset of REAL
for A being real number st z = rng f &amp; A >= max z holds
(low_toler (f,A)) [*] = low_toler (f,A)
proofend;

begin

definition
let X be non empty set ;
let f be PartFunc of [:X,X:],REAL;
func fam_class f ->  Subset of (PARTITIONS X) means :Def5: :: TAXONOM1:def 5
 for x being set holds
( x in it iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] &amp; Class R = x ) );
existence
 ex b1 being Subset of (PARTITIONS X) st
for x being set holds
( x in b1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] &amp; Class R = x ) )
proofend;
uniqueness
 for b1, b2 being Subset of (PARTITIONS X) st ( for x being set holds
( x in b1 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] &amp; Class R = x ) ) ) &amp; ( for x being set holds
( x in b2 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] &amp; Class R = x ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines fam_class TAXONOM1:def_5_:_
 for X being non empty set
for f being PartFunc of [:X,X:],REAL
for b3 being Subset of (PARTITIONS X) holds
( b3 = fam_class f iff for x being set holds
( x in b3 iff ex a being non negative real number ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] &amp; Class R = x ) ) );

theorem :: TAXONOM1:29
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for a being non negative real number st low_toler (f,a) is_reflexive_in X &amp; f is symmetric holds
fam_class f is non empty set
proofend;

theorem Th30: :: TAXONOM1:30
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL st f is symmetric &amp; f is nonnegative holds
{X} in fam_class f
proofend;

theorem Th31: :: TAXONOM1:31
for X being non empty set
for f being PartFunc of [:X,X:],REAL holds fam_class f is Classification of X
proofend;

theorem :: TAXONOM1:32
for X being non empty finite Subset of REAL
for f being Function of [:X,X:],REAL st SmallestPartition X in fam_class f &amp; f is symmetric &amp; f is nonnegative holds
fam_class f is Strong_Classification of X
proofend;

begin

definition
let M be MetrStruct ;
let a be real number ;
let x, y be Element of M;
predx,y are_in_tolerance_wrt a means :Def6: :: TAXONOM1:def 6
 dist (x,y) <= a;
end;

:: deftheorem Def6 defines are_in_tolerance_wrt TAXONOM1:def_6_:_
 for M being MetrStruct
for a being real number
for x, y being Element of M holds
( x,y are_in_tolerance_wrt a iff dist (x,y) <= a );

definition
let M be non empty MetrStruct ;
let a be real number ;
func dist_toler (M,a) ->  Relation of M means :Def7: :: TAXONOM1:def 7
 for x, y being Element of M holds
( [x,y] in it iff x,y are_in_tolerance_wrt a );
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 )
proofend;
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 ) ) &amp; ( for x, y being Element of M holds
( [x,y] in b2 iff x,y are_in_tolerance_wrt a ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines dist_toler TAXONOM1:def_7_:_
 for M being non empty MetrStruct
for a being real number
for b3 being Relation of M holds
( b3 = dist_toler (M,a) iff for x, y being Element of M holds
( [x,y] in b3 iff x,y are_in_tolerance_wrt a ) );

theorem Th33: :: TAXONOM1:33
for M being non empty MetrStruct
for a being real number holds dist_toler (M,a) = low_toler ( the distance of M,a)
proofend;

theorem :: TAXONOM1:34
for M being non empty Reflexive symmetric MetrStruct
for a being real number
for T being Relation of the carrier of M, the carrier of M st T = dist_toler (M,a) &amp; a >= 0 holds
T is Tolerance of the carrier of M
proofend;

definition
let M be non empty Reflexive symmetric MetrStruct ;
func fam_class_metr M ->  Subset of (PARTITIONS the carrier of M) means :Def8: :: TAXONOM1:def 8
 for x being set holds
( x in it iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] &amp; Class R = x ) );
existence
 ex b1 being Subset of (PARTITIONS the carrier of M) st
for x being set holds
( x in b1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] &amp; Class R = x ) )
proofend;
uniqueness
 for b1, b2 being Subset of (PARTITIONS the carrier of M) st ( for x being set holds
( x in b1 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] &amp; Class R = x ) ) ) &amp; ( for x being set holds
( x in b2 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] &amp; Class R = x ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines fam_class_metr TAXONOM1:def_8_:_
 for M being non empty Reflexive symmetric MetrStruct
for b2 being Subset of (PARTITIONS the carrier of M) holds
( b2 = fam_class_metr M iff for x being set holds
( x in b2 iff ex a being non negative real number ex R being Equivalence_Relation of M st
( R = (dist_toler (M,a)) [*] &amp; Class R = x ) ) );

theorem Th35: :: TAXONOM1:35
for M being non empty Reflexive symmetric MetrStruct holds fam_class_metr M = fam_class the distance of M
proofend;

theorem Th36: :: TAXONOM1:36
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
proofend;

theorem Th37: :: TAXONOM1:37
for a being real number
for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
dist_toler (M,a) = nabla the carrier of M
proofend;

theorem Th38: :: TAXONOM1:38
for a being real number
for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
dist_toler (M,a) = (dist_toler (M,a)) [*]
proofend;

theorem Th39: :: TAXONOM1:39
for a being real number
for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds
(dist_toler (M,a)) [*] = nabla the carrier of M
proofend;

theorem Th40: :: TAXONOM1:40
for M being non empty Reflexive symmetric bounded MetrStruct
for R being Equivalence_Relation of M
for a being non negative real number st a >= diameter ([#] M) &amp; R = (dist_toler (M,a)) [*] holds
Class R = { the carrier of M}
proofend;

registration
let M be non empty Reflexive symmetric triangle MetrStruct ;
let C be non empty bounded Subset of M;
cluster diameter C ->  non negative ;
coherence
 not diameter C is negative by TBSP_1:21;
end;

theorem Th41: :: TAXONOM1:41
for M being non empty bounded MetrSpace holds { the carrier of M} in fam_class_metr M
proofend;

theorem Th42: :: TAXONOM1:42
for M being non empty Reflexive symmetric MetrStruct holds fam_class_metr M is Classification of the carrier of M
proofend;

theorem :: TAXONOM1:43
for M being non empty bounded MetrSpace holds fam_class_metr M is Strong_Classification of the carrier of M
proofend;