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

Relations and Their Basic Properties

Edmund Woronowicz
Warsaw University, Bialystok
Supported by RPBP.III-24.C1


We define here: mode Relation as a set of pairs, the domain, the codomain, and the field of relation; the empty and the identity relations, the composition of relations, the image and the inverse image of a set under a relation. Two predicates, = and $\subseteq$, and three functions, $\cup$, $\cap$ and $\setminus$ are redefined. Basic facts about the above mentioned notions are presented.

MML Identifier: RELAT_1

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

Contents (PDF format)


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

Received March 15, 1989

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