Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### Lower Tolerance. Preliminaries to Wroclaw Taxonomy

**by****Mariusz Giero, and****Roman Matuszewski**- Received December 5, 2000
- MML identifier: TAXONOM1

- [ Mizar article, MML identifier index ]

environ vocabulary PARTFUN1, ARYTM, ZF_LANG, FINSEQ_1, RELAT_1, FUNCT_1, RELAT_2, REWRITE1, FINSEQ_5, ARYTM_1, EQREL_1, SETFAM_1, PUA2MSS1, PARTIT1, METRIC_1, TOLER_1, BOOLE, SUPINF_2, FINSET_1, SQUARE_1, LATTICES, TBSP_1, SUBSET_1, TAXONOM1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, PARTFUN1, STRUCT_0, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, PARTIT1, PRE_TOPC, METRIC_1, TBSP_1, FINSET_1, EQREL_1, ALG_1, REWRITE1, FINSEQ_1, PRE_CIRC, NAT_1, LANG1, FINSEQ_5; constructors PARTIT1, PUA2MSS1, ALG_1, REWRITE1, NAT_1, LANG1, FINSEQ_5, PRE_CIRC, TBSP_1, PRE_TOPC; clusters XREAL_0, EQREL_1, RELSET_1, ARYTM_3, STRUCT_0, SUBSET_1, FINSET_1, TBSP_1, MEMBERED, PARTFUN1; 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 number; definition cluster non negative (real number); 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,x,y be set 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_reflexive_in X & 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 number; 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 be real number 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 set 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 number 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 number 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 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}); 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 number 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 set holds x in it iff ex a being non negative (real number),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 number) 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 number, 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 number; 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 number 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 number, 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 set holds x in it iff ex a being non negative (real number),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 number) st a >= diameter [#]M & R = dist_toler(M,a)* holds Class R = {the carrier of M}; definition 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;

Back to top