Zajęcia 11, Mizar
[ Pobierz całość w formacie PDF ]
::10 stycznia 2008::Zaj,Bj(Bcia 11::Zadanko 1ex R st R <> {} & R is asymmetricproofreconsider R={[0,1]} as Relation by RELATION:1;take R;[0,1] in R by ENUMSET:def 3;hence R <> {} by RELATION:def 2;thus R is asymmetricprooflet x,y;assume [x,y] in R;then [x,y] = [0,1] by ENUMSET:def 3;then x=0 & y=1 by ENUMSET:2;then [y,x] <> [0,1] by ENUMSET:2;hence not [y,x] in R by ENUMSET:def 3;end;end;::Zadaanko 2ex P,R st P is symmetric & R is symmetric & P*R is not symmetricproofreconsider P={[0,0]} as Relation by RELATION:1;reconsider R={[0,1],[1,0]} as Relation by RELATION:2;take P,R;thus P is symmetricprooflet x,y;assume [x,y] in P;then [x,y] = [0,0] by ENUMSET:def 3;then x=0 & y=0 by ENUMSET:2;then [y,x] = [0,0] by RELATION:def 11;hence [y,x] in P by ENUMSET:def 3;end;thus R is symmetricprooflet x,y;assume [x,y] in R;then [x,y] = [0,1] or [x,y] =[1,0] by ENUMSET:def 4;then x=0 & y=1 or x=1 & y=0 by ENUMSET:2;then [y,x] = [1,0] or [y,x] = [0,1] by RELATION:def 11;hence [y,x] in R by ENUMSET:def 4;end;thus P*R is not symmetricprooftake a=0,b=1;thus [a,b] in P*RproofA1:[0,0] in P by ENUMSET:def 3;A2:[0,1] in R by ENUMSET:def 4;[0,1] in P*R by A1,A2,RELATION:def 7;hence thesis;end;thus not [b,a] in P*Rproofassume B1:[b,a] in P*R;then consider c such thatZ1:[b,c] in P & [c,a] in R by RELATION:def 7;[b,c]=[0,0] & ([c,a] = [0,1] or [c,a] = [1,0]) by Z1,ENUMSET:def 3,def 4;then b = 0 & c = 0 & (c = 0 & a = 1 or c = 1 & a = 0) by ENUMSET:2;then b = 0 & c = 0 & a = 1;hence contradiction;end;end;end;::Zadanko 3not ex P,R st P is symmetric & R is symmetric & P\/R is not symmetricproofend;::>,70::Zadanko 4ex P,R st P c= R & P is symmetric & not R is symmetricproofa0: 0<>1;then consider a,b being set such that a<>b;reconsider P={[0,0]} as Relation by RELATION:1;reconsider R={[0,0],[0,1]} as Relation by RELATION:2;take P,R;thus P c= Rprooflet x,y;assume [x,y] in P;then A1:[x,y] = [0,0] by ENUMSET:def 3;hence thesis by A1, ENUMSET:def 4;end;thus P is symmetricprooflet x,y;assume [x,y] in P;then [x,y] = [0,0] by ENUMSET:def 3;then x=0 & y=0 by ENUMSET:2;then [y,x]=[0,0];hence thesis by ENUMSET:def 3;end;thus not R is symmetricprooftake a=0,b=1;thus [a,b] in Rproof[0,1] in R by ENUMSET: def 4;hence thesis by ENUMSET: def 3;end;thus not [b,a] in Rproofassume F: [b,a] in R;H1: [0,1]<>[1,0] by ENUMSET:2;H2: [0,0]<>[1,0] by ENUMSET:2;then not [1,0] in R by H1,H2,ENUMSET: def 4;hence contradiction by F;end;end;end;::Zadanko 5ex P,R st P is asymmetric & R is asymmetric & P\/R is not asymmetricproofreconsider P={[0,1]} as Relation by RELATION:1;reconsider R={[1,0]} as Relation by RELATION:1;take P,R;thus P is asymmetricprooflet x,y;assume [x,y] in P;then [x,y] = [0,1] by ENUMSET:def 3;then x = 0 & y = 1 by ENUMSET:2;then [y,x] = [1,0];then [y,x] <> [0,1] by ENUMSET:2;hence thesis by ENUMSET:def 3;end;thus R is asymmetricprooflet x,y;assume [x,y] in R;then [x,y] = [1,0] by ENUMSET:def 3;then x = 1 & y = 0 by ENUMSET:2;then [y,x] = [0,1];then [y,x] <> [1,0] by ENUMSET:2;hence thesis by ENUMSET:def 3;end;thus P\/R is not asymmetricproofC1:[0,1] in P by ENUMSET:def 3;C2:[1,0] in R by ENUMSET:def 3;[0,1] in P\/R & [1,0] in P\/R by C1,C2, ENUMSET:def 6;hence thesis by RELATION:def 13;end;end;::> 70: Something remains to be proved [ Pobierz całość w formacie PDF ]