The Lattice of Real Numbers. The Lattice of Real Functions

Marek Chmur

Warsaw University, Bialystok

Supported by RPBP.III-24.C1.

Summary.

A proof of the fact, that $\llangle {\Bbb R}, {\rm max}, {\rm min} \rrangle$ is a lattice (real lattice). Some basic properties (real lattice is distributive and modular) of it are proved. The same is done for the set ${\Bbb R}^A$ with operations: max($f(A)$) and min($f(A)$), where ${\Bbb R}^A$ means the set of all functions from $A$ (being non-empty set) to $\Bbb R$, $f$ is just such a function.

MML Identifier: REAL_LAT

Contents (PDF format)

Bibliography

[1] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.

[2] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[3] Henryk Oryszczyszyn and Krzysztof Prazmowski. Real functions spaces. Journal of Formalized Mathematics, 2, 1990.

[4] Andrzej Trybulec. Function domains and Fr\aenkel operator. Journal of Formalized Mathematics, 2, 1990.

[5] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[6] Andrzej Trybulec and Czeslaw Bylinski. Some properties of real numbers operations: min, max, square, and square root. Journal of Formalized Mathematics, 1, 1989.

[7] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[8] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[9] Stanislaw Zukowski. Introduction to lattice theory. Journal of Formalized Mathematics, 1, 1989.