:: Lower Tolerance. {P}reliminaries to {W}roclaw Taxonomy
:: by Mariusz Giero and Roman Matuszewski
::
:: Received December 5, 2000
:: Copyright (c) 2000-2016 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;