:: Hierarchies and Classifications of Sets :: by Mariusz Giero :: :: Received December 28, 2001 :: Copyright (c) 2001-2012 Association of Mizar Users begin definition let A be RelStr ; attrA 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_:_ for A being RelStr holds ( A is with_superior iff ex x being Element of A st x is_superior_of the InternalRel of A ); definition let A be RelStr ; attrA 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_:_ for A being RelStr holds ( A is with_comparable_down iff 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 ) ); theorem Th1: :: TAXONOM2:1 for a being set holds ( not InclPoset {{a}} is empty & InclPoset {{a}} is reflexive & InclPoset {{a}} is transitive & InclPoset {{a}} is antisymmetric & InclPoset {{a}} is with_superior & InclPoset {{a}} is with_comparable_down ) proofend; registration cluster non empty strict reflexive transitive antisymmetric with_superior with_comparable_down for RelStr ; existence ex b1 being RelStr st ( not b1 is empty & b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_superior & b1 is with_comparable_down & b1 is strict ) proofend; end; definition mode Tree is with_superior with_comparable_down Poset; 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) proofend; theorem :: TAXONOM2:3 canceled; Th3: for X being non empty set for P being a_partition of X for x, y, z being set st x in P & y in P & z in x & z in y holds x = y by EQREL_1:70; 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 proofend; 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 proofend; begin definition let Y be set ; attrY 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_:_ for Y being set holds ( Y is hierarchic iff for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds x misses y ); registration cluster trivial -> hierarchic for set ; coherence for b1 being set st b1 is trivial holds b1 is hierarchic proofend; end; registration cluster non trivial hierarchic for set ; existence ex b1 being set st ( not b1 is trivial & b1 is hierarchic ) proofend; end; theorem Th6: :: TAXONOM2:6 {} is hierarchic proofend; theorem :: TAXONOM2:7 {{}} is hierarchic proofend; definition let Y be set ; mode Hierarchy of Y -> Subset-Family of Y means :Def4: :: TAXONOM2:def 4 it is hierarchic ; existence ex b1 being Subset-Family of Y st b1 is hierarchic proofend; end; :: deftheorem Def4 defines Hierarchy TAXONOM2:def_4_:_ for Y being set for b2 being Subset-Family of Y holds ( b2 is Hierarchy of Y iff b2 is hierarchic ); definition let Y be set ; attrY 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_:_ for Y being set holds ( Y is mutually-disjoint iff for x, y being set st x in Y & y in Y & x <> y holds x misses y ); Lm1: now__::_thesis:_for_x,_y_being_set_st_x_in_{{}}_&_y_in_{{}}_&_x_<>_y_holds_ x_misses_y let x, y be set ; ::_thesis: ( x in {{}} & y in {{}} & x <> y implies x misses y ) assume that A1: x in {{}} and A2: y in {{}} and A3: x <> y ; ::_thesis: x misses y x = {} by A1, TARSKI:def_1; hence x misses y by A2, A3, TARSKI:def_1; ::_thesis: verum end; registration let Y be set ; cluster mutually-disjoint for Element of bool (bool Y); existence ex b1 being Subset-Family of Y st b1 is mutually-disjoint proofend; end; theorem :: TAXONOM2:8 {} is mutually-disjoint proofend; theorem :: TAXONOM2:9 {{}} is mutually-disjoint by Def5, Lm1; theorem Th10: :: TAXONOM2:10 for a being set holds {a} is mutually-disjoint proofend; Lm2: now__::_thesis:_for_Y_being_set_ for_H_being_Hierarchy_of_Y_st_H_is_covering_holds_ 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_ union_B_=_Y let Y be set ; ::_thesis: for H being Hierarchy of Y st H is covering holds 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 union B = Y let H be Hierarchy of Y; ::_thesis: ( H is covering implies 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 union B = Y ) assume A1: H is covering ; ::_thesis: 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 union B = Y let B be mutually-disjoint Subset-Family of Y; ::_thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds B = C ) implies union B = Y ) 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: union B = Y Y c= union B proof let y be set ; :: according toTARSKI:def_3 ::_thesis: ( not y in Y or y in union B ) assume y in Y ; ::_thesis: y in union B 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:_y_in_union_B defpred S1[ set ] means $1 c= x; consider D being set such that A6: for a being set holds ( a in D iff ( a in B & S1[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 toTARSKI:def_3 ::_thesis: ( not s in {x} or s in H ) assume s in {x} ; ::_thesis: s in H hence s in H by A5, TARSKI:def_1; ::_thesis: verum end; assume A9: not y in union B ; ::_thesis: contradiction 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: ( p in B & not p in D & p <> x implies p misses x ) assume that A12: p in B and A13: not p in D and p <> x ; ::_thesis: p misses x 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: verum 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: ( p in (B \ D) \/ {x} & q in (B \ D) \/ {x} & p <> q implies p misses q ) assume that A16: p in (B \ D) \/ {x} and A17: q in (B \ D) \/ {x} and A18: p <> q ; ::_thesis: p misses q percases ( p in B \ D or p in {x} ) by A16, XBOOLE_0:def_3; supposeA19: p in B \ D ; ::_thesis: p misses q then A20: not p in D by XBOOLE_0:def_5; A21: p in B by A19, XBOOLE_0:def_5; percases ( q in B \ D or q in {x} ) by A17, XBOOLE_0:def_3; suppose q in B \ D ; ::_thesis: p misses q then q in B by XBOOLE_0:def_5; hence p misses q by A18, A21, Def5; ::_thesis: verum end; suppose q in {x} ; ::_thesis: p misses q then q = x by TARSKI:def_1; hence p misses q by A10, A18, A21, A20; ::_thesis: verum end; end; end; suppose p in {x} ; ::_thesis: p misses q then A22: p = x by TARSKI:def_1; percases ( q in B \ D or q in {x} ) by A17, XBOOLE_0:def_3; supposeA23: q in B \ D ; ::_thesis: p misses q 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: verum end; suppose q in {x} ; ::_thesis: p misses q hence p misses q by A18, A22, TARSKI:def_1; ::_thesis: verum end; end; end; end; 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 toTARSKI:def_3 ::_thesis: ( not s in union B or s in union ((B \ D) \/ {x}) ) assume s in union B ; ::_thesis: s in union ((B \ D) \/ {x}) then consider t being set such that A27: s in t and A28: t in B by TARSKI:def_4; percases ( t in D or not t in D ) ; suppose t in D ; ::_thesis: s in union ((B \ D) \/ {x}) then t c= x by A6; hence s in union ((B \ D) \/ {x}) by A25, A27, TARSKI:def_4; ::_thesis: verum end; suppose not t in D ; ::_thesis: s in union ((B \ D) \/ {x}) 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: verum end; end; 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: verum end; hence y in union B ; ::_thesis: verum end; hence union B = Y by XBOOLE_0:def_10; ::_thesis: verum end; Lm3: now__::_thesis:_for_Y_being_set_ for_H_being_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_ for_S1_being_Subset_of_Y_st_S1_in_B_holds_ S1_<>_{} let Y be set ; ::_thesis: for H being 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 for S1 being Subset of Y st S1 in B holds S1 <> {} let H be Hierarchy of Y; ::_thesis: 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 for S1 being Subset of Y st S1 in B holds S1 <> {} let B be mutually-disjoint Subset-Family of Y; ::_thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds B = C ) implies for S1 being Subset of Y st S1 in B holds S1 <> {} ) 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: for S1 being Subset of Y st S1 in B holds S1 <> {} let S1 be Subset of Y; ::_thesis: ( S1 in B implies S1 <> {} ) assume A3: S1 in B ; ::_thesis: S1 <> {} now__::_thesis:_not_S1_=_{} set C = B \ {{}}; assume A4: S1 = {} ; ::_thesis: contradiction A5: union B c= union (B \ {{}}) proof let x be set ; :: according toTARSKI:def_3 ::_thesis: ( not x in union B or x in union (B \ {{}}) ) assume x in union B ; ::_thesis: x in union (B \ {{}}) 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: verum end; A8: B \ {{}} is mutually-disjoint proof let x, y be set ; :: according toTAXONOM2:def_5 ::_thesis: ( x in B \ {{}} & y in B \ {{}} & x <> y implies x misses y ) assume that A9: x in B \ {{}} and A10: y in B \ {{}} and A11: x <> y ; ::_thesis: x misses y 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: verum 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: verum end; hence S1 <> {} ; ::_thesis: verum end; definition let Y be set ; let F be Subset-Family of Y; attrF 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_:_ for Y being set for F being Subset-Family of Y holds ( F is T_3 iff 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 ) ); theorem Th11: :: TAXONOM2:11 for Y being set for F being Subset-Family of Y st F = {} holds F is T_3 proofend; registration let Y be set ; cluster covering T_3 for Hierarchy of Y; existence ex b1 being Hierarchy of Y st ( b1 is covering & b1 is T_3 ) proofend; end; definition let Y be set ; let F be Subset-Family of Y; attrF 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_:_ for Y being set for F being Subset-Family of Y holds ( F is lower-bounded iff 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 ) ); 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 ) ) proofend; definition let Y be set ; let F be Subset-Family of Y; attrF 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_:_ for Y being set for F being Subset-Family of Y holds ( F is with_max's iff 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 ) ) ); begin 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 proofend; 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 proofend; 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 proofend; theorem Th16: :: TAXONOM2:16 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 & B c= C holds B = C ) holds B is a_partition of Y proofend; 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 ) proofend; Lm4: now__::_thesis:_for_x_being_non_empty_set_ for_y_being_set_st_x_c=_y_holds_ x_meets_y let x be non empty set ; ::_thesis: for y being set st x c= y holds x meets y A1: ex a being set st a in x by XBOOLE_0:def_1; let y be set ; ::_thesis: ( x c= y implies x meets y ) assume x c= y ; ::_thesis: x meets y hence x meets y by A1, XBOOLE_0:3; ::_thesis: verum 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 ) proofend; 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 ) ) proofend; 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 proofend;