:: TAXONOM1 semantic presentation

registration

cluster real non negative set ;
existence

proof end;

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

proof end;

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

proof end;

theorem Th3: :: TAXONOM1:3

for X being set
for R being Relation of X st R is_reflexive_in X holds
dom R = X

proof end;

theorem :: TAXONOM1:4

for X being set
for R being Relation of X st R is_reflexive_in X holds
rng R = X

proof end;

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

proof end;

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 [*]

proof end;

theorem Th7: :: TAXONOM1:7

for X being set
for R being Relation of X st R is_reflexive_in X & R is_symmetric_in X holds
R [*] is_symmetric_in X

proof end;

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

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

proof end;

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 [*]

proof end;

Lm1: now

let A be non empty set ; :: thesis:
let X, Y be a_partition of A; :: thesis:
assume ( X in {{A}} & Y in {{A}} ) ; :: thesis:
then ( X = {A} & Y = {A} ) by TARSKI:def 1;
hence ( X is_finer_than Y or Y is_finer_than X ) ; :: thesis:

end;

theorem Th11: :: TAXONOM1:11

for A being non empty set holds SmallestPartition A is_finer_than {A}

proof end;

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

proof end;

end;

:: deftheorem Def1 defines Classification TAXONOM1:def 1 :

theorem :: TAXONOM1:12

for A being non empty set holds {{A}} is Classification of A

proof end;

theorem :: TAXONOM1:13

for A being non empty set holds {(SmallestPartition A)} is Classification of A

proof end;

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

proof end;

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

proof end;

end;

:: deftheorem Def2 defines Strong_Classification TAXONOM1:def 2 :

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

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines low_toler TAXONOM1:def 3 :

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 & 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 number 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 number 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 number st a1 <= a2 holds
low_toler f,a1 c= low_toler f,a2

proof end;

definition

let X be set ;
let f be PartFunc of [:X,X:], REAL ;
attr f 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 :

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

proof end;

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 & f is symmetric holds
(low_toler f,a) [*] is Equivalence_Relation of X

proof end;

Lm2: for x being set
for X being non empty set
for a1, a2 being real non negative 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) [*] & 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

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

proof end;

theorem Th25: :: 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

proof end;

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 & 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 number 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 number 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 ;
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 real non negative number ex R being Equivalence_Relation of X st
( R = (low_toler f,a) [*] & Class R = x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines fam_class TAXONOM1:def 5 :

theorem :: TAXONOM1:29

for X being non empty set
for f being PartFunc of [:X,X:], REAL
for a being real non negative number 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

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

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

proof end;

definition

let M be MetrStruct ;
let a be real number ;
let x, y be Element of M;
pred x,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 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines dist_toler TAXONOM1:def 7 :

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

proof end;

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 & a >= 0 holds
T is Tolerance of the carrier of M

proof end;

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 real non negative number ex R being Equivalence_Relation of M st
( R = (dist_toler M,a) [*] & Class R = x ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines fam_class_metr TAXONOM1:def 8 :

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

proof end;

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

proof end;

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) [*]

proof end;

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

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 real non negative number 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;
cluster diameter C -> non negative ;
coherence by TBSP_1:29;

end;

theorem Th41: :: TAXONOM1:41

for M being non empty bounded MetrSpace holds {the carrier of M} in fam_class_metr M

proof end;

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;