environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
theorems ENUMSET;
begin
reserve A,B,C,M,X,Y,Z,U,a,b,c,x,y,z,u for set;
:: 2.107
for A,B holds
(A /\ B c= A & A /\ B c= B) &
(for X holds (X c= A & X c= B) implies X c= A /\ B)
proof
let A,B;
thus A /\ B c= A
proof
let a;
assume a in A /\ B;
hence a in A by ENUMSET:def 7;
end;
thus A /\ B c= B
proof
let a;
assume a in A /\ B;
hence a in B by ENUMSET:def 7;
end;
thus for X holds (X c= A & X c= B) implies X c= A /\ B
proof
let X;
assume X: X c= A & X c= B;
thus X c= A /\ B
proof
let x;
assume x in X;
then x in A & x in B by X,ENUMSET:def 10;
hence x in A /\ B by ENUMSET:def 7;
end;
end;
end;
:: 2.108
for A,B holds
(A c= A \/ B & B c= A \/ B) &
(for X st A c= X & B c= X holds A \/ B c= X)
proof
let A,B;
thus A c= A \/ B
proof
let a;
assume a in A;
hence a in A \/ B by ENUMSET:def 6;
end;
thus B c= A \/ B
proof
let a;
assume a in B;
hence a in A \/ B by ENUMSET:def 6;
end;
let X;
assume X: A c= X & B c= X;
thus A \/ B c= X
proof
let x;
assume x in A \/ B;
then x in A or x in B by ENUMSET:def 6;
hence x in X by X,ENUMSET:def 10;
end;
end;
:: 2.109
for A,B holds
(A \ B c= A & A \ B misses B) &
(for X st X c= A & X misses B holds X c= A \ B)
proof
let A,B;
thus A \ B c= A
proof
let a;
assume a in A \ B;
hence a in A by ENUMSET:def 8;
end;
thus A \ B misses B
proof
thus (A \ B) /\ B c= {}
proof
let a;
assume a in (A \ B) /\ B;
then a in A \ B & a in B by ENUMSET:def 7;
then a in A & not a in B & a in B by ENUMSET:def 8;
hence a in {};
end;
thus {} c= (A \ B) /\ B
proof
let a;
assume a in {};
hence a in (A \ B) /\ B by ENUMSET:def 1;
end;
end;
thus for X st X c= A & X misses B holds X c= A \ B
proof
let X;
assume X: X c= A & X misses B;
thus X c= A \ B
proof
let x;
assume x: x in X;
then
xa: x in A by X,ENUMSET:def 10;
not x in B
proof
assume x in B;
then x in X /\ B by x,ENUMSET:def 7;
then x in {} by X,ENUMSET:def 12;
hence thesis by ENUMSET:def 1;
end;
hence x in A \ B by xa,ENUMSET:def 8;
end;
end;
end;
union {A,B} = A \/ B
proof
thus union {A,B} c= A \/ B
proof
let a;
assume a in union {A,B};
then consider C such that
c: a in C & C in {A,B} by ENUMSET:def 13;
a in A or a in B by c,ENUMSET:def 4;
hence a in A \/ B by ENUMSET:def 6;
end;
thus A \/ B c= union {A,B}
proof
let a;
assume a in A \/ B;
then per cases by ENUMSET:def 6;
suppose a: a in A;
A in {A,B} by ENUMSET:def 4;
hence a in union {A,B} by a,ENUMSET:def 13;
end;
suppose a: a in B;
B in {A,B} by ENUMSET:def 4;
hence a in union {A,B} by a,ENUMSET:def 13;
end;
end;
end;
meet {A,B} = A /\ B
proof
A in {A,B} by ENUMSET:def 4;
then np: {A,B} <> {} by ENUMSET:def 1;
thus meet {A,B} c= A /\ B
proof
let a;
assume a: a in meet {A,B};
A in {A,B} & B in {A,B} by ENUMSET:def 4;
then a in A & a in B by a,ENUMSET:def 14,np;
hence a in A /\ B by ENUMSET:def 7;
end;
thus A /\ B c= meet {A,B}
proof
let a;
assume a in A /\ B;
then ab: a in A & a in B by ENUMSET:def 7;
for Y st Y in {A,B} holds a in Y
proof
let Y;
assume Y in {A,B};
then Y = A or Y = B by ENUMSET:def 4;
hence a in Y by ab;
end;
hence a in meet {A,B} by np,ENUMSET:def 14;
end;
end;
:: 6.28
X<>{} implies (for Y st Y in X holds meet X c= Y) &
for M st (for Y st Y in X holds M c= Y) holds M c= meet X
proof
assume X: X<>{};
thus for Y st Y in X holds meet X c= Y
proof
let Y;
assume yx: Y in X;
thus meet X c= Y
proof
let y;
assume y in meet X;
hence y in Y by yx,X,ENUMSET:def 14;
end;
end;
let M
such that m: for Y st Y in X holds M c= Y;
thus M c= meet X
proof
let x;
assume x: x in M;
for Z st Z in X holds x in Z
proof
let Z;
assume Z in X;
then M c= Z by m;
hence x in Z by x,ENUMSET:def 10;
end;
hence x in meet X by ENUMSET:def 14,X;
end;
end;
:: 6.29
(for Y st Y in X holds Y c= union X) &
for U st (for Y st Y in X holds Y c= U) holds union X c= U
proof
thus for Y st Y in X holds Y c= union X
proof
let Y;
assume y: Y in X;
thus Y c= union X
proof
let y;
assume y in Y;
hence y in union X by y,ENUMSET:def 13;
end;
end;
let U;
assume Y: for Y st Y in X holds Y c= U;
thus union X c= U
proof
let u;
assume u in union X;
then consider Y such that
y: u in Y & Y in X by ENUMSET:def 13;
Y c= U by Y,y;
hence u in U by y,ENUMSET:def 10;
end;
end;