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,C,a,b,c,x,y,z,A,B,C for set, P,Q,R,S,T 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.31
R c= R~ iff R = R~
proof
thus R c= R~ implies R = R~
proof
assume r: R c= R~;
hence R c= R~;
thus R~ c= R
proof
let a,b;
assume [a,b] in R~;
then [b,a] in R by RELATION:def 3;
then [b,a] in R~ by r,RELATION:def 9;
hence [a,b] in R by RELATION:def 3;
end;
end;
thus R = R~ implies R c= R~ by RELATION:def 10;
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;
::4.33
S is weakly_connected iff S \/ S~ \/ id(A) = [:A,A:]
proof
dr: dom S c= A & rng S c= A by RELAT_AB:def 5;
thus S is weakly_connected implies S \/ S~ \/ id(A) = [:A,A:]
proof
assume s: S is weakly_connected;
thus S \/ S~ \/ id(A) c= [:A,A:]
proof
let x,y;
assume [x,y] in S \/ S~ \/ id(A);
then [x,y] in S \/ S~ or [x,y] in id A by ENUMSET:def 6;
then [x,y] in S or [x,y] in S~ or [x,y] in id(A) by ENUMSET:def 6;
then per cases;
suppose [x,y] in S;
then x in dom S & y in rng S by RELAT_AB:def 1,def 2;
then x in A & y in A by ENUMSET:def 10,dr;
hence [x,y] in [:A,A:] by RELAT_AB:def 7;
end;
suppose [x,y] in S~;
then [y,x] in S by RELATION:def 3;
then y in dom S & x in rng S by RELAT_AB:def 1,def 2;
then x in A & y in A by ENUMSET:def 10,dr;
hence [x,y] in [:A,A:] by RELAT_AB:def 7;
end;
suppose [x,y] in id(A);
then x in A & x=y by RELAT_AB:def 6;
hence [x,y] in [:A,A:] by RELAT_AB:def 7;
end;
end;
thus [:A,A:] c= S \/ S~ \/ id(A)
proof
let x,y;
assume [x,y] in [:A,A:];
then consider x1,y1 being set such that
xy: x1 in A & y1 in A & [x,y] = [x1,y1] by RELAT_AB:def 7;
xy1: x=x1 & y=y1 by xy,ENUMSET:2;
per cases;
suppose x=y;
then [x,y] in id(A) by xy,xy1,RELAT_AB:def 6;
hence [x,y] in S \/ S~ \/ id(A) by ENUMSET:def 6;
end;
suppose x<>y;
then [x,y] in S or [y,x] in S by xy,xy1,s,RELAT_AB:def 9;
then [x,y] in S or [x,y] in S~ by RELATION:def 3;
then [x,y] in S \/ S~ by ENUMSET:def 6;
hence [x,y] in S \/ S~ \/ id(A) by ENUMSET:def 6;
end;
end;
end;
thus S \/ S~ \/ id(A) = [:A,A:] implies S is weakly_connected
proof
assume e: S \/ S~ \/ id(A) = [:A,A:];
let x,y be set;
assume xy: x in A & y in A & x <> y & not [x,y] in S;
then [x,y] in S \/ S~ \/ id(A) & not [x,y] in id(A) by e,RELAT_AB:def 7,def 6;
then [x,y] in S \/ S~ by ENUMSET:def 6;
then [x,y] in S~ by xy,ENUMSET:def 6;
hence [y,x] in S by RELATION:def 3;
end;
end;
::4.14
S is reflexive iff dom S=A & id (dom S \/ rng S) c= S
proof
thus S is reflexive implies dom S =A & id (dom S \/ rng S) c= S
proof
assume r: S is reflexive;
d: dom S c= A & rng S c= A by RELAT_AB:def 5;
A c= dom S
proof
let a;
assume a in A;
then [a,a] in S by r,RELAT_AB:def 8;
hence a in dom S by RELAT_AB:def 1;
end;
hence dom S = A by d,ENUMSET:def 11;
thus id (dom S \/ rng S) c= S
proof
let x,y;
assume [x,y] in id (dom S \/ rng S);
then e: x in dom S \/ rng S & x=y by RELAT_AB:def 6;
then x in dom S or x in rng S by ENUMSET:def 6;
then x in A by d,ENUMSET:def 10;
hence [x,y] in S by r,e,RELAT_AB:def 8;
end;
end;
thus dom S = A & id (dom S \/ rng S) c= S implies S is reflexive
proof
assume i: dom S = A & id (dom S \/ rng S) c= S;
let x;
assume x in A;
then x in dom S by i;
then x in dom S \/ rng S by ENUMSET:def 6;
then [x,x] in id (dom S \/ rng S) by RELAT_AB:def 6;
hence [x,x] in S by i,ENUMSET:def 10;
end;
end;