environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
theorems ENUMSET;
begin
reserve A,B,C,X,Y,Z,a,b,c,x,y,z for set;
::2.90
for A,B,C holds A\(B\/C) = (A\B)/\(A\C)
proof
let A,B,C be set;
thus A\(B\/C) c= (A\B)/\(A\C)
proof
let a be set;
assume a in A\(B\/C);
then a in A & not a in B \/ C by ENUMSET:def 8;
then a in A & not a in B & a in A & not a in C by ENUMSET:def 6;
then a in A\B & a in A\C by ENUMSET:def 8;
hence a in (A\B)/\(A\C) by ENUMSET:def 7;
end;
thus (A\B)/\(A\C) c= A\(B\/C)
proof
let a be set;
assume a in (A\B)/\(A\C);
then a in A\B & a in A\C by ENUMSET:def 7;
then a in A & not a in B & a in A & not a in C by ENUMSET:def 8;
then a in A & not a in (B\/C) by ENUMSET:def 6;
hence a in A\(B\/C) by ENUMSET:def 8;
end;
end;
::2.76
for A holds A \/ {} = A
proof
let A be set;
thus A \/ {} c= A
proof
let a be set;
assume a in A \/ {};
then a in A or a in {} by ENUMSET:def 6;
then a in A by ENUMSET:def 1;
hence a in A;
end;
thus A c= A \/ {}
proof
let a be set;
assume a in A;
hence a in A \/ {} by ENUMSET:def 6;
end;
end;
::2.76
A \/ {} = A
proof
thus A \/ {} c= A
proof
let a be set;
assume a in A \/ {};
then a in A or a in {} by ENUMSET:def 6;
hence a in A by ENUMSET:def 1;
end;
let a be set;
assume a in A;
hence a in A \/ {} by ENUMSET:def 6;
end;
::2.92
::not for A,B holds A /\ (A\/B) = B;
ex A,B st A /\ (A\/B) <> B
proof
take A={};
take B={1};
not 1 in A by ENUMSET:def 1;
then
j: not 1 in A /\ (A\/B) by ENUMSET:def 7;
1 in B by ENUMSET:def 3;
then not B c= A /\ (A\/B) by j,ENUMSET:def 10;
hence A /\ (A\/B) <> B by ENUMSET:def 11;
end;
::2.100 prawdziwa jest tylko implikacja w jedn± stronę, w drug± zdanie jest fałszywe - poniżej jest kontrprzykład
::(A c= B) iff (for C holds (B c= C) implies (C\A) /\ (C\B) = C\B)
(A c= B) implies ((B c= C) implies (C\A) /\ (C\B) = C\B)
proof
assume a: A c= B;
assume b: B c= C;
thus (C\A) /\ (C\B) c= C\B
proof
let a;
assume a in (C\A) /\ (C\B);
hence a in C\B by ENUMSET:def 7;
end;
thus C\B c= (C\A) /\ (C\B)
proof
let a;
assume a in C\B;
then a in C & not a in B by ENUMSET:def 8;
then a in C & not a in A & a in C & not a in B by a,ENUMSET:def 10;
then a in C\A & a in C\B by ENUMSET:def 8;
hence a in (C\A) /\ (C\B) by ENUMSET:def 7;
end;
end;
ex A,B,C st not (((B c= C) implies (C\A) /\ (C\B) = C\B) implies (A c= B))
proof
take A={1},B={},C={};
i: (B c= C) implies (C\A) /\ (C\B)= C\B
proof
assume b: B c= C;
thus (C\A) /\ (C\B) c= C\B
proof
let a;
assume a in (C\A) /\ (C\B);
hence a in C\B by ENUMSET:def 7;
end;
thus C\B c= (C\A) /\ (C\B)
proof
let a;
assume a in C\B;
then a in C & not a in B by ENUMSET:def 8;
hence thesis by ENUMSET:def 1;
end;
end;
1 in A & not 1 in B by ENUMSET:def 1,def 3;
then not A c= B by ENUMSET:def 10;
hence thesis by i;
end;
::2.100 Prawdziwe jest natomiast zdanie z kwantyfikatorem zbioru C po prawej stronie równoważno¶ci
(A c= B) iff (for C holds (B c= C) implies (C\A) /\ (C\B) = C\B)
proof
thus (A c= B) implies (for C holds (B c= C) implies (C\A) /\ (C\B) = C\B)
proof
assume a: A c= B;
let C;
assume b: B c= C;
thus (C\A) /\ (C\B) c= C\B
proof
let a;
assume a in (C\A) /\ (C\B);
hence a in C\B by ENUMSET:def 7;
end;
thus C\B c= (C\A) /\ (C\B)
proof
let a;
assume a in C\B;
then a in C & not a in B by ENUMSET:def 8;
then a in C & not a in B & a in C & not a in A by a,ENUMSET:def 10;
then a in (C\A) & a in (C\B) by ENUMSET:def 8;
hence thesis by ENUMSET:def 7;
end;
end;
thus (for C holds (B c= C) implies (C\A) /\ (C\B) = C\B) implies (A c= B)
proof
assume i: for C holds (B c= C) implies (C\A) /\ (C\B) = C\B;
let a;
assume a: a in A;
assume nb: not a in B;
set C = B \/ {a};
B c= C
proof
let b;
assume b in B;
hence b in C by ENUMSET:def 6;
end;
then ca: (C\A) /\ (C\B) = C\B by i;
a in {a} by ENUMSET:def 3;
then a in C by ENUMSET:def 6;
then a in C\B by nb,ENUMSET:def 8;
then a in (C\A) /\ (C\B) by ca,ENUMSET:1;
then a in C\A by ENUMSET:def 7;
hence contradiction by a,ENUMSET:def 8;
end;
end;