Products

Products of lattices augmented with a topology are treated by separating the relational product from the topological product. The product of a family of sets and the product of a family of relational structures were discussed in Section . The product of a family of topological spaces is defined in WAYBEL18 [27] as

definition let I be set, 
               J be TopSpace-yielding non-Empty ManySortedSet of I;
 func product J -> strict TopSpace means             :: WAYBEL18:def 3 
  the carrier of it = product Carrier J &
  product_prebasis J is prebasis of it;
end;

and we will not venture into the details of the definiens.

Item 3.4 from [25, p. 122] uses both products, the algebraic and the topological.

3.4. Lemma. (i) For every set $M$ we have $\Sigma (2^M) = (\Sigma 2)^M$; that is the Scott topology on $2^M$ and the product topology agree. ...

This fact is formalized as follows

theorem                                                 :: WAYBEL18:16
for I being non empty set,
    T being Scott TopAugmentation of product (I --> BoolePoset 1) 
holds
 the topology of T = the topology of product (I --> Sierpinski_Space);

where BoolePoset 1 is a RelStr with carrier equal to 2 ordered by inclusion. Natural numbers in MIZAR are von Neumann ordinals and thus: 0 = {}, 1 = {{}}, 2 = { {}, {{}} } ( = bool 1), and so on. Therefore I --> BoolePoset 1 is RelStr-yielding and the product of the latter is the relational product as mentioned on p. .

Sierpinski_Space is a topological space equal to TopStruct(# 2, 3 #) defined as

definition
 func Sierpinski_Space -> strict TopStruct means     :: WAYBEL18:def 9 
  the carrier of it = {0,1} &
  the topology of it = {{}, {1}, {0,1} };
end;

Hence, an indexed set of such spaces I --> Sierpinski_Space is TopSpace yielding and its product is the topological product mentioned above.

This overloading of product is very convenient but also potentially troublesome; namely, if M is a ManySortedSet and M has both the RelStr- and TopSpace-yielding attributes, then there is a question of whether product M is the relational product or the topological product? Currently in MIZAR the answer depends on the context which is controlled by the text author. However, there is no way to directly say which product is meant and this situation is not satisfactory. The way around the problem is to define synonyms for both products that will distinguish them notationally, see WAYBEL26 [15].

definition
 let I be set, J be RelStr-yielding ManySortedSet of I;
 redefine func product J; 
 synonym I-POS_prod J;
end;

definition
 let I be set, J be TopSpace-yielding non-Empty ManySortedSet of I;
 redefine func product J; 
 synonym I-TOP_prod J;
end;