:: Lower Tolerance. {P}reliminaries to {W}roclaw Taxonomy :: by Mariusz Giero and Roman Matuszewski :: :: Received December 5, 2000 :: Copyright (c) 2000-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, PARTFUN1, ZFMISC_1, XXREAL_0, CARD_1, FINSEQ_1, NAT_1, ARYTM_3, RELAT_1, FUNCT_1, RELAT_2, TARSKI, REWRITE1, FINSEQ_5, ARYTM_1, SUBSET_1, EQREL_1, SETFAM_1, PARTIT1, METRIC_1, SUPINF_2, FINSET_1, STRUCT_0, XXREAL_2, MEASURE5, TAXONOM1, REAL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, PARTFUN1, STRUCT_0, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, PARTIT1, METRIC_1, TBSP_1, FINSET_1, EQREL_1, ALG_1, REWRITE1, FINSEQ_1, XXREAL_2, NAT_1, LANG1, FINSEQ_5; constructors NAT_1, PARTIT1, FINSEQ_5, REWRITE1, TBSP_1, LANG1, XXREAL_2, RELSET_1, BINOP_1, BINOP_2, VALUED_0; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, EQREL_1, STRUCT_0, TBSP_1, XXREAL_2, BINOP_2, VALUED_0, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM; begin :: Preliminaries reserve A,X for non empty set; reserve f for PartFunc of [:X,X:],REAL; reserve a for Real; registration cluster non negative for Real; end; theorem :: TAXONOM1:1 for p being FinSequence, k being Nat st k+1 in dom p & not k in dom p holds k = 0; theorem :: TAXONOM1:2 for p being FinSequence, i,j being Nat st i in dom p & j in dom p & for k be Nat st k in dom p & k + 1 in dom p holds p.k = p.(k + 1) holds p.i = p.j; theorem :: TAXONOM1:3 for X being set, R being Relation of X st R is_reflexive_in X holds dom R = X ; theorem :: TAXONOM1:4 for X being set, R being Relation of X st R is_reflexive_in X holds rng R = X ; theorem :: TAXONOM1:5 for X being set, R being Relation of X st R is_reflexive_in X holds R[*] is_reflexive_in X; theorem :: TAXONOM1:6 for X being set,x,y be object for R be Relation of X st R is_reflexive_in X holds R reduces x,y & x in X implies [x,y] in R[*]; theorem :: TAXONOM1:7 for X being set, R being Relation of X st R is_symmetric_in X holds R[*] is_symmetric_in X; theorem :: TAXONOM1:8 for X being set, R being Relation of X st R is_reflexive_in X holds R[*] is_transitive_in X; theorem :: TAXONOM1:9 for X being non empty set, R being Relation of X st R is_reflexive_in X & R is_symmetric_in X holds R[*] is Equivalence_Relation of X ; theorem :: TAXONOM1:10 for R1,R2 being Relation of X holds R1 c= R2 implies R1[*] c= R2 [*]; theorem :: TAXONOM1:11 SmallestPartition A is_finer_than {A}; begin :: The notion of classification definition let A be non empty set; mode Classification of A -> Subset of PARTITIONS(A) means :: TAXONOM1:def 1 for X,Y being a_partition of A st X in it & Y in it holds X is_finer_than Y or Y is_finer_than X; end; theorem :: TAXONOM1:12 {{A}} is Classification of A; theorem :: TAXONOM1:13 {SmallestPartition A} is Classification of A; theorem :: TAXONOM1:14 for S being Subset of PARTITIONS(A) st S = {{A}, SmallestPartition A} holds S is Classification of A; definition let A be non empty set; mode Strong_Classification of A -> Subset of PARTITIONS(A) means :: TAXONOM1:def 2 it is Classification of A & {A} in it & SmallestPartition A in it; end; theorem :: TAXONOM1:15 for S being Subset of PARTITIONS(A) st S = {{A},SmallestPartition A} holds S is Strong_Classification of A; begin :: The tolerance on a non empty set definition let X be non empty set, f be PartFunc of [:X,X:], REAL, a be Real; func low_toler(f,a) -> Relation of X means :: TAXONOM1:def 3 for x,y being Element of X holds [x,y] in it iff f.(x,y) <= a; end; theorem :: TAXONOM1:16 f is Reflexive & a >= 0 implies low_toler(f,a) is_reflexive_in X; theorem :: TAXONOM1:17 f is symmetric implies low_toler(f,a) is_symmetric_in X; theorem :: TAXONOM1:18 a >= 0 & f is Reflexive symmetric implies low_toler(f,a) is Tolerance of X; theorem :: TAXONOM1:19 for X being non empty set, f being PartFunc of [:X,X:], REAL, a1 ,a2 being Real st a1 <= a2 holds low_toler(f,a1) c= low_toler(f,a2); definition let X be set; let f be PartFunc of [:X,X:], REAL; attr f is nonnegative means :: TAXONOM1:def 4 for x,y being Element of X holds f.(x,y) >= 0; end; theorem :: TAXONOM1:20 for X being non empty set, f being PartFunc of [:X,X:],REAL, x,y being object st f is nonnegative Reflexive discerning holds [x,y] in low_toler(f,0 ) implies x = y; theorem :: TAXONOM1:21 for X being non empty set, f being PartFunc of [:X,X:],REAL, x being Element of X st f is Reflexive discerning holds [x,x] in low_toler(f,0) ; theorem :: TAXONOM1:22 for X being non empty set, f being PartFunc of [:X,X:],REAL, a being Real st low_toler(f,a) is_reflexive_in X & f is symmetric holds low_toler(f,a)[*] is Equivalence_Relation of X; begin :: The partitions defined by lower tolerance theorem :: TAXONOM1:23 for X being non empty set, f being PartFunc of [:X,X:],REAL st f is nonnegative Reflexive discerning holds low_toler(f,0)[*] = low_toler(f,0); theorem :: TAXONOM1:24 for X being non empty set, f being PartFunc of [:X,X:],REAL, R being Equivalence_Relation of X st R = low_toler(f,0)[*] & f is nonnegative Reflexive discerning holds R = id X; theorem :: TAXONOM1:25 for X being non empty set, f being PartFunc of [:X,X:],REAL, R being Equivalence_Relation of X st R = low_toler(f,0)[*] & f is nonnegative Reflexive discerning holds Class R = SmallestPartition X; theorem :: TAXONOM1:26 for X being finite non empty Subset of REAL, f being Function of [:X,X:],REAL, z being finite non empty Subset of REAL, A being Real st z = rng f & A >= max z holds for x,y being Element of X holds f.(x,y) <= A; theorem :: TAXONOM1:27 for X being finite non empty Subset of REAL, f being Function of [:X,X:],REAL, z being finite non empty Subset of REAL, A being Real st z = rng f & A >= max z holds for R being Equivalence_Relation of X st R = low_toler(f,A)[*] holds Class R = {X}; theorem :: TAXONOM1:28 for X being finite non empty Subset of REAL, f being Function of [:X,X :],REAL, z being finite non empty Subset of REAL, A being Real st z = rng f & A >= max z holds low_toler(f,A)[*] = low_toler(f,A); begin :: The classification on a non empty set definition let X be non empty set, f being PartFunc of [:X,X:],REAL; func fam_class(f) -> Subset of PARTITIONS(X) means :: TAXONOM1:def 5 for x being object holds x in it iff ex a being non negative Real,R be Equivalence_Relation of X st R = low_toler(f,a)[*] & Class(R) = x; end; theorem :: TAXONOM1:29 for X being non empty set, f being PartFunc of [:X,X:],REAL, a being non negative Real st low_toler(f,a) is_reflexive_in X & f is symmetric holds fam_class(f) is non empty set; theorem :: TAXONOM1:30 for X being finite non empty Subset of REAL, f being Function of [:X,X:],REAL st f is symmetric nonnegative holds {X} in fam_class(f); theorem :: TAXONOM1:31 for X being non empty set, f being PartFunc of [:X,X:],REAL holds fam_class(f) is Classification of X; theorem :: TAXONOM1:32 for X being finite non empty Subset of REAL, f being Function of [:X,X :],REAL st (SmallestPartition X) in fam_class(f) & f is symmetric nonnegative holds fam_class(f) is Strong_Classification of X; begin :: The classification on a metric space definition let M be MetrStruct, a be Real, x,y be Element of M; pred x,y are_in_tolerance_wrt a means :: TAXONOM1:def 6 dist(x,y) <= a; end; definition let M be non empty MetrStruct, a be Real; func dist_toler(M,a) -> Relation of M means :: TAXONOM1:def 7 for x,y being Element of M holds [x,y] in it iff x,y are_in_tolerance_wrt a; end; theorem :: TAXONOM1:33 for M being non empty MetrStruct, a being Real holds dist_toler(M,a) = low_toler(the distance of M,a); theorem :: TAXONOM1:34 for M being non empty Reflexive symmetric MetrStruct, a being Real , T being Relation of the carrier of M,the carrier of M st T = dist_toler (M,a) & a >= 0 holds T is Tolerance of the carrier of M; definition let M be Reflexive symmetric non empty MetrStruct; func fam_class_metr(M) -> Subset of PARTITIONS(the carrier of M) means :: TAXONOM1:def 8 for x being object holds x in it iff ex a being non negative Real,R be Equivalence_Relation of M st R = dist_toler(M,a)[*] & Class(R) = x; end; theorem :: TAXONOM1:35 for M being Reflexive symmetric non empty MetrStruct holds fam_class_metr(M) = fam_class(the distance of M); theorem :: 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; theorem :: TAXONOM1:37 for M being Reflexive symmetric bounded non empty MetrStruct st a >= diameter [#]M holds dist_toler(M,a) = nabla the carrier of M; theorem :: TAXONOM1:38 for M being Reflexive symmetric bounded non empty MetrStruct st a >= diameter [#]M holds dist_toler(M,a) = dist_toler(M,a)[*]; theorem :: TAXONOM1:39 for M being Reflexive symmetric bounded non empty MetrStruct st a >= diameter [#]M holds dist_toler(M,a)[*] = nabla the carrier of M; theorem :: TAXONOM1:40 for M being Reflexive symmetric bounded non empty MetrStruct, R being Equivalence_Relation of M, a being non negative Real st a >= diameter [#]M & R = dist_toler(M,a)[*] holds Class R = {the carrier of M}; registration let M be Reflexive symmetric triangle non empty MetrStruct, C be non empty bounded Subset of M; cluster diameter C -> non negative; end; theorem :: TAXONOM1:41 for M being bounded non empty MetrSpace holds {the carrier of M} in fam_class_metr(M); theorem :: TAXONOM1:42 for M being Reflexive symmetric non empty MetrStruct holds fam_class_metr(M) is Classification of the carrier of M; theorem :: TAXONOM1:43 for M being bounded non empty MetrSpace holds fam_class_metr(M) is Strong_Classification of the carrier of M;