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


begin

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 b1 being Element of G holds b1 is a_partition of Y
proofend;
end;

theorem Th1: :: PARTIT_2:1
for Y being non empty set holds '/\' ({} (PARTITIONS Y)) = %O Y
proofend;

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
proofend;

theorem :: PARTIT_2:3
for Y being non empty set
for R being Relation of Y holds R c= nabla Y ;

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

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

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

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
proofend;

theorem Th8: :: PARTIT_2:8
for R being Relation
for Y being set st R is_reflexive_in Y holds
Y c= field R
proofend;

theorem Th9: :: PARTIT_2:9
for Y being set
for R being Relation of Y st R is_reflexive_in Y holds
Y = field R
proofend;

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
proofend;

begin

theorem Th11: :: PARTIT_2:11
for Y being non empty set
for a, b being Function of Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a
proofend;

theorem Th12: :: PARTIT_2:12
for Y being non empty set
for a, b being Function of 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)
proofend;

theorem :: PARTIT_2:13
for Y being non empty set
for a, b being Function of 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)
proofend;

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 &amp; Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
proofend;

theorem Th14: :: PARTIT_2:14
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 &amp; Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) = (ERl ('/\' Q)) * (ERl ('/\' P))
proofend;

theorem Th15: :: PARTIT_2:15
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: PARTIT_2:16
for Y being non empty set
for a being Function of 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)
proofend;

theorem :: PARTIT_2:17
for Y being non empty set
for a being Function of 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)
proofend;

begin

notation
let A, B be set ;
synonym  [#] (A,B) for [:A,B:];
end;

definition
let A, B be set ;
func {} (A,B) ->  Relation of A,B equals :: PARTIT_2:def 1
 {} ;
correctness
coherence
{} is Relation of A,B;
by RELSET_1:12;
:: original:[#]
redefine func [#] (A,B) ->  Relation of A,B;
correctness
coherence
[#] (A,B) is Relation of A,B;
proofend;
end;

:: deftheorem  defines {} PARTIT_2:def_1_:_
 for A, B being set holds {} (A,B) = {} ;

registration
let A, B be set ;
cluster {} (A,B) ->  empty ;
coherence
 {} (A,B) is empty ;
end;

theorem :: PARTIT_2:18
for X being non empty set holds field (id X) = X
proofend;

theorem :: PARTIT_2:19
op1 = {[{},{}]}
proofend;

theorem :: PARTIT_2:20
for A, B being set holds field ({} (A,B)) = {} by RELAT_1:40;

theorem :: PARTIT_2:21
for X being non empty set
for R being Relation of X st R is_reflexive_in X holds
( R is reflexive &amp; field R = X )
proofend;

theorem :: PARTIT_2:22
for X being non empty set
for R being Relation of X st R is_symmetric_in X holds
R is symmetric
proofend;

theorem :: PARTIT_2:23
for X, S being non empty set
for R being Relation of X st R is symmetric holds
R is_symmetric_in S
proofend;

theorem :: PARTIT_2:24
for X, S being non empty set
for R being Relation of X st R is antisymmetric holds
R is_antisymmetric_in S
proofend;

theorem :: PARTIT_2:25
for X being non empty set
for R being Relation of X st R is_antisymmetric_in X holds
R is antisymmetric
proofend;

theorem :: PARTIT_2:26
for X, S being non empty set
for R being Relation of X st R is transitive holds
R is_transitive_in S
proofend;

theorem :: PARTIT_2:27
for X being non empty set
for R being Relation of X st R is_transitive_in X holds
R is transitive
proofend;

theorem :: PARTIT_2:28
for X, S being non empty set
for R being Relation of X st R is asymmetric holds
R is_asymmetric_in S
proofend;

theorem :: PARTIT_2:29
for X being non empty set
for R being Relation of X st R is_asymmetric_in X holds
R is asymmetric
proofend;

theorem :: PARTIT_2:30
for X, S being non empty set
for R being Relation of X st R is irreflexive &amp; field R c= S holds
R is_irreflexive_in S
proofend;

theorem :: PARTIT_2:31
for X being non empty set
for R being Relation of X st R is_irreflexive_in X holds
R is irreflexive
proofend;

:: Some existence conditions on non-empty relations
registration
cluster empty Relation-like  ->  irreflexive asymmetric transitive for set ;
coherence
 for b1 being Relation st b1 is empty holds
( b1 is irreflexive &amp; b1 is asymmetric &amp; b1 is transitive )
proofend;
end;

:: Double negation property of the internal Complement
definition
let f be Function;
attrf is involutive  means :Def2: :: PARTIT_2:def 2
 for x being set st x in dom f holds
f . (f . x) = x;
end;

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

definition
let X be non empty set ;
let f be UnOp of X;
:: original:involutive
redefine attrf is involutive  means :: PARTIT_2:def 3
 for x being Element of X holds f . (f . x) = x;
compatibility
 ( f is involutive iff for x being Element of X holds f . (f . x) = x )
proofend;
end;

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

registration
cluster op1  ->  involutive for Function;
coherence
 for b1 being Function st b1 = op1 holds
b1 is involutive
proofend;
end;

registration
let X be set ;
cluster id X ->  involutive ;
coherence
 id X is involutive
proofend;
end;