:: by Mariusz Giero and Roman Matuszewski

::

:: Received December 5, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

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

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

proof end;

theorem Th6: :: TAXONOM1:6

for X being set

for x, y being object

for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds

[x,y] in R [*]

for x, y being object

for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds

[x,y] in R [*]

proof end;

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

for R being Relation of X st R is_reflexive_in X & R is_symmetric_in X holds

R [*] is Equivalence_Relation of X

proof end;

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

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;
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

definition

let A be non empty set ;

ex b_{1} being Subset of (PARTITIONS A) st

for X, Y being a_partition of A st X in b_{1} & Y in b_{1} & not X is_finer_than Y holds

Y is_finer_than X

end;
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 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;

ex b

for X, Y being a_partition of A st X in b

Y is_finer_than X

proof end;

:: deftheorem Def1 defines Classification TAXONOM1:def 1 :

for A being non empty set

for b_{2} being Subset of (PARTITIONS A) holds

( b_{2} is Classification of A iff for X, Y being a_partition of A st X in b_{2} & Y in b_{2} & not X is_finer_than Y holds

Y is_finer_than X );

for A being non empty set

for b

( b

Y is_finer_than X );

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

for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds

S is Classification of A

proof end;

definition

let A be non empty set ;

ex b_{1} being Subset of (PARTITIONS A) st

( b_{1} is Classification of A & {A} in b_{1} & SmallestPartition A in b_{1} )

end;
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 ( it is Classification of A & {A} in it & SmallestPartition A in it );

ex b

( b

proof end;

:: deftheorem Def2 defines Strong_Classification TAXONOM1:def 2 :

for A being non empty set

for b_{2} being Subset of (PARTITIONS A) holds

( b_{2} is Strong_Classification of A iff ( b_{2} is Classification of A & {A} in b_{2} & SmallestPartition A in b_{2} ) );

for A being non empty set

for b

( b

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

for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds

S is Strong_Classification of A

proof end;

definition

let X be non empty set ;

let f be PartFunc of [:X,X:],REAL;

let a be Real;

ex b_{1} being Relation of X st

for x, y being Element of X holds

( [x,y] in b_{1} iff f . (x,y) <= a )

for b_{1}, b_{2} being Relation of X st ( for x, y being Element of X holds

( [x,y] in b_{1} iff f . (x,y) <= a ) ) & ( for x, y being Element of X holds

( [x,y] in b_{2} iff f . (x,y) <= a ) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of [:X,X:],REAL;

let a be Real;

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 for x, y being Element of X holds

( [x,y] in it iff f . (x,y) <= a );

ex b

for x, y being Element of X holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof 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

for b_{4} being Relation of X holds

( b_{4} = low_toler (f,a) iff for x, y being Element of X holds

( [x,y] in b_{4} iff f . (x,y) <= a ) );

for X being non empty set

for f being PartFunc of [:X,X:],REAL

for a being Real

for b

( b

( [x,y] in b

theorem Th16: :: TAXONOM1:16

for X being non empty set

for f being PartFunc of [:X,X:],REAL

for a being Real st f is Reflexive & a >= 0 holds

low_toler (f,a) is_reflexive_in X

for f being PartFunc of [:X,X:],REAL

for a being Real st f is Reflexive & a >= 0 holds

low_toler (f,a) is_reflexive_in X

proof end;

theorem Th17: :: TAXONOM1:17

for X being non empty set

for f being PartFunc of [:X,X:],REAL

for a being Real st f is symmetric holds

low_toler (f,a) is_symmetric_in X

for f being PartFunc of [:X,X:],REAL

for a being Real st f is symmetric holds

low_toler (f,a) is_symmetric_in X

proof end;

theorem Th18: :: TAXONOM1:18

for X being non empty set

for f being PartFunc of [:X,X:],REAL

for a being Real st a >= 0 & f is Reflexive & f is symmetric holds

low_toler (f,a) is Tolerance of X

for f being PartFunc of [:X,X:],REAL

for a being Real st a >= 0 & f is Reflexive & f is symmetric holds

low_toler (f,a) is Tolerance of X

proof end;

theorem Th19: :: TAXONOM1:19

for X being non empty set

for f being PartFunc of [:X,X:],REAL

for a1, a2 being Real st a1 <= a2 holds

low_toler (f,a1) c= low_toler (f,a2)

for f being PartFunc of [:X,X:],REAL

for a1, a2 being Real st a1 <= a2 holds

low_toler (f,a1) c= low_toler (f,a2)

proof end;

:: deftheorem 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 );

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 object st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds

x = y

for f being PartFunc of [:X,X:],REAL

for x, y being object st f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds

x = y

proof end;

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 & f is discerning holds

[x,x] in low_toler (f,0)

for f being PartFunc of [:X,X:],REAL

for x being Element of X st f is Reflexive & f is discerning holds

[x,x] in low_toler (f,0)

proof end;

theorem Th22: :: TAXONOM1:22

for X being non empty set

for f being PartFunc of [:X,X:],REAL

for 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

for f being PartFunc of [:X,X:],REAL

for 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 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)

proof end;

theorem Th23: :: TAXONOM1:23

for X being non empty set

for f being PartFunc of [:X,X:],REAL st f is nonnegative & f is Reflexive & f is discerning holds

(low_toler (f,0)) [*] = low_toler (f,0)

for f being PartFunc of [:X,X:],REAL st f is nonnegative & f is Reflexive & f is discerning holds

(low_toler (f,0)) [*] = low_toler (f,0)

proof end;

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)) [*] & f is nonnegative & f is Reflexive & f is discerning holds

R = id X

for f being PartFunc of [:X,X:],REAL

for R being Equivalence_Relation of X st R = (low_toler (f,0)) [*] & f is nonnegative & f is Reflexive & f is discerning holds

R = id X

proof end;

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)) [*] & f is nonnegative & f is Reflexive & f is discerning holds

Class R = SmallestPartition X by Th24;

for f being PartFunc of [:X,X:],REAL

for R being Equivalence_Relation of X st R = (low_toler (f,0)) [*] & f is nonnegative & f is Reflexive & 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 st z = rng f & A >= max z holds

for x, y being Element of X holds f . (x,y) <= A

for f being Function of [:X,X:],REAL

for z being non empty finite Subset of REAL

for A being Real st z = rng f & A >= max z holds

for x, y being Element of X holds f . (x,y) <= A

proof end;

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 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}

for f being Function of [:X,X:],REAL

for z being non empty finite Subset of REAL

for 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 end;

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 st z = rng f & A >= max z holds

(low_toler (f,A)) [*] = low_toler (f,A)

for f being Function of [:X,X:],REAL

for z being non empty finite Subset of REAL

for A being Real st z = rng f & A >= max z holds

(low_toler (f,A)) [*] = low_toler (f,A)

proof end;

definition

let X be non empty set ;

let f be PartFunc of [:X,X:],REAL;

ex b_{1} being Subset of (PARTITIONS X) st

for x being object holds

( x in b_{1} iff ex a being non negative Real ex R being Equivalence_Relation of X st

( R = (low_toler (f,a)) [*] & Class R = x ) )

for b_{1}, b_{2} being Subset of (PARTITIONS X) st ( for x being object holds

( x in b_{1} iff ex a being non negative Real ex R being Equivalence_Relation of X st

( R = (low_toler (f,a)) [*] & Class R = x ) ) ) & ( for x being object holds

( x in b_{2} iff ex a being non negative Real ex R being Equivalence_Relation of X st

( R = (low_toler (f,a)) [*] & Class R = x ) ) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of [:X,X:],REAL;

func fam_class f -> Subset of (PARTITIONS X) means :Def5: :: TAXONOM1:def 5

for x being object holds

( x in it iff ex a being non negative Real ex R being Equivalence_Relation of X st

( R = (low_toler (f,a)) [*] & Class R = x ) );

existence for x being object holds

( x in it iff ex a being non negative Real ex R being Equivalence_Relation of X st

( R = (low_toler (f,a)) [*] & Class R = x ) );

ex b

for x being object holds

( x in b

( R = (low_toler (f,a)) [*] & Class R = x ) )

proof end;

uniqueness for b

( x in b

( R = (low_toler (f,a)) [*] & Class R = x ) ) ) & ( for x being object holds

( x in b

( R = (low_toler (f,a)) [*] & Class R = x ) ) ) holds

b

proof end;

:: deftheorem Def5 defines fam_class TAXONOM1:def 5 :

for X being non empty set

for f being PartFunc of [:X,X:],REAL

for b_{3} being Subset of (PARTITIONS X) holds

( b_{3} = fam_class f iff for x being object holds

( x in b_{3} iff ex a being non negative Real ex R being Equivalence_Relation of X st

( R = (low_toler (f,a)) [*] & Class R = x ) ) );

for X being non empty set

for f being PartFunc of [:X,X:],REAL

for b

( b

( x in b

( R = (low_toler (f,a)) [*] & 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 st low_toler (f,a) is_reflexive_in X & f is symmetric holds

fam_class f is non empty set

for f being PartFunc of [:X,X:],REAL

for a being non negative Real st low_toler (f,a) is_reflexive_in X & f is symmetric holds

fam_class f is non empty set

proof end;

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 & f is nonnegative holds

{X} in fam_class f

for f being Function of [:X,X:],REAL st f is symmetric & f is nonnegative holds

{X} in fam_class f

proof end;

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

for f being PartFunc of [:X,X:],REAL holds fam_class f is Classification of X

proof end;

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 & f is symmetric & f is nonnegative holds

fam_class f is Strong_Classification of X

for f being Function of [:X,X:],REAL st SmallestPartition X in fam_class f & f is symmetric & f is nonnegative holds

fam_class f is Strong_Classification of X

proof end;

:: deftheorem defines are_in_tolerance_wrt TAXONOM1:def 6 :

for M being MetrStruct

for a being Real

for x, y being Element of M holds

( x,y are_in_tolerance_wrt a iff dist (x,y) <= a );

for M being MetrStruct

for a being Real

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;

ex b_{1} being Relation of M st

for x, y being Element of M holds

( [x,y] in b_{1} iff x,y are_in_tolerance_wrt a )

for b_{1}, b_{2} being Relation of M st ( for x, y being Element of M holds

( [x,y] in b_{1} iff x,y are_in_tolerance_wrt a ) ) & ( for x, y being Element of M holds

( [x,y] in b_{2} iff x,y are_in_tolerance_wrt a ) ) holds

b_{1} = b_{2}

end;
let a be Real;

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 for x, y being Element of M holds

( [x,y] in it iff x,y are_in_tolerance_wrt a );

ex b

for x, y being Element of M holds

( [x,y] in b

proof end;

uniqueness for b

( [x,y] in b

( [x,y] in b

b

proof end;

:: deftheorem Def7 defines dist_toler TAXONOM1:def 7 :

for M being non empty MetrStruct

for a being Real

for b_{3} being Relation of M holds

( b_{3} = dist_toler (M,a) iff for x, y being Element of M holds

( [x,y] in b_{3} iff x,y are_in_tolerance_wrt a ) );

for M being non empty MetrStruct

for a being Real

for b

( b

( [x,y] in b

theorem Th33: :: TAXONOM1:33

for M being non empty MetrStruct

for a being Real holds dist_toler (M,a) = low_toler ( the distance of M,a)

for a being Real holds dist_toler (M,a) = low_toler ( the distance of M,a)

proof end;

theorem :: TAXONOM1:34

for M being non empty Reflexive symmetric MetrStruct

for a being Real

for 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

for a being Real

for 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 end;

definition

let M be non empty Reflexive symmetric MetrStruct ;

ex b_{1} being Subset of (PARTITIONS the carrier of M) st

for x being object holds

( x in b_{1} iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) )

for b_{1}, b_{2} being Subset of (PARTITIONS the carrier of M) st ( for x being object holds

( x in b_{1} iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being object holds

( x in b_{2} iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) holds

b_{1} = b_{2}

end;
func fam_class_metr M -> Subset of (PARTITIONS the carrier of M) means :Def8: :: TAXONOM1:def 8

for x being object holds

( x in it iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) );

existence for x being object holds

( x in it iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) );

ex b

for x being object holds

( x in b

( R = (dist_toler (M,a)) [*] & Class R = x ) )

proof end;

uniqueness for b

( x in b

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being object holds

( x in b

( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) holds

b

proof end;

:: deftheorem Def8 defines fam_class_metr TAXONOM1:def 8 :

for M being non empty Reflexive symmetric MetrStruct

for b_{2} being Subset of (PARTITIONS the carrier of M) holds

( b_{2} = fam_class_metr M iff for x being object holds

( x in b_{2} iff ex a being non negative Real ex R being Equivalence_Relation of M st

( R = (dist_toler (M,a)) [*] & Class R = x ) ) );

for M being non empty Reflexive symmetric MetrStruct

for b

( b

( x in b

( R = (dist_toler (M,a)) [*] & 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

proof end;

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

for R being Equivalence_Relation of M st R = (dist_toler (M,0)) [*] holds

Class R = SmallestPartition the carrier of M

proof end;

theorem Th37: :: TAXONOM1:37

for a being Real

for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds

dist_toler (M,a) = nabla the carrier of M

for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds

dist_toler (M,a) = nabla the carrier of M

proof end;

theorem Th38: :: TAXONOM1:38

for a being Real

for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds

dist_toler (M,a) = (dist_toler (M,a)) [*]

for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds

dist_toler (M,a) = (dist_toler (M,a)) [*]

proof end;

theorem Th39: :: TAXONOM1:39

for a being Real

for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds

(dist_toler (M,a)) [*] = nabla the carrier of M

for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds

(dist_toler (M,a)) [*] = nabla the carrier of M

proof end;

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 st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds

Class R = { the carrier of M}

for R being Equivalence_Relation of M

for a being non negative Real st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds

Class R = { the carrier of M}

proof end;

registration

let M be non empty Reflexive symmetric triangle MetrStruct ;

let C be non empty bounded Subset of M;

coherence

not diameter C is negative by TBSP_1:21;

end;
let C be non empty bounded Subset of M;

coherence

not diameter C is negative by TBSP_1:21;

theorem Th42: :: TAXONOM1:42

for M being non empty Reflexive symmetric MetrStruct holds fam_class_metr M is Classification of the carrier of M

proof end;

theorem :: TAXONOM1:43

for M being non empty bounded MetrSpace holds fam_class_metr M is Strong_Classification of the carrier of M

proof end;