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]