partit_2.miz
begin
reserve Y for non
empty
set,
a for
Function of Y,
BOOLEAN ,
G for
Subset of (
PARTITIONS Y),
P,Q for
a_partition of Y;
definition
let Y be non
empty
set, G be non
empty
Subset of (
PARTITIONS Y);
:: original:
Element
redefine
mode
Element of G ->
a_partition of Y ;
coherence
proof
let p be
Element of G;
thus thesis by
PARTIT1:def 3;
end;
end
theorem ::
PARTIT_2:1
Th1: (
'/\' (
{} (
PARTITIONS Y)))
= (
%O Y)
proof
for x be
set holds x
in (
%O Y) iff ex h be
Function, F be
Subset-Family of Y st (
dom h)
= (
{} (
PARTITIONS Y)) & (
rng h)
= F & (for d be
set st d
in (
{} (
PARTITIONS Y)) holds (h
. d)
in d) & x
= (
Intersect F) & x
<>
{}
proof
let x be
set;
hereby
reconsider h =
{} as
Function;
assume x
in (
%O Y);
then
A1: x
in
{Y} by
PARTIT1:def 8;
take h, F = (
{} (
bool Y));
thus (
dom h)
= (
{} (
PARTITIONS Y));
thus (
rng h)
= F;
thus for d be
set st d
in (
{} (
PARTITIONS Y)) holds (h
. d)
in d;
x
= Y by
A1,
TARSKI:def 1;
hence x
= (
Intersect F) by
SETFAM_1:def 9;
thus x
<>
{} by
A1,
TARSKI:def 1;
end;
given h be
Function, F be
Subset-Family of Y such that
A2: (
dom h)
= (
{} (
PARTITIONS Y)) & (
rng h)
= F and for d be
set st d
in (
{} (
PARTITIONS Y)) holds (h
. d)
in d and
A3: x
= (
Intersect F) and x
<>
{} ;
F
=
{} by
A2,
RELAT_1: 42;
then x
= Y by
A3,
SETFAM_1:def 9;
then x
in
{Y} by
TARSKI:def 1;
hence thesis by
PARTIT1:def 8;
end;
hence thesis by
BVFUNC_2:def 1;
end;
theorem ::
PARTIT_2:2
Th2: for R,S be
Equivalence_Relation of Y holds (R
\/ S)
c= (R
* S)
proof
let R,S be
Equivalence_Relation of Y;
let x,y be
Element of Y;
assume
A1:
[x, y]
in (R
\/ S);
per cases by
A1,
XBOOLE_0:def 3;
suppose
A2:
[x, y]
in R;
[y, y]
in S by
EQREL_1: 5;
hence thesis by
A2,
RELAT_1:def 8;
end;
suppose
A3:
[x, y]
in S;
[x, x]
in R by
EQREL_1: 5;
hence thesis by
A3,
RELAT_1:def 8;
end;
end;
theorem ::
PARTIT_2:3
for R be
Relation of Y holds R
c= (
nabla Y);
theorem ::
PARTIT_2:4
Th4: for R be
Equivalence_Relation of Y holds ((
nabla Y)
* R)
= (
nabla Y) & (R
* (
nabla Y))
= (
nabla Y)
proof
let R be
Equivalence_Relation of Y;
((
nabla Y)
\/ R)
c= ((
nabla Y)
* R) by
Th2;
then (
nabla Y)
c= ((
nabla Y)
* R) by
EQREL_1: 1;
hence ((
nabla Y)
* R)
= (
nabla Y);
((
nabla Y)
\/ R)
c= (R
* (
nabla Y)) by
Th2;
then (
nabla Y)
c= (R
* (
nabla Y)) by
EQREL_1: 1;
hence thesis;
end;
theorem ::
PARTIT_2:5
Th5: for P be
a_partition of Y, x,y be
Element of Y holds
[x, y]
in (
ERl P) iff x
in (
EqClass (y,P))
proof
let P be
a_partition of Y, x,y be
Element of Y;
hereby
assume
[x, y]
in (
ERl P);
then ex A be
Subset of Y st A
in P & x
in A & y
in A by
PARTIT1:def 6;
hence x
in (
EqClass (y,P)) by
EQREL_1:def 6;
end;
y
in (
EqClass (y,P)) by
EQREL_1:def 6;
hence thesis by
PARTIT1:def 6;
end;
theorem ::
PARTIT_2:6
for P,Q,R be
a_partition of Y st (
ERl R)
= ((
ERl P)
* (
ERl Q)) holds for x,y be
Element of Y holds x
in (
EqClass (y,R)) iff ex z be
Element of Y st x
in (
EqClass (z,P)) & z
in (
EqClass (y,Q))
proof
let P,Q,R be
a_partition of Y such that
A1: (
ERl R)
= ((
ERl P)
* (
ERl Q));
let x,y be
Element of Y;
hereby
assume x
in (
EqClass (y,R));
then
[x, y]
in (
ERl R) by
Th5;
then
consider z be
Element of Y such that
A2:
[x, z]
in (
ERl P) and
A3:
[z, y]
in (
ERl Q) by
A1,
RELSET_1: 28;
take z;
thus x
in (
EqClass (z,P)) by
A2,
Th5;
thus z
in (
EqClass (y,Q)) by
A3,
Th5;
end;
given z be
Element of Y such that
A4: x
in (
EqClass (z,P)) & z
in (
EqClass (y,Q));
[x, z]
in (
ERl P) &
[z, y]
in (
ERl Q) by
A4,
Th5;
then
[x, y]
in (
ERl R) by
A1,
RELAT_1:def 8;
hence thesis by
Th5;
end;
theorem ::
PARTIT_2:7
Th7: for R,S be
Relation, Y be
set st R
is_reflexive_in Y & S
is_reflexive_in Y holds (R
* S)
is_reflexive_in Y
proof
let R,S be
Relation, Y be
set such that
A1: R
is_reflexive_in Y & S
is_reflexive_in Y;
let x be
object;
assume x
in Y;
then
[x, x]
in R &
[x, x]
in S by
A1;
hence thesis by
RELAT_1:def 8;
end;
theorem ::
PARTIT_2:8
Th8: for R be
Relation, Y be
set st R
is_reflexive_in Y holds Y
c= (
field R)
proof
let R be
Relation, Y be
set such that
A1: R
is_reflexive_in Y;
let x be
object;
assume x
in Y;
then
[x, x]
in R by
A1;
hence thesis by
RELAT_1: 15;
end;
theorem ::
PARTIT_2:9
Th9: for Y be
set, R be
Relation of Y st R
is_reflexive_in Y holds Y
= (
field R)
proof
let Y be
set, R be
Relation of Y;
assume R
is_reflexive_in Y;
hence Y
c= (
field R) by
Th8;
(
field R)
c= (Y
\/ Y) by
RELSET_1: 8;
hence thesis;
end;
theorem ::
PARTIT_2:10
for R,S be
Equivalence_Relation of Y st (R
* S)
= (S
* R) holds (R
* S) is
Equivalence_Relation of Y
proof
let R,S be
Equivalence_Relation of Y such that
A1: (R
* S)
= (S
* R);
A2: (
field S)
= Y by
ORDERS_1: 12;
then
A3: S
is_reflexive_in Y by
RELAT_2:def 9;
A4: (
field R)
= Y by
ORDERS_1: 12;
then R
is_reflexive_in Y by
RELAT_2:def 9;
then (R
* S)
is_reflexive_in Y by
A3,
Th7;
then
A5: (
field (R
* S))
= Y & (
dom (R
* S))
= Y by
ORDERS_1: 13;
A6: (R
* S)
is_symmetric_in Y
proof
A7: S
is_symmetric_in Y by
A2,
RELAT_2:def 11;
let x,y be
object such that
A8: x
in Y and
A9: y
in Y;
assume
[x, y]
in (R
* S);
then
consider z be
object such that
A10:
[x, z]
in R and
A11:
[z, y]
in S by
RELAT_1:def 8;
z
in (
field S) by
A11,
RELAT_1: 15;
then
A12:
[y, z]
in S by
A2,
A7,
A9,
A11;
A13: R
is_symmetric_in Y by
A4,
RELAT_2:def 11;
z
in (
field R) by
A10,
RELAT_1: 15;
then
[z, x]
in R by
A4,
A13,
A8,
A10;
hence thesis by
A1,
A12,
RELAT_1:def 8;
end;
A14: (R
* R)
c= R & (S
* S)
c= S by
RELAT_2: 27;
((R
* S)
* (R
* S))
= (((R
* S)
* R)
* S) by
RELAT_1: 36
.= ((R
* (R
* S))
* S) by
A1,
RELAT_1: 36
.= (((R
* R)
* S)
* S) by
RELAT_1: 36
.= ((R
* R)
* (S
* S)) by
RELAT_1: 36;
then ((R
* S)
* (R
* S))
c= (R
* S) by
A14,
RELAT_1: 31;
hence thesis by
A5,
A6,
PARTFUN1:def 2,
RELAT_2: 27,
RELAT_2:def 11;
end;
begin
theorem ::
PARTIT_2:11
Th11: for a,b be
Function of Y,
BOOLEAN st a
'<' b holds (
'not' b)
'<' (
'not' a)
proof
let a,b be
Function of Y,
BOOLEAN such that
A1: a
'<' b;
let x be
Element of Y;
assume
A2: ((
'not' b)
. x)
=
TRUE ;
(b
. x)
= ((
'not' (
'not' b))
. x)
.= (
'not'
TRUE ) by
A2,
MARGREL1:def 19
.=
FALSE ;
then (a
. x)
<>
TRUE by
A1;
then (a
. x)
=
FALSE by
XBOOLEAN:def 3;
hence ((
'not' a)
. x)
= (
'not'
FALSE ) by
MARGREL1:def 19
.=
TRUE ;
end;
theorem ::
PARTIT_2:12
Th12: for a,b be
Function of Y,
BOOLEAN , G be
Subset of (
PARTITIONS Y), P be
a_partition of Y st a
'<' b holds (
All (a,P,G))
'<' (
All (b,P,G))
proof
let a,b be
Function of Y,
BOOLEAN , G be
Subset of (
PARTITIONS Y), P be
a_partition of Y such that
A1: a
'<' b;
let x be
Element of Y;
assume
A2: ((
All (a,P,G))
. x)
=
TRUE ;
A3: (
All (a,P,G))
= (
B_INF (a,(
CompF (P,G)))) by
BVFUNC_2:def 9;
A4: for y be
Element of Y st y
in (
EqClass (x,(
CompF (P,G)))) holds (b
. y)
=
TRUE
proof
let y be
Element of Y;
assume y
in (
EqClass (x,(
CompF (P,G))));
then (a
. y)
=
TRUE by
A3,
A2,
BVFUNC_1:def 16;
hence thesis by
A1;
end;
(
All (b,P,G))
= (
B_INF (b,(
CompF (P,G)))) by
BVFUNC_2:def 9;
hence thesis by
A4,
BVFUNC_1:def 16;
end;
theorem ::
PARTIT_2:13
for a,b be
Function of Y,
BOOLEAN , G be
Subset of (
PARTITIONS Y), P be
a_partition of Y st a
'<' b holds (
Ex (a,P,G))
'<' (
Ex (b,P,G))
proof
let a,b be
Function of Y,
BOOLEAN , G be
Subset of (
PARTITIONS Y), P be
a_partition of Y;
A1: (
Ex (b,P,G))
= (
Ex ((
'not' (
'not' b)),P,G))
.= (
'not' (
All ((
'not' b),P,G))) by
BVFUNC_2: 18;
assume a
'<' b;
then (
'not' b)
'<' (
'not' a) by
Th11;
then
A2: (
All ((
'not' b),P,G))
'<' (
All ((
'not' a),P,G)) by
Th12;
(
Ex (a,P,G))
= (
Ex ((
'not' (
'not' a)),P,G))
.= (
'not' (
All ((
'not' a),P,G))) by
BVFUNC_2: 18;
hence thesis by
A1,
A2,
Th11;
end;
begin
Lm1: G is
independent implies for P,Q be
Subset of (
PARTITIONS Y) st P
c= G & Q
c= G holds ((
ERl (
'/\' P))
* (
ERl (
'/\' Q)))
c= ((
ERl (
'/\' Q))
* (
ERl (
'/\' P)))
proof
assume
A1: G is
independent;
let P,Q be
Subset of (
PARTITIONS Y) such that
A2: P
c= G and
A3: Q
c= G;
per cases ;
suppose P
=
{} ;
then P
= (
{} (
PARTITIONS Y));
then ((
ERl (
'/\' Q))
* (
ERl (
'/\' P)))
= ((
ERl (
'/\' Q))
* (
ERl (
%O Y))) by
Th1
.= ((
ERl (
'/\' Q))
* (
nabla Y)) by
PARTIT1: 33
.= (
nabla Y) by
Th4;
hence thesis;
end;
suppose Q
=
{} ;
then Q
= (
{} (
PARTITIONS Y));
then ((
ERl (
'/\' Q))
* (
ERl (
'/\' P)))
= ((
ERl (
%O Y))
* (
ERl (
'/\' P))) by
Th1
.= ((
nabla Y)
* (
ERl (
'/\' P))) by
PARTIT1: 33
.= (
nabla Y) by
Th4;
hence thesis;
end;
suppose
A4: P
<>
{} & Q
<>
{} ;
then
reconsider G9 = G as non
empty
Subset of (
PARTITIONS Y) by
A2;
let x,y be
Element of Y;
assume
[x, y]
in ((
ERl (
'/\' P))
* (
ERl (
'/\' Q)));
then
consider z be
Element of Y such that
A5:
[x, z]
in (
ERl (
'/\' P)) and
A6:
[z, y]
in (
ERl (
'/\' Q)) by
RELSET_1: 28;
consider A be
Subset of Y such that
A7: A
in (
'/\' P) and
A8: x
in A and
A9: z
in A by
A5,
PARTIT1:def 6;
consider B be
Subset of Y such that
A10: B
in (
'/\' Q) and
A11: z
in B and
A12: y
in B by
A6,
PARTIT1:def 6;
consider hQ be
Function, FQ be
Subset-Family of Y such that
A13: (
dom hQ)
= Q & (
rng hQ)
= FQ and
A14: for d be
set st d
in Q holds (hQ
. d)
in d and
A15: B
= (
Intersect FQ) and B
<>
{} by
A10,
BVFUNC_2:def 1;
consider hP be
Function, FP be
Subset-Family of Y such that
A16: (
dom hP)
= P & (
rng hP)
= FP and
A17: for d be
set st d
in P holds (hP
. d)
in d and
A18: A
= (
Intersect FP) and A
<>
{} by
A7,
BVFUNC_2:def 1;
reconsider P, Q as non
empty
Subset of (
PARTITIONS Y) by
A4;
deffunc
P(
Element of P) = (
EqClass (y,$1));
consider hP9 be
Function of P, (
bool Y) such that
A19: for p be
Element of P holds (hP9
. p)
=
P(p) from
FUNCT_2:sch 4;
deffunc
Q(
Element of Q) = (
EqClass (x,$1));
consider hQ9 be
Function of Q, (
bool Y) such that
A20: for p be
Element of Q holds (hQ9
. p)
=
Q(p) from
FUNCT_2:sch 4;
deffunc
P(
set) = $1;
A21: for d be
Element of G9 holds (
bool Y)
meets
P(d)
proof
let d be
Element of G9;
d
meets d;
hence (
bool Y)
meets d by
XBOOLE_1: 63;
end;
consider h9 be
Function of G9, (
bool Y) such that
A22: for d be
Element of G9 holds (h9
. d)
in
P(d) from
FUNCT_2:sch 10(
A21);
set h = ((h9
+* hP9)
+* hQ9);
A23: (
dom hQ9)
= Q by
FUNCT_2:def 1;
A24: (
dom hP9)
= P by
FUNCT_2:def 1;
A25: for d be
set st d
in P holds (h
. d)
= (hP9
. d)
proof
let d be
set;
assume
A26: d
in P;
then
reconsider d9 = d as
Element of P;
per cases ;
suppose
A27: d
in Q;
then
A28: (hQ
. d)
in FQ by
A13,
FUNCT_1:def 3;
then
A29: y
in (hQ
. d) by
A12,
A15,
SETFAM_1: 43;
A30: z
in (hQ
. d) by
A11,
A15,
A28,
SETFAM_1: 43;
A31: (hQ
. d)
in d by
A14,
A27;
A32: (hP
. d)
in FP by
A16,
A26,
FUNCT_1:def 3;
then
A33: x
in (hP
. d) by
A8,
A18,
SETFAM_1: 43;
A34: z
in (hP
. d) by
A9,
A18,
A32,
SETFAM_1: 43;
A35: (hP
. d)
in d by
A17,
A26;
thus (h
. d)
= (hQ9
. d) by
A23,
A27,
FUNCT_4: 13
.= (
EqClass (x,d9)) by
A20,
A27
.= (hP
. d) by
A35,
A33,
EQREL_1:def 6
.= (
EqClass (z,d9)) by
A35,
A34,
EQREL_1:def 6
.= (hQ
. d) by
A31,
A30,
EQREL_1:def 6
.= (
EqClass (y,d9)) by
A31,
A29,
EQREL_1:def 6
.= (hP9
. d) by
A19;
end;
suppose not d
in Q;
hence (h
. d)
= ((h9
+* hP9)
. d) by
A23,
FUNCT_4: 11
.= (hP9
. d) by
A24,
A26,
FUNCT_4: 13;
end;
end;
reconsider FP9 = (
rng hP9), FQ9 = (
rng hQ9) as
Subset-Family of Y;
set A9 = (
Intersect FP9), B9 = (
Intersect FQ9);
for a be
set st a
in FP9 holds y
in a
proof
let a be
set;
assume a
in FP9;
then
consider b be
object such that
A36: b
in (
dom hP9) and
A37: (hP9
. b)
= a by
FUNCT_1:def 3;
reconsider b as
Element of P by
A36;
a
= (
EqClass (y,b)) by
A19,
A37;
hence thesis by
EQREL_1:def 6;
end;
then
A38: y
in A9 by
SETFAM_1: 43;
for a be
set st a
in FQ9 holds x
in a
proof
let a be
set;
assume a
in FQ9;
then
consider b be
object such that
A39: b
in (
dom hQ9) and
A40: (hQ9
. b)
= a by
FUNCT_1:def 3;
reconsider b as
Element of Q by
A39;
a
= (
EqClass (x,b)) by
A20,
A40;
hence thesis by
EQREL_1:def 6;
end;
then
A41: x
in B9 by
SETFAM_1: 43;
A42: for d be
set st d
in Q holds (hQ9
. d)
in d
proof
let d be
set;
assume d
in Q;
then
reconsider d as
Element of Q;
(hQ9
. d)
= (
EqClass (x,d)) by
A20;
hence thesis;
end;
(
rng (h9
+* hP9))
c= ((
rng h9)
\/ (
rng hP9)) by
FUNCT_4: 17;
then (
rng (h9
+* hP9))
c= (
bool Y) by
XBOOLE_1: 1;
then (
rng h)
c= ((
rng (h9
+* hP9))
\/ (
rng hQ9)) & ((
rng (h9
+* hP9))
\/ (
rng hQ9))
c= (
bool Y) by
FUNCT_4: 17,
XBOOLE_1: 8;
then
reconsider F = (
rng h) as
Subset-Family of Y by
XBOOLE_1: 1;
A43: (
dom h)
= ((
dom (h9
+* hP9))
\/ Q) by
A23,
FUNCT_4:def 1
.= (((
dom h9)
\/ P)
\/ Q) by
A24,
FUNCT_4:def 1
.= ((G
\/ P)
\/ Q) by
FUNCT_2:def 1
.= (G
\/ Q) by
A2,
XBOOLE_1: 12
.= G by
A3,
XBOOLE_1: 12;
A44: for d be
set st d
in P holds (hP9
. d)
in d
proof
let d be
set;
assume d
in P;
then
reconsider d as
Element of P;
(hP9
. d)
= (
EqClass (y,d)) by
A19;
hence thesis;
end;
for d be
set st d
in G holds (h
. d)
in d
proof
let d be
set;
assume
A45: d
in G;
G
= ((P
\/ Q)
\/ G) by
A2,
A3,
XBOOLE_1: 8,
XBOOLE_1: 12
.= ((G
\ (P
\/ Q))
\/ (P
\/ Q)) by
XBOOLE_1: 39;
then
A46: d
in (G
\ (P
\/ Q)) or d
in (P
\/ Q) by
A45,
XBOOLE_0:def 3;
per cases by
A46,
XBOOLE_0:def 3;
suppose
A47: d
in Q;
then (h
. d)
= (hQ9
. d) by
A23,
FUNCT_4: 13;
hence thesis by
A42,
A47;
end;
suppose
A48: d
in P;
then (h
. d)
= (hP9
. d) by
A25;
hence thesis by
A44,
A48;
end;
suppose
A49: d
in (G
\ (P
\/ Q));
then not d
in (P
\/ Q) by
XBOOLE_0:def 5;
then h
= (h9
+* (hP9
+* hQ9)) & not d
in (
dom (hP9
+* hQ9)) by
A24,
A23,
FUNCT_4: 14,
FUNCT_4:def 1;
then
A50: (h
. d)
= (h9
. d) by
FUNCT_4: 11;
d
in G by
A49,
XBOOLE_0:def 5;
hence thesis by
A22,
A50;
end;
end;
then (
Intersect F)
<>
{} by
A1,
A43,
BVFUNC_2:def 5;
then
consider t be
Element of Y such that
A51: t
in (
Intersect F) by
SUBSET_1: 4;
for a be
set st a
in FP9 holds t
in a
proof
let a be
set;
assume a
in FP9;
then
consider b be
object such that
A52: b
in (
dom hP9) and
A53: (hP9
. b)
= a by
FUNCT_1:def 3;
(hP9
. b)
= (h
. b) by
A25,
A52;
then a
in F by
A2,
A24,
A43,
A52,
A53,
FUNCT_1:def 3;
hence thesis by
A51,
SETFAM_1: 43;
end;
then
A54: t
in A9 by
SETFAM_1: 43;
then A9
in (
'/\' P) by
A44,
A24,
BVFUNC_2:def 1;
then
A55:
[t, y]
in (
ERl (
'/\' P)) by
A38,
A54,
PARTIT1:def 6;
for a be
set st a
in FQ9 holds t
in a
proof
let a be
set;
assume a
in FQ9;
then
consider b be
object such that
A56: b
in (
dom hQ9) and
A57: (hQ9
. b)
= a by
FUNCT_1:def 3;
reconsider b as
Element of Q by
A56;
(hQ9
. b)
= (h
. b) by
A56,
FUNCT_4: 13;
then a
in F by
A3,
A23,
A43,
A56,
A57,
FUNCT_1:def 3;
hence thesis by
A51,
SETFAM_1: 43;
end;
then
A58: t
in B9 by
SETFAM_1: 43;
then B9
in (
'/\' Q) by
A42,
A23,
BVFUNC_2:def 1;
then
[x, t]
in (
ERl (
'/\' Q)) by
A41,
A58,
PARTIT1:def 6;
hence thesis by
A55,
RELSET_1: 28;
end;
end;
theorem ::
PARTIT_2:14
Th14: G is
independent implies for P,Q be
Subset of (
PARTITIONS Y) st P
c= G & Q
c= G holds ((
ERl (
'/\' P))
* (
ERl (
'/\' Q)))
= ((
ERl (
'/\' Q))
* (
ERl (
'/\' P))) by
Lm1;
theorem ::
PARTIT_2:15
Th15: G is
independent implies (
All ((
All (a,P,G)),Q,G))
= (
All ((
All (a,Q,G)),P,G))
proof
set A = (G
\
{P}), B = (G
\
{Q});
A1: (
CompF (P,G))
= (
'/\' A) by
BVFUNC_2:def 7;
A2: A
c= G & B
c= G by
XBOOLE_1: 36;
A3: (
CompF (Q,G))
= (
'/\' B) by
BVFUNC_2:def 7;
assume G is
independent;
then
A4: ((
ERl (
'/\' A))
* (
ERl (
'/\' B)))
= ((
ERl (
'/\' B))
* (
ERl (
'/\' A))) by
A2,
Th14;
A5: for y be
Element of Y holds ((for x be
Element of Y st x
in (
EqClass (y,(
CompF (Q,G)))) holds ((
B_INF (a,(
CompF (P,G))))
. x)
=
TRUE ) implies ((
B_INF ((
B_INF (a,(
CompF (Q,G)))),(
CompF (P,G))))
. y)
=
TRUE ) & ( not (for x be
Element of Y st x
in (
EqClass (y,(
CompF (Q,G)))) holds ((
B_INF (a,(
CompF (P,G))))
. x)
=
TRUE ) implies ((
B_INF ((
B_INF (a,(
CompF (Q,G)))),(
CompF (P,G))))
. y)
=
FALSE )
proof
let y be
Element of Y;
hereby
assume
A6: for x be
Element of Y st x
in (
EqClass (y,(
CompF (Q,G)))) holds ((
B_INF (a,(
CompF (P,G))))
. x)
=
TRUE ;
for x be
Element of Y st x
in (
EqClass (y,(
CompF (P,G)))) holds ((
B_INF (a,(
CompF (Q,G))))
. x)
=
TRUE
proof
let x be
Element of Y;
assume x
in (
EqClass (y,(
CompF (P,G))));
then
A7:
[x, y]
in (
ERl (
'/\' A)) by
A1,
Th5;
for z be
Element of Y st z
in (
EqClass (x,(
CompF (Q,G)))) holds (a
. z)
=
TRUE
proof
let z be
Element of Y;
assume z
in (
EqClass (x,(
CompF (Q,G))));
then
[z, x]
in (
ERl (
'/\' B)) by
A3,
Th5;
then
[z, y]
in ((
ERl (
'/\' A))
* (
ERl (
'/\' B))) by
A4,
A7,
RELAT_1:def 8;
then
consider u be
object such that
A8:
[z, u]
in (
ERl (
'/\' A)) and
A9:
[u, y]
in (
ERl (
'/\' B)) by
RELAT_1:def 8;
u
in (
field (
ERl (
'/\' B))) by
A9,
RELAT_1: 15;
then
reconsider u as
Element of Y by
ORDERS_1: 12;
u
in (
EqClass (y,(
CompF (Q,G)))) by
A3,
A9,
Th5;
then
A10: ((
B_INF (a,(
CompF (P,G))))
. u)
<>
FALSE by
A6;
z
in (
EqClass (u,(
CompF (P,G)))) by
A1,
A8,
Th5;
hence thesis by
A10,
BVFUNC_1:def 16;
end;
hence thesis by
BVFUNC_1:def 16;
end;
hence ((
B_INF ((
B_INF (a,(
CompF (Q,G)))),(
CompF (P,G))))
. y)
=
TRUE by
BVFUNC_1:def 16;
end;
given x be
Element of Y such that
A11: x
in (
EqClass (y,(
CompF (Q,G)))) and
A12: ((
B_INF (a,(
CompF (P,G))))
. x)
<>
TRUE ;
consider z be
Element of Y such that
A13: z
in (
EqClass (x,(
CompF (P,G)))) and
A14: (a
. z)
<>
TRUE by
A12,
BVFUNC_1:def 16;
A15:
[x, y]
in (
ERl (
'/\' B)) by
A3,
A11,
Th5;
[z, x]
in (
ERl (
'/\' A)) by
A1,
A13,
Th5;
then
[z, y]
in ((
ERl (
'/\' B))
* (
ERl (
'/\' A))) by
A4,
A15,
RELAT_1:def 8;
then
consider u be
object such that
A16:
[z, u]
in (
ERl (
'/\' B)) and
A17:
[u, y]
in (
ERl (
'/\' A)) by
RELAT_1:def 8;
u
in (
field (
ERl (
'/\' B))) by
A16,
RELAT_1: 15;
then
reconsider u as
Element of Y by
ORDERS_1: 12;
z
in (
EqClass (u,(
CompF (Q,G)))) by
A3,
A16,
Th5;
then
A18: ((
B_INF (a,(
CompF (Q,G))))
. u)
=
FALSE by
A14,
BVFUNC_1:def 16;
u
in (
EqClass (y,(
CompF (P,G)))) by
A1,
A17,
Th5;
hence thesis by
A18,
BVFUNC_1:def 16;
end;
thus (
All ((
All (a,P,G)),Q,G))
= (
B_INF ((
All (a,P,G)),(
CompF (Q,G)))) by
BVFUNC_2:def 9
.= (
B_INF ((
B_INF (a,(
CompF (P,G)))),(
CompF (Q,G)))) by
BVFUNC_2:def 9
.= (
B_INF ((
B_INF (a,(
CompF (Q,G)))),(
CompF (P,G)))) by
A5,
BVFUNC_1:def 16
.= (
B_INF ((
All (a,Q,G)),(
CompF (P,G)))) by
BVFUNC_2:def 9
.= (
All ((
All (a,Q,G)),P,G)) by
BVFUNC_2:def 9;
end;
theorem ::
PARTIT_2:16
G is
independent implies (
Ex ((
Ex (a,P,G)),Q,G))
= (
Ex ((
Ex (a,Q,G)),P,G))
proof
assume
A1: G is
independent;
thus (
Ex ((
Ex (a,P,G)),Q,G))
= (
'not' (
'not' (
Ex ((
Ex (a,P,G)),Q,G))))
.= (
'not' (
All ((
'not' (
Ex (a,P,G))),Q,G))) by
BVFUNC_2: 19
.= (
'not' (
All ((
All ((
'not' a),P,G)),Q,G))) by
BVFUNC_2: 19
.= (
'not' (
All ((
All ((
'not' a),Q,G)),P,G))) by
A1,
Th15
.= (
'not' (
All ((
'not' (
Ex (a,Q,G))),P,G))) by
BVFUNC_2: 19
.= (
'not' (
'not' (
Ex ((
Ex (a,Q,G)),P,G)))) by
BVFUNC_2: 19
.= (
Ex ((
Ex (a,Q,G)),P,G));
end;
theorem ::
PARTIT_2:17
for a be
Function of Y,
BOOLEAN , G be
Subset of (
PARTITIONS Y), P,Q be
a_partition of Y st G is
independent holds (
Ex ((
All (a,P,G)),Q,G))
'<' (
All ((
Ex (a,Q,G)),P,G))
proof
let a be
Function of Y,
BOOLEAN , G be
Subset of (
PARTITIONS Y), P,Q be
a_partition of Y such that
A1: G is
independent;
set A = (G
\
{P}), B = (G
\
{Q});
A
c= G & B
c= G by
XBOOLE_1: 36;
then
A2: ((
ERl (
'/\' A))
* (
ERl (
'/\' B)))
= ((
ERl (
'/\' B))
* (
ERl (
'/\' A))) by
A1,
Th14;
A3: (
CompF (P,G))
= (
'/\' A) by
BVFUNC_2:def 7;
A4: (
Ex ((
All (a,P,G)),Q,G))
= (
B_SUP ((
All (a,P,G)),(
CompF (Q,G)))) by
BVFUNC_2:def 10;
A5: (
CompF (Q,G))
= (
'/\' B) by
BVFUNC_2:def 7;
let x be
Element of Y such that
A6: ((
Ex ((
All (a,P,G)),Q,G))
. x)
=
TRUE ;
A7: for z be
Element of Y st z
in (
EqClass (x,(
CompF (P,G)))) holds ((
Ex (a,Q,G))
. z)
=
TRUE
proof
let z be
Element of Y;
consider y be
Element of Y such that
A8: y
in (
EqClass (x,(
CompF (Q,G)))) and
A9: ((
All (a,P,G))
. y)
=
TRUE by
A6,
A4,
BVFUNC_1:def 17;
assume z
in (
EqClass (x,(
CompF (P,G))));
then
[z, x]
in (
ERl (
'/\' A)) by
A3,
Th5;
then
A10:
[x, z]
in (
ERl (
'/\' A)) by
EQREL_1: 6;
[y, x]
in (
ERl (
'/\' B)) by
A5,
A8,
Th5;
then
[y, z]
in ((
ERl (
'/\' A))
* (
ERl (
'/\' B))) by
A2,
A10,
RELAT_1:def 8;
then
consider u be
object such that
A11:
[y, u]
in (
ERl (
'/\' A)) and
A12:
[u, z]
in (
ERl (
'/\' B)) by
RELAT_1:def 8;
u
in (
field (
ERl (
'/\' B))) by
A12,
RELAT_1: 15;
then
reconsider u as
Element of Y by
ORDERS_1: 12;
[u, y]
in (
ERl (
'/\' A)) by
A11,
EQREL_1: 6;
then (
All (a,P,G))
= (
B_INF (a,(
CompF (P,G)))) & u
in (
EqClass (y,(
CompF (P,G)))) by
A3,
Th5,
BVFUNC_2:def 9;
then
A13: (a
. u)
=
TRUE by
A9,
BVFUNC_1:def 16;
(
Ex (a,Q,G))
= (
B_SUP (a,(
CompF (Q,G)))) & u
in (
EqClass (z,(
CompF (Q,G)))) by
A5,
A12,
Th5,
BVFUNC_2:def 10;
hence thesis by
A13,
BVFUNC_1:def 17;
end;
(
All ((
Ex (a,Q,G)),P,G))
= (
B_INF ((
Ex (a,Q,G)),(
CompF (P,G)))) by
BVFUNC_2:def 9;
hence thesis by
A7,
BVFUNC_1:def 16;
end;
begin
reserve x,y,z for
set,
S,X for non
empty
set,
R for
Relation of X;
notation
let A,B be
set;
synonym
[#] (A,B) for
[:A,B:];
end
definition
let A,B be
set;
::
PARTIT_2:def1
func
{} (A,B) ->
Relation of A, B equals
{} ;
correctness by
RELSET_1: 12;
:: original:
[#]
redefine
func
[#] (A,B) ->
Relation of A, B ;
correctness
proof
(
[#] (A,B))
c=
[:A, B:];
hence thesis;
end;
end
registration
let A,B be
set;
cluster (
{} (A,B)) ->
empty;
coherence ;
end
theorem ::
PARTIT_2:18
(
field (
id X))
= X
proof
(
dom (
id X))
= X & (
rng (
id X))
= X;
then (
field (
id X))
= (X
\/ X) by
RELAT_1:def 6;
hence thesis;
end;
theorem ::
PARTIT_2:19
op1
=
{
[
{} ,
{} ]}
proof
{
{} }
= (
dom
op1 ) by
FUNCT_2:def 1;
then
{}
in (
dom
op1 ) by
TARSKI:def 1;
then
[
{} , (
op1
.
{} )]
in
op1 by
FUNCT_1:def 2;
then
A1:
{
[
{} , (
op1
.
{} )]}
c=
op1 by
ZFMISC_1: 31;
(
rng
op1 )
=
{(
op1
.
{} )} by
FUNCT_2: 48;
then
A2: (
op1
.
{} )
=
{} by
ZFMISC_1: 18;
op1
c=
[:
{
{} },
{
{} }:];
then
op1
c=
{
[
{} ,
{} ]} by
ZFMISC_1: 29;
hence thesis by
A2,
A1;
end;
theorem ::
PARTIT_2:20
for A,B be
set holds (
field (
{} (A,B)))
=
{} by
RELAT_1: 40;
theorem ::
PARTIT_2:21
R
is_reflexive_in X implies R is
reflexive & (
field R)
= X by
Th9;
theorem ::
PARTIT_2:22
R
is_symmetric_in X implies R is
symmetric
proof
assume
A1: R
is_symmetric_in X;
let x,y be
object;
(
field R)
c= (X
\/ X) by
RELSET_1: 8;
hence thesis by
A1;
end;
theorem ::
PARTIT_2:23
R is
symmetric implies R
is_symmetric_in S
proof
assume R is
symmetric;
then
A1: R
is_symmetric_in (
field R);
let x,y be
object;
assume x
in S & y
in S;
assume
A2:
[x, y]
in R;
then x
in (
field R) & y
in (
field R) by
RELAT_1: 15;
hence thesis by
A1,
A2;
end;
theorem ::
PARTIT_2:24
R is
antisymmetric implies R
is_antisymmetric_in S
proof
assume R is
antisymmetric;
then
A1: R
is_antisymmetric_in (
field R);
let x,y be
object;
assume x
in S & y
in S;
assume
A2:
[x, y]
in R;
then x
in (
field R) & y
in (
field R) by
RELAT_1: 15;
hence thesis by
A1,
A2;
end;
theorem ::
PARTIT_2:25
R
is_antisymmetric_in X implies R is
antisymmetric
proof
assume
A1: R
is_antisymmetric_in X;
let x,y be
object;
(
field R)
c= (X
\/ X) by
RELSET_1: 8;
hence thesis by
A1;
end;
theorem ::
PARTIT_2:26
R is
transitive implies R
is_transitive_in S
proof
assume R is
transitive;
then
A1: R
is_transitive_in (
field R);
let x,y,z be
object;
assume x
in S & y
in S & z
in S;
assume
A2:
[x, y]
in R;
then
A3: x
in (
field R) by
RELAT_1: 15;
assume
A4:
[y, z]
in R;
then y
in (
field R) & z
in (
field R) by
RELAT_1: 15;
hence thesis by
A1,
A2,
A4,
A3;
end;
theorem ::
PARTIT_2:27
R
is_transitive_in X implies R is
transitive
proof
assume
A1: R
is_transitive_in X;
let x,y,z be
object;
(
field R)
c= (X
\/ X) by
RELSET_1: 8;
hence thesis by
A1;
end;
theorem ::
PARTIT_2:28
R is
asymmetric implies R
is_asymmetric_in S
proof
assume R is
asymmetric;
then
A1: R
is_asymmetric_in (
field R);
let x,y be
object;
assume x
in S & y
in S;
assume
A2:
[x, y]
in R;
then x
in (
field R) & y
in (
field R) by
RELAT_1: 15;
hence thesis by
A1,
A2;
end;
theorem ::
PARTIT_2:29
R
is_asymmetric_in X implies R is
asymmetric
proof
assume
A1: R
is_asymmetric_in X;
let x,y be
object;
(
field R)
c= (X
\/ X) by
RELSET_1: 8;
hence thesis by
A1;
end;
theorem ::
PARTIT_2:30
R is
irreflexive & (
field R)
c= S implies R
is_irreflexive_in S
proof
assume that
A1: R is
irreflexive and
A2: (
field R)
c= S;
let x be
object;
S
= ((
field R)
\/ (S
\ (
field R))) by
A2,
XBOOLE_1: 45;
then
A3: x
in S implies x
in (
field R) or x
in (S
\ (
field R)) by
XBOOLE_0:def 3;
A4: x
in (S
\ (
field R)) implies not
[x, x]
in R
proof
assume x
in (S
\ (
field R));
then x
in (S
\ ((
dom R)
\/ (
rng R))) by
RELAT_1:def 6;
then x
in ((S
\ (
dom R))
/\ (S
\ (
rng R))) by
XBOOLE_1: 53;
then x
in (S
\ (
rng R)) by
XBOOLE_0:def 4;
then not x
in (
rng R) by
XBOOLE_0:def 5;
hence thesis by
XTUPLE_0:def 13;
end;
R
is_irreflexive_in (
field R) by
A1;
hence thesis by
A3,
A4;
end;
theorem ::
PARTIT_2:31
R
is_irreflexive_in X implies R is
irreflexive
proof
A1: (
field R)
c= (X
\/ X) by
RELSET_1: 8;
assume R
is_irreflexive_in X;
then for x be
object holds x
in (
field R) implies not
[x, x]
in R by
A1;
then R
is_irreflexive_in (
field R);
hence thesis;
end;
registration
cluster
empty ->
irreflexive
asymmetric
transitive for
Relation;
coherence
proof
let R be
Relation;
assume
A1: R is
empty;
hence for x be
object holds x
in (
field R) implies not
[x, x]
in R;
thus for x,y be
object holds x
in (
field R) & y
in (
field R) &
[x, y]
in R implies not
[y, x]
in R by
A1;
thus for x,y,z be
object holds x
in (
field R) & y
in (
field R) & z
in (
field R) &
[x, y]
in R &
[y, z]
in R implies
[x, z]
in R by
A1;
end;
end
definition
let f be
Function;
::
PARTIT_2:def2
attr f is
involutive means for x be
set st x
in (
dom f) holds (f
. (f
. x))
= x;
end
definition
let X;
let f be
UnOp of X;
:: original:
involutive
redefine
::
PARTIT_2:def3
attr f is
involutive means for x be
Element of X holds (f
. (f
. x))
= x;
compatibility
proof
(
dom f)
= X by
PARTFUN1:def 2;
hence f is
involutive implies for x be
Element of X holds (f
. (f
. x))
= x;
assume
A1: for x be
Element of X holds (f
. (f
. x))
= x;
let x be
set;
assume x
in (
dom f);
hence thesis by
A1;
end;
end
registration
cluster
op1 ->
involutive;
coherence
proof
op1 is
involutive
proof
let a be
Element of
{
0 };
a
=
{} by
TARSKI:def 1;
hence (
op1
. (
op1
. a))
= a by
FUNCT_2: 50;
end;
hence thesis;
end;
end
registration
let X be
set;
cluster (
id X) ->
involutive;
coherence
proof
set f = (
id X);
let a be
set;
assume a
in (
dom f);
then a
in X;
then (f
. a)
= a by
FUNCT_1: 17;
hence thesis;
end;
end