Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Tuples, Projections and Cartesian Products


Andrzej Trybulec
Warsaw University, Bialystok
Supported by RPBP.III-24.C1.

Summary.

The purpose of this article is to define projections of ordered pairs, and to introduce triples and quadruples, and their projections. The theorems in this paper may be roughly divided into two groups: theorems describing basic properties of introduced concepts and theorems related to the regularity, analogous to those proved for ordered pairs by Cz. Byli\'nski [1]. Cartesian products of subsets are redefined as subsets of Cartesian products.

MML Identifier: MCART_1

The terminology and notation used in this paper have been introduced in the following articles [3] [2] [1] [4]

Contents (PDF format)

Bibliography

[1] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[2] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
[3] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[4] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received March 30, 1989


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