:: Classes of Independent Partitions
:: by Andrzej Trybulec
::
:: Received February 14, 2001
:: Copyright (c) 2001 Association of Mizar Users

definition

let Y be non empty set ;
let G be non empty Subset of (PARTITIONS Y);
:: original: Element
redefine mode Element of G -> a_partition of Y;
coherence
for b₁ being Element of G holds b₁ is a_partition of Y

proof end;

end;

theorem Th1: :: PARTIT_2:1

for Y being non empty set holds '/\' ({} (PARTITIONS Y)) = %O Y

proof end;

theorem Th2: :: PARTIT_2:2

for Y being non empty set
for R, S being Equivalence_Relation of Y holds R \/ S c= R * S

proof end;

theorem Th3: :: PARTIT_2:3

for Y being non empty set
for R being Relation of Y holds R c= nabla Y

proof end;

theorem Th4: :: PARTIT_2:4

for Y being non empty set
for R being Equivalence_Relation of Y holds
( (nabla Y) * R = nabla Y & R * (nabla Y) = nabla Y )

proof end;

theorem Th5: :: PARTIT_2:5

for Y being non empty set
for P being a_partition of Y
for x, y being Element of Y holds
( [x,y] in ERl P iff x in EqClass y,P )

proof end;

theorem :: PARTIT_2:6

for Y being non empty set
for P, Q, R being a_partition of Y st ERl R = (ERl P) * (ERl Q) holds
for x, y being Element of Y holds
( x in EqClass y,R iff ex z being Element of Y st
( x in EqClass z,P & z in EqClass y,Q ) )

proof end;

theorem Th7: :: PARTIT_2:7

for R, S being Relation
for Y being set st R is_reflexive_in Y & S is_reflexive_in Y holds
R * S is_reflexive_in Y

proof end;

theorem Th8: :: PARTIT_2:8

for R being Relation
for Y being set st R is_reflexive_in Y holds
Y c= field R

proof end;

theorem :: PARTIT_2:9

for Y being set
for R being Relation of Y st R is_reflexive_in Y holds
Y = field R

proof end;

theorem :: PARTIT_2:10

for Y being non empty set
for R, S being Equivalence_Relation of Y st R * S = S * R holds
R * S is Equivalence_Relation of Y

proof end;

theorem Th11: :: PARTIT_2:11

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a

proof end;

theorem :: PARTIT_2:12

canceled;

theorem Th13: :: PARTIT_2:13

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
All a,P,G '<' All b,P,G

proof end;

theorem :: PARTIT_2:14

canceled;

theorem :: PARTIT_2:15

for Y being non empty set
for a, b being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P being a_partition of Y st a '<' b holds
Ex a,P,G '<' Ex b,P,G

proof end;

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))

proof end;

theorem Th16: :: PARTIT_2:16

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)) = (ERl ('/\' Q)) * (ERl ('/\' P))

proof end;

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

proof end;

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

proof end;

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

proof end;