Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

Miscellaneous Facts about Relation Structure

Agnieszka Julia Marasik
Warsaw University, Bialystok


In the article notation and facts necessary to start with formalization of continuous lattices according to [5] are introduced.

This work was partially supported by the Office of Naval Research Grant N00014-95-1-1336.

MML Identifier: YELLOW_5

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

Contents (PDF format)

  1. Introduction
  2. Difference in Relation Structure
  3. Lower-bound in Relation Structure
  4. Boolean Lattices


[1] Grzegorz Bancerek. Complete lattices. Journal of Formalized Mathematics, 4, 1992.
[2] Grzegorz Bancerek. Bounds in posets and relational substructures. Journal of Formalized Mathematics, 8, 1996.
[3] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Journal of Formalized Mathematics, 8, 1996.
[4] Czeslaw Bylinski. Galois connections. Journal of Formalized Mathematics, 8, 1996.
[5] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. \em A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York, 1980.
[6] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.

Received November 8, 1996

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