Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

**Andrzej Trybulec**- Warsaw University, Bialystok

- The article deals with parameterized families of sets. When treated in a similar way as sets (due to systematic overloading notation used for sets) they are called many sorted sets. For instance, if $x$ and $X$ are two many-sorted sets (with the same set of indices $I$) then relation $x \in X$ is defined as $\forall_{i \in I} x_i \in X_i$.\par I was prompted by a remark in a paper by Tarlecki and Wirsing: ``Throughout the paper we deal with many-sorted sets, functions, relations etc. ... We feel free to use any standard set-theoretic notation without explicit use of indices'' [6, p. 97]. The aim of this work was to check the feasibility of such approach in Mizar. It works.\par Let us observe some peculiarities: \begin{itemize} \item[-] empty set (i.e. the many sorted set with empty set of indices) belongs to itself (theorem 133), \item[-] we get two different inclusions $X \subseteq Y$ iff $\forall_{i \in I} X_i \subseteq Y_i$ and $X \sqsubseteq Y$ iff $\forall_x x \in X \Rightarrow x \in Y$ equivalent only for sets that yield non empty values. \end{itemize} Therefore the care is advised.

- Preliminaries
- Lattice Properties of Many Sorted Sets
- The Empty Many Sorted Set
- The Difference and the Symmetric Difference
- Meeting and Overlapping
- The Second Inclusion
- Non empty set of sorts
- Non Empty and Non-empty Many Sorted Sets

- [1]
Grzegorz Bancerek.
Cardinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Czeslaw Bylinski.
A classical first order language.
*Journal of Formalized Mathematics*, 2, 1990. - [4]
Katarzyna Jankowska.
Matrices. Abelian group of matrices.
*Journal of Formalized Mathematics*, 3, 1991. - [5]
Yatsuka Nakamura and Andrzej Trybulec.
A mathematical model of CPU.
*Journal of Formalized Mathematics*, 4, 1992. - [6] Andrzej Tarlecki and Martin Wirsing. Continuous abstract data types. \em Fundamenta Informaticae, 9(1):95--125, 1986.
- [7]
Andrzej Trybulec.
Binary operations applied to functions.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [9]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]