TAXONOM2: Hierarchies and Classifications of Sets

definition

let A be RelStr ;

attr A is with_superior means :: TAXONOM2:def 1
ex x being Element of A st x is_superior_of the InternalRel of A;

end;

:: deftheorem defines with_superior TAXONOM2:def 1 :

definition

let A be RelStr ;

attr A is with_comparable_down means :Def2: :: TAXONOM2:def 2
for x, y being Element of A holds
( for z being Element of A holds
( not z <= x or not z <= y ) or x <= y or y <= x );

end;

:: deftheorem Def2 defines with_comparable_down TAXONOM2:def 2 :

registration

cluster non empty strict reflexive transitive antisymmetric with_superior with_comparable_down for RelStr ;

existence

proof end;

end;

theorem Th2: :: TAXONOM2:2

for X being non empty set
for EqR being Equivalence_Relation of X
for x, y, z being set st z in Class (EqR,x) & z in Class (EqR,y) holds
Class (EqR,x) = Class (EqR,y)

proof end;

theorem :: TAXONOM2:3

canceled;

theorem Th4: :: TAXONOM2:4

for X being non empty set
for C, x being set st C is Classification of X & x in union C holds
x c= X

proof end;

theorem :: TAXONOM2:5

for X being non empty set
for C being set st C is Strong_Classification of X holds
InclPoset (union C) is Tree

proof end;

definition

let Y be set ;

attr Y is hierarchic means :Def3: :: TAXONOM2:def 3
for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds
x misses y;

end;

:: deftheorem Def3 defines hierarchic TAXONOM2:def 3 :

registration

cluster trivial -> hierarchic for set ;

coherence

proof end;

end;

registration

cluster non trivial hierarchic for set ;

existence

proof end;

end;

theorem Th6: :: TAXONOM2:6

{} is hierarchic

proof end;

definition

let Y be set ;

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

existence

proof end;

end;

:: deftheorem Def4 defines Hierarchy TAXONOM2:def 4 :

definition

let Y be set ;

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

end;

:: deftheorem Def5 defines mutually-disjoint TAXONOM2:def 5 :

Lm1: now :: thesis:

let x, y be set ; :: thesis:
assume that
A1: x in {{}} and
A2: y in {{}} and
A3: x <> y ; :: thesis:
x = {} by A1, TARSKI:def 1;
hence x misses y by A2, A3, TARSKI:def 1; :: thesis:

end;

registration

let Y be set ;

cluster mutually-disjoint for Element of bool (bool Y);

existence

proof end;

end;

theorem Th10: :: TAXONOM2:10

for a being set holds {a} is mutually-disjoint

proof end;

Lm2: now :: thesis:

let Y be set ; :: thesis:
let H be Hierarchy of Y; :: thesis:
assume A1: H is covering ; :: thesis:
let B be mutually-disjoint Subset-Family of Y; :: thesis:
assume that
A2: B c= H and
A3: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ; :: thesis:
Y c= union B

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in Y ; :: thesis:
then y in union H by A1, ABIAN:4;
then consider x being set such that
A4: y in x and
A5: x in H by TARSKI:def 4;

now :: thesis:

defpred S₁[ set ] means $1 c= x;
consider D being set such that
A6: for a being set holds
( a in D iff ( a in B & S₁[a] ) ) from XBOOLE_0:sch 1();
set C = (B \ D) \/ {x};
A7: B \ D c= (B \ D) \/ {x} by XBOOLE_1:7;
A8: {x} c= H

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume s in {x} ; :: thesis:
hence s in H by A5, TARSKI:def 1; :: thesis:

end;

assume A9: not y in union B ; :: thesis:
A10: for p being set st p in B & not p in D & p <> x holds
p misses x

proof

A11: H is hierarchic by Def4;
let p be set ; :: thesis:
assume that
A12: p in B and
A13: not p in D and
p <> x ; :: thesis:
A14: not x c= p by A4, A9, A12, TARSKI:def 4;
not p c= x by A6, A12, A13;
hence p misses x by A2, A5, A12, A14, A11, Def3; :: thesis:

end;

A15: for p, q being set st p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q holds
p misses q

proof

let p, q be set ; :: thesis:
assume that
A16: p in (B \ D) \/ {x} and
A17: q in (B \ D) \/ {x} and
A18: p <> q ; :: thesis:

per cases by A16, XBOOLE_0:def 3;

suppose A19: p in B \ D ; :: thesis:

then A20: not p in D by XBOOLE_0:def 5;
A21: p in B by A19, XBOOLE_0:def 5;

per cases by A17, XBOOLE_0:def 3;

suppose q in B \ D ; :: thesis:

then q in B by XBOOLE_0:def 5;
hence p misses q by A18, A21, Def5; :: thesis:

end;

suppose q in {x} ; :: thesis:

then q = x by TARSKI:def 1;
hence p misses q by A10, A18, A21, A20; :: thesis:

end;

suppose p in {x} ; :: thesis:

then A22: p = x by TARSKI:def 1;

per cases by A17, XBOOLE_0:def 3;

suppose A23: q in B \ D ; :: thesis:

then A24: not q in D by XBOOLE_0:def 5;
q in B by A23, XBOOLE_0:def 5;
hence p misses q by A10, A18, A22, A24; :: thesis:

end;

suppose q in {x} ; :: thesis:

hence p misses q by A18, A22, TARSKI:def 1; :: thesis:

end;

x in {x} by TARSKI:def 1;
then A25: x in (B \ D) \/ {x} by XBOOLE_0:def 3;
A26: union B c= union ((B \ D) \/ {x})

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume s in union B ; :: thesis:
then consider t being set such that
A27: s in t and
A28: t in B by TARSKI:def 4;

per cases ;

suppose t in D ; :: thesis:

then t c= x by A6;
hence s in union ((B \ D) \/ {x}) by A25, A27, TARSKI:def 4; :: thesis:

end;

suppose not t in D ; :: thesis:

then t in B \ D by A28, XBOOLE_0:def 5;
hence s in union ((B \ D) \/ {x}) by A7, A27, TARSKI:def 4; :: thesis:

end;

A29: x in {x} by TARSKI:def 1;
B \ D c= B by XBOOLE_1:36;
then A30: B \ D c= H by A2, XBOOLE_1:1;
then (B \ D) \/ {x} c= H by A8, XBOOLE_1:8;
then (B \ D) \/ {x} is mutually-disjoint Subset-Family of Y by A15, Def5, XBOOLE_1:1;
then A31: B = (B \ D) \/ {x} by A3, A30, A8, A26, XBOOLE_1:8;
{x} c= (B \ D) \/ {x} by XBOOLE_1:7;
hence contradiction by A4, A9, A31, A29, TARSKI:def 4; :: thesis:

end;

hence y in union B ; :: thesis:

end;

hence union B = Y by XBOOLE_0:def 10; :: thesis:

end;

Lm3: now :: thesis:

let Y be set ; :: thesis:
let H be Hierarchy of Y; :: thesis:
let B be mutually-disjoint Subset-Family of Y; :: thesis:
assume that
A1: B c= H and
A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds
B = C ; :: thesis:
let S1 be Subset of Y; :: thesis:
assume A3: S1 in B ; :: thesis:

now :: thesis:

set C = B \ {{}};
assume A4: S1 = {} ; :: thesis:
A5: union B c= union (B \ {{}})

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union B ; :: thesis:
then consider y being set such that
A6: x in y and
A7: y in B by TARSKI:def 4;
not y in {{}} by A6, TARSKI:def 1;
then y in B \ {{}} by A7, XBOOLE_0:def 5;
hence x in union (B \ {{}}) by A6, TARSKI:def 4; :: thesis:

end;

A8: B \ {{}} is mutually-disjoint

proof

let x, y be set ; :: according to TAXONOM2:def 5 :: thesis:
assume that
A9: x in B \ {{}} and
A10: y in B \ {{}} and
A11: x <> y ; :: thesis:
A12: y in B by A10, XBOOLE_0:def 5;
x in B by A9, XBOOLE_0:def 5;
hence x misses y by A11, A12, Def5; :: thesis:

end;

B \ {{}} c= B by XBOOLE_1:36;
then B \ {{}} c= H by A1, XBOOLE_1:1;
then B = B \ {{}} by A2, A5, A8;
then not {} in {{}} by A3, A4, XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

hence S1 <> {} ; :: thesis:

end;

definition

let Y be set ;
let F be Subset-Family of Y;

attr F is T_3 means :Def6: :: TAXONOM2:def 6
for A being Subset of Y st A in F holds
for x being Element of Y st not x in A holds
ex B being Subset of Y st
( x in B & B in F & A misses B );

end;

:: deftheorem Def6 defines T_3 TAXONOM2:def 6 :

theorem Th11: :: TAXONOM2:11

for Y being set
for F being Subset-Family of Y st F = {} holds
F is T_3

proof end;

registration

let Y be set ;

cluster covering T_3 for Hierarchy of Y;

existence

proof end;

end;

definition

let Y be set ;
let F be Subset-Family of Y;

attr F is lower-bounded means :Def7: :: TAXONOM2:def 7
for B being set st B <> {} & B c= F & B is c=-linear holds
ex c being set st
( c in F & c c= meet B );

end;

:: deftheorem Def7 defines lower-bounded TAXONOM2:def 7 :

theorem Th12: :: TAXONOM2:12

for Y being set
for S1 being Subset of Y
for B being mutually-disjoint Subset-Family of Y st ( for b being 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 ) )

proof end;

definition

let Y be set ;
let F be Subset-Family of Y;

attr F is with_max's means :Def8: :: TAXONOM2:def 8
for S being Subset of Y st S in F holds
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;

:: deftheorem Def8 defines with_max's TAXONOM2:def 8 :

theorem :: TAXONOM2:13

for Y being set
for H being covering Hierarchy of Y st H is with_max's holds
ex P being a_partition of Y st P c= H

proof end;

theorem :: TAXONOM2:14

for Y being set
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

proof end;

theorem :: TAXONOM2:15

for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
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

proof end;

theorem Th16: :: TAXONOM2:16

proof end;

theorem Th17: :: TAXONOM2:17

for Y being set
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds
for A being Subset of Y st A in H holds
ex P being a_partition of Y st
( A in P & P c= H )

proof end;

Lm4: now :: thesis:

let x be non empty set ; :: thesis:
A1: ex a being set st a in x by XBOOLE_0:def 1;
let y be set ; :: thesis:
assume x c= y ; :: thesis:
hence x meets y by A1, XBOOLE_0:3; :: thesis:

end;

theorem Th18: :: TAXONOM2:18

for X, h being non empty set
for Pmin being a_partition of X
for hw being set st hw in Pmin & h c= hw holds
for PS being a_partition of X st h in PS & ( for x being set holds
( not x in PS or x c= hw or hw c= x or hw misses x ) ) holds
for PT being set st ( for a being set 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 )

proof end;

theorem Th19: :: TAXONOM2:19

for X, h being non empty set st h c= X holds
for Pmax being a_partition of X st ex hy being set st
( hy in Pmax & hy c= h ) & ( for x being set holds
( not x in Pmax or x c= h or h c= x or h misses x ) ) holds
for Pb being set st ( for x being set 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 holds
for hw being set st hw in Pmin & h c= hw holds
Pb \/ {h} is_finer_than Pmin ) )

proof end;

theorem :: TAXONOM2:20

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

proof end;