Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

## Basic Notions and Properties of Orthoposets

Markus Moschner
Saarland University
This paper was worked out while the author was visiting the University of Bia{\l}ystok in autumn 2002.

### Summary.

Orthoposets are defined. The approach is the standard one via order relation similar to common text books on algebra like [9].

This work has been partially supported by the CALCULEMUS project (FP5 grant HPRN-CT-2000-00102).

#### MML Identifier: OPOSET_1

The terminology and notation used in this paper have been introduced in the following articles [12] [14] [6] [3] [15] [17] [4] [16] [5] [13] [10] [8] [2] [7] [1] [11]

#### Contents (PDF format)

1. General Notions and Properties
2. Basic Poset Notions

#### Bibliography

[1] Grzegorz Bancerek. Bounds in posets and relational substructures. Journal of Formalized Mathematics, 8, 1996.
[2] Grzegorz Bancerek. Directed sets, nets, ideals, filters, and maps. Journal of Formalized Mathematics, 8, 1996.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Galois connections. Journal of Formalized Mathematics, 8, 1996.
[8] Adam Grabowski. Robbins algebras vs. Boolean algebras. Journal of Formalized Mathematics, 13, 2001.
[9] George Gr\"atzer. \em General Lattice Theory. Academic Press, New York, 1978.
[10] Michal Muzalewski. Construction of rings and left-, right-, and bi-modules over a ring. Journal of Formalized Mathematics, 2, 1990.
[11] Krzysztof Retel. The class of series --- parallel graphs. Journal of Formalized Mathematics, 14, 2002.
[12] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[13] Wojciech A. Trybulec. Partially ordered sets. Journal of Formalized Mathematics, 1, 1989.
[14] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[15] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[16] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.
[17] Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Journal of Formalized Mathematics, 1, 1989.

Received February 11, 2003

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