10 Zajęcia, Mizar
[ Pobierz całość w formacie PDF ]
beginreserve P,Q,R,S,T for Relation, a,b,c,d,x,y,z,u for set;::6 Grudnia 2007::Zaj,Bj(Bcia nr 10::Zadanko 1{} is antisymmetricprooflet x,y;assume [x,y] in {};then [y,x] in {} by RELATION:def 2;then not [y,x] in {} by RELATION:def 2;hence thesis;end;::Zadanko 2R is asymmetric implies R is antisymmetricproofassume A1: R is asymmetric;thus R is antisymmetricprooflet x,y;assume [x,y] in R & [y,x] in R;then not [y,x] in R & [y,x] in R by RELATION:def 13, A1;hence thesis;end;end;::Zadanko 3R*R c= R iff R is transitiveproofthus R*R c= R implies R is transitiveproofassume B1: R*R c= R;thus R is transitiveprooflet x,y,z;assume [x,y] in R & [y,z] in R;then [x,z] in R*R by RELATION:def 7;then [x,z] in R by B1, RELATION:def 9;hence thesis;end;end;thus R is transitive implies R*R c= Rproofassume C2: R is transitive;thus R*R c= Rprooflet x,y;assume [x,y] in R*R;then consider z such thatC1: [x,z] in R & [z,y] in R by RELATION:def 7;[x,y] in R by RELATION:def 12, C2, C1;hence thesis;end;end;end;::Zadanko 4R is irreflexive & R is transitive implies R is asymmetricproofassume X1: R is irreflexive & R is transitive;thus R is asymmetricprooflet x,y;assume X2: [x,y] in R;X3: not [x,x] in R by RELATION:def 15, X1;X4: not [y,y] in R by RELATION:def 15, X1;not [y,x] in R by RELATION:def 12, X2, X3, X4, X1;hence thesis;end;end;::Zadanko 5P is transitive & R is transitive implies P/\R is transitiveproofassume D1: P is transitive & R is transitive;thus P/\R is transitiveprooflet 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/\R by RELATION:def 5;then D2: [x,y] in P & [x,y] in R & [y,z] in P & [y,z] in R by RELATION:def 5;then D3: [x,z] in P & [x,z] in R by RELATION:def 12, D1;hence thesis by RELATION:def 5, D3;end;end;::Zadanko 6R~ c= R iff R is symmetricproofthus R~c= R implies R is symmetricproofassume F1: R~ c= R;thus R is symmetricprooflet x,y;assume [x,y] in R;then [y,x] in R~ by RELATION:def 3;then [y,x] in R by RELATION:def 9, F1;hence thesis;end;end;thus R is symmetric implies R~ c= Rproofassume F2: R is symmetric;thus R~ c= Rprooflet x,y;assume [x,y] in R~;then [y,x] in R by RELATION:def 3;then [x,y] in R by RELATION:def 11, F2;hence thesis;end;end;end;
[ Pobierz całość w formacie PDF ]