:: The Lattice of Real Numbers. The Lattice of Real Functions
:: by Marek Chmur
::
:: Received May 22, 1990
:: Copyright (c) 1990-2018 Association of Mizar Users

definition
func minreal -> BinOp of REAL means :Def1: :: REAL_LAT:def 1
for x, y being Real holds it . (x,y) = min (x,y);
existence
ex b1 being BinOp of REAL st
for x, y being Real holds b1 . (x,y) = min (x,y)
proof end;
uniqueness
for b1, b2 being BinOp of REAL st ( for x, y being Real holds b1 . (x,y) = min (x,y) ) & ( for x, y being Real holds b2 . (x,y) = min (x,y) ) holds
b1 = b2
proof end;
func maxreal -> BinOp of REAL means :Def2: :: REAL_LAT:def 2
for x, y being Real holds it . (x,y) = max (x,y);
existence
ex b1 being BinOp of REAL st
for x, y being Real holds b1 . (x,y) = max (x,y)
proof end;
uniqueness
for b1, b2 being BinOp of REAL st ( for x, y being Real holds b1 . (x,y) = max (x,y) ) & ( for x, y being Real holds b2 . (x,y) = max (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines minreal REAL_LAT:def 1 :
for b1 being BinOp of REAL holds
( b1 = minreal iff for x, y being Real holds b1 . (x,y) = min (x,y) );

:: deftheorem Def2 defines maxreal REAL_LAT:def 2 :
for b1 being BinOp of REAL holds
( b1 = maxreal iff for x, y being Real holds b1 . (x,y) = max (x,y) );

definition
coherence ;
end;

:: deftheorem defines Real_Lattice REAL_LAT:def 3 :

registration
coherence ;
end;

registration
coherence
not Real_Lattice is empty
;
end;

registration
let a, b be Element of Real_Lattice;
identify a "\/" b with max (a,b);
compatibility
a "\/" b = max (a,b)
by Def2;
identify a "/\" b with min (a,b);
compatibility
a "/\" b = min (a,b)
by Def1;
end;

Lm1: for a, b, c being Element of Real_Lattice holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
by XXREAL_0:34;

Lm2: for a, b being Element of Real_Lattice holds (a "/\" b) "\/" b = b
by XXREAL_0:36;

Lm3: for a, b, c being Element of Real_Lattice holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
by XXREAL_0:33;

Lm4: for a, b being Element of Real_Lattice holds a "/\" (a "\/" b) = a
by XXREAL_0:35;

registration
coherence
proof end;
end;

Lm5: for a, b, c being Element of Real_Lattice holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
by XXREAL_0:38;

theorem Th1: :: REAL_LAT:1
for p, q being Element of Real_Lattice holds maxreal . (p,q) = maxreal . (q,p)
proof end;

theorem Th2: :: REAL_LAT:2
for p, q being Element of Real_Lattice holds minreal . (p,q) = minreal . (q,p)
proof end;

theorem Th3: :: REAL_LAT:3
for p, q, r being Element of Real_Lattice holds
( 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) )
proof end;

theorem Th4: :: REAL_LAT:4
for p, q, r being Element of Real_Lattice holds
( 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) )
proof end;

theorem Th5: :: REAL_LAT:5
for p, q being Element of Real_Lattice holds
( maxreal . ((minreal . (p,q)),q) = q & maxreal . (q,(minreal . (p,q))) = q & maxreal . (q,(minreal . (q,p))) = q & maxreal . ((minreal . (q,p)),q) = q )
proof end;

theorem Th6: :: REAL_LAT:6
for p, q being Element of Real_Lattice holds
( minreal . (q,(maxreal . (q,p))) = q & minreal . ((maxreal . (p,q)),q) = q & minreal . (q,(maxreal . (p,q))) = q & minreal . ((maxreal . (q,p)),q) = q )
proof end;

theorem Th7: :: REAL_LAT:7
for p, q, r being Element of Real_Lattice holds minreal . (q,(maxreal . (p,r))) = maxreal . ((minreal . (q,p)),(minreal . (q,r)))
proof end;

registration
coherence by Lm5;
end;

definition
let A be non empty set ;
func maxfuncreal A -> BinOp of (Funcs (A,REAL)) means :Def4: :: REAL_LAT:def 4
for f, g being Element of Funcs (A,REAL) holds it . (f,g) = maxreal .: (f,g);
existence
ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = maxreal .: (f,g)
proof end;
uniqueness
for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = maxreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = maxreal .: (f,g) ) holds
b1 = b2
proof end;
func minfuncreal A -> BinOp of (Funcs (A,REAL)) means :Def5: :: REAL_LAT:def 5
for f, g being Element of Funcs (A,REAL) holds it . (f,g) = minreal .: (f,g);
existence
ex b1 being BinOp of (Funcs (A,REAL)) st
for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = minreal .: (f,g)
proof end;
uniqueness
for b1, b2 being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b1 . (f,g) = minreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = minreal .: (f,g) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines maxfuncreal REAL_LAT:def 4 :
for A being non empty set
for b2 being BinOp of (Funcs (A,REAL)) holds
( b2 = maxfuncreal A iff for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = maxreal .: (f,g) );

:: deftheorem Def5 defines minfuncreal REAL_LAT:def 5 :
for A being non empty set
for b2 being BinOp of (Funcs (A,REAL)) holds
( b2 = minfuncreal A iff for f, g being Element of Funcs (A,REAL) holds b2 . (f,g) = minreal .: (f,g) );

Lm6: for A, B being non empty set
for x being Element of A
for f being Function of A,B holds x in dom f

proof end;

theorem Th8: :: REAL_LAT:8
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . (f,g) = () . (g,f)
proof end;

theorem Th9: :: REAL_LAT:9
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . (f,g) = () . (g,f)
proof end;

theorem Th10: :: REAL_LAT:10
for A being non empty set
for f, g, h being Element of Funcs (A,REAL) holds () . ((() . (f,g)),h) = () . (f,(() . (g,h)))
proof end;

theorem Th11: :: REAL_LAT:11
for A being non empty set
for f, g, h being Element of Funcs (A,REAL) holds () . ((() . (f,g)),h) = () . (f,(() . (g,h)))
proof end;

theorem Th12: :: REAL_LAT:12
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . (f,(() . (f,g))) = f
proof end;

theorem Th13: :: REAL_LAT:13
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . ((() . (f,g)),f) = f
proof end;

theorem Th14: :: REAL_LAT:14
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . ((() . (g,f)),f) = f
proof end;

theorem :: REAL_LAT:15
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . (f,(() . (g,f))) = f
proof end;

theorem Th16: :: REAL_LAT:16
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . (f,(() . (f,g))) = f
proof end;

theorem Th17: :: REAL_LAT:17
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . (f,(() . (g,f))) = f
proof end;

theorem Th18: :: REAL_LAT:18
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . ((() . (g,f)),f) = f
proof end;

theorem :: REAL_LAT:19
for A being non empty set
for f, g being Element of Funcs (A,REAL) holds () . ((() . (f,g)),f) = f
proof end;

theorem Th20: :: REAL_LAT:20
for A being non empty set
for f, g, h being Element of Funcs (A,REAL) holds () . (f,(() . (g,h))) = () . ((() . (f,g)),(() . (f,h)))
proof end;

Lm7: for A being non empty set
for a, b, c being Element of LattStr(# (Funcs (A,REAL)),(),() #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

by Th10;

Lm8: for A being non empty set
for a, b, c being Element of LattStr(# (Funcs (A,REAL)),(),() #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

by Th11;

definition
let A be non empty set ;
func RealFunc_Lattice A -> non empty strict LattStr equals :: REAL_LAT:def 6
LattStr(# (Funcs (A,REAL)),(),() #);
coherence
LattStr(# (Funcs (A,REAL)),(),() #) is non empty strict LattStr
;
end;

:: deftheorem defines RealFunc_Lattice REAL_LAT:def 6 :
for A being non empty set holds RealFunc_Lattice A = LattStr(# (Funcs (A,REAL)),(),() #);

registration
let A be non empty set ;
coherence
for b1 being non empty LattStr st b1 = RealFunc_Lattice A holds
( b1 is join-commutative & b1 is join-associative & b1 is meet-absorbing & b1 is meet-commutative & b1 is meet-associative & b1 is join-absorbing )
by ;
end;

theorem Th21: :: REAL_LAT:21
for A being non empty set
for p, q being Element of () holds () . (p,q) = () . (q,p)
proof end;

theorem Th22: :: REAL_LAT:22
for A being non empty set
for p, q being Element of () holds () . (p,q) = () . (q,p)
proof end;

theorem :: REAL_LAT:23
for A being non empty set
for p, q, r being Element of () holds
( () . (p,(() . (q,r))) = () . ((() . (q,r)),p) & () . (p,(() . (q,r))) = () . ((() . (p,q)),r) & () . (p,(() . (q,r))) = () . ((() . (q,p)),r) & () . (p,(() . (q,r))) = () . ((() . (r,p)),q) & () . (p,(() . (q,r))) = () . ((() . (r,q)),p) & () . (p,(() . (q,r))) = () . ((() . (p,r)),q) )
proof end;

theorem :: REAL_LAT:24
for A being non empty set
for p, q, r being Element of () holds
( () . (p,(() . (q,r))) = () . ((() . (q,r)),p) & () . (p,(() . (q,r))) = () . ((() . (p,q)),r) & () . (p,(() . (q,r))) = () . ((() . (q,p)),r) & () . (p,(() . (q,r))) = () . ((() . (r,p)),q) & () . (p,(() . (q,r))) = () . ((() . (r,q)),p) & () . (p,(() . (q,r))) = () . ((() . (p,r)),q) )
proof end;

theorem :: REAL_LAT:25
for A being non empty set
for p, q being Element of () holds
( () . ((() . (p,q)),q) = q & () . (q,(() . (p,q))) = q & () . (q,(() . (q,p))) = q & () . ((() . (q,p)),q) = q )
proof end;

theorem :: REAL_LAT:26
for A being non empty set
for p, q being Element of () holds
( () . (q,(() . (q,p))) = q & () . ((() . (p,q)),q) = q & () . (q,(() . (p,q))) = q & () . ((() . (q,p)),q) = q )
proof end;

theorem :: REAL_LAT:27
for A being non empty set
for p, q, r being Element of () holds () . (q,(() . (p,r))) = () . ((() . (q,p)),(() . (q,r))) by Th20;

theorem :: REAL_LAT:28
for A being non empty set holds RealFunc_Lattice A is D_Lattice
proof end;