:: LATTICE8 semantic presentation

definition

let A be non empty set ;
let P, R be Relation of A;
:: original: c=
redefine pred P c= R means :: LATTICE8:def 1
for a, b being Element of A st [a,b] in P holds
[a,b] in R;
compatibility

proof end;

end;

:: deftheorem defines c= LATTICE8:def 1 :

definition

let L be RelStr ;
attr L is finitely_typed means :Def2: :: LATTICE8:def 2
ex A being non empty set st
( ( for e being set st e in the carrier of L holds
e is Equivalence_Relation of A ) & ex o being Nat st
for e1, e2 being Equivalence_Relation of A
for x, y being set st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of A st
( len F = o & x,y are_joint_by F,e1,e2 ) );

end;

:: deftheorem Def2 defines finitely_typed LATTICE8:def 2 :

definition

let L be lower-bounded LATTICE;
let n be Nat;
pred L has_a_representation_of_type<= n means :Def3: :: LATTICE8:def 3
ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st
( f is one-to-one & Image f is finitely_typed & ex e being Equivalence_Relation of A st
( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= n );

end;

:: deftheorem Def3 defines has_a_representation_of_type<= LATTICE8:def 3 :

registration

cluster lower-bounded distributive finite RelStr ;
existence

proof end;

end;

Lm1: not 1 is even

proof end;

Lm2: 2 is even

proof end;

registration

let A be non trivial set ;
cluster non empty full non trivial finitely_typed SubRelStr of EqRelLATT A;
existence

proof end;

end;

theorem Th1: :: LATTICE8:1

for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds succ {} c= DistEsti d

proof end;

theorem :: LATTICE8:2

for L being trivial Semilattice holds L is modular

proof end;

theorem :: LATTICE8:3

for A being non empty set
for L being non empty Sublattice of EqRelLATT A holds
( L is trivial or ex e being Equivalence_Relation of A st
( e in the carrier of L & e <> id A ) )

proof end;

theorem Th4: :: LATTICE8:4

for L1, L2 being lower-bounded LATTICE
for f being Function of L1,L2 st f is infs-preserving & f is sups-preserving holds
( f is meet-preserving & f is join-preserving )

proof end;

theorem Th5: :: LATTICE8:5

for L1, L2 being lower-bounded LATTICE st L1,L2 are_isomorphic & L1 is modular holds
L2 is modular

proof end;

theorem Th6: :: LATTICE8:6

for S being non empty lower-bounded Poset
for T being non empty Poset
for f being monotone Function of S,T holds Image f is lower-bounded

proof end;

theorem Th7: :: LATTICE8:7

for L being lower-bounded LATTICE
for x, y being Element of L
for A being non empty set
for f being Homomorphism of L,(EqRelLATT A) st f is one-to-one & (corestr f) . x <= (corestr f) . y holds
x <= y

proof end;

theorem Th8: :: LATTICE8:8

for A being non trivial set
for L being non empty full finitely_typed Sublattice of EqRelLATT A
for e being Equivalence_Relation of A st e in the carrier of L & e <> id A & type_of L <= 2 holds
L is modular

proof end;

theorem Th9: :: LATTICE8:9

for L being lower-bounded LATTICE st L has_a_representation_of_type<= 2 holds
L is modular

proof end;

definition

let A be set ;
func new_set2 A -> set equals :: LATTICE8:def 4
A \/ {{A},{{A}}};
correctness ;

end;

:: deftheorem defines new_set2 LATTICE8:def 4 :

registration

let A be set ;
cluster new_set2 A -> non empty ;
coherence

proof end;

end;

definition

let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
func new_bi_fun2 d,q -> BiFunction of (new_set2 A),L means :Def5: :: LATTICE8:def 5
( ( for u, v being Element of A holds it . u,v = d . u,v ) & it . {A},{A} = Bottom L & it . {{A}},{{A}} = Bottom L & it . {A},{{A}} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & it . {{A}},{A} = ((d . (q `1 ),(q `2 )) "\/" (q `3 )) "/\" (q `4 ) & ( for u being Element of A holds
( it . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & it . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & it . u,{{A}} = (d . u,(q `2 )) "\/" (q `3 ) & it . {{A}},u = (d . u,(q `2 )) "\/" (q `3 ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines new_bi_fun2 LATTICE8:def 5 :

theorem Th10: :: LATTICE8:10

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2 d,q is zeroed

proof end;

theorem Th11: :: LATTICE8:11

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun2 d,q is symmetric

proof end;

theorem Th12: :: LATTICE8:12

for A being non empty set
for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] st d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) holds
new_bi_fun2 d,q is u.t.i.

proof end;

theorem Th13: :: LATTICE8:13

for A being set holds A c= new_set2 A by XBOOLE_1:7;

theorem Th14: :: LATTICE8:14

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds d c= new_bi_fun2 d,q

proof end;

definition

let A be non empty set ;
let O be Ordinal;
func ConsecutiveSet2 A,O -> set means :Def6: :: LATTICE8:def 6
ex L0 being T-Sequence st
( it = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set2 (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness

proof end;

end;

:: deftheorem Def6 defines ConsecutiveSet2 LATTICE8:def 6 :

theorem Th15: :: LATTICE8:15

for A being non empty set holds ConsecutiveSet2 A,{} = A

proof end;

theorem Th16: :: LATTICE8:16

for A being non empty set
for O being Ordinal holds ConsecutiveSet2 A,(succ O) = new_set2 (ConsecutiveSet2 A,O)

proof end;

theorem Th17: :: LATTICE8:17

for A being non empty set
for O being Ordinal
for T being T-Sequence st O <> {} & O is_limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet2 A,O1 ) holds
ConsecutiveSet2 A,O = union (rng T)

proof end;

registration

let A be non empty set ;
let O be Ordinal;
cluster ConsecutiveSet2 A,O -> non empty ;
coherence

proof end;

end;

theorem Th18: :: LATTICE8:18

for A being non empty set
for O being Ordinal holds A c= ConsecutiveSet2 A,O

proof end;

definition

let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
assume A1: O in dom q ;
func Quadr2 q,O -> Element of [:(ConsecutiveSet2 A,O),(ConsecutiveSet2 A,O),the carrier of L,the carrier of L:] equals :Def7: :: LATTICE8:def 7
q . O;
correctness

proof end;

end;

:: deftheorem Def7 defines Quadr2 LATTICE8:def 7 :

definition

let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
func ConsecutiveDelta2 q,O -> set means :Def8: :: LATTICE8:def 8
ex L0 being T-Sequence st
( it = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun2 (BiFun (L0 . C),(ConsecutiveSet2 A,C),L),(Quadr2 q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness

proof end;

end;

:: deftheorem Def8 defines ConsecutiveDelta2 LATTICE8:def 8 :

theorem Th19: :: LATTICE8:19

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta2 q,{} = d

proof end;

theorem Th20: :: LATTICE8:20

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,(succ O) = new_bi_fun2 (BiFun (ConsecutiveDelta2 q,O),(ConsecutiveSet2 A,O),L),(Quadr2 q,O)

proof end;

theorem Th21: :: LATTICE8:21

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for T being T-Sequence
for O being Ordinal st O <> {} & O is_limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveDelta2 q,O1 ) holds
ConsecutiveDelta2 q,O = union (rng T)

proof end;

theorem Th22: :: LATTICE8:22

for A being non empty set
for O, O1, O2 being Ordinal st O1 c= O2 holds
ConsecutiveSet2 A,O1 c= ConsecutiveSet2 A,O2

proof end;

theorem Th23: :: LATTICE8:23

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is BiFunction of (ConsecutiveSet2 A,O),L

proof end;

definition

let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
:: original: ConsecutiveDelta2
redefine func ConsecutiveDelta2 q,O -> BiFunction of (ConsecutiveSet2 A,O),L;
coherence by Th23;

end;

theorem Th24: :: LATTICE8:24

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds d c= ConsecutiveDelta2 q,O

proof end;

theorem Th25: :: LATTICE8:25

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for O1, O2 being Ordinal
for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta2 q,O1 c= ConsecutiveDelta2 q,O2

proof end;

theorem Th26: :: LATTICE8:26

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is zeroed

proof end;

theorem Th27: :: LATTICE8:27

for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is symmetric

proof end;

theorem Th28: :: LATTICE8:28

for A being non empty set
for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 q,O is u.t.i.

proof end;

theorem :: LATTICE8:29

for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 q,O is distance_function of (ConsecutiveSet2 A,O),L by Th26, Th27, Th28;

definition

let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
func NextSet2 d -> set equals :: LATTICE8:def 9
ConsecutiveSet2 A,(DistEsti d);
correctness ;

end;

:: deftheorem defines NextSet2 LATTICE8:def 9 :

registration

let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
cluster NextSet2 d -> non empty ;
coherence ;

end;

definition

let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
func NextDelta2 q -> set equals :: LATTICE8:def 10
ConsecutiveDelta2 q,(DistEsti d);
correctness ;

end;

:: deftheorem defines NextDelta2 LATTICE8:def 10 :

definition

let A be non empty set ;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let q be QuadrSeq of d;
:: original: NextDelta2
redefine func NextDelta2 q -> distance_function of (NextSet2 d),L;
coherence by Th26, Th27, Th28;

end;

definition

let A be non empty set ;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set ;
let dq be distance_function of Aq,L;
pred Aq,dq is_extension2_of A,d means :Def11: :: LATTICE8:def 11
ex q being QuadrSeq of d st
( Aq = NextSet2 d & dq = NextDelta2 q );

end;

:: deftheorem Def11 defines is_extension2_of LATTICE8:def 11 :

theorem Th30: :: LATTICE8:30

for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension2_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . x,y <= a "\/" b holds
ex z1, z2 being Element of Aq st
( dq . x,z1 = a & dq . z1,z2 = ((d . x,y) "\/" a) "/\" b & dq . z2,y = a )

proof end;

definition

let A be non empty set ;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
mode ExtensionSeq2 of A,d -> Function means :Def12: :: LATTICE8:def 12
( dom it = NAT & it . 0 = [A,d] & ( for n being Nat ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A',d' & it . n = [A',d'] & it . (n + 1) = [Aq,dq] ) ) );
existence

proof end;

end;

:: deftheorem Def12 defines ExtensionSeq2 LATTICE8:def 12 :

theorem Th31: :: LATTICE8:31

for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) `1 c= (S . l) `1

proof end;

theorem Th32: :: LATTICE8:32

for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for S being ExtensionSeq2 of A,d
for k, l being Nat st k <= l holds
(S . k) `2 c= (S . l) `2

proof end;

theorem Th33: :: LATTICE8:33

for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set st FS = union { ((S . i) `1 ) where i is Nat : verum } holds
union { ((S . i) `2 ) where i is Nat : verum } is distance_function of FS,L

proof end;

theorem Th34: :: LATTICE8:34

for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1 ) where i is Nat : verum } & FD = union { ((S . i) `2 ) where i is Nat : verum } & FD . x,y <= a "\/" b holds
ex z1, z2 being Element of FS st
( FD . x,z1 = a & FD . z1,z2 = ((FD . x,y) "\/" a) "/\" b & FD . z2,y = a )

proof end;

Lm3: for m being Nat holds
( not m in Seg 4 or m = 1 or m = 2 or m = 3 or m = 4 )

proof end;

Lm4: for j being Nat st 1 <= j & j < 4 & not j = 1 & not j = 2 holds
j = 3

proof end;

theorem Th35: :: LATTICE8:35

for L being lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for f being Homomorphism of L,(EqRelLATT FS)
for e1, e2 being Equivalence_Relation of FS
for x, y being set st f = alpha FD & FS = union { ((S . i) `1 ) where i is Nat : verum } & FD = union { ((S . i) `2 ) where i is Nat : verum } & e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 2 + 2 & x,y are_joint_by F,e1,e2 )

proof end;

theorem Th36: :: LATTICE8:36

for L being lower-bounded modular LATTICE holds L has_a_representation_of_type<= 2

proof end;

theorem :: LATTICE8:37

for L being lower-bounded LATTICE holds
( L has_a_representation_of_type<= 2 iff L is modular ) by Th9, Th36;