The abstract of the Mizar article:

Hierarchies and Classifications of Sets

by

Mariusz Giero

Received December 28, 2001

MML identifier: TAXONOM2

[ Mizar article, MML identifier index ]

environ

 vocabulary TAXONOM2, TAXONOM1, ABIAN, EQREL_1, TARSKI, PUA2MSS1, REALSET1,
      SETFAM_1, YELLOW_1, WELLORD2, HAHNBAN, ZFMISC_1, BOOLE, ORDERS_1,
      RELAT_1, RELAT_2, PARTIT1, ORDERS_2, LATTICES, TREES_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, REALSET1, RELAT_1,
      ORDINAL1, RELSET_1, STRUCT_0, ORDERS_1, EQREL_1, ABIAN, PARTIT1,
      ORDERS_2, YELLOW_1, TAXONOM1;
 constructors ORDERS_2, PUA2MSS1, TAXONOM1, ABIAN, YELLOW_1;
 clusters SUBSET_1, RELSET_1, PARTIT1, YELLOW_1, XBOOLE_0, PARTFUN1;
 requirements BOOLE, SUBSET;


begin

reserve A for RelStr;
reserve X for non empty set;
reserve PX,PY,PZ,Y,a,b,c,x,y for set;
reserve S1,S2 for Subset of Y;

definition let A;
  attr A is with_superior means
:: TAXONOM2:def 1
    ex x be Element of A st x is_superior_of the InternalRel of A;
end;

definition let A;
  attr A is with_comparable_down means
:: TAXONOM2:def 2
  for x,y be Element of A holds
     (ex z be Element of A st z <= x & z <= y) implies
     (x <= y or y <= x);
end;

theorem :: TAXONOM2:1
for a being set holds
     InclPoset {{a}} is non empty reflexive transitive antisymmetric
                      with_superior with_comparable_down;

definition
 cluster non empty reflexive transitive antisymmetric with_superior
         with_comparable_down strict RelStr;
end;

definition
 mode Tree is with_superior with_comparable_down Poset;
end;

theorem :: TAXONOM2:2
for EqR being Equivalence_Relation of X,
   x,y,z be set holds
   z in Class(EqR,x) & z in Class(EqR,y) implies Class(EqR,x) = Class(EqR,y);

theorem :: TAXONOM2:3
for P being a_partition of X,
    x,y,z being set st x in P & y in P & z in x & z in y holds x = y;

theorem :: TAXONOM2:4
for C,x be set st C is Classification of X & x in union C
        holds x c= X;

theorem :: TAXONOM2:5
    for C being set st
  C is Strong_Classification of X
  holds InclPoset union C is Tree;

begin

definition let Y;
  attr Y is hierarchic means
:: TAXONOM2:def 3
for x,y be set st (x in Y & y in Y) holds (x c= y or y c= x or x misses y);
end;

definition
  cluster trivial -> hierarchic set;
end;

definition
  cluster non trivial hierarchic set;
end;

theorem :: TAXONOM2:6
{} is hierarchic;

theorem :: TAXONOM2:7
  {{}} is hierarchic;

definition let Y;
  mode Hierarchy of Y -> Subset-Family of Y means
:: TAXONOM2:def 4
  it is hierarchic;
end;

definition let Y;
  attr Y is mutually-disjoint means
:: TAXONOM2:def 5
  for x,y be set st x in Y & y in Y & x <> y holds x misses y;
end;

definition let Y;
  cluster mutually-disjoint Subset-Family of Y;
end;

theorem :: TAXONOM2:8
  {} is mutually-disjoint;

theorem :: TAXONOM2:9
  {{}} is mutually-disjoint;

theorem :: TAXONOM2:10
{a} is mutually-disjoint;

definition let Y; let F be Subset-Family of Y;
 attr F is T_3 means
:: TAXONOM2:def 6
 for A be Subset of Y st A in F
 for x be Element of Y st not x in A
   ex B be Subset of Y st x in B & B in F & A misses B;
end;

theorem :: TAXONOM2:11
for F be Subset-Family of Y st F = {} holds F is T_3;

definition let Y;
 cluster covering T_3 Hierarchy of Y;
end;

definition let Y; let F be Subset-Family of Y;
 attr F is lower-bounded means
:: TAXONOM2:def 7

  for B being set st
      B <> {} & B c= F & B is c=-linear ex c st (c in F & c c= meet B);
end;

theorem :: TAXONOM2:12
 for B being mutually-disjoint Subset-Family of Y
     st for b be set st b in B holds S1 misses b & Y <> {}
 holds B \/ {S1} is mutually-disjoint Subset-Family of Y
       & (S1 <> {} implies union (B \/ {S1}) <> union B);

definition let Y; let F be Subset-Family of Y;
 attr F is with_max's means
:: TAXONOM2:def 8

  for S being Subset of Y st S in F
   ex T being Subset of Y st S c= T & T in F &
    for V being Subset of Y st T c= V & V in F holds V = Y;
end;

begin

theorem :: TAXONOM2:13
    for H being covering Hierarchy of Y st H is with_max's
      ex P being a_partition of Y st P c= H;

theorem :: TAXONOM2:14
   for H being covering Hierarchy of Y
 for B being mutually-disjoint Subset-Family of Y st
         B c= H &
   for C  being mutually-disjoint Subset-Family of Y st
     C c= H & union B c= union C holds B = C
 holds B is a_partition of Y;

theorem :: TAXONOM2:15
   for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H
 for A being Subset of Y
 for B being mutually-disjoint Subset-Family of Y st
        A in B & B c= H &
   for C  being mutually-disjoint Subset-Family of Y st
     A in C & C c= H & union B c= union C holds union B = union C
 holds B is a_partition of Y;

theorem :: TAXONOM2:16
 for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H
 for A being Subset of Y
 for B being mutually-disjoint Subset-Family of Y st
        A in B & B c= H &
   for C  being mutually-disjoint Subset-Family of Y st
     A in C & C c= H & B c= C holds B = C
 holds B is a_partition of Y;

theorem :: TAXONOM2:17
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H
for A being Subset of Y st A in H
      ex P being a_partition of Y st A in P & P c= H;

theorem :: TAXONOM2:18
for h being non empty set
for Pmin being a_partition of X
for hw being set st hw in Pmin & h c= hw
for PS being a_partition of X st h in PS &
         for x st x in PS holds (x c= hw or hw c= x or hw misses x)
for PT be set st (for a holds a in PT iff a in PS & a c= hw)
holds PT \/ (Pmin \ {hw}) is a_partition of X &
      PT \/ (Pmin \ {hw}) is_finer_than Pmin;

theorem :: TAXONOM2:19
for h being non empty set st h c= X
for Pmax being a_partition of X st
  ( (ex hy be set st hy in Pmax & hy c= h) &
   for x st x in Pmax holds (x c= h or h c= x or h misses x))
for Pb be set st
    (for x holds x in Pb iff (x in Pmax & x misses h))
holds Pb \/ {h} is a_partition of X &
      Pmax is_finer_than (Pb \/ {h})&
      (for Pmin being a_partition of X st Pmax is_finer_than Pmin
       for hw being set st hw in Pmin & h c= hw holds
       (Pb \/ {h}) is_finer_than Pmin);

theorem :: TAXONOM2:20
  for H being covering T_3 Hierarchy of X st H is lower-bounded & not {} in H &
    (for C1 be set st
           (C1 <> {} & C1 c= PARTITIONS(X) &
           (for P1,P2 be set st P1 in C1 & P2 in C1 holds
                P1 is_finer_than P2 or P2 is_finer_than P1)) holds
        (ex PX,PY st (PX in C1 & PY in C1
         & for PZ st PZ in C1 holds
           PZ is_finer_than PY & PX is_finer_than PZ)))
    ex C being Classification of X st union C = H;