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

begin

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 b₁ being BinOp of REAL st
for x, y being Real holds b₁ . x,y = min x,y

proof end;

uniqueness
for b₁, b₂ being BinOp of REAL st ( for x, y being Real holds b₁ . x,y = min x,y ) & ( for x, y being Real holds b₂ . x,y = min x,y ) holds
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
ex b₁ being BinOp of REAL st
for x, y being Real holds b₁ . x,y = max x,y

proof end;

uniqueness
for b₁, b₂ being BinOp of REAL st ( for x, y being Real holds b₁ . x,y = max x,y ) & ( for x, y being Real holds b₂ . x,y = max x,y ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines minreal REAL_LAT:def 1 :

for b₁ being BinOp of REAL holds
( b₁ = minreal iff for x, y being Real holds b₁ . x,y = min x,y );

:: deftheorem Def2 defines maxreal REAL_LAT:def 2 :

for b₁ being BinOp of REAL holds
( b₁ = maxreal iff for x, y being Real holds b₁ . x,y = max x,y );

definition

canceled;
func Real_Lattice -> strict LattStr equals :: REAL_LAT:def 4
LattStr(# REAL ,maxreal ,minreal #);
coherence
LattStr(# REAL ,maxreal ,minreal #) is strict LattStr ;

end;

:: deftheorem REAL_LAT:def 3 :

canceled;

:: deftheorem defines Real_Lattice REAL_LAT:def 4 :

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

registration

cluster -> real Element of the carrier of Real_Lattice ;
coherence
for b₁ being Element of Real_Lattice holds b₁ is real by XREAL_0:def 1;

end;

registration

cluster Real_Lattice -> non empty strict ;
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 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;

registration

cluster Real_Lattice -> strict Lattice-like ;
coherence
Real_Lattice is Lattice-like

proof end;

end;

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

for p, q being Element of Real_Lattice holds maxreal . p,q = maxreal . q,p

proof end;

theorem Th9: :: REAL_LAT:9

for p, q being Element of Real_Lattice holds minreal . p,q = minreal . q,p

proof end;

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 )

proof end;

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 )

proof end;

theorem Th12: :: REAL_LAT:12

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 Th13: :: REAL_LAT:13

for q, p 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 Th14: :: REAL_LAT:14

for q, p, r being Element of Real_Lattice holds minreal . q,(maxreal . p,r) = maxreal . (minreal . q,p),(minreal . q,r)

proof end;

registration

cluster Real_Lattice -> strict distributive ;
coherence
Real_Lattice is distributive by Lm7, LATTICES:def 11;

end;

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 b₁ being BinOp of (Funcs A,REAL ) st
for f, g being Element of Funcs A,REAL holds b₁ . f,g = maxreal .: f,g

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs A,REAL ) st ( for f, g being Element of Funcs A,REAL holds b₁ . f,g = maxreal .: f,g ) & ( for f, g being Element of Funcs A,REAL holds b₂ . f,g = maxreal .: f,g ) holds
b₁ = b₂

proof end;

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

proof end;

uniqueness
for b₁, b₂ being BinOp of (Funcs A,REAL ) st ( for f, g being Element of Funcs A,REAL holds b₁ . f,g = minreal .: f,g ) & ( for f, g being Element of Funcs A,REAL holds b₂ . f,g = minreal .: f,g ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines maxfuncreal REAL_LAT:def 5 :

for A being non empty set
for b₂ being BinOp of (Funcs A,REAL ) holds
( b₂ = maxfuncreal A iff for f, g being Element of Funcs A,REAL holds b₂ . f,g = maxreal .: f,g );

:: deftheorem Def6 defines minfuncreal REAL_LAT:def 6 :

for A being non empty set
for b₂ being BinOp of (Funcs A,REAL ) holds
( b₂ = minfuncreal A iff for f, g being Element of Funcs A,REAL holds b₂ . f,g = minreal .: f,g );

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

proof end;

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

for A being non empty set
for f, g being Element of Funcs A,REAL holds (maxfuncreal A) . f,g = (maxfuncreal A) . g,f

proof end;

theorem Th21: :: REAL_LAT:21

for A being non empty set
for f, g being Element of Funcs A,REAL holds (minfuncreal A) . f,g = (minfuncreal A) . g,f

proof end;

theorem Th22: :: REAL_LAT:22

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)

proof end;

theorem Th23: :: REAL_LAT:23

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)

proof end;

theorem Th24: :: REAL_LAT:24

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

proof end;

theorem Th25: :: REAL_LAT:25

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

proof end;

theorem Th26: :: REAL_LAT:26

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

proof end;

theorem :: REAL_LAT:27

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

proof end;

theorem Th28: :: REAL_LAT:28

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

proof end;

theorem Th29: :: REAL_LAT:29

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

proof end;

theorem Th30: :: REAL_LAT:30

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

proof end;

theorem :: REAL_LAT:31

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

proof end;

theorem Th32: :: REAL_LAT:32

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)

proof end;

definition

let A be non empty set ;
let x be Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #);
canceled;
canceled;
func @ x -> Element of Funcs A,REAL equals :: REAL_LAT:def 9
x;
coherence
x is Element of Funcs A,REAL ;

end;

:: deftheorem REAL_LAT:def 7 :

canceled;

:: deftheorem REAL_LAT:def 8 :

canceled;

:: deftheorem defines @ REAL_LAT:def 9 :

for A being non empty set
for x being Element of LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) holds @ x = x;

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;

definition

let A be non empty set ;
func RealFunc_Lattice A -> strict Lattice equals :: REAL_LAT:def 10
LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #);
coherence
LattStr(# (Funcs A,REAL ),(maxfuncreal A),(minfuncreal A) #) is strict Lattice

proof end;

end;

:: deftheorem defines RealFunc_Lattice REAL_LAT:def 10 :

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

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

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

proof end;

theorem Th41: :: REAL_LAT:41

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

proof end;

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 )

proof end;

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 )

proof end;

theorem :: REAL_LAT:44

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 )

proof end;

theorem :: REAL_LAT:45

for A being non empty set
for q, p 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:46

for A being non empty set
for q, p, 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 Th32;

theorem :: REAL_LAT:47

for A being non empty set holds RealFunc_Lattice A is D_Lattice

proof end;