begin
:: deftheorem LATTICE8:def 1 :
canceled;
:: deftheorem Def2 defines finitely_typed LATTICE8:def 2 :
for L being RelStr holds
( L is finitely_typed iff 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 Element of 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 ) ) );
:: deftheorem Def3 defines has_a_representation_of_type<= LATTICE8:def 3 :
for L being lower-bounded LATTICE
for n being Element of NAT holds
( L has_a_representation_of_type<= n iff 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 ) );
Lm1:
not 1 is even
Lm2:
2 is even
theorem Th1:
theorem
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
begin
theorem Th8:
theorem Th9:
:: deftheorem defines new_set2 LATTICE8:def 4 :
for A being set holds new_set2 A = A \/ {{A},{{A}}};
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:
( ( 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
ex b1 being BiFunction of (new_set2 A),L st
( ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({A},{{A}}) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) & b1 . ({{A}},{A}) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) & ( for u being Element of A holds
( b1 . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & b1 . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & b1 . (u,{{A}}) = (d . (u,(q `2))) "\/" (q `3) & b1 . ({{A}},u) = (d . (u,(q `2))) "\/" (q `3) ) ) )
uniqueness
for b1, b2 being BiFunction of (new_set2 A),L st ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({A},{{A}}) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) & b1 . ({{A}},{A}) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) & ( for u being Element of A holds
( b1 . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & b1 . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & b1 . (u,{{A}}) = (d . (u,(q `2))) "\/" (q `3) & b1 . ({{A}},u) = (d . (u,(q `2))) "\/" (q `3) ) ) & ( for u, v being Element of A holds b2 . (u,v) = d . (u,v) ) & b2 . ({A},{A}) = Bottom L & b2 . ({{A}},{{A}}) = Bottom L & b2 . ({A},{{A}}) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) & b2 . ({{A}},{A}) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) & ( for u being Element of A holds
( b2 . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & b2 . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & b2 . (u,{{A}}) = (d . (u,(q `2))) "\/" (q `3) & b2 . ({{A}},u) = (d . (u,(q `2))) "\/" (q `3) ) ) holds
b1 = b2
end;
:: deftheorem Def5 defines new_bi_fun2 LATTICE8:def 5 :
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:]
for b5 being BiFunction of (new_set2 A),L holds
( b5 = new_bi_fun2 (d,q) iff ( ( for u, v being Element of A holds b5 . (u,v) = d . (u,v) ) & b5 . ({A},{A}) = Bottom L & b5 . ({{A}},{{A}}) = Bottom L & b5 . ({A},{{A}}) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) & b5 . ({{A}},{A}) = ((d . ((q `1),(q `2))) "\/" (q `3)) "/\" (q `4) & ( for u being Element of A holds
( b5 . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & b5 . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & b5 . (u,{{A}}) = (d . (u,(q `2))) "\/" (q `3) & b5 . ({{A}},u) = (d . (u,(q `2))) "\/" (q `3) ) ) ) );
theorem Th10:
theorem Th11:
theorem Th12:
theorem
canceled;
theorem Th14:
:: deftheorem Def6 defines ConsecutiveSet2 LATTICE8:def 6 :
for A being non empty set
for O being Ordinal
for b3 being set holds
( b3 = ConsecutiveSet2 (A,O) iff ex L0 being T-Sequence st
( b3 = 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)) ) ) );
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
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:
q . O;
correctness
coherence
q . O is Element of [:(ConsecutiveSet2 (A,O)),(ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:];
end;
:: deftheorem Def7 defines Quadr2 LATTICE8:def 7 :
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 st O in dom q holds
Quadr2 (q,O) = q . O;
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:
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
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = 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)) ) );
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = 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)) ) ) & ex L0 being T-Sequence st
( b2 = 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)) ) ) holds
b1 = b2;
end;
:: deftheorem Def8 defines ConsecutiveDelta2 LATTICE8:def 8 :
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
for b6 being set holds
( b6 = ConsecutiveDelta2 (q,O) iff ex L0 being T-Sequence st
( b6 = 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)) ) ) );
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem
:: deftheorem defines NextSet2 LATTICE8:def 9 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L holds NextSet2 d = ConsecutiveSet2 (A,(DistEsti d));
:: deftheorem defines NextDelta2 LATTICE8:def 10 :
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 NextDelta2 q = ConsecutiveDelta2 (q,(DistEsti d));
:: deftheorem Def11 defines is_extension2_of LATTICE8:def 11 :
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 holds
( Aq,dq is_extension2_of A,d iff ex q being QuadrSeq of d st
( Aq = NextSet2 d & dq = NextDelta2 q ) );
theorem Th30:
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 )
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:
(
dom it = NAT &
it . 0 = [A,d] & ( for
n being
Element of
NAT ex
A9 being non
empty set ex
d9 being
distance_function of
A9,
L ex
Aq being non
empty set ex
dq being
distance_function of
Aq,
L st
(
Aq,
dq is_extension2_of A9,
d9 &
it . n = [A9,d9] &
it . (n + 1) = [Aq,dq] ) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = [A,d] & ( for n being Element of NAT ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & b1 . n = [A9,d9] & b1 . (n + 1) = [Aq,dq] ) ) )
end;
:: deftheorem Def12 defines ExtensionSeq2 LATTICE8:def 12 :
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for b4 being Function holds
( b4 is ExtensionSeq2 of A,d iff ( dom b4 = NAT & b4 . 0 = [A,d] & ( for n being Element of NAT ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension2_of A9,d9 & b4 . n = [A9,d9] & b4 . (n + 1) = [Aq,dq] ) ) ) );
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
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 Element of NAT : verum } &
FD = union { ((S . i) `2) where i is Element of 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 )
Lm3:
for m being Element of NAT holds
( not m in Seg 4 or m = 1 or m = 2 or m = 3 or m = 4 )
Lm4:
for j being Element of NAT st 1 <= j & j < 4 & not j = 1 & not j = 2 holds
j = 3
theorem Th35:
theorem Th36:
theorem