begin
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem
begin
theorem Th11:
theorem
canceled;
theorem Th13:
theorem
canceled;
theorem
begin
Lm1:
for Y being non empty set
for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
theorem Th16:
theorem Th17:
for
Y being non
empty set for
a being
Element of
Funcs (
Y,
BOOLEAN)
for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
All (
(All (a,P,G)),
Q,
G)
= All (
(All (a,Q,G)),
P,
G)
theorem
for
Y being non
empty set for
a being
Element of
Funcs (
Y,
BOOLEAN)
for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
Ex (
(Ex (a,P,G)),
Q,
G)
= Ex (
(Ex (a,Q,G)),
P,
G)
theorem
for
Y being non
empty set for
a being
Element of
Funcs (
Y,
BOOLEAN)
for
G being
Subset of
(PARTITIONS Y) for
P,
Q being
a_partition of
Y st
G is
independent holds
Ex (
(All (a,P,G)),
Q,
G)
'<' All (
(Ex (a,Q,G)),
P,
G)
begin
:: deftheorem defines {} PARTIT_2:def 1 :
for A, B being set holds {} (A,B) = {} ;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def2 defines involutive PARTIT_2:def 2 :
for f being Function holds
( f is involutive iff for x being set st x in dom f holds
f . (f . x) = x );
:: deftheorem defines involutive PARTIT_2:def 3 :
for X being non empty set
for f being UnOp of X holds
( f is involutive iff for x being Element of X holds f . (f . x) = x );