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 {};
then contradiction by RELATION:def 2;
hence x=y;
end;
P is transitive & R is transitive implies P/\R is transitive
proof
assume t: P is transitive & R is transitive;
thus P/\R is transitive
proof
let x,y,z;
assume [x,y] in P/\R & [y,z] in P/\R;
then [x,y] in P & [x,y] in R & [y,z] in P & [y,z] in R by RELATION:def 5;
then [x,z] in P & [x,z] in R by t,RELATION:def 12;
hence [x,z] in P/\R 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]},R={[2,1]} 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,1] & [y,z]=[2,1] by ENUMSET:def 3;
then x=2 & y=1 & y=2 & z=1 by ENUMSET:2;
hence [x,z] in R;
end;
thus P\/R is not transitive
proof
[1,2] in P & [2,1] in R by ENUMSET:def 3;
then r: [1,2] in P\/R & [2,1] in P\/R by RELATION:def 4;
now
assume [1,1] in P \/ R;
then [1,1] in P or [1,1] in R by RELATION:def 4;
then [1,1] = [1,2] or [1,1] = [2,1] by ENUMSET:def 3;
hence contradiction by ENUMSET:2;
end;
hence thesis by r,RELATION:def 12;
end;
end;
P c= R & R is irreflexive implies P is irreflexive
proof
assume z: P c= R;
assume r: R is irreflexive;
let x;
not [x,x] in R by r,RELATION:def 15;
hence not [x,x] in P by z,RELATION:def 9;
end;
ex P,R st P c= R & P is not symmetric & R is symmetric
proof
reconsider P={[1,2]},R={[1,2],[2,1]} as Relation by RELATION:1,2;
take P,R;
thus P c= R
proof
let x,y;
assume [x,y] in P;
then [x,y]=[1,2] by ENUMSET:def 3;
hence [x,y] in R by ENUMSET:def 4;
end;
j: [1,2] in P by ENUMSET:def 3;
now
assume [2,1] in P;
then [2,1] = [1,2] by ENUMSET:def 3;
hence contradiction by ENUMSET:2;
end;
hence P is not symmetric by j,RELATION:def 11;
thus R is symmetric
proof
let x,y;
assume [x,y] in R;
then [x,y] = [1,2] or [x,y] = [2,1] by ENUMSET:def 4;
then x=1 & y=2 or x=2 & y=1 by ENUMSET:2;
then [y,x] = [2,1] or [y,x] = [1,2] by ENUMSET:2;
hence [y,x] in R by ENUMSET:def 4;
end;
end;
ex P,R st P c= R & P is symmetric & R is not symmetric
proof
take P={};
reconsider R={[1,2]} as Relation by RELATION:1;
take R;
thus P c= R
proof
let x,y;
assume [x,y] in P;
hence thesis by ENUMSET:def 1;
end;
thus P is symmetric
proof
let x,y;
assume [x,y] in P;
hence thesis by ENUMSET:def 1;
end;
[2,1] <> [1,2] by ENUMSET:2;
then [1,2] in R & not [2,1] in R by ENUMSET:def 3;
hence not R is symmetric by RELATION:def 11;
end;
ex P,R st P c= R & P is asymmetric & R is not asymmetric
proof
take P={};
reconsider R={[1,1]} as Relation by RELATION:1;
take R;
thus P c= R
proof
let x,y;
assume [x,y] in P;
hence thesis by ENUMSET:def 1;
end;
thus P is asymmetric
proof
let x,y;
assume [x,y] in P;
hence thesis by ENUMSET:def 1;
end;
[1,1] in R by ENUMSET:def 3;
hence not R is asymmetric by RELATION:def 13;
end;