:: by Marek Chmur

::

:: Received May 22, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

definition

ex b_{1} being BinOp of REAL st

for x, y being Real holds b_{1} . (x,y) = min (x,y)

for b_{1}, b_{2} being BinOp of REAL st ( for x, y being Real holds b_{1} . (x,y) = min (x,y) ) & ( for x, y being Real holds b_{2} . (x,y) = min (x,y) ) holds

b_{1} = b_{2}

ex b_{1} being BinOp of REAL st

for x, y being Real holds b_{1} . (x,y) = max (x,y)

for b_{1}, b_{2} being BinOp of REAL st ( for x, y being Real holds b_{1} . (x,y) = max (x,y) ) & ( for x, y being Real holds b_{2} . (x,y) = max (x,y) ) holds

b_{1} = b_{2}
end;

func minreal -> BinOp of REAL means :Def1: :: REAL_LAT:def 1

for x, y being Real holds it . (x,y) = min (x,y);

existence for x, y being Real holds it . (x,y) = min (x,y);

ex b

for x, y being Real holds b

proof end;

uniqueness for b

b

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 for x, y being Real holds it . (x,y) = max (x,y);

ex b

for x, y being Real holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines minreal REAL_LAT:def 1 :

for b_{1} being BinOp of REAL holds

( b_{1} = minreal iff for x, y being Real holds b_{1} . (x,y) = min (x,y) );

for b

( b

:: deftheorem Def2 defines maxreal REAL_LAT:def 2 :

for b_{1} being BinOp of REAL holds

( b_{1} = maxreal iff for x, y being Real holds b_{1} . (x,y) = max (x,y) );

for b

( b

:: deftheorem defines Real_Lattice REAL_LAT:def 3 :

Real_Lattice = LattStr(# REAL,maxreal,minreal #);

Real_Lattice = LattStr(# REAL,maxreal,minreal #);

registration

let a, b be Element of Real_Lattice;

compatibility

a "\/" b = max (a,b) by Def2;

compatibility

a "/\" b = min (a,b) by Def1;

end;
compatibility

a "\/" b = max (a,b) by Def2;

compatibility

a "/\" b = min (a,b) by Def1;

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
end;

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

by XXREAL_0:38;

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) )

( 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) )

( 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 )

( 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 )

( 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
end;

definition

let A be non empty set ;

ex b_{1} being BinOp of (Funcs (A,REAL)) st

for f, g being Element of Funcs (A,REAL) holds b_{1} . (f,g) = maxreal .: (f,g)

for b_{1}, b_{2} being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b_{1} . (f,g) = maxreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b_{2} . (f,g) = maxreal .: (f,g) ) holds

b_{1} = b_{2}

ex b_{1} being BinOp of (Funcs (A,REAL)) st

for f, g being Element of Funcs (A,REAL) holds b_{1} . (f,g) = minreal .: (f,g)

for b_{1}, b_{2} being BinOp of (Funcs (A,REAL)) st ( for f, g being Element of Funcs (A,REAL) holds b_{1} . (f,g) = minreal .: (f,g) ) & ( for f, g being Element of Funcs (A,REAL) holds b_{2} . (f,g) = minreal .: (f,g) ) holds

b_{1} = b_{2}

end;
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 for f, g being Element of Funcs (A,REAL) holds it . (f,g) = maxreal .: (f,g);

ex b

for f, g being Element of Funcs (A,REAL) holds b

proof end;

uniqueness for b

b

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 for f, g being Element of Funcs (A,REAL) holds it . (f,g) = minreal .: (f,g);

ex b

for f, g being Element of Funcs (A,REAL) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines maxfuncreal REAL_LAT:def 4 :

for A being non empty set

for b_{2} being BinOp of (Funcs (A,REAL)) holds

( b_{2} = maxfuncreal A iff for f, g being Element of Funcs (A,REAL) holds b_{2} . (f,g) = maxreal .: (f,g) );

for A being non empty set

for b

( b

:: deftheorem Def5 defines minfuncreal REAL_LAT:def 5 :

for A being non empty set

for b_{2} being BinOp of (Funcs (A,REAL)) holds

( b_{2} = minfuncreal A iff for f, g being Element of Funcs (A,REAL) holds b_{2} . (f,g) = minreal .: (f,g) );

for A being non empty set

for b

( b

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 (maxfuncreal A) . (f,g) = (maxfuncreal A) . (g,f)

for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,g) = (maxfuncreal A) . (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 (minfuncreal A) . (f,g) = (minfuncreal A) . (g,f)

for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,g) = (minfuncreal A) . (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 (maxfuncreal A) . (((maxfuncreal A) . (f,g)),h) = (maxfuncreal A) . (f,((maxfuncreal A) . (g,h)))

for f, g, h being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((maxfuncreal A) . (f,g)),h) = (maxfuncreal A) . (f,((maxfuncreal A) . (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 (minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (g,h)))

for f, g, h being Element of Funcs (A,REAL) holds (minfuncreal A) . (((minfuncreal A) . (f,g)),h) = (minfuncreal A) . (f,((minfuncreal A) . (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 (maxfuncreal A) . (f,((minfuncreal A) . (f,g))) = f

for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,((minfuncreal A) . (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 (maxfuncreal A) . (((minfuncreal A) . (f,g)),f) = f

for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((minfuncreal A) . (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 (maxfuncreal A) . (((minfuncreal A) . (g,f)),f) = f

for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (((minfuncreal A) . (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 (maxfuncreal A) . (f,((minfuncreal A) . (g,f))) = f

for f, g being Element of Funcs (A,REAL) holds (maxfuncreal A) . (f,((minfuncreal A) . (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 (minfuncreal A) . (f,((maxfuncreal A) . (f,g))) = f

for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (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 (minfuncreal A) . (f,((maxfuncreal A) . (g,f))) = f

for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (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 (minfuncreal A) . (((maxfuncreal A) . (g,f)),f) = f

for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (((maxfuncreal A) . (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 (minfuncreal A) . (((maxfuncreal A) . (f,g)),f) = f

for f, g being Element of Funcs (A,REAL) holds (minfuncreal A) . (((maxfuncreal A) . (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 (minfuncreal A) . (f,((maxfuncreal A) . (g,h))) = (maxfuncreal A) . (((minfuncreal A) . (f,g)),((minfuncreal A) . (f,h)))

for f, g, h being Element of Funcs (A,REAL) holds (minfuncreal A) . (f,((maxfuncreal A) . (g,h))) = (maxfuncreal A) . (((minfuncreal A) . (f,g)),((minfuncreal A) . (f,h)))

proof end;

Lm7: 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 Th10;

Lm8: 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 Th11;

definition

let A be non empty set ;

LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #) is non empty strict LattStr ;

end;
func RealFunc_Lattice A -> non empty strict LattStr equals :: REAL_LAT:def 6

LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #);

coherence LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #);

LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #) is non empty strict LattStr ;

:: deftheorem defines RealFunc_Lattice REAL_LAT:def 6 :

for A being non empty set holds RealFunc_Lattice A = LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #);

for A being non empty set holds RealFunc_Lattice A = LattStr(# (Funcs (A,REAL)),(maxfuncreal A),(minfuncreal A) #);

registration

let A be non empty set ;

for b_{1} being non empty LattStr st b_{1} = RealFunc_Lattice A holds

( b_{1} is join-commutative & b_{1} is join-associative & b_{1} is meet-absorbing & b_{1} is meet-commutative & b_{1} is meet-associative & b_{1} is join-absorbing )
by Th8, Th10, Th14, Th9, Th11, Th16;

end;
cluster RealFunc_Lattice A -> non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing for non empty LattStr ;

coherence for b

( b

theorem Th21: :: REAL_LAT:21

for A being non empty set

for p, q being Element of (RealFunc_Lattice A) holds (maxfuncreal A) . (p,q) = (maxfuncreal A) . (q,p)

for p, q being Element of (RealFunc_Lattice A) holds (maxfuncreal A) . (p,q) = (maxfuncreal A) . (q,p)

proof end;

theorem Th22: :: REAL_LAT:22

for A being non empty set

for p, q being Element of (RealFunc_Lattice A) holds (minfuncreal A) . (p,q) = (minfuncreal A) . (q,p)

for p, q being Element of (RealFunc_Lattice A) holds (minfuncreal A) . (p,q) = (minfuncreal A) . (q,p)

proof end;

theorem :: REAL_LAT:23

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) )

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) )

proof end;

theorem :: REAL_LAT:24

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) )

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) )

proof end;

theorem :: REAL_LAT:25

for A being non empty set

for p, q being Element of (RealFunc_Lattice A) holds

( (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 )

for p, q being Element of (RealFunc_Lattice A) holds

( (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 )

proof end;

theorem :: REAL_LAT:26

for A being non empty set

for p, q being Element of (RealFunc_Lattice A) holds

( (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 )

for p, q being Element of (RealFunc_Lattice A) holds

( (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 )

proof end;

theorem :: REAL_LAT:27

for A being non empty set

for p, q, r being Element of (RealFunc_Lattice A) holds (minfuncreal A) . (q,((maxfuncreal A) . (p,r))) = (maxfuncreal A) . (((minfuncreal A) . (q,p)),((minfuncreal A) . (q,r))) by Th20;

for p, q, r being Element of (RealFunc_Lattice A) holds (minfuncreal A) . (q,((maxfuncreal A) . (p,r))) = (maxfuncreal A) . (((minfuncreal A) . (q,p)),((minfuncreal A) . (q,r))) by Th20;