Caves Travel Diving Graphics Mizar Texts Cuisine Lemkov Contact Map RSS Polski
Trybiks' Dive Mizar Articles Boolean Properties of Sets YAC Software
  Back

Mizar

Eddie

Articles

Equivalence of Deterministic and Epsilon Nondeterministic Automata

Labelled State Transition Systems

Regular Expression Quantifiers - at least m Occurrences

String Rewriting Systems

Regular Expression Quantifiers - m to n Occurrences

Formal Languages- Concatenation and Closure

Boolean Properties of Sets

Homomorphisms and Isomorphisms of Groups; Quotient Group

Integers

Mizar-MSE Syntax

Boolean Properties of Sets
The article contains the definition of the empty set and (Mizar-MSE) axioms that introduce elements of sets, set inclusion, the union, intersection, and difference of sets. Next, several facts concerning the above mentioned relations and functions are proved. Some of the theorems were taken from [1].

Because functions cannot be defined in Mizar-MSE, all theorems had to be formulated and proved using predicate calculus only.

Sections:
  • Axioms
  • Subsets
  • Union of Sets
  • Intersection of Sets
  • Difference of Sets
Bibliography:
[1] Library Committee: "Boolean Properties of Sets - Theorems", Mizar Mathematical Library, 2002.

Full article
                 :::::::::::::::::::::::::::::::::::::
                 :: 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;


Top