:: 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 b_{1} being Element of G holds b_{1} is a_partition of Y

end;
let G be non empty Subset of (PARTITIONS Y);

:: original: Element

redefine mode Element of G -> a_partition of Y;

coherence

for b

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 )

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

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

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

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

for R, S being Equivalence_Relation of Y st R * S = S * R holds

R * S is Equivalence_Relation of Y

proof end;

begin

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)

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)

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;

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

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

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

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)

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)

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;

begin

definition

let A, B be set ;

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;

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

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 )

for R being Relation of X st R is_reflexive_in X holds

( R is reflexive & field R = X )

proof end;

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

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

for R being Relation of X st R is_antisymmetric_in X holds

R is antisymmetric

proof end;

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

for R being Relation of X st R is transitive holds

R is_transitive_in S

proof end;

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

for R being Relation of X st R is asymmetric holds

R is_asymmetric_in S

proof end;

theorem :: PARTIT_2:30

for X, S being non empty set

for R being Relation of X st R is irreflexive & field R c= S holds

R is_irreflexive_in S

for R being Relation of X st R is irreflexive & field R c= S holds

R is_irreflexive_in S

proof end;

:: Some existence conditions on non-empty relations

registration

coherence

for b_{1} being Relation st b_{1} is empty holds

( b_{1} is irreflexive & b_{1} is asymmetric & b_{1} is transitive )

end;
for b

( b

proof end;

:: Double negation property of the internal Complement

definition

let f be Function;

end;
attr f is involutive means :Def2: :: PARTIT_2:def 2

for x being set st x in dom f holds

f . (f . x) = x;

for x being set st x in dom f holds

f . (f . x) = x;

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

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;

( f is involutive iff for x being Element of X holds f . (f . x) = x )

end;
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 redefine attr f is involutive means :: PARTIT_2:def 3

for x being Element of X holds f . (f . x) = x;

( f is involutive iff for x being Element of X holds f . (f . x) = x )

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

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

registration
end;