environ
vocabularies ENUMSET,RELATION,RELAT_AB;
notations ENUMSET,RELATION,RELAT_AB;
constructors ENUMSET,RELATION,RELAT_AB;
definitions ENUMSET,RELATION,RELAT_AB;
equalities ENUMSET,RELATION,RELAT_AB;
theorems ENUMSET,RELATION,RELAT_AB;
begin
reserve A,B,X,Y,Z,V,a,b,c,d,e,x,y,z for set, P,Q,R for Relation,
S for Relation of A,A;
ex R st not R \ R~ is symmetric
proof
reconsider R={[1,2]} as Relation by RELATION:1;
take R;
r: [1,2] in R by ENUMSET:def 3;
not [1,2] in R~
proof
assume [1,2] in R~;
then [2,1] in R by RELATION:def 3;
then [2,1] = [1,2] by ENUMSET:def 3;
hence contradiction by ENUMSET:2;
end;
then
j: [1,2] in R\R~ by r,RELATION:def 6;
[2,1] <> [1,2] by ENUMSET:2;
then not [2,1] in R by ENUMSET:def 3;
then not [2,1] in R\R~ by RELATION:def 6;
hence not R \ R~ is symmetric by j,RELATION:def 11;
end;
R \ R~ is antisymmetric
proof
let a,b;
assume [a,b] in R \ R~ & [b,a] in R \ R~;
then [a,b] in R & not [a,b] in R~ & [b,a] in R & not [b,a] in R~ by RELATION:def 6;
then contradiction by RELATION:def 3;
hence a=b;
end;
R is transitive implies R~ is transitive
proof
assume r: R is transitive;
let a,b,c;
assume [a,b] in R~ & [b,c] in R~;
then [b,a] in R & [c,b] in R by RELATION:def 3;
then [c,a] in R by r,RELATION:def 12;
hence [a,c] in R~ by RELATION:def 3;
end;
:: 4.30
R is symmetric iff R~ c= R
proof
thus R is symmetric implies R~ c= R
proof
assume s: R is symmetric;
let a,b;
assume [a,b] in R~;
then [b,a] in R by RELATION:def 3;
hence [a,b] in R by s,RELATION:def 11;
end;
thus R~ c= R implies R is symmetric
proof
assume r: R~ c= R;
let a,b;
assume [a,b] in R;
then [b,a] in R~ by RELATION:def 3;
hence [b,a] in R by r,RELATION:def 9;
end;
end;
:: 4.39
R is transitive iff R*R c= R
proof
thus R is transitive implies R*R c= R
proof
assume t: R is transitive;
let a,b;
assume [a,b] in R*R;
then consider c such that
c: [a,c] in R & [c,b] in R by RELATION:def 7;
thus [a,b] in R by c,t,RELATION:def 12;
end;
thus R*R c= R implies R is transitive
proof
assume r: R*R c= R;
let a,b,c;
assume [a,b] in R & [b,c] in R;
then [a,c] in R*R by RELATION:def 7;
hence [a,c] in R by r,RELATION:def 9;
end;
end;