begin
theorem Th1:
theorem Th2:
theorem Th3:
begin
:: deftheorem defines EqRelLATT LATTICE5:def 1 :
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
:: deftheorem defines complete LATTICE5:def 2 :
begin
:: deftheorem Def3 defines are_joint_by LATTICE5:def 3 :
theorem
canceled;
theorem Th12:
Lm1:
now
let i,
n,
m be
Element of
NAT ;
( 1 <= i & i < n + m & not ( 1 <= i & i < n ) & not ( n = i & i < n + m ) implies ( n + 1 <= i & i < n + m ) )assume
( 1
<= i &
i < n + m )
;
( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n + 1 <= i & i < n + m ) )then
( ( 1
<= i &
i < n ) or (
n = i &
i < n + m ) or (
n < i &
i < n + m ) )
by XXREAL_0:1;
hence
( ( 1
<= i &
i < n ) or (
n = i &
i < n + m ) or (
n + 1
<= i &
i < n + m ) )
by NAT_1:13;
verum
end;
theorem
canceled;
theorem Th14:
definition
let X be non
empty set ;
let Y be
Sublattice of
EqRelLATT X;
given e being
Equivalence_Relation of
X such that A1:
e in the
carrier of
Y
and A2:
e <> id X
;
given o being
Element of
NAT such that A3:
for
e1,
e2 being
Equivalence_Relation of
X for
x,
y being
set st
e1 in the
carrier of
Y &
e2 in the
carrier of
Y &
[x,y] in e1 "\/" e2 holds
ex
F being non
empty FinSequence of
X st
(
len F = o &
x,
y are_joint_by F,
e1,
e2 )
;
func type_of Y -> Element of
NAT means :
Def4:
( ( for
e1,
e2 being
Equivalence_Relation of
X for
x,
y being
set st
e1 in the
carrier of
Y &
e2 in the
carrier of
Y &
[x,y] in e1 "\/" e2 holds
ex
F being non
empty FinSequence of
X st
(
len F = it + 2 &
x,
y are_joint_by F,
e1,
e2 ) ) & ex
e1,
e2 being
Equivalence_Relation of
X ex
x,
y being
set st
(
e1 in the
carrier of
Y &
e2 in the
carrier of
Y &
[x,y] in e1 "\/" e2 & ( for
F being non
empty FinSequence of
X holds
( not
len F = it + 1 or not
x,
y are_joint_by F,
e1,
e2 ) ) ) );
existence
ex b1 being Element of NAT st
( ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) )
uniqueness
for b1, b2 being Element of NAT st ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) & ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b2 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b2 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) holds
b1 = b2
end;
:: deftheorem Def4 defines type_of LATTICE5:def 4 :
for
X being non
empty set for
Y being
Sublattice of
EqRelLATT X st ex
e being
Equivalence_Relation of
X st
(
e in the
carrier of
Y &
e <> id X ) & ex
o being
Element of
NAT st
for
e1,
e2 being
Equivalence_Relation of
X for
x,
y being
set st
e1 in the
carrier of
Y &
e2 in the
carrier of
Y &
[x,y] in e1 "\/" e2 holds
ex
F being non
empty FinSequence of
X st
(
len F = o &
x,
y are_joint_by F,
e1,
e2 ) holds
for
b3 being
Element of
NAT holds
(
b3 = type_of Y iff ( ( for
e1,
e2 being
Equivalence_Relation of
X for
x,
y being
set st
e1 in the
carrier of
Y &
e2 in the
carrier of
Y &
[x,y] in e1 "\/" e2 holds
ex
F being non
empty FinSequence of
X st
(
len F = b3 + 2 &
x,
y are_joint_by F,
e1,
e2 ) ) & ex
e1,
e2 being
Equivalence_Relation of
X ex
x,
y being
set st
(
e1 in the
carrier of
Y &
e2 in the
carrier of
Y &
[x,y] in e1 "\/" e2 & ( for
F being non
empty FinSequence of
X holds
( not
len F = b3 + 1 or not
x,
y are_joint_by F,
e1,
e2 ) ) ) ) );
theorem Th15:
begin
:: deftheorem LATTICE5:def 5 :
canceled;
:: deftheorem Def6 defines symmetric LATTICE5:def 6 :
:: deftheorem Def7 defines zeroed LATTICE5:def 7 :
:: deftheorem Def8 defines u.t.i. LATTICE5:def 8 :
definition
let A be non
empty set ;
let L be
lower-bounded LATTICE;
let d be
distance_function of
A,
L;
func alpha d -> Function of
L,
(EqRelLATT A) means :
Def9:
for
e being
Element of
L ex
E being
Equivalence_Relation of
A st
(
E = it . e & ( for
x,
y being
Element of
A holds
(
[x,y] in E iff
d . x,
y <= e ) ) );
existence
ex b1 being Function of L,(EqRelLATT A) st
for e being Element of L ex E being Equivalence_Relation of A st
( E = b1 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) )
uniqueness
for b1, b2 being Function of L,(EqRelLATT A) st ( for e being Element of L ex E being Equivalence_Relation of A st
( E = b1 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) ) ) & ( for e being Element of L ex E being Equivalence_Relation of A st
( E = b2 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def9 defines alpha LATTICE5:def 9 :
theorem Th16:
theorem Th17:
begin
:: deftheorem defines new_set LATTICE5:def 10 :
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_fun d,
q -> BiFunction of
(new_set A),
L means :
Def11:
( ( 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}}} = Bottom L &
it . {{A}},
{{{A}}} = q `3 &
it . {{{A}}},
{{A}} = q `3 &
it . {A},
{{A}} = q `4 &
it . {{A}},
{A} = q `4 &
it . {A},
{{{A}}} = (q `3 ) "\/" (q `4 ) &
it . {{{A}}},
{A} = (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 `1 )) "\/" (q `3 )) "\/" (q `4 ) &
it . {{A}},
u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) &
it . u,
{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) &
it . {{{A}}},
u = (d . u,(q `2 )) "\/" (q `4 ) ) ) );
existence
ex b1 being BiFunction of (new_set 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}}} = Bottom L & b1 . {{A}},{{{A}}} = q `3 & b1 . {{{A}}},{{A}} = q `3 & b1 . {A},{{A}} = q `4 & b1 . {{A}},{A} = q `4 & b1 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & b1 . {{{A}}},{A} = (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 `1 )) "\/" (q `3 )) "\/" (q `4 ) & b1 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b1 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & b1 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) )
uniqueness
for b1, b2 being BiFunction of (new_set 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}}} = Bottom L & b1 . {{A}},{{{A}}} = q `3 & b1 . {{{A}}},{{A}} = q `3 & b1 . {A},{{A}} = q `4 & b1 . {{A}},{A} = q `4 & b1 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & b1 . {{{A}}},{A} = (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 `1 )) "\/" (q `3 )) "\/" (q `4 ) & b1 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b1 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & b1 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) & ( 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}}} = Bottom L & b2 . {{A}},{{{A}}} = q `3 & b2 . {{{A}}},{{A}} = q `3 & b2 . {A},{{A}} = q `4 & b2 . {{A}},{A} = q `4 & b2 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & b2 . {{{A}}},{A} = (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 `1 )) "\/" (q `3 )) "\/" (q `4 ) & b2 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b2 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & b2 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines new_bi_fun LATTICE5:def 11 :
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_set A),
L holds
(
b5 = new_bi_fun 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}}} = Bottom L &
b5 . {{A}},
{{{A}}} = q `3 &
b5 . {{{A}}},
{{A}} = q `3 &
b5 . {A},
{{A}} = q `4 &
b5 . {{A}},
{A} = q `4 &
b5 . {A},
{{{A}}} = (q `3 ) "\/" (q `4 ) &
b5 . {{{A}}},
{A} = (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 `1 )) "\/" (q `3 )) "\/" (q `4 ) &
b5 . {{A}},
u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) &
b5 . u,
{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) &
b5 . {{{A}}},
u = (d . u,(q `2 )) "\/" (q `4 ) ) ) ) );
theorem Th18:
theorem Th19:
theorem Th20:
theorem
canceled;
theorem Th22:
definition
let A be non
empty set ;
let L be
lower-bounded LATTICE;
let d be
BiFunction of
A,
L;
func DistEsti d -> Cardinal means :
Def12:
it,
{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent ;
existence
ex b1 being Cardinal st b1,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent
uniqueness
for b1, b2 being Cardinal st b1,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent & b2,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent holds
b1 = b2
end;
:: deftheorem Def12 defines DistEsti LATTICE5:def 12 :
theorem Th23:
:: deftheorem Def13 defines ConsecutiveSet LATTICE5:def 13 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
definition
let A be non
empty set ;
let L be
lower-bounded LATTICE;
let d be
BiFunction of
A,
L;
mode QuadrSeq of
d -> T-Sequence of
[:A,A,the carrier of L,the carrier of L:] means :
Def14:
(
dom it is
Cardinal &
it is
one-to-one &
rng it = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } );
existence
ex b1 being T-Sequence of [:A,A,the carrier of L,the carrier of L:] st
( dom b1 is Cardinal & b1 is one-to-one & rng b1 = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } )
end;
:: deftheorem Def14 defines QuadrSeq LATTICE5:def 14 :
for
A being non
empty set for
L being
lower-bounded LATTICE for
d being
BiFunction of
A,
L for
b4 being
T-Sequence of
[:A,A,the carrier of L,the carrier of L:] holds
(
b4 is
QuadrSeq of
d iff (
dom b4 is
Cardinal &
b4 is
one-to-one &
rng b4 = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } ) );
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 Quadr q,
O -> Element of
[:(ConsecutiveSet A,O),(ConsecutiveSet A,O),the carrier of L,the carrier of L:] equals :
Def15:
q . O;
correctness
coherence
q . O is Element of [:(ConsecutiveSet A,O),(ConsecutiveSet A,O),the carrier of L,the carrier of L:];
end;
:: deftheorem Def15 defines Quadr LATTICE5:def 15 :
theorem Th28:
:: deftheorem Def16 defines BiFun LATTICE5:def 16 :
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 ConsecutiveDelta q,
O -> set means :
Def17:
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_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),
(Quadr 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_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),(Quadr 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_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),(Quadr 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_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),(Quadr 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 Def17 defines ConsecutiveDelta LATTICE5:def 17 :
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
:: deftheorem defines NextSet LATTICE5:def 18 :
:: deftheorem defines NextDelta LATTICE5:def 19 :
:: deftheorem Def20 defines is_extension_of LATTICE5:def 20 :
theorem Th40:
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_extension_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,
z3 being
Element of
Aq st
(
dq . x,
z1 = a &
dq . z2,
z3 = a &
dq . z1,
z2 = b &
dq . z3,
y = b )
definition
let A be non
empty set ;
let L be
lower-bounded LATTICE;
let d be
distance_function of
A,
L;
mode ExtensionSeq of
A,
d -> Function means :
Def21:
(
dom it = NAT &
it . 0 = [A,d] & ( for
n being
Element of
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_extension_of A',
d' &
it . n = [A',d'] &
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 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_extension_of A',d' & b1 . n = [A',d'] & b1 . (n + 1) = [Aq,dq] ) ) )
end;
:: deftheorem Def21 defines ExtensionSeq LATTICE5:def 21 :
theorem Th41:
theorem Th42:
definition
let L be
lower-bounded LATTICE;
func BasicDF L -> distance_function of the
carrier of
L,
L means :
Def22:
for
x,
y being
Element of
L holds
( (
x <> y implies
it . x,
y = x "\/" y ) & (
x = y implies
it . x,
y = Bottom L ) );
existence
ex b1 being distance_function of the carrier of L,L st
for x, y being Element of L holds
( ( x <> y implies b1 . x,y = x "\/" y ) & ( x = y implies b1 . x,y = Bottom L ) )
uniqueness
for b1, b2 being distance_function of the carrier of L,L st ( for x, y being Element of L holds
( ( x <> y implies b1 . x,y = x "\/" y ) & ( x = y implies b1 . x,y = Bottom L ) ) ) & ( for x, y being Element of L holds
( ( x <> y implies b2 . x,y = x "\/" y ) & ( x = y implies b2 . x,y = Bottom L ) ) ) holds
b1 = b2
end;
:: deftheorem Def22 defines BasicDF LATTICE5:def 22 :
theorem Th43:
Lm2:
now
let j be
Element of
NAT ;
( 1 <= j & j < 5 & not j = 1 & not j = 2 & not j = 3 implies j = 4 )assume that A1:
1
<= j
and A2:
j < 5
;
( j = 1 or j = 2 or j = 3 or j = 4 )
j < 4
+ 1
by A2;
then
j <= 4
by NAT_1:13;
then
(
j = 0 or
j = 1 or
j = 2 or
j = 3 or
j = 4 )
by NAT_1:29;
hence
(
j = 1 or
j = 2 or
j = 3 or
j = 4 )
by A1;
verum
end;
theorem Th44:
theorem Th45:
for
L being
lower-bounded LATTICE for
S being
ExtensionSeq 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,
z3 being
Element of
FS st
(
FD . x,
z1 = a &
FD . z2,
z3 = a &
FD . z1,
z2 = b &
FD . z3,
y = b )
theorem Th46:
for
L being
lower-bounded LATTICE for
S being
ExtensionSeq 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
x,
y being
Element of
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 Element of NAT : verum } &
FD = union { ((S . i) `2 ) where i is Element of 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 = 3
+ 2 &
x,
y are_joint_by F,
e1,
e2 )
theorem