:: Classes of Independent Partitions
:: by Andrzej Trybulec
::
:: Received February 14, 2001
:: Copyright (c) 2001 Association of Mizar Users
theorem Th1: :: PARTIT_2:1
theorem Th2: :: PARTIT_2:2
theorem Th3: :: PARTIT_2:3
theorem Th4: :: PARTIT_2:4
theorem Th5: :: PARTIT_2:5
theorem :: PARTIT_2:6
theorem Th7: :: PARTIT_2:7
theorem Th8: :: PARTIT_2:8
theorem :: PARTIT_2:9
theorem :: PARTIT_2:10
theorem Th11: :: PARTIT_2:11
theorem :: PARTIT_2:12
canceled;
theorem Th13: :: PARTIT_2:13
theorem :: PARTIT_2:14
canceled;
theorem :: PARTIT_2:15
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: :: PARTIT_2:16
theorem Th17: :: PARTIT_2:17
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 :: PARTIT_2:18
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 :: PARTIT_2:19
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