Artykuł zawiera definicje zbioru pustego i aksjomaty (w sensie MizaraMSE) opisujące
należenie do zbiorów, zawieranie zbiorów, sumę, iloczyn i różnicę zbiorów.
Następnie przeprowadzone są dowody kilkunastu faktów dotyczących
wyżej wymienionych relacji i funkcji. Część twierdzeń zaczerpniętych została z [1].
Ze względu na brak możliwości definiowania funkcji w MizarzeMSE,
wszystkie twierdzenia musiały być sformułowane i udowodnione jedynie za pomocą rachunku predykatów.
Sekcje:
 Aksjomaty
 Podzbiory
 Suma zbiorów
 Iloczyn zbiorów
 Różnica zbiorów
Bibliografia:
[1] Library Committee: "Boolean Properties of Sets  Theorems",
Mizar Mathematical Library, 2002.
:::::::::::::::::::::::::::::::::::::
:: Written by Michal Trybulec 2007 ::
:::::::::::::::::::::::::::::::::::::
environ
:: Everything is a set:
sort set;
:: A set is an element of another set:
pred set in set;
:: A set is a subset of another set:
pred set subset_of set;
:: A set is the union of two sets:
pred set union_of set, set;
:: A set is the intersection of two sets:
pred set inter_of set, set;
:: A set is the difference of two sets:
pred set diff_of set, set;
reserve x, y, z, A, B, C for set;
:: The empty set is a set with no elements in it:
given empty being set such that
AxEmpty:
not ex x st x in empty;
:: Two sets are equal if exactly the same elements are in both sets:
AxEquality:
for A, B holds
A = B iff
for x holds x in A iff x in B;
:: A set is a subset of another set
:: if all its elements are also in the other set:
AxSubset:
for A, B holds
A subset_of B iff
for x st x in A holds x in B;
:: A set is the union of two sets if each of its elements
:: is in one of those two sets:
AxUnion:
for A, B, C holds
A union_of B, C iff
for x holds x in A iff x in B or x in C;
:: A set is the intersection of two sets if each of its elements
:: is in both of those two sets:
AxInter:
for A, B, C holds
A inter_of B, C iff
for x holds x in A iff x in B & x in C;
:: A set is the difference of two sets if it includes
:: only those elements of the first set that are not in the second set:
AxDiff:
for A, B, C holds
A diff_of B, C iff
for x holds x in A iff x in B & not x in C;
begin
:::::::::::::::::::::::::::::::::::::
:: Subsets ::
:::::::::::::::::::::::::::::::::::::
:: The empty set is a subset of all sets.
:: {} c= A;
ThSubset10:
for A holds empty subset_of A
proof
let A;
now
let x;
assume x in empty;
hence x in A by AxEmpty;
end;
hence thesis by AxSubset;
end;
:: A set is a subset of itself (reflexivity of the subset relation).
:: A c= A;
ThSubset20:
for A holds A subset_of A
proof
let A;
now
let x;
assume x in A;
hence x in A;
end;
hence thesis by AxSubset;
end;
:: Another proof of A c= A  by contradiction.
ThSubset20':
for A holds A subset_of A
proof
let A;
assume not A subset_of A;
then ex x st x in A & not x in A by AxSubset;
then consider x such that
L: x in A & not x in A;
thus contradiction by L;
end;
:: If B is a subset of A, and C is a subset of B,
:: then C is a subset of A (transitivity of the subset relation).
:: A c= B & B c= C implies A c= C;
ThSubset30:
for A, B, C st C subset_of B & B subset_of A holds C subset_of A
proof
let A, B, C;
assume
A: C subset_of B & B subset_of A;
BA:
for x st x in B holds x in A by A, AxSubset;
CB:
for x st x in C holds x in B by A, AxSubset;
now
let x;
assume x in C;
then x in B by CB, AxSubset;
hence x in A by BA, AxSubset;
end;
hence thesis by AxSubset;
end;
:: If two sets are each other's subsets, then they are equal
:: (antisymmetry of the subset relation).
:: A c= B & B c= A iff A = B;
ThSubset40:
for A, B holds A subset_of B & B subset_of A iff A = B
proof
let A, B;
thus A subset_of B & B subset_of A implies A = B
proof
assume
A: A subset_of B & B subset_of A;
BA: for x st x in B holds x in A by A, AxSubset;
AB: for x st x in A holds x in B by A, AxSubset;
now
let x;
thus x in A iff x in B by AB, BA;
end;
hence thesis by AxEquality;
end;
assume A = B;
then
A: for x holds x in A iff x in B by AxEquality;
AB:
now
let x;
thus x in A implies x in B by A;
end;
BA:
now
let x;
thus x in B implies x in A by A;
end;
thus thesis by AB, BA, AxSubset;
end;
:: If a set is a subset of the empty set, it is itself empty.
:: A c= {} implies A = {};
ThSubset50:
for A st A subset_of empty holds A = empty
proof
let A;
assume
A: A subset_of empty;
empty subset_of A by ThSubset10;
hence thesis by A, ThSubset40;
end;
:::::::::::::::::::::::::::::::::::::
:: Union ::
:::::::::::::::::::::::::::::::::::::
:: The union of a set with itself is the set itself.
:: A \/ A = A;
ThUnion10:
for A holds A union_of A, A
proof
let A;
now
let x;
thus x in A iff x in A or x in A;
end;
hence thesis by AxUnion;
end;
:: The order of the sets in the union is irrelevant
:: (commutativity of the union function).
:: A \/ B = B \/ A;
ThUnion20:
for A, B, C st C union_of A, B holds C union_of B, A
proof
let A, B, C;
assume C union_of A, B;
then
A: for x holds x in C iff x in A or x in B by AxUnion;
now
let x;
thus x in C iff x in B or x in A by A;
end;
hence thesis by AxUnion;
end;
:: The union of a set with its subset is the set itself.
:: A c= B implies A \/ B = B;
ThUnion30:
for A, B st A subset_of B holds B union_of A, B
proof
let A, B;
assume A subset_of B;
then
A: for x st x in A holds x in B by AxSubset;
now
let x;
thus x in B iff x in A or x in B by A;
end;
hence thesis by AxUnion;
end;
:: The union of a set and the empty set is the set itself.
:: {} \/ A = A;
ThUnion40:
for A holds A union_of empty, A
proof
let A;
empty subset_of A by ThSubset10;
hence thesis by ThUnion30;
end;
:: If the union of two sets is empty, then both sets are empty.
:: {} = A \/ B implies A = {};
ThUnion50:
for A, B st empty union_of A, B holds A = empty
proof
let A, B;
assume empty union_of A, B;
then
A: for x holds x in empty iff x in A or x in B by AxUnion;
now
let x;
assume x in A;
hence x in empty by A;
end;
then
B: A subset_of empty by AxSubset;
empty subset_of A by ThSubset10;
hence thesis by B, ThSubset40;
end;
:: Associativity of the union function.
:: (A \/ B) \/ C = A \/ (B \/ C);
ThUnion60:
for A, B, C, AB, BC, D being set st
AB union_of A, B & BC union_of B, C holds
D union_of AB, C iff D union_of A, BC
proof
let A, B, C, AB, BC, D be set;
assume
A: AB union_of A, B & BC union_of B, C;
AB:
for x holds x in AB iff x in A or x in B by A, AxUnion;
BC:
for x holds x in BC iff x in B or x in C by A, AxUnion;
thus D union_of AB, C implies D union_of A, BC
proof
assume D union_of AB, C;
then
DAB: for x holds x in D iff x in AB or x in C by AxUnion;
now
let x;
x in D iff x in AB or x in C by DAB;
then x in D iff x in A or x in B or x in C by AB;
hence x in D iff x in A or x in BC by BC;
end;
hence thesis by AxUnion;
end;
assume D union_of A, BC;
then
DBC:
for x holds x in D iff x in A or x in BC by AxUnion;
now
let x;
x in D iff x in A or x in BC by DBC;
then x in D iff x in A or x in B or x in C by BC;
hence x in D iff x in AB or x in C by AB;
end;
hence thesis by AxUnion;
end;
:: A \/ B = A \/ (A \/ B):
ThUnion70:
for A, B, AB, AAB being set st
AB union_of A, B & AAB union_of A, AB holds
AB = AAB
proof
let A, B, AB, AAB be set;
assume
A: AB union_of A, B & AAB union_of A, AB;
AB:
for x holds x in AB iff x in A or x in B by A, AxUnion;
AAB:
for x holds x in AAB iff x in A or x in AB by A, AxUnion;
for x holds x in AB iff x in AAB
proof
let x;
thus x in AB implies x in AAB by AAB;
assume x in AAB;
then x in A or x in AB by AAB;
hence thesis by AB;
end;
hence thesis by AxEquality;
end;
:: Both arguments of the union function are subsets of the result.
:: A \/ B = C implies A c= C;
ThUnion80:
for A, B, C st C union_of A, B holds A subset_of C
proof
let A, B, C;
assume C union_of A, B;
then
A: for x holds x in C iff x in A or x in B by AxUnion;
now
let x;
assume x in A;
hence x in C by A;
end;
hence thesis by AxSubset;
end;
:: The union of two subsets of a set is too a subset of this set.
:: A c= C & B c= C implies A \/ B c= C;
ThUnion90:
for A, B, C, AB being set st
AB union_of A, B & A subset_of C & B subset_of C holds
AB subset_of C
proof
let A, B, C, AB be set;
assume
A: AB union_of A, B & A subset_of C & B subset_of C;
AB:
for x holds x in AB iff x in A or x in B by A, AxUnion;
AC:
for x st x in A holds x in C by A, AxSubset;
BC:
for x st x in B holds x in C by A, AxSubset;
now
let x;
assume x in AB;
then x in A or x in B by AB;
hence x in C by AC, BC;
end;
hence thesis by AxSubset;
end;
:::::::::::::::::::::::::::::::::::::
:: Intersection ::
:::::::::::::::::::::::::::::::::::::
:: The intersection of a set with itself is the set itself.
:: A /\ A = A;
ThInter10:
for A holds A inter_of A, A
proof
let A;
now
let x;
thus x in A iff x in A & x in A;
end;
hence thesis by AxInter;
end;
:: The order of the sets in the intersection is irrelevant
:: (commutativity of the intersection function).
:: A /\ B = B /\ A;
ThInter20:
for A, B, C st C inter_of A, B holds C inter_of B, A
proof
let A, B, C;
assume C inter_of A, B;
then
A: for x holds x in C iff x in A & x in B by AxInter;
now
let x;
thus x in C iff x in B & x in A by A;
end;
hence thesis by AxInter;
end;
:: The intersection of a set with its subset is the subset.
:: A c= B implies A /\ B = A;
ThInter30:
for A, B st A subset_of B holds A inter_of A, B
proof
let A, B;
assume A subset_of B;
then
A: for x st x in A holds x in B by AxSubset;
now
let x;
thus x in A iff x in A & x in B by A;
end;
hence thesis by AxInter;
end;
:: The intersection of a set and the empty set is empty.
:: {} /\ A = {};
ThInter40:
for A holds empty inter_of empty, A
proof
let A;
empty subset_of A by ThSubset10;
hence thesis by ThInter30;
end;
:: Associativity of the intersection function.
:: (A /\ B) /\ C = A /\ (B /\ C);
ThInter60:
for A, B, C, AB, BC, D being set st
AB inter_of A, B & BC inter_of B, C holds
D inter_of AB, C iff D inter_of A, BC
proof
let A, B, C, AB, BC, D be set;
assume
A: AB inter_of A, B & BC inter_of B, C;
AB:
for x holds x in AB iff x in A & x in B by A, AxInter;
BC:
for x holds x in BC iff x in B & x in C by A, AxInter;
thus D inter_of AB, C implies D inter_of A, BC
proof
assume D inter_of AB, C;
then
DAB: for x holds x in D iff x in AB & x in C by AxInter;
now
let x;
x in D iff x in AB & x in C by DAB;
then x in D iff x in A & x in B & x in C by AB;
hence x in D iff x in A & x in BC by BC;
end;
hence thesis by AxInter;
end;
assume D inter_of A, BC;
then
DBC:
for x holds x in D iff x in A & x in BC by AxInter;
now
let x;
x in D iff x in A & x in BC by DBC;
then x in D iff x in A & x in B & x in C by BC;
hence x in D iff x in AB & x in C by AB;
end;
hence thesis by AxInter;
end;
:: A /\ B = A /\ (A /\ B):
ThInter70:
for A, B, AB, AAB being set st
AB inter_of A, B & AAB inter_of A, AB holds
AB = AAB
proof
let A, B, AB, AAB be set;
assume
A: AB inter_of A, B & AAB inter_of A, AB;
AB:
for x holds x in AB iff x in A & x in B by A, AxInter;
AAB:
for x holds x in AAB iff x in A & x in AB by A, AxInter;
for x holds x in AB iff x in AAB
proof
let x;
thus x in AB implies x in AAB
proof
assume
C: x in AB;
then x in A & x in B by AB;
hence thesis by C, AAB;
end;
assume x in AAB;
then x in A & x in AB by AAB;
hence thesis by AB;
end;
hence thesis by AxEquality;
end;
:: Both arguments of the intersection function are supersets of the result.
:: A /\ B = C implies C c= A;
ThInter80:
for A, B, C st C inter_of A, B holds C subset_of A
proof
let A, B, C;
assume C inter_of A, B;
then
A: for x holds x in C iff x in A & x in B by AxInter;
now
let x;
assume x in C;
hence x in A by A;
end;
hence thesis by AxSubset;
end;
:: The intersection of two supersets of a set is too a superset of this set.
:: C c= A & C c= B implies C c= A /\ B;
ThInter90:
for A, B, C, AB being set st
AB inter_of A, B & C subset_of A & C subset_of B holds
C subset_of AB
proof
let A, B, C, AB be set;
assume
A: AB inter_of A, B & C subset_of A & C subset_of B;
AB:
for x holds x in AB iff x in A & x in B by A, AxInter;
AC:
for x st x in C holds x in A by A, AxSubset;
BC:
for x st x in C holds x in B by A, AxSubset;
now
let x;
assume x in C;
then x in A & x in B by AC, BC;
hence x in AB by AB;
end;
hence thesis by AxSubset;
end;
:: Distributiveness of intersection over union:
:: A /\ (B \/ C) = (A /\ B) \/ (A /\ C);
for A, B, C, BuC, AiB, AiC, AiBuC, AuBiAuC being set st
AiBuC inter_of A, BuC & BuC union_of B, C &
AuBiAuC union_of AiB, AiC & AiB inter_of A, B & AiC inter_of A, C holds
AiBuC = AuBiAuC
proof
let A, B, C, BuC, AiB, AiC, AiBuC, AiBuAiC be set such that
A: AiBuC inter_of A, BuC & BuC union_of B, C &
AiBuAiC union_of AiB, AiC & AiB inter_of A, B & AiC inter_of A, C;
AiBuC:
for x holds x in AiBuC iff x in A & x in BuC by A, AxInter;
BuC:
for x holds x in BuC iff x in B or x in C by A, AxUnion;
AiBuAiC:
for x holds x in AiBuAiC iff x in AiB or x in AiC by A, AxUnion;
AiB:
for x holds x in AiB iff x in A & x in B by A, AxInter;
AiC:
for x holds x in AiC iff x in A & x in C by A, AxInter;
for x holds x in AiBuC iff x in AiBuAiC
proof
let x;
thus x in AiBuC implies x in AiBuAiC
proof
assume x in AiBuC;
then x in A & x in BuC by AiBuC;
then x in A & (x in B or x in C) by BuC;
then x in A & x in B or x in A & x in C;
then x in AiB or x in A & x in C by AiB;
then x in AiB or x in AiC by AiC;
hence thesis by AiBuAiC;
end;
assume x in AiBuAiC;
then x in AiB or x in AiC by AiBuAiC;
then x in AiB or x in A & x in C by AiC;
then x in A & x in B or x in A & x in C by AiB;
then x in A & (x in B or x in C);
then x in A & x in BuC by BuC;
hence thesis by AiBuC;
end;
hence thesis by AxEquality;
end;
:: Distributiveness of union over intersection:
:: A \/ (B /\ C) = (A \/ B) /\ (A \/ C);
for A, B, C, BiC, AuB, AuC, AuBiC, AuBiAuC being set st
AuBiC union_of A, BiC & BiC inter_of B, C &
AuBiAuC inter_of AuB, AuC & AuB union_of A, B & AuC union_of A, C holds
AuBiC = AuBiAuC
proof
let A, B, C, BiC, AuB, AuC, AuBiC, AuBiAuC be set such that
A: AuBiC union_of A, BiC & BiC inter_of B, C &
AuBiAuC inter_of AuB, AuC & AuB union_of A, B & AuC union_of A, C;
AuBiC:
for x holds x in AuBiC iff x in A or x in BiC by A, AxUnion;
BiC:
for x holds x in BiC iff x in B & x in C by A, AxInter;
AuBiAuC:
for x holds x in AuBiAuC iff x in AuB & x in AuC by A, AxInter;
AuB:
for x holds x in AuB iff x in A or x in B by A, AxUnion;
AuC:
for x holds x in AuC iff x in A or x in C by A, AxUnion;
for x holds x in AuBiC iff x in AuBiAuC
proof
let x;
thus x in AuBiC implies x in AuBiAuC
proof
assume x in AuBiC;
then x in A or x in BiC by AuBiC;
then x in A or (x in B & x in C) by BiC;
then (x in A or x in B) & (x in A or x in C);
then x in AuB & (x in A or x in C) by AuB;
then x in AuB & x in AuC by AuC;
hence thesis by AuBiAuC;
end;
assume x in AuBiAuC;
then x in AuB & x in AuC by AuBiAuC;
then x in AuB & (x in A or x in C) by AuC;
then (x in A or x in B) & (x in A or x in C) by AuB;
then x in A or (x in B & x in C);
then x in A or x in BiC by BiC;
hence thesis by AuBiC;
end;
hence thesis by AxEquality;
end;
:::::::::::::::::::::::::::::::::::::
:: Difference ::
:::::::::::::::::::::::::::::::::::::
:: The difference of a set and its superset is an empty set:
:: A c= B implies A \ B = {}
ThDiff10:
for A, B st A subset_of B holds empty diff_of A, B
proof
let A, B;
assume A subset_of B;
then
A: for x st x in A holds x in B by AxSubset;
now
let x;
thus x in empty iff x in A & not x in B
proof
thus x in empty implies x in A & not x in B
proof
assume x in empty;
hence x in A & not x in B by AxEmpty;
end;
assume x in A & not x in B;
hence x in empty by A;
end;
end;
hence thesis by AxDiff;
end;
:: The difference of an empty set and a set is an empty set:
:: {} \ A = {}
ThDiff20:
for A holds empty diff_of empty, A
proof
let A;
empty subset_of A by ThSubset10;
hence thesis by ThDiff10;
end;
:: If two sets have no common elements, their difference is equal to the first set:
:: A /\ B = {} implies A = A \ B
ThDiff30:
for A, B st empty inter_of A, B holds A diff_of A, B
proof
let A, B;
assume empty inter_of A, B;
then
A: for x holds x in empty iff x in A & x in B by AxInter;
B:
not ex x st x in A & x in B
proof
assume ex x st x in A & x in B;
then consider x such that
C: x in A & x in B;
x in empty by A, C;
hence contradiction by AxEmpty;
end;
now
let x;
thus x in A iff x in A & not x in B
proof
thus x in A implies x in A & not x in B
proof
assume x in A;
hence x in A & not x in B by B;
end;
assume x in A & not x in B;
hence x in A;
end;
end;
hence thesis by AxDiff;
end;
:: The difference of a set and an empty set is the set itself:
:: A = A \ {}
ThDiff40:
for A holds A diff_of A, empty
proof
let A;
empty inter_of empty, A by ThInter40;
then empty inter_of A, empty by ThInter20;
hence thesis by ThDiff30;
end;
:: The difference of a set with that set is an empty set:
:: A \ A = {}
ThDiff50:
for A holds empty diff_of A, A
proof
let A;
A subset_of A by ThSubset20;
hence thesis by ThDiff10;
end;
:: The difference of two sets is a subsets of the first set:
:: A \ B c= A
ThDiff60:
for A, B, AmB being set st AmB diff_of A, B holds AmB subset_of A
proof
let A, B, AmB be set;
assume AmB diff_of A, B;
then
A: for x holds x in AmB iff x in A & not x in B by AxDiff;
now
let x;
assume x in AmB;
hence x in A by A;
end;
hence thesis by AxSubset;
end;
:: The intersection of the difference of two sets with the second set is an empty set:
:: (A \ B) /\ B = {}
ThDiff70:
for A, B, AmB being set st AmB diff_of A, B holds empty inter_of AmB, B
proof
let A, B, AmB be set;
assume AmB diff_of A, B;
then
A: for x holds x in AmB iff x in A & not x in B by AxDiff;
now
let x;
thus x in empty iff x in AmB & x in B
proof
thus x in empty implies x in AmB & x in B
proof
assume x in empty;
hence x in AmB & x in B by AxEmpty;
end;
assume x in AmB & x in B;
hence x in empty by A;
end;
end;
hence thesis by AxInter;
end;
:: The difference of the difference of two sets and the second set
:: is equal to the difference of these two sets:
:: (A \ B) \ B = A \ B
ThDiff80:
for A, B, AmB being set st AmB diff_of A, B holds AmB diff_of AmB, B
proof
let A, B, AmB be set;
assume AmB diff_of A, B;
then
A: for x holds x in AmB iff x in A & not x in B by AxDiff;
now
let x;
thus x in AmB iff x in AmB & not x in B
proof
thus x in AmB implies x in AmB & not x in B
proof
assume x in AmB;
hence thesis by A;
end;
assume x in AmB & not x in B;
hence x in AmB;
end;
end;
hence thesis by AxDiff;
end;
Góra
