:: Hierarchies and Classifications of Sets
::  by Mariusz Giero
::
:: Received December 28, 2001
:: Copyright (c) 2001-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 ORDERS_2, XBOOLE_0, SUBSET_1, ORDERS_1, XXREAL_0, YELLOW_1,
      RELAT_2, WELLORD2, RELAT_1, TARSKI, TREES_1, EQREL_1, TAXONOM1, SETFAM_1,
      ZFMISC_1, ABIAN, PRE_TOPC, LATTICES, ORDINAL1, PARTIT1, TAXONOM2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
      RELSET_1, STRUCT_0, ORDERS_2, EQREL_1, ABIAN, PARTIT1, ORDERS_1,
      YELLOW_1, TAXONOM1;
 constructors ABIAN, YELLOW_1, TAXONOM1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, EQREL_1, YELLOW_1;
 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;

registration
  cluster non empty reflexive transitive antisymmetric with_superior
    with_comparable_down strict for 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);

::$CT


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;

registration
  cluster trivial -> hierarchic for set;
end;

registration
  cluster non trivial hierarchic for 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;

registration
  let Y;
  cluster mutually-disjoint for 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;

registration
  let Y;
  cluster covering T_3 for 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;