:: Classes of Independent Partitions
:: by Andrzej Trybulec
::
:: Received February 14, 2001
:: Copyright (c) 2001-2021 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 b1 being Element of G holds b1 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 :: 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 )
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 Th9: :: 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 Function of Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a
proof end;

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)
proof end;

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

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)
proof end;

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)
proof end;

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)
proof end;

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;
proof end;
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
proof end;

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

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 & field R = X ) by Th9;

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
proof end;

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

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

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
proof end;

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

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
proof end;

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

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
proof end;

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

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
proof end;

:: 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 & b1 is asymmetric & b1 is transitive )
proof end;
end;

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

:: deftheorem 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 attr f 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 )
proof end;
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
proof end;
end;

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