begin
definition
func minreal -> BinOp of
REAL means :
Def1:
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:
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 holds a "\/" b = b "\/" a
;
Lm2:
for a, b, c being Element of holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
by XXREAL_0:34;
Lm3:
for a, b being Element of holds (a "/\" b) "\/" b = b
by XXREAL_0:36;
Lm4:
for a, b being Element of holds a "/\" b = b "/\" a
;
Lm5:
for a, b, c being Element of holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
by XXREAL_0:33;
Lm6:
for a, b being Element of holds a "/\" (a "\/" b) = a
by XXREAL_0:35;
Lm7:
for a, b, c being Element of holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
by XXREAL_0:38;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
for
p,
q,
r being
Element of 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:
for
p,
q,
r being
Element of 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:
theorem Th13:
theorem Th14:
definition
let A be non
empty set ;
func maxfuncreal A -> BinOp of
Funcs A,
REAL means :
Def5:
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:
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem
theorem Th32:
:: 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 holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
by Th22;
Lm10:
for A being non empty set
for a, b, c being Element of holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
by Th23;
:: deftheorem defines RealFunc_Lattice REAL_LAT:def 10 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th40:
theorem Th41:
theorem
for
A being non
empty set for
p,
q,
r being
Element of 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
for
A being non
empty set for
p,
q,
r being
Element of 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
theorem
theorem
theorem