The abstract of the Mizar article:

The Lattice of Real Numbers. The Lattice of Real Functions

by

Marek Chmur

Received May 22, 1990

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;