:: The Lattice of Real Numbers. The Lattice of Real Functions :: by Marek Chmur :: :: Received May 22, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies REAL_1, BINOP_1, NUMBERS, FUNCT_1, XXREAL_0, SUBSET_1, LATTICES, XBOOLE_0, EQREL_1, FUNCT_2, RELAT_1, REAL_LAT, MEMBERED, STRUCT_0, FUNCT_7; notations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, MEMBERED, STRUCT_0, LATTICES, BINOP_1, FUNCSDOM, RELAT_1, FUNCT_2; constructors SQUARE_1, LATTICES, FUNCSDOM, RELSET_1, MEMBERED, XXREAL_0; registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, LATTICES, MEMBERED; 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 func Real_Lattice -> strict LattStr equals :: REAL_LAT:def 3 LattStr (# REAL, maxreal, minreal #); end; registration cluster the carrier of Real_Lattice -> real-membered; end; registration cluster Real_Lattice -> non empty; end; reserve a,b,c for Element of Real_Lattice; registration let a,b be Element of Real_Lattice; identify a "\/" b with max(a,b); identify a "/\" b with min(a,b); end; registration cluster Real_Lattice -> Lattice-like; end; reserve p,q,r for Element of Real_Lattice; theorem :: REAL_LAT:1 maxreal.(p,q) = maxreal.(q,p); theorem :: REAL_LAT:2 minreal.(p,q) = minreal.(q,p); theorem :: REAL_LAT:3 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:4 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:5 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:6 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:7 minreal.(q,maxreal.(p,r))=maxreal.(minreal.(q,p),minreal.(q,r)); registration 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 4 it.(f,g) = maxreal.:(f,g); func minfuncreal(A) -> BinOp of Funcs(A,REAL) means :: REAL_LAT:def 5 it.(f,g) = minreal.:(f,g); end; theorem :: REAL_LAT:8 (maxfuncreal(A)).(f,g) = (maxfuncreal(A)).(g,f); theorem :: REAL_LAT:9 (minfuncreal(A)).(f,g) = (minfuncreal(A)).(g,f); theorem :: REAL_LAT:10 (maxfuncreal(A)).((maxfuncreal(A)).(f,g),h) =(maxfuncreal(A)).(f ,(maxfuncreal(A)).(g,h)); theorem :: REAL_LAT:11 (minfuncreal(A)).((minfuncreal(A)).(f,g),h) =(minfuncreal(A)).(f ,(minfuncreal(A)).(g,h)); theorem :: REAL_LAT:12 (maxfuncreal(A)).(f,(minfuncreal(A)).(f,g))=f; theorem :: REAL_LAT:13 (maxfuncreal(A)).((minfuncreal(A)).(f,g),f)=f; theorem :: REAL_LAT:14 (maxfuncreal(A)).((minfuncreal(A)).(g,f),f)=f; theorem :: REAL_LAT:15 (maxfuncreal(A)).(f,(minfuncreal(A)).(g,f))=f; theorem :: REAL_LAT:16 (minfuncreal(A)).(f,(maxfuncreal(A)).(f,g))=f; theorem :: REAL_LAT:17 (minfuncreal(A)).(f,(maxfuncreal(A)).(g,f))=f; theorem :: REAL_LAT:18 (minfuncreal(A)).((maxfuncreal(A)).(g,f),f)=f; theorem :: REAL_LAT:19 (minfuncreal(A)).((maxfuncreal(A)).(f,g),f)=f; theorem :: REAL_LAT:20 (minfuncreal(A)).(f,(maxfuncreal(A)).(g,h)) = (maxfuncreal(A)).( (minfuncreal(A)).(f,g),(minfuncreal(A)).(f,h)); definition let A; func RealFunc_Lattice A -> non empty strict LattStr equals :: REAL_LAT:def 6 LattStr (# Funcs(A,REAL), maxfuncreal A, minfuncreal A #); end; reserve L for non empty LattStr, p,q,r for Element of L; registration let A; cluster RealFunc_Lattice A -> join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing for non empty LattStr; end; reserve p,q,r for Element of RealFunc_Lattice(A); theorem :: REAL_LAT:21 (maxfuncreal(A)).(p,q) = (maxfuncreal(A)).(q,p); theorem :: REAL_LAT:22 (minfuncreal(A)).(p,q) = (minfuncreal(A)).(q,p); theorem :: REAL_LAT:23 (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:24 (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:25 (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:26 (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:27 (minfuncreal(A)).(q,(maxfuncreal(A)).(p,r)) =(maxfuncreal(A)).(( minfuncreal(A)).(q,p),(minfuncreal(A)).(q,r)); theorem :: REAL_LAT:28 RealFunc_Lattice(A) is D_Lattice;