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;