:: Classes of Independent Partitions
:: by Andrzej Trybulec
::
:: Received February 14, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, MARGREL1, PARTIT1, EQREL_1, FUNCT_1,
SETFAM_1, RELAT_1, ZFMISC_1, TARSKI, RELAT_2, XBOOLEAN, BVFUNC_2,
BVFUNC_1, FUNCT_4, FUNCT_5, OPOSET_1, BINOP_1, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, MARGREL1, RELAT_1,
RELAT_2, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_5,
EQREL_1, PARTIT1, BVFUNC_1, BVFUNC_2;
constructors SETFAM_1, FUNCT_4, XCMPLX_0, BVFUNC_1, BVFUNC_2, RELSET_1,
FUNCT_5, RELAT_2, DOMAIN_1, BINOP_1, NUMBERS;
registrations SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, EQREL_1, MARGREL1,
PARTIT1, RELSET_1, XBOOLE_0, FUNCT_2;
requirements SUBSET, BOOLE, ARITHM, NUMERALS;
definitions BVFUNC_1, TARSKI, RELAT_2, XBOOLE_0, RELSET_1;
equalities XBOOLEAN, EQREL_1, ORDINAL1;
expansions BVFUNC_1, RELAT_2, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, BVFUNC_1, BVFUNC_2, RELSET_1, PARTIT1,
SETFAM_1, SUBSET_1, FUNCT_4, RELAT_1, EQREL_1, RELAT_2, XBOOLE_0,
XBOOLE_1, PARTFUN1, ORDERS_1, XBOOLEAN, MARGREL1, ZFMISC_1, XTUPLE_0;
schemes FUNCT_2;
begin :: Preliminaries
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;
redefine mode Element of G -> a_partition of Y; :: redefines Element (SUBSET_1, definition)
coherence
proof
let p be Element of G;
thus thesis by PARTIT1:def 3;
end;
end;
theorem Th1:
'/\' {} PARTITIONS Y = %O Y
proof
for x being set holds x in %O Y iff ex h being Function, F being
Subset-Family of Y st dom h={} PARTITIONS Y & rng h = F & (for d being 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 being 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 being Function, F being Subset-Family of Y such that
A2: dom h={} PARTITIONS Y & rng h = F and
for d being 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 Th2:
for R,S being 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
for R being Relation of Y holds R c= nabla Y;
theorem Th4:
for R being Equivalence_Relation of Y holds (nabla Y)*R = nabla Y
& R*nabla Y = nabla Y
proof
let R being 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 Th5:
for P being a_partition of Y, x,y being 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 being 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
for P,Q,R being a_partition of Y st ERl(R) = ERl(P)*ERl(Q) 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
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 being 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 being 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 Th7:
for R,S being Relation, Y being 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 Th8:
for R being Relation, Y being 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 Th9:
for Y being set, R being 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
for R,S being 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 being 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,def 11;
end;
begin :: Boolean-valued Functions
theorem Th11:
for a,b being Function of Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a
proof
let a,b being 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 Th12:
for a,b being Function of Y,BOOLEAN, G being Subset of PARTITIONS(Y),
P being 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 being 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
for a,b being Function of Y,BOOLEAN,
G being Subset of PARTITIONS(Y), P being 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 :: Independent Families of Partitions
Lm1: G is independent implies 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
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 being Element of Y such that
A5: [x,z] in ERl('/\'P) and
A6: [z,y] in ERl('/\'Q) by RELSET_1:28;
consider A being 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 being 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 being Function, FQ being Subset-Family of Y such that
A13: dom hQ = Q & rng hQ = FQ and
A14: for d being 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 being Function, FP being Subset-Family of Y such that
A16: dom hP = P & rng hP = FP and
A17: for d being 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 being Function of P, bool Y such that
A19: for p being Element of P holds hP9.p = P(p) from FUNCT_2:sch 4;
deffunc Q(Element of Q) = EqClass(x,$1);
consider hQ9 being Function of Q, bool Y such that
A20: for p being Element of Q holds hQ9.p = Q(p) from FUNCT_2:sch 4;
deffunc P(set) = $1;
A21: for d being 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 being Function of G9, bool Y such that
A22: for d being 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 being 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 being set st a in FP9 holds y in a
proof
let a be set;
assume a in FP9;
then consider b being 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 being set st a in FQ9 holds x in a
proof
let a be set;
assume a in FQ9;
then consider b being 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 being 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 being 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 being 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,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,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 being Element of Y such that
A51: t in Intersect F by SUBSET_1:4;
for a being set st a in FP9 holds t in a
proof
let a be set;
assume a in FP9;
then consider b being 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 being set st a in FQ9 holds t in a
proof
let a be set;
assume a in FQ9;
then consider b being 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 Th14:
G is independent implies 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:
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 being Element of Y holds ( (for x being 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 being 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 being Element of Y st x in EqClass(y,CompF(Q,G)) holds
B_INF(a,CompF(P,G)).x=TRUE;
for x being 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 being 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 being 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 being 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 being 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 being 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
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
for a being Function of Y,BOOLEAN, G being Subset of PARTITIONS(
Y), 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
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 being Element of Y such that
A6: Ex(All(a,P,G),Q,G).x = TRUE;
A7: for z being 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 being 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 being 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 :: Moved from OPOSET_1, 2010.03.11, A.T.
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;
func {}(A,B) -> Relation of A,B equals
{};
correctness by RELSET_1:12;
redefine func [#](A,B) -> Relation of A,B; :: redefines [#] (PARTIT_2, synonym) → [: (ZFMISC_1, definition)
correctness
proof
[#](A,B) c= [:A,B:];
hence thesis;
end;
end;
registration let A,B be set;
cluster {}(A,B) -> empty;
coherence;
end;
theorem
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
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
for A,B being set holds field {}(A,B) = {} by RELAT_1:40;
theorem
R is_reflexive_in X implies R is reflexive & field R = X
by Th9;
theorem
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
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
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
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
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
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
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
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
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
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 being object holds x in field R implies not [x,x] in R by A1;
then R is_irreflexive_in field R;
hence thesis;
end;
:: Some existence conditions on non-empty relations
registration
cluster empty -> irreflexive asymmetric transitive for Relation;
coherence
proof let R be Relation;
assume
A1: R is empty;
hence for x being object holds x in field R implies not [x,x] in R;
thus for x,y being 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 being 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;
:: Double negation property of the internal Complement
definition
let f be Function;
attr f is involutive means
for x being set st x in dom f holds f.(f.x) = x;
end;
definition
let X;
let f be UnOp of X;
redefine attr f is involutive means :: redefines involutive (PARTIT_2, definition)
for x being Element of X holds f.(f.x) = x;
compatibility
proof
dom f = X by PARTFUN1:def 2;
hence f is involutive implies for x being Element of X holds f.(f.x) = x;
assume
A1: for x being 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 for Function;
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;