Products

Dealing formally with products of families of sets is quite tedious work especially since everyday practice tends to sweep certain problems under the carpet. For instance, associativity of the Cartesian product

$$(X \times Y) \times Z = X \times (Y \times Z)$$

is often taken for granted and both sides of the equality are treated as being equal to $X \times Y \times Z$ which is understood as a set of triples. Formally, each of the three is a different entity although one can easily introduce the obvious isomorphisms among them. MML offers the following means for dealing with products of sets.

• The binary Cartesian product is defined in ZFMISC_1 [18] as a set of pairs.

  definition let X1,X2;
   func [: X1,X2 :] means                          :: ZFMISC_1:def 2
    z in it iff ex x,y st x in X1 & y in X2 & z = [x,y];
  end;
  

  We have also products of three sets [: X1,X2,X3 :] defined as [:[:X1,X2:],X3:], and of four sets [: X1,X2,X3,X4 :] defined as [:[:X1,X2,X3:],X4:].
• The product of an arbitrary family of sets is defined in CARD_3 [2].

  definition let f be Function;
    func product f -> set means                      :: CARD_3:def 5
     x in it iff ex g being Function st x = g & dom g = dom f &
                  for x st x in dom f holds g.x in f.x;
  end;
  

It is a bit surprising that despite some efforts at unifying the two notations (see FUNCT_6 [3]), they have not been unified completely. It turns out that trying to work with product <* X, Y *>, that is a product of a sequence of sets with length 2, needs quite an investment for developing additional constructors corresponding to the ones already existing for [: X, Y :].

At the start of the project, MML contained definitions for products for some algebraic structures (Abelian groups and universal algebras), but we had to define the product for relational structures in YELLOW_1 [26]

definition let I be set, J be RelStr-yielding ManySortedSet of I;
 func product J -> strict RelStr means               :: YELLOW_1:def 4
  the carrier of it = product Carrier J &
  for x,y being Element of the carrier of it st x in product Carrier J 
   holds x <= y iff 
         ex f, g being Function 
          st f = x & g = y &
             for i be set st i in I 
              ex R being RelStr, xi, yi being Element of R
               st R = J.i & xi = f.i & yi = g.i & xi <= yi;
end;

where the set I plays the role of an index set and Carrier is defined in PRALG_1 [38]

definition
 let J be set, A be 1-sorted-yielding ManySortedSet of J;
 func Carrier A -> ManySortedSet of J means          :: PRALG_1:def 13  
  for j being set st j in J
   ex R being 1-sorted st R = A.j & it.j = the carrier of R;
end;

(see Section  for more details).

Introducing the notions is only a small part of the tedious job of formalization and before the notions can be used conveniently, one has to prove quite a number of theorems giving the frequently used properties of the introduced notions. It is quite difficult to foresee all of the needed properties of these notions and thus their characterization is spread all over MML Recently, the MIZAR team has started a project to reorganize MML and put it into EMM - Encyclopedia of Mathematics in MIZAR. EMM will still consist of articles, albeit monographical in nature, and MML articles will be treated as ``raw'' material. At the time of this writing, only materials related to Boolean properties of sets in the spirit of the eliminated article BOOLE [57] are included in EMM as articles XBOOLE_0 and XBOOLE_1. Originally, the contents of these articles were spread over 17 MML articles. . Let us quote just one example of such a fact.

theorem                                                 :: YELLOW16:38 
 for I being non empty set,
     J, K being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds K.i is SubRelStr of J.i
   holds product K is SubRelStr of product J;

Similar to the product of two sets we have the product of two RelStrs defined in YELLOW_3 [33]

definition let X, Y be RelStr;
 func [: X, Y: ] -> strict RelStr means              :: YELLOW_3:def 2
  the carrier of it = [: the carrier of X, the carrier of Y :] &
  the InternalRel of it = 
                     [" the InternalRel of X, the InternalRel of Y "];
end;

where the product of two relations is also defined in YELLOW_3 [33]

definition let P, R be Relation;
 func [" P, R "] -> Relation means                   :: YELLOW_3:def 1
  for x, y being set 
   holds [x,y] in it iff
         ex p, q, s, t being set 
          st x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R;
end;

The same question we asked above for the product of two sets is also applicable here: could we have just one product for RelStr and express [: X,Y: ] as product <* X, Y *>? Probably the inertia of the MIZAR authors or lack of discipline is to be blamed for still having both of these notions. This situation indicates the kind of housekeeping work needed for maintaining a knowledge base for mathematics, especially when the base becomes sizable--MML is still minuscule from the viewpoint of a data base covering most of mathematics.

Products of topological structures are discussed in Section .