The Lattice of Real Numbers. The Lattice of Real Functions
Marek Chmur · 1990
Summary. A proof of the fact, that 〈R,max,min 〉 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 R A with operations: max ( f(A)) and min ( f(A)), where R A means the set of all functions from A (being non-empty set) to R, f is just such a function. MML Identifier:REAL_LAT. WWW:http://mizar.org/JFM/Vol2/real_lat.html The articles [7], [5], [6], [9], [1], [3], [8], [2], and [4] provide the notation and terminology for this paper. In this paper x, y denote real numbers. The binary operation minR on R is defined as follows: (Def. 1) minR(x, y) = min(x,y). The binary operation maxR on R is defined as follows: (Def. 2) maxR(x, y) = max(x,y). The strict lattice structure RL is defined as follows: (Def. 4) 1 RL = 〈R,maxR,minR〉. Let us mention that every element of RL is real. One can verify that RL is non empty. Let us mention that RL is lattice-like. In the sequel p, q, r are elements of RL. We now state several propositions: (8) 2 maxR(p, q) = maxR(q, p). (9) minR(p, q) = minR(q, p). (10)(i) maxR(p, maxR(q, r)) = maxR(maxR(q, r), p), (ii) maxR(p, maxR(q, r)) = maxR(maxR(p, q), r), (iii) maxR(p, maxR(q, r)) = maxR(maxR(q, p), r), (iv) maxR(p, maxR(q, r)) = maxR(maxR(r, p), q), (v) maxR(p, maxR(q, r)) = maxR(maxR(r, q), p), and (vi) maxR(p, maxR(q, r)) = maxR(maxR(p, r), q). 1 The definition (Def. 3) has been removed. 2 The propositions (1)–(7) have been removed.