:: REAL_LAT semantic presentation

definition

func minreal -> BinOp of REAL means :Def1: :: REAL_LAT:def 1
for b₁, b₂ being Real holds a₁ . b₁,b₂ = min b₁,b₂;
existence

proof end;

uniqueness

proof end;

func maxreal -> BinOp of REAL means :Def2: :: REAL_LAT:def 2
for b₁, b₂ being Real holds a₁ . b₁,b₂ = max b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines minreal REAL_LAT:def 1 :

:: deftheorem Def2 defines maxreal REAL_LAT:def 2 :

definition

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

end;

:: deftheorem Def3 REAL_LAT:def 3 :

:: deftheorem Def4 defines Real_Lattice REAL_LAT:def 4 :

registration

cluster -> real Element of the carrier of Real_Lattice ;
coherence by XREAL_0:def 1;

end;

registration

cluster Real_Lattice -> non empty strict ;
coherence ;

end;

Lemma3: for b₁, b₂ being Element of Real_Lattice holds b₁ "\/" b₂ = b₂ "\/" b₁

proof end;

Lemma4: for b₁, b₂, b₃ being Element of Real_Lattice holds b₁ "\/" (b₂ "\/" b₃) = (b₁ "\/" b₂) "\/" b₃

proof end;

Lemma5: for b₁, b₂ being Element of Real_Lattice holds (b₁ "/\" b₂) "\/" b₂ = b₂

proof end;

Lemma6: for b₁, b₂ being Element of Real_Lattice holds b₁ "/\" b₂ = b₂ "/\" b₁

proof end;

Lemma7: for b₁, b₂, b₃ being Element of Real_Lattice holds b₁ "/\" (b₂ "/\" b₃) = (b₁ "/\" b₂) "/\" b₃

proof end;

Lemma8: for b₁, b₂ being Element of Real_Lattice holds b₁ "/\" (b₁ "\/" b₂) = b₁

proof end;

registration

cluster Real_Lattice -> non empty strict Lattice-like ;
coherence

proof end;

end;

Lemma9: for b₁, b₂, b₃ being Element of Real_Lattice holds b₁ "/\" (b₂ "\/" b₃) = (b₁ "/\" b₂) "\/" (b₁ "/\" b₃)

proof end;

theorem Th1: :: REAL_LAT:1

canceled;

theorem Th2: :: REAL_LAT:2

canceled;

theorem Th3: :: REAL_LAT:3

canceled;

theorem Th4: :: REAL_LAT:4

canceled;

theorem Th5: :: REAL_LAT:5

canceled;

theorem Th6: :: REAL_LAT:6

canceled;

theorem Th7: :: REAL_LAT:7

canceled;

theorem Th8: :: REAL_LAT:8

for b₁, b₂ being Element of Real_Lattice holds maxreal . b₁,b₂ = maxreal . b₂,b₁

proof end;

theorem Th9: :: REAL_LAT:9

for b₁, b₂ being Element of Real_Lattice holds minreal . b₁,b₂ = minreal . b₂,b₁

proof end;

theorem Th10: :: REAL_LAT:10

for b₁, b₂, b₃ being Element of Real_Lattice holds
( maxreal . b₁,(maxreal . b₂,b₃) = maxreal . (maxreal . b₂,b₃),b₁ & maxreal . b₁,(maxreal . b₂,b₃) = maxreal . (maxreal . b₁,b₂),b₃ & maxreal . b₁,(maxreal . b₂,b₃) = maxreal . (maxreal . b₂,b₁),b₃ & maxreal . b₁,(maxreal . b₂,b₃) = maxreal . (maxreal . b₃,b₁),b₂ & maxreal . b₁,(maxreal . b₂,b₃) = maxreal . (maxreal . b₃,b₂),b₁ & maxreal . b₁,(maxreal . b₂,b₃) = maxreal . (maxreal . b₁,b₃),b₂ )

proof end;

theorem Th11: :: REAL_LAT:11

for b₁, b₂, b₃ being Element of Real_Lattice holds
( minreal . b₁,(minreal . b₂,b₃) = minreal . (minreal . b₂,b₃),b₁ & minreal . b₁,(minreal . b₂,b₃) = minreal . (minreal . b₁,b₂),b₃ & minreal . b₁,(minreal . b₂,b₃) = minreal . (minreal . b₂,b₁),b₃ & minreal . b₁,(minreal . b₂,b₃) = minreal . (minreal . b₃,b₁),b₂ & minreal . b₁,(minreal . b₂,b₃) = minreal . (minreal . b₃,b₂),b₁ & minreal . b₁,(minreal . b₂,b₃) = minreal . (minreal . b₁,b₃),b₂ )

proof end;

theorem Th12: :: REAL_LAT:12

for b₁, b₂ being Element of Real_Lattice holds
( maxreal . (minreal . b₁,b₂),b₂ = b₂ & maxreal . b₂,(minreal . b₁,b₂) = b₂ & maxreal . b₂,(minreal . b₂,b₁) = b₂ & maxreal . (minreal . b₂,b₁),b₂ = b₂ )

proof end;

theorem Th13: :: REAL_LAT:13

for b₁, b₂ being Element of Real_Lattice holds
( minreal . b₁,(maxreal . b₁,b₂) = b₁ & minreal . (maxreal . b₂,b₁),b₁ = b₁ & minreal . b₁,(maxreal . b₂,b₁) = b₁ & minreal . (maxreal . b₁,b₂),b₁ = b₁ )

proof end;

theorem Th14: :: REAL_LAT:14

for b₁, b₂, b₃ being Element of Real_Lattice holds minreal . b₁,(maxreal . b₂,b₃) = maxreal . (minreal . b₁,b₂),(minreal . b₁,b₃)

proof end;

registration

cluster Real_Lattice -> non empty strict Lattice-like distributive ;
coherence by Lemma9, LATTICES:def 11;

end;

definition

let c₁ be non empty set ;
func maxfuncreal c₁ -> BinOp of Funcs a₁,REAL means :Def5: :: REAL_LAT:def 5
for b₁, b₂ being Element of Funcs a₁,REAL holds a₂ . b₁,b₂ = maxreal .: b₁,b₂;
existence

proof end;

uniqueness

proof end;

func minfuncreal c₁ -> BinOp of Funcs a₁,REAL means :Def6: :: REAL_LAT:def 6
for b₁, b₂ being Element of Funcs a₁,REAL holds a₂ . b₁,b₂ = minreal .: b₁,b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines maxfuncreal REAL_LAT:def 5 :

:: deftheorem Def6 defines minfuncreal REAL_LAT:def 6 :

Lemma19: for b₁, b₂ being non empty set
for b₃ being Element of b₁
for b₄ being Function of b₁,b₂ holds b₃ in dom b₄

proof end;

theorem Th15: :: REAL_LAT:15

canceled;

theorem Th16: :: REAL_LAT:16

canceled;

theorem Th17: :: REAL_LAT:17

canceled;

theorem Th18: :: REAL_LAT:18

canceled;

theorem Th19: :: REAL_LAT:19

canceled;

theorem Th20: :: REAL_LAT:20

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (maxfuncreal b₁) . b₂,b₃ = (maxfuncreal b₁) . b₃,b₂

proof end;

theorem Th21: :: REAL_LAT:21

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (minfuncreal b₁) . b₂,b₃ = (minfuncreal b₁) . b₃,b₂

proof end;

theorem Th22: :: REAL_LAT:22

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL holds (maxfuncreal b₁) . ((maxfuncreal b₁) . b₂,b₃),b₄ = (maxfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄)

proof end;

theorem Th23: :: REAL_LAT:23

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL holds (minfuncreal b₁) . ((minfuncreal b₁) . b₂,b₃),b₄ = (minfuncreal b₁) . b₂,((minfuncreal b₁) . b₃,b₄)

proof end;

theorem Th24: :: REAL_LAT:24

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (maxfuncreal b₁) . b₂,((minfuncreal b₁) . b₂,b₃) = b₂

proof end;

theorem Th25: :: REAL_LAT:25

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (maxfuncreal b₁) . ((minfuncreal b₁) . b₂,b₃),b₂ = b₂

proof end;

theorem Th26: :: REAL_LAT:26

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (maxfuncreal b₁) . ((minfuncreal b₁) . b₂,b₃),b₃ = b₃

proof end;

theorem Th27: :: REAL_LAT:27

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (maxfuncreal b₁) . b₂,((minfuncreal b₁) . b₃,b₂) = b₂

proof end;

theorem Th28: :: REAL_LAT:28

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (minfuncreal b₁) . b₂,((maxfuncreal b₁) . b₂,b₃) = b₂

proof end;

theorem Th29: :: REAL_LAT:29

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (minfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₂) = b₂

proof end;

theorem Th30: :: REAL_LAT:30

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (minfuncreal b₁) . ((maxfuncreal b₁) . b₂,b₃),b₃ = b₃

proof end;

theorem Th31: :: REAL_LAT:31

for b₁ being non empty set
for b₂, b₃ being Element of Funcs b₁,REAL holds (minfuncreal b₁) . ((maxfuncreal b₁) . b₂,b₃),b₂ = b₂

proof end;

theorem Th32: :: REAL_LAT:32

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Funcs b₁,REAL holds (minfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄) = (maxfuncreal b₁) . ((minfuncreal b₁) . b₂,b₃),((minfuncreal b₁) . b₂,b₄)

proof end;

definition

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

end;

:: deftheorem Def7 REAL_LAT:def 7 :

:: deftheorem Def8 REAL_LAT:def 8 :

:: deftheorem Def9 defines @ REAL_LAT:def 9 :

Lemma31: for b₁ being non empty set
for b₂, b₃, b₄ being Element of LattStr(# (Funcs b₁,REAL ),(maxfuncreal b₁),(minfuncreal b₁) #) holds b₂ "\/" (b₃ "\/" b₄) = (b₂ "\/" b₃) "\/" b₄
by Th22;

Lemma32: for b₁ being non empty set
for b₂, b₃, b₄ being Element of LattStr(# (Funcs b₁,REAL ),(maxfuncreal b₁),(minfuncreal b₁) #) holds b₂ "/\" (b₃ "/\" b₄) = (b₂ "/\" b₃) "/\" b₄
by Th23;

definition

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

proof end;

end;

:: deftheorem Def10 defines RealFunc_Lattice REAL_LAT:def 10 :

theorem Th33: :: REAL_LAT:33

canceled;

theorem Th34: :: REAL_LAT:34

canceled;

theorem Th35: :: REAL_LAT:35

canceled;

theorem Th36: :: REAL_LAT:36

canceled;

theorem Th37: :: REAL_LAT:37

canceled;

theorem Th38: :: REAL_LAT:38

canceled;

theorem Th39: :: REAL_LAT:39

canceled;

theorem Th40: :: REAL_LAT:40

for b₁ being non empty set
for b₂, b₃ being Element of (RealFunc_Lattice b₁) holds (maxfuncreal b₁) . b₂,b₃ = (maxfuncreal b₁) . b₃,b₂

proof end;

theorem Th41: :: REAL_LAT:41

for b₁ being non empty set
for b₂, b₃ being Element of (RealFunc_Lattice b₁) holds (minfuncreal b₁) . b₂,b₃ = (minfuncreal b₁) . b₃,b₂

proof end;

theorem Th42: :: REAL_LAT:42

for b₁ being non empty set
for b₂, b₃, b₄ being Element of (RealFunc_Lattice b₁) holds
( (maxfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄) = (maxfuncreal b₁) . ((maxfuncreal b₁) . b₃,b₄),b₂ & (maxfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄) = (maxfuncreal b₁) . ((maxfuncreal b₁) . b₂,b₃),b₄ & (maxfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄) = (maxfuncreal b₁) . ((maxfuncreal b₁) . b₃,b₂),b₄ & (maxfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄) = (maxfuncreal b₁) . ((maxfuncreal b₁) . b₄,b₂),b₃ & (maxfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄) = (maxfuncreal b₁) . ((maxfuncreal b₁) . b₄,b₃),b₂ & (maxfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄) = (maxfuncreal b₁) . ((maxfuncreal b₁) . b₂,b₄),b₃ )

proof end;

theorem Th43: :: REAL_LAT:43

for b₁ being non empty set
for b₂, b₃, b₄ being Element of (RealFunc_Lattice b₁) holds
( (minfuncreal b₁) . b₂,((minfuncreal b₁) . b₃,b₄) = (minfuncreal b₁) . ((minfuncreal b₁) . b₃,b₄),b₂ & (minfuncreal b₁) . b₂,((minfuncreal b₁) . b₃,b₄) = (minfuncreal b₁) . ((minfuncreal b₁) . b₂,b₃),b₄ & (minfuncreal b₁) . b₂,((minfuncreal b₁) . b₃,b₄) = (minfuncreal b₁) . ((minfuncreal b₁) . b₃,b₂),b₄ & (minfuncreal b₁) . b₂,((minfuncreal b₁) . b₃,b₄) = (minfuncreal b₁) . ((minfuncreal b₁) . b₄,b₂),b₃ & (minfuncreal b₁) . b₂,((minfuncreal b₁) . b₃,b₄) = (minfuncreal b₁) . ((minfuncreal b₁) . b₄,b₃),b₂ & (minfuncreal b₁) . b₂,((minfuncreal b₁) . b₃,b₄) = (minfuncreal b₁) . ((minfuncreal b₁) . b₂,b₄),b₃ )

proof end;

theorem Th44: :: REAL_LAT:44

for b₁ being non empty set
for b₂, b₃ being Element of (RealFunc_Lattice b₁) holds
( (maxfuncreal b₁) . ((minfuncreal b₁) . b₂,b₃),b₃ = b₃ & (maxfuncreal b₁) . b₃,((minfuncreal b₁) . b₂,b₃) = b₃ & (maxfuncreal b₁) . b₃,((minfuncreal b₁) . b₃,b₂) = b₃ & (maxfuncreal b₁) . ((minfuncreal b₁) . b₃,b₂),b₃ = b₃ )

proof end;

theorem Th45: :: REAL_LAT:45

for b₁ being non empty set
for b₂, b₃ being Element of (RealFunc_Lattice b₁) holds
( (minfuncreal b₁) . b₂,((maxfuncreal b₁) . b₂,b₃) = b₂ & (minfuncreal b₁) . ((maxfuncreal b₁) . b₃,b₂),b₂ = b₂ & (minfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₂) = b₂ & (minfuncreal b₁) . ((maxfuncreal b₁) . b₂,b₃),b₂ = b₂ )

proof end;

theorem Th46: :: REAL_LAT:46

for b₁ being non empty set
for b₂, b₃, b₄ being Element of (RealFunc_Lattice b₁) holds (minfuncreal b₁) . b₂,((maxfuncreal b₁) . b₃,b₄) = (maxfuncreal b₁) . ((minfuncreal b₁) . b₂,b₃),((minfuncreal b₁) . b₂,b₄) by Th32;

theorem Th47: :: REAL_LAT:47

for b₁ being non empty set holds RealFunc_Lattice b₁ is D_Lattice

proof end;