:: TAXONOM1 semantic presentation begin registration clusterV11() ext-real non negative real for set ; existence not for b1 being real number holds b1 is negative proof take 0 ; ::_thesis: not 0 is negative thus not 0 is negative ; ::_thesis: verum 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 let p be FinSequence; ::_thesis: for k being Nat st k + 1 in dom p & not k in dom p holds k = 0 let k be Nat; ::_thesis: ( k + 1 in dom p & not k in dom p implies k = 0 ) assume that A1: k + 1 in dom p and A2: not k in dom p ; ::_thesis: k = 0 assume k <> 0 ; ::_thesis: contradiction 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 contradiction by A2, A3, FINSEQ_3:25; ::_thesis: verum 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 let p be FinSequence; ::_thesis: 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 let i, j be Nat; ::_thesis: ( 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) ) implies p . i = p . j ) assume that A1: ( i in dom p & j in dom p ) and A2: for k being Nat st k in dom p & k + 1 in dom p holds p . k = p . (k + 1) ; ::_thesis: p . i = p . j defpred S1[ 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 S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] let j be Nat; ::_thesis: ( k + 1 in dom p & j in dom p implies p . (k + 1) = p . j ) assume that A5: k + 1 in dom p and A6: j in dom p ; ::_thesis: p . (k + 1) = p . j percases ( k in dom p or not k in dom p ) ; supposeA7: k in dom p ; ::_thesis: p . (k + 1) = p . j hence p . (k + 1) = p . k by A2, A5 .= p . j by A4, A6, A7 ; ::_thesis: verum end; supposeA8: not k in dom p ; ::_thesis: p . (k + 1) = p . j defpred S2[ Nat] means ( \$1 in dom p implies p . \$1 = p . 1 ); A9: for w being Nat st S2[w] holds S2[w + 1] proof let w be Nat; ::_thesis: ( S2[w] implies S2[w + 1] ) assume A10: S2[w] ; ::_thesis: S2[w + 1] assume A11: w + 1 in dom p ; ::_thesis: p . (w + 1) = p . 1 percases ( w in dom p or not w in dom p ) ; suppose w in dom p ; ::_thesis: p . (w + 1) = p . 1 hence p . (w + 1) = p . 1 by A2, A10, A11; ::_thesis: verum end; suppose not w in dom p ; ::_thesis: p . (w + 1) = p . 1 then w = 0 by A11, Th1; hence p . (w + 1) = p . 1 ; ::_thesis: verum end; end; end; A12: S2[ 0 ] by FINSEQ_3:24; A13: for k being Nat holds S2[k] from NAT_1:sch_2(A12, A9); k = 0 by A5, A8, Th1; hence p . (k + 1) = p . j by A6, A13; ::_thesis: verum end; end; end; A14: S1[ 0 ] by FINSEQ_3:24; for k being Nat holds S1[k] from NAT_1:sch_2(A14, A3); hence p . i = p . j by A1; ::_thesis: verum 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 let X be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds dom R = X let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies dom R = X ) assume A1: R is_reflexive_in X ; ::_thesis: dom R = X for x being set st x in X holds ex y being set st [x,y] in R proof let x be set ; ::_thesis: ( x in X implies ex y being set st [x,y] in R ) assume A2: x in X ; ::_thesis: ex y being set st [x,y] in R take x ; ::_thesis: [x,x] in R thus [x,x] in R by A1, A2, RELAT_2:def_1; ::_thesis: verum end; hence dom R = X by RELSET_1:9; ::_thesis: verum 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 let X be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds rng R = X let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies rng R = X ) assume A1: R is_reflexive_in X ; ::_thesis: rng R = X for x being set st x in X holds ex y being set st [y,x] in R proof let x be set ; ::_thesis: ( x in X implies ex y being set st [y,x] in R ) assume A2: x in X ; ::_thesis: ex y being set st [y,x] in R consider x1 being set such that A3: x1 = x ; take x1 ; ::_thesis: [x1,x] in R thus [x1,x] in R by A1, A2, A3, RELAT_2:def_1; ::_thesis: verum end; hence rng R = X by RELSET_1:10; ::_thesis: verum 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 let X be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds R [*] is_reflexive_in X let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies R [*] is_reflexive_in X ) assume A1: R is_reflexive_in X ; ::_thesis: R [*] is_reflexive_in X now__::_thesis:_for_x_being_set_st_x_in_X_holds_ [x,x]_in_R_[*] let x be set ; ::_thesis: ( x in X implies [x,x] in R [*] ) assume x in X ; ::_thesis: [x,x] in R [*] then A2: [x,x] in R by A1, RELAT_2:def_1; R c= R [*] by LANG1:18; hence [x,x] in R [*] by A2; ::_thesis: verum end; hence R [*] is_reflexive_in X by RELAT_2:def_1; ::_thesis: verum 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 let X, x, y be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X & R reduces x,y & x in X holds [x,y] in R [*] let R be Relation of X; ::_thesis: ( R is_reflexive_in X & R reduces x,y & x in X implies [x,y] in R [*] ) assume A1: R is_reflexive_in X ; ::_thesis: ( not R reduces x,y or not x in X or [x,y] in R [*] ) assume that A2: R reduces x,y and A3: x in X ; ::_thesis: [x,y] in R [*] percases ( [x,y] in R [*] or x = y ) by A2, REWRITE1:20; suppose [x,y] in R [*] ; ::_thesis: [x,y] in R [*] hence [x,y] in R [*] ; ::_thesis: verum end; supposeA4: x = y ; ::_thesis: [x,y] in R [*] R [*] is_reflexive_in X by A1, Th5; hence [x,y] in R [*] by A3, A4, RELAT_2:def_1; ::_thesis: verum end; end; end; 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 proof let X be set ; ::_thesis: for R being Relation of X st R is_symmetric_in X holds R [*] is_symmetric_in X let R be Relation of X; ::_thesis: ( R is_symmetric_in X implies R [*] is_symmetric_in X ) assume A1: R is_symmetric_in X ; ::_thesis: R [*] is_symmetric_in X now__::_thesis:_for_x,_y_being_set_st_x_in_X_&_y_in_X_&_[x,y]_in_R_[*]_holds_ [y,x]_in_R_[*] let x, y be set ; ::_thesis: ( x in X & y in X & [x,y] in R [*] implies [y,x] in R [*] ) assume that x in X and y in X and A2: [x,y] in R [*] ; ::_thesis: [y,x] in R [*] A3: ( x in field R & y in field R ) by A2, FINSEQ_1:def_16; 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_16; consider r being FinSequence such that A8: r = Rev p ; A9: now__::_thesis:_for_j_being_Nat_st_j_>=_1_&_j_<_len_r_holds_ [(r_._j),(r_._(j_+_1))]_in_R let j be Nat; ::_thesis: ( j >= 1 & j < len r implies [(r . j),(r . (j + 1))] in R ) assume that A10: j >= 1 and A11: j < len r ; ::_thesis: [(r . j),(r . (j + 1))] in 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; ::_thesis: verum 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, FINSEQ_5:def_3; hence [y,x] in R [*] by A3, A19, A9, FINSEQ_1:def_16; ::_thesis: verum end; hence R [*] is_symmetric_in X by RELAT_2:def_3; ::_thesis: verum 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 let X be set ; ::_thesis: for R being Relation of X st R is_reflexive_in X holds R [*] is_transitive_in X let R be Relation of X; ::_thesis: ( R is_reflexive_in X implies R [*] is_transitive_in X ) assume A1: R is_reflexive_in X ; ::_thesis: R [*] is_transitive_in X now__::_thesis:_for_x,_y,_z_being_set_st_x_in_X_&_y_in_X_&_z_in_X_&_[x,y]_in_R_[*]_&_[y,z]_in_R_[*]_holds_ [x,z]_in_R_[*] let x, y, z be set ; ::_thesis: ( x in X & y in X & z in X & [x,y] in R [*] & [y,z] in R [*] implies [x,z] in R [*] ) assume that A2: x in X and y in X and z in X and A3: ( [x,y] in R [*] & [y,z] in R [*] ) ; ::_thesis: [x,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; ::_thesis: verum end; hence R [*] is_transitive_in X by RELAT_2:def_8; ::_thesis: verum 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 let X be non empty set ; ::_thesis: for R being Relation of X st R is_reflexive_in X & R is_symmetric_in X holds R [*] is Equivalence_Relation of X let R be Relation of X; ::_thesis: ( R is_reflexive_in X & R is_symmetric_in X implies R [*] is Equivalence_Relation of X ) assume that A1: R is_reflexive_in X and A2: R is_symmetric_in X ; ::_thesis: R [*] is Equivalence_Relation of 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 R [*] is Equivalence_Relation of X by A3, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum 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 let X be non empty set ; ::_thesis: for R1, R2 being Relation of X st R1 c= R2 holds R1 [*] c= R2 [*] let R1, R2 be Relation of X; ::_thesis: ( R1 c= R2 implies R1 [*] c= R2 [*] ) assume A1: R1 c= R2 ; ::_thesis: R1 [*] c= R2 [*] now__::_thesis:_for_p_being_set_st_p_in_R1_[*]_holds_ p_in_R2_[*] A2: field R1 c= field R2 by A1, RELAT_1:16; let p be set ; ::_thesis: ( p in R1 [*] implies p in R2 [*] ) assume A3: p in R1 [*] ; ::_thesis: p in R2 [*] consider x, y being set 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_16; A7: now__::_thesis:_for_i_being_Nat_st_i_>=_1_&_i_<_len_r_holds_ [(r_._i),(r_._(i_+_1))]_in_R2 let i be Nat; ::_thesis: ( i >= 1 & i < len r implies [(r . i),(r . (i + 1))] in R2 ) assume ( i >= 1 & i < len r ) ; ::_thesis: [(r . i),(r . (i + 1))] in R2 then [(r . i),(r . (i + 1))] in R1 by A6; hence [(r . i),(r . (i + 1))] in R2 by A1; ::_thesis: verum end; ( x in field R1 & y in field R1 ) by A3, A4, FINSEQ_1:def_16; hence p in R2 [*] by A4, A5, A2, A7, FINSEQ_1:def_16; ::_thesis: verum end; hence R1 [*] c= R2 [*] by TARSKI:def_3; ::_thesis: verum 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 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} proof let A be non empty set ; ::_thesis: SmallestPartition A is_finer_than {A} let X be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not X in SmallestPartition A or ex b1 being set st ( b1 in {A} & X c= b1 ) ) assume A1: X in SmallestPartition A ; ::_thesis: ex b1 being set st ( b1 in {A} & X c= b1 ) take A ; ::_thesis: ( A in {A} & X c= A ) thus ( A in {A} & X c= A ) by A1, TARSKI:def_1; ::_thesis: verum end; 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 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 ; ::_thesis: for X, Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds Y is_finer_than X thus for X, Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds Y is_finer_than X by Lm1; ::_thesis: verum end; 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 proof let A be non empty set ; ::_thesis: {{A}} is Classification of A {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; :: according to TAXONOM1:def_1 ::_thesis: for Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds Y is_finer_than X thus for Y being a_partition of A st X in S & Y in S & not X is_finer_than Y holds Y is_finer_than X by Lm1; ::_thesis: verum end; hence {{A}} is Classification of A ; ::_thesis: verum end; theorem :: TAXONOM1:13 for A being non empty set holds {(SmallestPartition A)} is Classification of A proof let A be non empty set ; ::_thesis: {(SmallestPartition A)} is Classification of A 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; :: according to TAXONOM1:def_1 ::_thesis: ( X in S & Y in S & not X is_finer_than Y implies Y is_finer_than X ) assume that A1: X in S and A2: Y in S ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X ) X = SmallestPartition 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; hence {(SmallestPartition A)} is Classification of A ; ::_thesis: verum 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 let A be non empty set ; ::_thesis: for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds S is Classification of A let S be Subset of (PARTITIONS A); ::_thesis: ( S = {{A},(SmallestPartition A)} implies S is Classification of A ) assume A1: S = {{A},(SmallestPartition A)} ; ::_thesis: S is Classification of A let X, Y be a_partition of A; :: according to TAXONOM1:def_1 ::_thesis: ( X in S & Y in S & not X is_finer_than Y implies Y is_finer_than X ) assume that A2: X in S and A3: Y in S ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X ) percases ( X = {A} or X = SmallestPartition A ) by A1, A2, TARSKI:def_2; supposeA4: X = {A} ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X ) percases ( Y = {A} or Y = SmallestPartition A ) by A1, A3, TARSKI:def_2; suppose Y = {A} ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X ) hence ( X is_finer_than Y or Y is_finer_than X ) by A4; ::_thesis: verum end; suppose Y = SmallestPartition A ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X ) hence ( X is_finer_than Y or Y is_finer_than X ) by A4, Th11; ::_thesis: verum end; end; end; supposeA5: X = SmallestPartition A ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X ) percases ( Y = SmallestPartition A or Y = {A} ) by A1, A3, TARSKI:def_2; suppose Y = SmallestPartition A ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X ) hence ( X is_finer_than Y or Y is_finer_than X ) by A5; ::_thesis: verum end; suppose Y = {A} ; ::_thesis: ( X is_finer_than Y or Y is_finer_than X ) hence ( X is_finer_than Y or Y is_finer_than X ) by A5, Th11; ::_thesis: verum end; end; end; end; 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 ex b1 being Subset of (PARTITIONS A) st ( b1 is Classification of A & {A} in b1 & SmallestPartition A in b1 ) 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 ; ::_thesis: ( S is Classification of A & {A} in S & SmallestPartition A in S ) thus ( S is Classification of A & {A} in S & SmallestPartition A in S ) by Th14, TARSKI:def_2; ::_thesis: verum end; 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 proof let A be non empty set ; ::_thesis: for S being Subset of (PARTITIONS A) st S = {{A},(SmallestPartition A)} holds S is Strong_Classification of A let S be Subset of (PARTITIONS A); ::_thesis: ( S = {{A},(SmallestPartition A)} implies S is Strong_Classification of A ) assume A1: S = {{A},(SmallestPartition A)} ; ::_thesis: S is Strong_Classification of 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 S is Strong_Classification of A by A2, Def2; ::_thesis: verum end; 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 ) proof defpred S1[ 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 S1[x,y] ) from RELSET_1:sch_2(); take R ; ::_thesis: for x, y being Element of X holds ( [x,y] in R iff f . (x,y) <= a ) thus for x, y being Element of X holds ( [x,y] in R iff f . (x,y) <= a ) by A1; ::_thesis: verum end; 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 proof let R1, R2 be Relation of X; ::_thesis: ( ( for x, y being Element of X holds ( [x,y] in R1 iff f . (x,y) <= a ) ) & ( for x, y being Element of X holds ( [x,y] in R2 iff f . (x,y) <= a ) ) implies R1 = R2 ) assume 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 ) ; ::_thesis: R1 = R2 A4: for c, d being set st [c,d] in R2 holds [c,d] in R1 proof let c, d be set ; ::_thesis: ( [c,d] in R2 implies [c,d] in R1 ) assume A5: [c,d] in R2 ; ::_thesis: [c,d] in R1 then reconsider c1 = c, d1 = d as Element of X by ZFMISC_1:87; f . (c1,d1) <= a by A3, A5; hence [c,d] in R1 by A2; ::_thesis: verum end; for c, d being set st [c,d] in R1 holds [c,d] in R2 proof let c, d be set ; ::_thesis: ( [c,d] in R1 implies [c,d] in R2 ) assume A6: [c,d] in R1 ; ::_thesis: [c,d] in R2 then reconsider c1 = c, d1 = d as Element of X by ZFMISC_1:87; f . (c1,d1) <= a by A2, A6; hence [c,d] in R2 by A3; ::_thesis: verum end; hence R1 = R2 by A4, RELAT_1:def_2; ::_thesis: verum end; 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 & a >= 0 holds low_toler (f,a) is_reflexive_in X proof let X be non empty set ; ::_thesis: 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 let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being real number st f is Reflexive & a >= 0 holds low_toler (f,a) is_reflexive_in X let a be real number ; ::_thesis: ( f is Reflexive & a >= 0 implies low_toler (f,a) is_reflexive_in X ) assume A1: ( f is Reflexive & a >= 0 ) ; ::_thesis: low_toler (f,a) is_reflexive_in X now__::_thesis:_for_x_being_set_st_x_in_X_holds_ [x,x]_in_low_toler_(f,a) let x be set ; ::_thesis: ( x in X implies [x,x] in low_toler (f,a) ) assume x in X ; ::_thesis: [x,x] in low_toler (f,a) 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; ::_thesis: verum end; hence low_toler (f,a) is_reflexive_in X by RELAT_2:def_1; ::_thesis: verum 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 let X be non empty set ; ::_thesis: 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 let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being real number st f is symmetric holds low_toler (f,a) is_symmetric_in X let a be real number ; ::_thesis: ( f is symmetric implies low_toler (f,a) is_symmetric_in X ) assume A1: f is symmetric ; ::_thesis: low_toler (f,a) is_symmetric_in X now__::_thesis:_for_x,_y_being_set_st_x_in_X_&_y_in_X_&_[x,y]_in_low_toler_(f,a)_holds_ [y,x]_in_low_toler_(f,a) let x, y be set ; ::_thesis: ( x in X & y in X & [x,y] in low_toler (f,a) implies [y,x] in low_toler (f,a) ) assume that A2: ( x in X & y in X ) and A3: [x,y] in low_toler (f,a) ; ::_thesis: [y,x] 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; ::_thesis: verum end; hence low_toler (f,a) is_symmetric_in X by RELAT_2:def_3; ::_thesis: verum 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 let X be non empty set ; ::_thesis: 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 let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being real number st a >= 0 & f is Reflexive & f is symmetric holds low_toler (f,a) is Tolerance of X let a be real number ; ::_thesis: ( a >= 0 & f is Reflexive & f is symmetric implies low_toler (f,a) is Tolerance of X ) set T = low_toler (f,a); assume that A1: a >= 0 and A2: ( f is Reflexive & f is symmetric ) ; ::_thesis: low_toler (f,a) is Tolerance of X A3: low_toler (f,a) is_reflexive_in X by A1, A2, Th16; A4: dom (low_toler (f,a)) = X by A1, A2, Th3, Th16; then A5: field (low_toler (f,a)) = X \/ (rng (low_toler (f,a))) by RELAT_1:def_6 .= X by XBOOLE_1:12 ; then low_toler (f,a) is_symmetric_in field (low_toler (f,a)) by A2, Th17; hence low_toler (f,a) is Tolerance of X by A3, A4, A5, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_11; ::_thesis: verum 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 let X be non empty set ; ::_thesis: 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) let f be PartFunc of [:X,X:],REAL; ::_thesis: for a1, a2 being real number st a1 <= a2 holds low_toler (f,a1) c= low_toler (f,a2) let a1, a2 be real number ; ::_thesis: ( a1 <= a2 implies low_toler (f,a1) c= low_toler (f,a2) ) assume A1: a1 <= a2 ; ::_thesis: low_toler (f,a1) c= low_toler (f,a2) now__::_thesis:_for_p_being_set_st_p_in_low_toler_(f,a1)_holds_ p_in_low_toler_(f,a2) let p be set ; ::_thesis: ( p in low_toler (f,a1) implies p in low_toler (f,a2) ) assume A2: p in low_toler (f,a1) ; ::_thesis: p in low_toler (f,a2) consider x, y being set 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; ::_thesis: verum end; hence low_toler (f,a1) c= low_toler (f,a2) by TARSKI:def_3; ::_thesis: verum end; 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 & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) holds x = y proof let X be non empty set ; ::_thesis: 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 let f be PartFunc of [:X,X:],REAL; ::_thesis: 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 let x, y be set ; ::_thesis: ( f is nonnegative & f is Reflexive & f is discerning & [x,y] in low_toler (f,0) implies x = y ) assume A1: ( f is nonnegative & f is Reflexive & f is discerning ) ; ::_thesis: ( not [x,y] in low_toler (f,0) or x = y ) assume A2: [x,y] in low_toler (f,0) ; ::_thesis: x = y 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, Def4; hence x = y by A1, METRIC_1:def_3; ::_thesis: verum 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 let X be non empty set ; ::_thesis: 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) let f be PartFunc of [:X,X:],REAL; ::_thesis: for x being Element of X st f is Reflexive & f is discerning holds [x,x] in low_toler (f,0) let x be Element of X; ::_thesis: ( f is Reflexive & f is discerning implies [x,x] in low_toler (f,0) ) assume ( f is Reflexive & f is discerning ) ; ::_thesis: [x,x] in low_toler (f,0) then f . (x,x) = 0 by METRIC_1:def_2; hence [x,x] in low_toler (f,0) by Def3; ::_thesis: verum 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 let X be non empty set ; ::_thesis: 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 let f be PartFunc of [:X,X:],REAL; ::_thesis: 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 let a be real number ; ::_thesis: ( low_toler (f,a) is_reflexive_in X & f is symmetric implies (low_toler (f,a)) [*] is Equivalence_Relation of X ) assume that A1: low_toler (f,a) is_reflexive_in X and A2: f is symmetric ; ::_thesis: (low_toler (f,a)) [*] is Equivalence_Relation of X now__::_thesis:_for_x,_y_being_set_st_x_in_X_&_y_in_X_&_[x,y]_in_low_toler_(f,a)_holds_ [y,x]_in_low_toler_(f,a) let x, y be set ; ::_thesis: ( x in X & y in X & [x,y] in low_toler (f,a) implies [y,x] in low_toler (f,a) ) assume that A3: ( x in X & y in X ) and A4: [x,y] in low_toler (f,a) ; ::_thesis: [y,x] 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; ::_thesis: verum end; then low_toler (f,a) is_symmetric_in X by RELAT_2:def_3; hence (low_toler (f,a)) [*] is Equivalence_Relation of X by A1, Th9; ::_thesis: verum end; 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)) [*] & R2 = (low_toler (f,a2)) [*] holds Class (R1,x) c= Class (R2,x) proof let x be set ; ::_thesis: 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)) [*] & R2 = (low_toler (f,a2)) [*] holds Class (R1,x) c= Class (R2,x) let X be non empty set ; ::_thesis: 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)) [*] & R2 = (low_toler (f,a2)) [*] holds Class (R1,x) c= Class (R2,x) let a1, a2 be non negative real number ; ::_thesis: ( a1 <= a2 implies 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) ) assume A1: a1 <= a2 ; ::_thesis: 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) let f be PartFunc of [:X,X:],REAL; ::_thesis: 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) let R1, R2 be Equivalence_Relation of X; ::_thesis: ( R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] implies Class (R1,x) c= Class (R2,x) ) assume A2: ( R1 = (low_toler (f,a1)) [*] & R2 = (low_toler (f,a2)) [*] ) ; ::_thesis: Class (R1,x) c= Class (R2,x) now__::_thesis:_for_z1_being_set_st_z1_in_Class_(R1,x)_holds_ z1_in_Class_(R2,x) let z1 be set ; ::_thesis: ( z1 in Class (R1,x) implies z1 in Class (R2,x) ) assume z1 in Class (R1,x) ; ::_thesis: z1 in Class (R2,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; ::_thesis: verum end; hence Class (R1,x) c= Class (R2,x) by TARSKI:def_3; ::_thesis: verum end; begin 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 let X be non empty set ; ::_thesis: 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) let f be PartFunc of [:X,X:],REAL; ::_thesis: ( f is nonnegative & f is Reflexive & f is discerning implies (low_toler (f,0)) [*] = low_toler (f,0) ) assume A1: ( f is nonnegative & f is Reflexive & f is discerning ) ; ::_thesis: (low_toler (f,0)) [*] = low_toler (f,0) now__::_thesis:_for_p_being_set_st_p_in_(low_toler_(f,0))_[*]_holds_ p_in_low_toler_(f,0) let p be set ; ::_thesis: ( p in (low_toler (f,0)) [*] implies p in low_toler (f,0) ) assume A2: p in (low_toler (f,0)) [*] ; ::_thesis: p in low_toler (f,0) consider x, y being set 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__::_thesis:_for_i_being_Nat_st_i_in_dom_r_&_i_+_1_in_dom_r_holds_ r_._i_=_r_._(i_+_1) let i be Nat; ::_thesis: ( i in dom r & i + 1 in dom r implies r . i = r . (i + 1) ) assume ( i in dom r & i + 1 in dom r ) ; ::_thesis: r . i = r . (i + 1) then [(r . i),(r . (i + 1))] in low_toler (f,0) by REWRITE1:def_2; hence r . i = r . (i + 1) by A1, Th20; ::_thesis: verum 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; ::_thesis: verum end; then ( low_toler (f,0) c= (low_toler (f,0)) [*] & (low_toler (f,0)) [*] c= low_toler (f,0) ) by LANG1:18, TARSKI:def_3; hence (low_toler (f,0)) [*] = low_toler (f,0) by XBOOLE_0:def_10; ::_thesis: verum 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 let X be non empty set ; ::_thesis: 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 let f be PartFunc of [:X,X:],REAL; ::_thesis: 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 let R be Equivalence_Relation of X; ::_thesis: ( R = (low_toler (f,0)) [*] & f is nonnegative & f is Reflexive & f is discerning implies R = id X ) assume that A1: R = (low_toler (f,0)) [*] and A2: ( f is nonnegative & f is Reflexive & f is discerning ) ; ::_thesis: R = id X A3: for x, y being set st x in X & x = y holds [x,y] in (low_toler (f,0)) [*] proof let x, y be set ; ::_thesis: ( x in X & x = y implies [x,y] in (low_toler (f,0)) [*] ) assume ( x in X & x = y ) ; ::_thesis: [x,y] in (low_toler (f,0)) [*] then [x,y] in low_toler (f,0) by A2, Th21; hence [x,y] in (low_toler (f,0)) [*] by A2, Th23; ::_thesis: verum end; for x, y being set st [x,y] in (low_toler (f,0)) [*] holds ( x in X & x = y ) proof let x, y be set ; ::_thesis: ( [x,y] in (low_toler (f,0)) [*] implies ( x in X & x = y ) ) assume [x,y] in (low_toler (f,0)) [*] ; ::_thesis: ( x in X & x = y ) then [x,y] in low_toler (f,0) by A2, Th23; hence ( x in X & x = y ) by A2, Th20, ZFMISC_1:87; ::_thesis: verum end; hence R = id X by A1, A3, RELAT_1:def_10; ::_thesis: verum 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; 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 let X be non empty finite Subset of REAL; ::_thesis: 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 let f be Function of [:X,X:],REAL; ::_thesis: 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 let z be non empty finite Subset of REAL; ::_thesis: 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 let A be real number ; ::_thesis: ( z = rng f & A >= max z implies for x, y being Element of X holds f . (x,y) <= A ) assume that A1: z = rng f and A2: A >= max z ; ::_thesis: for x, y being Element of X holds f . (x,y) <= A now__::_thesis:_for_x,_y_being_Element_of_X_holds_f_._(x,y)_<=_A let x, y be Element of X; ::_thesis: f . (x,y) <= A f . [x,y] = f . (x,y) ; then reconsider c = f . [x,y] as real number ; 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; ::_thesis: verum end; hence for x, y being Element of X holds f . (x,y) <= A ; ::_thesis: verum 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 let X be non empty finite Subset of REAL; ::_thesis: 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} let f be Function of [:X,X:],REAL; ::_thesis: 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} let z be non empty finite Subset of REAL; ::_thesis: 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} let A be real number ; ::_thesis: ( z = rng f & A >= max z implies for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds Class R = {X} ) assume A1: ( z = rng f & A >= max z ) ; ::_thesis: for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds Class R = {X} now__::_thesis:_for_R_being_Equivalence_Relation_of_X_st_R_=_(low_toler_(f,A))_[*]_holds_ Class_R_=_{X} let R be Equivalence_Relation of X; ::_thesis: ( R = (low_toler (f,A)) [*] implies Class R = {X} ) assume A2: R = (low_toler (f,A)) [*] ; ::_thesis: Class R = {X} A3: for x being set st x in X holds X = Class (R,x) proof let x be set ; ::_thesis: ( x in X implies X = Class (R,x) ) assume x in X ; ::_thesis: X = Class (R,x) then reconsider x9 = x as Element of X ; now__::_thesis:_for_x1_being_set_st_x1_in_X_holds_ x1_in_Class_(R,x) let x1 be set ; ::_thesis: ( x1 in X implies x1 in Class (R,x) ) assume x1 in X ; ::_thesis: x1 in Class (R,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; ::_thesis: verum end; then X c= Class (R,x) by TARSKI:def_3; hence X = Class (R,x) by XBOOLE_0:def_10; ::_thesis: verum end; now__::_thesis:_for_a_being_set_st_a_in_{X}_holds_ a_in_Class_R let a be set ; ::_thesis: ( a in {X} implies a in Class R ) assume a in {X} ; ::_thesis: a in Class R then A5: a = X by TARSKI:def_1; consider x being set 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; ::_thesis: verum end; then A7: {X} c= Class R by TARSKI:def_3; now__::_thesis:_for_a_being_set_st_a_in_Class_R_holds_ a_in_{X} let a be set ; ::_thesis: ( a in Class R implies a in {X} ) assume a in Class R ; ::_thesis: a in {X} then ex x being set 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; ::_thesis: verum end; then Class R c= {X} by TARSKI:def_3; hence Class R = {X} by A7, XBOOLE_0:def_10; ::_thesis: verum end; hence for R being Equivalence_Relation of X st R = (low_toler (f,A)) [*] holds Class R = {X} ; ::_thesis: verum 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 let X be non empty finite Subset of REAL; ::_thesis: 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) let f be Function of [:X,X:],REAL; ::_thesis: 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) let z be non empty finite Subset of REAL; ::_thesis: for A being real number st z = rng f & A >= max z holds (low_toler (f,A)) [*] = low_toler (f,A) let A be real number ; ::_thesis: ( z = rng f & A >= max z implies (low_toler (f,A)) [*] = low_toler (f,A) ) assume A1: ( z = rng f & A >= max z ) ; ::_thesis: (low_toler (f,A)) [*] = low_toler (f,A) now__::_thesis:_for_p_being_set_st_p_in_(low_toler_(f,A))_[*]_holds_ p_in_low_toler_(f,A) let p be set ; ::_thesis: ( p in (low_toler (f,A)) [*] implies p in low_toler (f,A) ) assume p in (low_toler (f,A)) [*] ; ::_thesis: p in low_toler (f,A) then consider x, y being set 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; ::_thesis: verum end; then ( low_toler (f,A) c= (low_toler (f,A)) [*] & (low_toler (f,A)) [*] c= low_toler (f,A) ) by LANG1:18, TARSKI:def_3; hence (low_toler (f,A)) [*] = low_toler (f,A) by XBOOLE_0:def_10; ::_thesis: verum end; 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)) [*] & 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)) [*] & Class R = x ) ) proof defpred S1[ set ] means ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = \$1 ); consider A being set such that A1: for x being set holds ( x in A iff ( x in PARTITIONS X & S1[x] ) ) from XBOOLE_0:sch_1(); A c= PARTITIONS X proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A or a in PARTITIONS X ) assume a in A ; ::_thesis: a in PARTITIONS X hence a in PARTITIONS X by A1; ::_thesis: verum end; then reconsider A1 = A as Subset of (PARTITIONS X) ; take A1 ; ::_thesis: for x being set holds ( x in A1 iff ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = x ) ) let x be set ; ::_thesis: ( x in A1 iff ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = x ) ) thus ( x in A1 implies ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = x ) ) by A1; ::_thesis: ( ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = x ) implies x in A1 ) given a being non negative real number , R being Equivalence_Relation of X such that A2: ( R = (low_toler (f,a)) [*] & Class R = x ) ; ::_thesis: x in A1 Class R in PARTITIONS X by PARTIT1:def_3; hence x in A1 by A1, A2; ::_thesis: verum end; 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)) [*] & Class R = x ) ) ) & ( 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)) [*] & Class R = x ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex a being non negative real number ex R being 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 set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from LMOD_7:sch_1(); let X1, X2 be Subset of (PARTITIONS X); ::_thesis: ( ( for x being set holds ( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = x ) ) ) & ( for x being set holds ( x in X2 iff ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = x ) ) ) implies X1 = X2 ) assume ( ( for x being set holds ( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = x ) ) ) & ( for x being set holds ( x in X2 iff ex a being non negative real number ex R being Equivalence_Relation of X st ( R = (low_toler (f,a)) [*] & Class R = x ) ) ) ) ; ::_thesis: X1 = X2 hence X1 = X2 by A3; ::_thesis: verum end; 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)) [*] & 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 & f is symmetric holds fam_class f is non empty set proof let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL for a being non negative real number st low_toler (f,a) is_reflexive_in X & f is symmetric holds fam_class f is non empty set let f be PartFunc of [:X,X:],REAL; ::_thesis: for a being non negative real number st low_toler (f,a) is_reflexive_in X & f is symmetric holds fam_class f is non empty set let a be non negative real number ; ::_thesis: ( low_toler (f,a) is_reflexive_in X & f is symmetric implies fam_class f is non empty set ) assume ( low_toler (f,a) is_reflexive_in X & f is symmetric ) ; ::_thesis: fam_class f is non empty set 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 fam_class f is non empty set ; ::_thesis: verum 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 let X be non empty finite Subset of REAL; ::_thesis: for f being Function of [:X,X:],REAL st f is symmetric & f is nonnegative holds {X} in fam_class f let f be Function of [:X,X:],REAL; ::_thesis: ( f is symmetric & f is nonnegative implies {X} in fam_class f ) assume A1: ( f is symmetric & f is nonnegative ) ; ::_thesis: {X} in fam_class f dom f = [:X,X:] by FUNCT_2:def_1; then reconsider rn = rng f as non empty finite Subset of REAL by RELAT_1:42; reconsider A1 = max rn as real number ; now__::_thesis:_not_A1_is_negative set x = the Element of X; assume A2: A1 is negative ; ::_thesis: contradiction f . ( the Element of X, the Element of X) <= A1 by Th26; hence contradiction by A1, A2, Def4; ::_thesis: verum end; then reconsider A19 = A1 as non negative real number ; now__::_thesis:_for_x_being_set_st_x_in_X_holds_ [x,x]_in_low_toler_(f,A1) let x be set ; ::_thesis: ( x in X implies [x,x] in low_toler (f,A1) ) assume x in X ; ::_thesis: [x,x] in low_toler (f,A1) then reconsider x1 = x as Element of X ; f . (x1,x1) <= A1 by Th26; hence [x,x] in low_toler (f,A1) by Def3; ::_thesis: verum 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 {X} in fam_class f by Th27; ::_thesis: verum 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 let X be non empty set ; ::_thesis: for f being PartFunc of [:X,X:],REAL holds fam_class f is Classification of X let f be PartFunc of [:X,X:],REAL; ::_thesis: fam_class f is Classification of X for A, B being a_partition of X st A in fam_class f & B in fam_class f & not A is_finer_than B holds B is_finer_than A proof let A, B be a_partition of X; ::_thesis: ( A in fam_class f & B in fam_class f & not A is_finer_than B implies B is_finer_than A ) assume that A1: A in fam_class f and A2: B in fam_class f ; ::_thesis: ( A is_finer_than B or B is_finer_than A ) consider a1 being non negative real number , 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 number , R2 being Equivalence_Relation of X such that A5: R2 = (low_toler (f,a2)) [*] and A6: Class R2 = B by A2, Def5; now__::_thesis:_(_A_is_finer_than_B_or_B_is_finer_than_A_) percases ( a1 <= a2 or a1 > a2 ) ; supposeA7: a1 <= a2 ; ::_thesis: ( A is_finer_than B or B is_finer_than A ) now__::_thesis:_for_x_being_set_st_x_in_A_holds_ ex_y_being_set_st_ (_y_in_B_&_x_c=_y_) let x be set ; ::_thesis: ( x in A implies ex y being set st ( y in B & x c= y ) ) assume x in A ; ::_thesis: ex y being set st ( y in B & x c= y ) then consider c being set 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 = y; ::_thesis: ( y in B & x c= y ) thus y in B by A6, A8, A10, EQREL_1:def_3; ::_thesis: x c= y thus x c= y by A3, A5, A7, A9, A10, Lm2; ::_thesis: verum end; hence ( A is_finer_than B or B is_finer_than A ) by SETFAM_1:def_2; ::_thesis: verum end; supposeA11: a1 > a2 ; ::_thesis: ( A is_finer_than B or B is_finer_than A ) now__::_thesis:_for_y_being_set_st_y_in_B_holds_ ex_x_being_set_st_ (_x_in_A_&_y_c=_x_) let y be set ; ::_thesis: ( y in B implies ex x being set st ( x in A & y c= x ) ) assume y in B ; ::_thesis: ex x being set st ( x in A & y c= x ) then consider c being set 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 = x; ::_thesis: ( x in A & y c= x ) thus x in A by A4, A12, A14, EQREL_1:def_3; ::_thesis: y c= x thus y c= x by A3, A5, A11, A13, A14, Lm2; ::_thesis: verum end; hence ( A is_finer_than B or B is_finer_than A ) by SETFAM_1:def_2; ::_thesis: verum end; end; end; hence ( A is_finer_than B or B is_finer_than A ) ; ::_thesis: verum end; hence fam_class f is Classification of X by Def1; ::_thesis: verum 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 let X be non empty finite Subset of REAL; ::_thesis: 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 let f be Function of [:X,X:],REAL; ::_thesis: ( SmallestPartition X in fam_class f & f is symmetric & f is nonnegative implies fam_class f is Strong_Classification of X ) assume that A1: SmallestPartition X in fam_class f and A2: ( f is symmetric & f is nonnegative ) ; ::_thesis: fam_class f is Strong_Classification of X A3: fam_class f is Classification of X by Th31; {X} in fam_class f by A2, Th30; hence fam_class f is Strong_Classification of X by A1, A3, Def2; ::_thesis: verum end; 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 ) proof defpred S1[ 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 S1[x,y] ) from RELSET_1:sch_2(); reconsider R = R as Relation of M ; take R ; ::_thesis: for x, y being Element of M holds ( [x,y] in R iff x,y are_in_tolerance_wrt a ) thus for x, y being Element of M holds ( [x,y] in R iff x,y are_in_tolerance_wrt a ) by A1; ::_thesis: verum end; 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 proof let A, B be Relation of M; ::_thesis: ( ( for x, y being Element of M holds ( [x,y] in A iff x,y are_in_tolerance_wrt a ) ) & ( for x, y being Element of M holds ( [x,y] in B iff x,y are_in_tolerance_wrt a ) ) implies A = B ) assume 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 ) ; ::_thesis: A = B A4: for c, d being set st [c,d] in B holds [c,d] in A proof let c, d be set ; ::_thesis: ( [c,d] in B implies [c,d] in A ) assume A5: [c,d] in B ; ::_thesis: [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 A3, A5; hence [c,d] in A by A2; ::_thesis: verum end; for c, d being set st [c,d] in A holds [c,d] in B proof let c, d be set ; ::_thesis: ( [c,d] in A implies [c,d] in B ) assume A6: [c,d] in A ; ::_thesis: [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 A2, A6; hence [c,d] in B by A3; ::_thesis: verum end; hence A = B by A4, RELAT_1:def_2; ::_thesis: verum end; 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) proof let M be non empty MetrStruct ; ::_thesis: for a being real number holds dist_toler (M,a) = low_toler ( the distance of M,a) let a be real number ; ::_thesis: dist_toler (M,a) = low_toler ( the distance of M,a) now__::_thesis:_for_z_being_set_st_z_in_low_toler_(_the_distance_of_M,a)_holds_ z_in_dist_toler_(M,a) let z be set ; ::_thesis: ( z in low_toler ( the distance of M,a) implies z in dist_toler (M,a) ) assume A1: z in low_toler ( the distance of M,a) ; ::_thesis: z in dist_toler (M,a) consider x, y being set 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 by Def6; hence z in dist_toler (M,a) by A3, Def7; ::_thesis: verum end; then A4: low_toler ( the distance of M,a) c= dist_toler (M,a) by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in_dist_toler_(M,a)_holds_ z_in_low_toler_(_the_distance_of_M,a) let z be set ; ::_thesis: ( z in dist_toler (M,a) implies z in low_toler ( the distance of M,a) ) assume A5: z in dist_toler (M,a) ; ::_thesis: z in low_toler ( the distance of M,a) consider x, y being set 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 by Def6; hence z in low_toler ( the distance of M,a) by A7, Def3; ::_thesis: verum end; then dist_toler (M,a) c= low_toler ( the distance of M,a) by TARSKI:def_3; hence dist_toler (M,a) = low_toler ( the distance of M,a) by A4, XBOOLE_0:def_10; ::_thesis: verum 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 let M be non empty Reflexive symmetric MetrStruct ; ::_thesis: 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 let a be real number ; ::_thesis: 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 let T be Relation of the carrier of M, the carrier of M; ::_thesis: ( T = dist_toler (M,a) & a >= 0 implies T is Tolerance of the carrier of M ) assume that A1: T = dist_toler (M,a) and A2: a >= 0 ; ::_thesis: T is Tolerance of the carrier of M A3: ( the distance of M is symmetric & the distance of M is Reflexive ) by METRIC_1:def_6, METRIC_1:def_8; T = low_toler ( the distance of M,a) by A1, Th33; hence T is Tolerance of the carrier of M by A2, A3, Th18; ::_thesis: verum 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 non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & 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)) [*] & Class R = x ) ) proof defpred S1[ set ] means ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = \$1 ); consider X being set such that A1: for x being set holds ( x in X iff ( x in PARTITIONS the carrier of M & S1[x] ) ) from XBOOLE_0:sch_1(); X c= PARTITIONS the carrier of M proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in PARTITIONS the carrier of M ) assume a in X ; ::_thesis: a in PARTITIONS the carrier of M hence a in PARTITIONS the carrier of M by A1; ::_thesis: verum end; then reconsider X1 = X as Subset of (PARTITIONS the carrier of M) ; take X1 ; ::_thesis: for x being set holds ( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = x ) ) let x be set ; ::_thesis: ( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = x ) ) thus ( x in X1 implies ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = x ) ) by A1; ::_thesis: ( ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = x ) implies x in X1 ) given a being non negative real number , R being Equivalence_Relation of M such that A2: ( R = (dist_toler (M,a)) [*] & Class R = x ) ; ::_thesis: x in X1 Class R in PARTITIONS the carrier of M by PARTIT1:def_3; hence x in X1 by A1, A2; ::_thesis: verum end; 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)) [*] & Class R = x ) ) ) & ( 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)) [*] & Class R = x ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex a being non negative real number ex R being 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 set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from LMOD_7:sch_1(); let X1, X2 be Subset of (PARTITIONS the carrier of M); ::_thesis: ( ( for x being set holds ( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being set holds ( x in X2 iff ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) implies X1 = X2 ) assume ( ( for x being set holds ( x in X1 iff ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) & ( for x being set holds ( x in X2 iff ex a being non negative real number ex R being Equivalence_Relation of M st ( R = (dist_toler (M,a)) [*] & Class R = x ) ) ) ) ; ::_thesis: X1 = X2 hence X1 = X2 by A3; ::_thesis: verum end; 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)) [*] & 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 let M be non empty Reflexive symmetric MetrStruct ; ::_thesis: fam_class_metr M = fam_class the distance of M now__::_thesis:_for_z_being_set_st_z_in_fam_class_the_distance_of_M_holds_ z_in_fam_class_metr_M let z be set ; ::_thesis: ( z in fam_class the distance of M implies z in fam_class_metr M ) assume z in fam_class the distance of M ; ::_thesis: z in fam_class_metr M then consider a being non negative real number , R being 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; ::_thesis: verum end; then A3: fam_class the distance of M c= fam_class_metr M by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in_fam_class_metr_M_holds_ z_in_fam_class_the_distance_of_M let z be set ; ::_thesis: ( z in fam_class_metr M implies z in fam_class the distance of M ) assume z in fam_class_metr M ; ::_thesis: z in fam_class the distance of M then consider a being non negative real number , R being 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; ::_thesis: verum end; then fam_class_metr M c= fam_class the distance of M by TARSKI:def_3; hence fam_class_metr M = fam_class the distance of M by A3, XBOOLE_0:def_10; ::_thesis: verum 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 let M be non empty MetrSpace; ::_thesis: for R being Equivalence_Relation of M st R = (dist_toler (M,0)) [*] holds Class R = SmallestPartition the carrier of M now__::_thesis:_for_x,_y_being_Element_of_M_holds_the_distance_of_M_._(x,y)_>=_0 let x, y be Element of M; ::_thesis: the distance of M . (x,y) >= 0 dist (x,y) >= 0 by METRIC_1:5; hence the distance of M . (x,y) >= 0 by METRIC_1:def_1; ::_thesis: verum end; then A1: the distance of M is nonnegative by Def4; let R be Equivalence_Relation of M; ::_thesis: ( R = (dist_toler (M,0)) [*] implies Class R = SmallestPartition the carrier of M ) assume R = (dist_toler (M,0)) [*] ; ::_thesis: Class R = SmallestPartition the carrier of M then ( the distance of M is Reflexive & the distance of M is discerning & (low_toler ( the distance of M,0)) [*] = R ) by Th33, METRIC_1:def_6, METRIC_1:def_7; hence Class R = SmallestPartition the carrier of M by A1, Th24; ::_thesis: verum 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 let a be real number ; ::_thesis: for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds dist_toler (M,a) = nabla the carrier of M let M be non empty Reflexive symmetric bounded MetrStruct ; ::_thesis: ( a >= diameter ([#] M) implies dist_toler (M,a) = nabla the carrier of M ) assume A1: a >= diameter ([#] M) ; ::_thesis: dist_toler (M,a) = nabla the carrier of M now__::_thesis:_for_z_being_set_st_z_in_nabla_the_carrier_of_M_holds_ z_in_dist_toler_(M,a) let z be set ; ::_thesis: ( z in nabla the carrier of M implies z in dist_toler (M,a) ) assume z in nabla the carrier of M ; ::_thesis: z in dist_toler (M,a) then consider x, y being set 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 by Def6; hence z in dist_toler (M,a) by A3, Def7; ::_thesis: verum end; then nabla the carrier of M c= dist_toler (M,a) by TARSKI:def_3; hence dist_toler (M,a) = nabla the carrier of M by XBOOLE_0:def_10; ::_thesis: verum 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 let a be real number ; ::_thesis: for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds dist_toler (M,a) = (dist_toler (M,a)) [*] let M be non empty Reflexive symmetric bounded MetrStruct ; ::_thesis: ( a >= diameter ([#] M) implies dist_toler (M,a) = (dist_toler (M,a)) [*] ) assume A1: a >= diameter ([#] M) ; ::_thesis: dist_toler (M,a) = (dist_toler (M,a)) [*] (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 dist_toler (M,a) = (dist_toler (M,a)) [*] by XBOOLE_0:def_10; ::_thesis: verum 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 let a be real number ; ::_thesis: for M being non empty Reflexive symmetric bounded MetrStruct st a >= diameter ([#] M) holds (dist_toler (M,a)) [*] = nabla the carrier of M let M be non empty Reflexive symmetric bounded MetrStruct ; ::_thesis: ( a >= diameter ([#] M) implies (dist_toler (M,a)) [*] = nabla the carrier of M ) assume A1: a >= diameter ([#] M) ; ::_thesis: (dist_toler (M,a)) [*] = nabla the carrier of M dist_toler (M,a) = (dist_toler (M,a)) [*] by A1, Th38; hence (dist_toler (M,a)) [*] = nabla the carrier of M by A1, Th37; ::_thesis: verum 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 number st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds Class R = { the carrier of M} proof let M be non empty Reflexive symmetric bounded MetrStruct ; ::_thesis: for R being Equivalence_Relation of M for a being non negative real number st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds Class R = { the carrier of M} let R be Equivalence_Relation of M; ::_thesis: for a being non negative real number st a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] holds Class R = { the carrier of M} let a be non negative real number ; ::_thesis: ( a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] implies Class R = { the carrier of M} ) assume A1: ( a >= diameter ([#] M) & R = (dist_toler (M,a)) [*] ) ; ::_thesis: Class R = { the carrier of M} Class (nabla the carrier of M) = { the carrier of M} by MSUALG_9:4; hence Class R = { the carrier of M} by A1, Th39; ::_thesis: verum 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 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 proof let M be non empty bounded MetrSpace; ::_thesis: { the carrier of M} in fam_class_metr M set a = diameter ([#] M); the distance of M is symmetric by METRIC_1:def_8; then low_toler ( the distance of M,(diameter ([#] M))) is_symmetric_in the carrier of M by Th17; then A1: dist_toler (M,(diameter ([#] M))) 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,(diameter ([#] M))) is_reflexive_in the carrier of M by Th16; then dist_toler (M,(diameter ([#] M))) is_reflexive_in the carrier of M by Th33; then reconsider R = (dist_toler (M,(diameter ([#] M)))) [*] as Equivalence_Relation of M by A1, Th9; Class R = { the carrier of M} by Th40; hence { the carrier of M} in fam_class_metr M by Def8; ::_thesis: verum 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 let M be non empty Reflexive symmetric MetrStruct ; ::_thesis: fam_class_metr M is Classification of the carrier of M fam_class_metr M = fam_class the distance of M by Th35; hence fam_class_metr M is Classification of the carrier of M by Th31; ::_thesis: verum 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 reconsider a = 0 as non negative real number ; let M be non empty bounded MetrSpace; ::_thesis: fam_class_metr M is Strong_Classification of the carrier of 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 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 fam_class_metr M is Strong_Classification of the carrier of M by A2, Def2; ::_thesis: verum end;