:: The Lattice of Real Numbers. The Lattice of Real Functions
:: by Marek Chmur
::
:: Received May 22, 1990
:: Copyright (c) 1990 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
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
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
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
end;
:: deftheorem Def1 defines minreal REAL_LAT:def 1 :
:: deftheorem Def2 defines maxreal REAL_LAT:def 2 :
:: deftheorem REAL_LAT:def 3 :
canceled;
:: deftheorem defines Real_Lattice REAL_LAT:def 4 :
Lm1:
for a, b being Element of Real_Lattice holds a "\/" b = b "\/" a
;
Lm2:
for a, b, c being Element of Real_Lattice holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
by XXREAL_0:34;
Lm3:
for a, b being Element of Real_Lattice holds (a "/\" b) "\/" b = b
by XXREAL_0:36;
Lm4:
for a, b being Element of Real_Lattice holds a "/\" b = b "/\" a
;
Lm5:
for a, b, c being Element of Real_Lattice holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
by XXREAL_0:33;
Lm6:
for a, b being Element of Real_Lattice holds a "/\" (a "\/" b) = a
by XXREAL_0:35;
Lm7:
for a, b, c being Element of Real_Lattice holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
by XXREAL_0:38;
theorem :: REAL_LAT:1
canceled;
theorem :: REAL_LAT:2
canceled;
theorem :: REAL_LAT:3
canceled;
theorem :: REAL_LAT:4
canceled;
theorem :: REAL_LAT:5
canceled;
theorem :: REAL_LAT:6
canceled;
theorem :: REAL_LAT:7
canceled;
theorem Th8: :: REAL_LAT:8
theorem Th9: :: REAL_LAT:9
theorem Th10: :: REAL_LAT:10
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 )
theorem Th11: :: REAL_LAT:11
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 )
theorem Th12: :: REAL_LAT:12
theorem Th13: :: REAL_LAT:13
theorem Th14: :: REAL_LAT:14
definition
let A be non
empty set ;
func maxfuncreal 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 = 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
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
func minfuncreal A -> BinOp of
Funcs A,
REAL means :
Def6:
:: REAL_LAT:def 6
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
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
end;
:: deftheorem Def5 defines maxfuncreal REAL_LAT:def 5 :
:: deftheorem Def6 defines minfuncreal REAL_LAT:def 6 :
Lm8:
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
theorem :: REAL_LAT:15
canceled;
theorem :: REAL_LAT:16
canceled;
theorem :: REAL_LAT:17
canceled;
theorem :: REAL_LAT:18
canceled;
theorem :: REAL_LAT:19
canceled;
theorem Th20: :: REAL_LAT:20
theorem Th21: :: REAL_LAT:21
theorem Th22: :: REAL_LAT:22
theorem Th23: :: REAL_LAT:23
theorem Th24: :: REAL_LAT:24
theorem Th25: :: REAL_LAT:25
theorem Th26: :: REAL_LAT:26
theorem :: REAL_LAT:27
theorem Th28: :: REAL_LAT:28
theorem Th29: :: REAL_LAT:29
theorem Th30: :: REAL_LAT:30
theorem :: REAL_LAT:31
theorem Th32: :: REAL_LAT:32
:: deftheorem REAL_LAT:def 7 :
canceled;
:: deftheorem REAL_LAT:def 8 :
canceled;
:: deftheorem defines @ REAL_LAT:def 9 :
Lm9:
for A being non empty set
for a, b, c being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
by Th22;
Lm10:
for A being non empty set
for a, b, c being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
by Th23;
:: deftheorem defines RealFunc_Lattice REAL_LAT:def 10 :
theorem :: REAL_LAT:33
canceled;
theorem :: REAL_LAT:34
canceled;
theorem :: REAL_LAT:35
canceled;
theorem :: REAL_LAT:36
canceled;
theorem :: REAL_LAT:37
canceled;
theorem :: REAL_LAT:38
canceled;
theorem :: REAL_LAT:39
canceled;
theorem Th40: :: REAL_LAT:40
theorem Th41: :: REAL_LAT:41
theorem :: REAL_LAT:42
for
A being non
empty set for
p,
q,
r being
Element of
(RealFunc_Lattice A) holds
(
(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
for
A being non
empty set for
p,
q,
r being
Element of
(RealFunc_Lattice A) holds
(
(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
theorem :: REAL_LAT:45
theorem :: REAL_LAT:46
theorem :: REAL_LAT:47