environ
vocabularies ENUMSET,RELATION;
notations ENUMSET,RELATION;
constructors ENUMSET,RELATION;
definitions ENUMSET,RELATION;
equalities ENUMSET,RELATION;
theorems ENUMSET,RELATION;
begin
reserve x,y,z,A,B,C for set, P,Q,R,S,T for Relation;
{} is antisymmetric
proof
let x,y;
assume [x,y] in {} & [y,x] in {};
hence x=y by RELATION:def 2;
end;
:: 4.34
R is symmetric & S is symmetric implies R \/ S is symmetric
proof
assume that
r: R is symmetric and
s: S is symmetric;
thus R \/ S is symmetric
proof
let x,y;
assume [x,y] in R \/ S;
then [x,y] in R or [x,y] in S by RELATION:def 4;
then [y,x] in R or [y,x] in S by r,s,RELATION:def 11;
hence [y,x] in R \/ S by RELATION:def 4;
end;
end;
:: 4.35
R is transitive & S is transitive implies R /\ S is transitive
proof
assume that
r: R is transitive and
s: S is transitive;
thus R /\ S is transitive
proof
let x,y,z;
assume [x,y] in R /\ S & [y,z] in R /\ S;
then [x,y] in R & [x,y] in S & [y,z] in R & [y,z] in S by RELATION:def 5;
then [x,z] in R & [x,z] in S by r,s,RELATION:def 12;
hence [x,z] in R /\ S by RELATION:def 5;
end;
end;
ex P,R st P is transitive & R is transitive & P\/R is not transitive
proof
reconsider P={[1,2]} as Relation by RELATION:1;
reconsider R={[2,3]} as Relation by RELATION:1;
take P,R;
thus P is transitive
proof
let x,y,z;
assume [x,y] in P & [y,z] in P;
then [x,y]=[1,2] & [y,z] = [1,2] by ENUMSET:def 3;
then x=1 & y=2 & y=1 & z=2 by ENUMSET:2;
hence [x,z] in P;
end;
thus R is transitive
proof
let x,y,z;
assume [x,y] in R & [y,z] in R;
then [x,y]=[2,3] & [y,z] = [2,3] by ENUMSET:def 3;
then x=2 & y=3 & y=2 & z=3 by ENUMSET:2;
hence [x,z] in R;
end;
thus P \/ R is not transitive
proof
[1,2] in P by ENUMSET:def 3;
then a: [1,2] in P \/ R by RELATION:def 4;
[2,3] in R by ENUMSET:def 3;
then b: [2,3] in P \/ R by RELATION:def 4;
not [1,3] in P \/ R
proof
assume [1,3] in P \/ R;
then [1,3] in P or [1,3] in R by RELATION:def 4;
then [1,3] = [1,2] or [1,3] = [2,3] by ENUMSET:def 3;
then (1=1 & 3=2) or (1=2 & 3=3) by ENUMSET:2;
hence contradiction;
end;
hence thesis by a,b,RELATION:def 12;
end;
end;