Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998
Association of Mizar Users
A Theory of Partitions. Part I

Shunichi Kobayashi

Shinshu University, Nagano

Kui Jia

Shinshu University, Nagano
Summary.

In this paper, we define join and meet operations between
partitions. The properties of these operations are proved.
Then we introduce the correspondence
between partitions and equivalence relations which preserve
join and meet operations.
The properties of these relationships are proved.
MML Identifier:
PARTIT1
The terminology and notation used in this paper have been
introduced in the following articles
[10]
[6]
[11]
[1]
[12]
[4]
[5]
[7]
[2]
[3]
[8]
[9]

Preliminaries

Join and Meet Operation Between Partitions

Partitions and Equivalence Relations
Bibliography
 [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek.
Minimal signature for partial algebra.
Journal of Formalized Mathematics,
7, 1995.
 [3]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
 [6]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
 [7]
Beata Padlewska.
Families of sets.
Journal of Formalized Mathematics,
1, 1989.
 [8]
Konrad Raczkowski and Pawel Sadowski.
Equivalence relations and classes of abstraction.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Alexander Yu. Shibakov and Andrzej Trybulec.
The Cantor set.
Journal of Formalized Mathematics,
7, 1995.
 [10]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [11]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [12]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received October 5, 1998
[
Download a postscript version,
MML identifier index,
Mizar home page]