Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### The Lattice of Real Numbers. The Lattice of Real Functions

by
Marek Chmur

MML identifier: REAL_LAT
[ Mizar article, MML identifier index ]

```environ

vocabulary BINOP_1, FUNCT_1, SQUARE_1, LATTICES, ARYTM, FUNCT_2, RELAT_1,
QC_LANG1, REAL_LAT;
notation XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, SQUARE_1, STRUCT_0,
LATTICES, BINOP_1, FUNCSDOM, RELAT_1, FUNCT_2, FRAENKEL;
constructors SQUARE_1, LATTICES, FUNCSDOM, MEMBERED, XBOOLE_0;
clusters LATTICES, RLSUB_2, RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: LATTICE of REAL NUMBERS

reserve x,y for Real;

definition
func minreal-> BinOp of REAL means
:: REAL_LAT:def 1
it.(x,y)=min(x,y);

func maxreal-> BinOp of REAL means
:: REAL_LAT:def 2
it.(x,y)=max(x,y);
end;

definition
canceled;

func Real_Lattice -> strict LattStr equals
:: REAL_LAT:def 4
LattStr (# REAL, maxreal, minreal #);
end;

definition
cluster -> real Element of Real_Lattice;
end;

definition
cluster Real_Lattice -> non empty;
end;

reserve p,q,a,b,c for Element of Real_Lattice;

definition
cluster Real_Lattice -> Lattice-like;
end;

reserve p,q,r for Element of Real_Lattice;

canceled 7;

theorem :: REAL_LAT:8
maxreal.(p,q) = maxreal.(q,p);

theorem :: REAL_LAT:9
minreal.(p,q) = minreal.(q,p);

theorem :: REAL_LAT:10
maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(q,r)),p) &
maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(p,q)),r) &
maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(q,p)),r) &
maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(r,p)),q) &
maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(r,q)),p) &
maxreal.(p,(maxreal.(q,r)))=maxreal.((maxreal.(p,r)),q);

theorem :: REAL_LAT:11
minreal.(p,(minreal.(q,r)))=minreal.((minreal.(q,r)),p) &
minreal.(p,(minreal.(q,r)))=minreal.((minreal.(p,q)),r) &
minreal.(p,(minreal.(q,r)))=minreal.((minreal.(q,p)),r) &
minreal.(p,(minreal.(q,r)))=minreal.((minreal.(r,p)),q) &
minreal.(p,(minreal.(q,r)))=minreal.((minreal.(r,q)),p) &
minreal.(p,(minreal.(q,r)))=minreal.((minreal.(p,r)),q);

theorem :: REAL_LAT:12
maxreal.(minreal.(p,q),q)=q & maxreal.(q,minreal.(p,q))=q &
maxreal.(q,minreal.(q,p))=q & maxreal.(minreal.(q,p),q)=q;

theorem :: REAL_LAT:13
minreal.(q,maxreal.(q,p))=q & minreal.(maxreal.(p,q),q)=q &
minreal.(q,maxreal.(p,q))=q & minreal.(maxreal.(q,p),q)=q;

theorem :: REAL_LAT:14
minreal.(q,maxreal.(p,r))=maxreal.(minreal.(q,p),minreal.(q,r));

definition
cluster Real_Lattice -> distributive;
end;

reserve A,B for non empty set;
reserve f,g,h for Element of Funcs(A,REAL);

definition let A;
func maxfuncreal(A) -> BinOp of Funcs(A,REAL) means
:: REAL_LAT:def 5
it.(f,g) = maxreal.:(f,g);

func minfuncreal(A) -> BinOp of Funcs(A,REAL) means
:: REAL_LAT:def 6
it.(f,g) = minreal.:(f,g);
end;

canceled 5;

theorem :: REAL_LAT:20
(maxfuncreal(A)).(f,g) = (maxfuncreal(A)).(g,f);

theorem :: REAL_LAT:21
(minfuncreal(A)).(f,g) = (minfuncreal(A)).(g,f);

theorem :: REAL_LAT:22
(maxfuncreal(A)).((maxfuncreal(A)).(f,g),h)
=(maxfuncreal(A)).(f,(maxfuncreal(A)).(g,h));

theorem :: REAL_LAT:23
(minfuncreal(A)).((minfuncreal(A)).(f,g),h)
=(minfuncreal(A)).(f,(minfuncreal(A)).(g,h));

theorem :: REAL_LAT:24
(maxfuncreal(A)).(f,(minfuncreal(A)).(f,g))=f;

theorem :: REAL_LAT:25
(maxfuncreal(A)).((minfuncreal(A)).(f,g),f)=f;

theorem :: REAL_LAT:26
(maxfuncreal(A)).((minfuncreal(A)).(g,f),f)=f;

theorem :: REAL_LAT:27
(maxfuncreal(A)).(f,(minfuncreal(A)).(g,f))=f;

theorem :: REAL_LAT:28
(minfuncreal(A)).(f,(maxfuncreal(A)).(f,g))=f;

theorem :: REAL_LAT:29
(minfuncreal(A)).(f,(maxfuncreal(A)).(g,f))=f;

theorem :: REAL_LAT:30
(minfuncreal(A)).((maxfuncreal(A)).(g,f),f)=f;

theorem :: REAL_LAT:31
(minfuncreal(A)).((maxfuncreal(A)).(f,g),f)=f;

theorem :: REAL_LAT:32
(minfuncreal(A)).(f,(maxfuncreal(A)).(g,h)) =
(maxfuncreal(A)).((minfuncreal(A)).(f,g),(minfuncreal(A)).(f,h));

reserve p,q,r for Element of
LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);

definition let A;
let x be Element of
LattStr(# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
canceled 2;

func @x->Element of Funcs(A,REAL) equals
:: REAL_LAT:def 9
x;
end;

definition let A;
func RealFunc_Lattice(A) -> strict Lattice equals
:: REAL_LAT:def 10
LattStr (# Funcs(A,REAL), maxfuncreal(A), minfuncreal(A) #);
end;

reserve p,q,r for Element of RealFunc_Lattice(A);

canceled 7;

theorem :: REAL_LAT:40
(maxfuncreal(A)).(p,q) = (maxfuncreal(A)).(q,p);

theorem :: REAL_LAT:41
(minfuncreal(A)).(p,q) = (minfuncreal(A)).(q,p);

theorem :: REAL_LAT:42
(maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
=(maxfuncreal(A)).(((maxfuncreal(A)).(q,r)),p) &
(maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
=(maxfuncreal(A)).(((maxfuncreal(A)).(p,q)),r) &
(maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
=(maxfuncreal(A)).(((maxfuncreal(A)).(q,p)),r) &
(maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
=(maxfuncreal(A)).(((maxfuncreal(A)).(r,p)),q) &
(maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
=(maxfuncreal(A)).(((maxfuncreal(A)).(r,q)),p) &
(maxfuncreal(A)).(p,((maxfuncreal(A)).(q,r)))
=(maxfuncreal(A)).(((maxfuncreal(A)).(p,r)),q);

theorem :: REAL_LAT:43
(minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
=(minfuncreal(A)).(((minfuncreal(A)).(q,r)),p) &
(minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
=(minfuncreal(A)).(((minfuncreal(A)).(p,q)),r) &
(minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
=(minfuncreal(A)).(((minfuncreal(A)).(q,p)),r) &
(minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
=(minfuncreal(A)).(((minfuncreal(A)).(r,p)),q) &
(minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
=(minfuncreal(A)).(((minfuncreal(A)).(r,q)),p) &
(minfuncreal(A)).(p,((minfuncreal(A)).(q,r)))
=(minfuncreal(A)).(((minfuncreal(A)).(p,r)),q);

theorem :: REAL_LAT:44
(maxfuncreal(A)).((minfuncreal(A)).(p,q),q)=q &
(maxfuncreal(A)).(q,(minfuncreal(A)).(p,q))=q &
(maxfuncreal(A)).(q,(minfuncreal(A)).(q,p))=q &
(maxfuncreal(A)).((minfuncreal(A)).(q,p),q)=q;

theorem :: REAL_LAT:45
(minfuncreal(A)).(q,(maxfuncreal(A)).(q,p))=q &
(minfuncreal(A)).((maxfuncreal(A)).(p,q),q)=q &
(minfuncreal(A)).(q,(maxfuncreal(A)).(p,q))=q &
(minfuncreal(A)).((maxfuncreal(A)).(q,p),q)=q;

theorem :: REAL_LAT:46
(minfuncreal(A)).(q,(maxfuncreal(A)).(p,r))
=(maxfuncreal(A)).((minfuncreal(A)).(q,p),(minfuncreal(A)).(q,r));

theorem :: REAL_LAT:47
RealFunc_Lattice(A) is D_Lattice;
```