Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003
Association of Mizar Users
On the Sets Inhabited by Numbers

Andrzej Trybulec

University of Bialystok
Summary.

The information that all members of a set enjoy a property expressed
by an adjective can be processed in a systematic way. The purpose
of the work is to find out how to do that. If it works, `membered'
will become a reserved word and the work with it will be automated.
I have chosen {\it membered} rather than {\it inhabited} because of
the compatibility with the Automath terminology.
The phrase $\tau$ {\it inhabits}
$\theta$ could be translated to $\tau$ {\bfseries\itshape is}
$\theta$ in Mizar.
This work has been partially supported by the CALCULEMUS
grant HPRNCT200000102.
The terminology and notation used in this paper have been
introduced in the following articles
[5]
[8]
[4]
[6]
[3]
[7]
[1]
[2]
Contents (PDF format)
Acknowledgments
I am grateful to Dr. Czeslaw Bylinski for the discussion,
particularly for his advice to prove more trivial but useful theorems.
Bibliography
 [1]
Grzegorz Bancerek.
The ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek.
Sequences of ordinal numbers.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Andrzej Kondracki.
Basic properties of rational numbers.
Journal of Formalized Mathematics,
2, 1990.
 [4]
Beata Padlewska.
Families of sets.
Journal of Formalized Mathematics,
1, 1989.
 [5]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
 [6]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
 [7]
Michal J. Trybulec.
Integers.
Journal of Formalized Mathematics,
2, 1990.
 [8]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received August 23, 2003
[
Download a postscript version,
MML identifier index,
Mizar home page]