:: Hierarchies and Classifications of Sets
:: by Mariusz Giero
::
:: Received December 28, 2001
:: Copyright (c) 2001 Association of Mizar Users
:: deftheorem defines with_superior TAXONOM2:def 1 :
:: deftheorem Def2 defines with_comparable_down TAXONOM2:def 2 :
theorem Th1: :: TAXONOM2:1
theorem Th2: :: TAXONOM2:2
theorem Th3: :: TAXONOM2:3
theorem Th4: :: TAXONOM2:4
theorem :: TAXONOM2:5
:: deftheorem Def3 defines hierarchic TAXONOM2:def 3 :
theorem Th6: :: TAXONOM2:6
theorem :: TAXONOM2:7
:: deftheorem Def4 defines Hierarchy TAXONOM2:def 4 :
:: deftheorem Def5 defines mutually-disjoint TAXONOM2:def 5 :
theorem :: TAXONOM2:8
theorem :: TAXONOM2:9
theorem Th10: :: TAXONOM2:10
Lm2:
now
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 = Ylet 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 = Ylet 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 to TARSKI: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
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
assume A9:
not
y in union B
;
:: thesis: contradictionA10:
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
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})
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;
:: deftheorem Def6 defines T_3 TAXONOM2:def 6 :
theorem Th11: :: TAXONOM2:11
:: deftheorem Def7 defines lower-bounded TAXONOM2:def 7 :
theorem Th12: :: TAXONOM2:12
:: deftheorem Def8 defines with_max's TAXONOM2:def 8 :
theorem :: TAXONOM2:13
theorem :: TAXONOM2:14
theorem :: TAXONOM2:15
theorem Th16: :: TAXONOM2:16
theorem Th17: :: TAXONOM2:17
theorem Th18: :: TAXONOM2:18
theorem Th19: :: TAXONOM2:19
theorem :: TAXONOM2:20