let L be lower-bounded LATTICE; for S being ExtensionSeq of the carrier of L, BasicDF L
for FS being non empty set st FS = union { ((S . i) `1) where i is Element of NAT : verum } holds
union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L
let S be ExtensionSeq of the carrier of L, BasicDF L; for FS being non empty set st FS = union { ((S . i) `1) where i is Element of NAT : verum } holds
union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L
let FS be non empty set ; ( FS = union { ((S . i) `1) where i is Element of NAT : verum } implies union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L )
assume A1:
FS = union { ((S . i) `1) where i is Element of NAT : verum }
; union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L
reconsider FS = FS as non empty set ;
set A = the carrier of L;
set FD = union { ((S . i) `2) where i is Element of NAT : verum } ;
then A6:
{ ((S . i) `2) where i is Element of NAT : verum } is c=-linear
;
{ ((S . i) `2) where i is Element of NAT : verum } c= PFuncs ([:FS,FS:], the carrier of L)
proof
let z be
object ;
TARSKI:def 3 ( not z in { ((S . i) `2) where i is Element of NAT : verum } or z in PFuncs ([:FS,FS:], the carrier of L) )
assume
z in { ((S . i) `2) where i is Element of NAT : verum }
;
z in PFuncs ([:FS,FS:], the carrier of L)
then consider j being
Element of
NAT such that A7:
z = (S . j) `2
;
consider A9 being non
empty set ,
d9 being
distance_function of
A9,
L,
Aq being non
empty set ,
dq being
distance_function of
Aq,
L such that
Aq,
dq is_extension_of A9,
d9
and A8:
S . j = [A9,d9]
and
S . (j + 1) = [Aq,dq]
by Def20;
A9 = [A9,d9] `1
;
then
A9 in { ((S . i) `1) where i is Element of NAT : verum }
by A8;
then
(
dom d9 = [:A9,A9:] &
A9 c= FS )
by A1, FUNCT_2:def 1, ZFMISC_1:74;
then A9:
(
rng d9 c= the
carrier of
L &
dom d9 c= [:FS,FS:] )
by ZFMISC_1:96;
z = d9
by A7, A8;
hence
z in PFuncs (
[:FS,FS:], the
carrier of
L)
by A9, PARTFUN1:def 3;
verum
end;
then
union { ((S . i) `2) where i is Element of NAT : verum } in PFuncs ([:FS,FS:], the carrier of L)
by A6, TREES_2:40;
then A10:
ex g being Function st
( union { ((S . i) `2) where i is Element of NAT : verum } = g & dom g c= [:FS,FS:] & rng g c= the carrier of L )
by PARTFUN1:def 3;
(S . 0) `1 in { ((S . i) `1) where i is Element of NAT : verum }
;
then reconsider X = { ((S . i) `1) where i is Element of NAT : verum } as non empty set ;
set LL = { [:I,I:] where I is Element of X : I in X } ;
set PP = { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } ;
defpred S1[ object , object ] means $2 = (S . $1) `2 ;
A11:
{ [:I,I:] where I is Element of X : I in X } = { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
proof
thus
{ [:I,I:] where I is Element of X : I in X } c= { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
XBOOLE_0:def 10 { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } c= { [:I,I:] where I is Element of X : I in X }
let x be
object ;
TARSKI:def 3 ( not x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } or x in { [:I,I:] where I is Element of X : I in X } )
assume
x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
;
x in { [:I,I:] where I is Element of X : I in X }
then consider j being
Element of
NAT such that A14:
x = [:((S . j) `1),((S . j) `1):]
;
(S . j) `1 in X
;
hence
x in { [:I,I:] where I is Element of X : I in X }
by A14;
verum
end;
reconsider FD = union { ((S . i) `2) where i is Element of NAT : verum } as Function by A10;
A15:
for x being object st x in NAT holds
ex y being object st S1[x,y]
;
consider F being Function such that
A16:
dom F = NAT
and
A17:
for x being object st x in NAT holds
S1[x,F . x]
from CLASSES1:sch 1(A15);
A18:
rng F = { ((S . i) `2) where i is Element of NAT : verum }
F is Function-yielding
proof
let x be
object ;
FUNCOP_1:def 6 ( not x in proj1 F or F . x is set )
assume
x in dom F
;
F . x is set
then reconsider j =
x as
Element of
NAT by A16;
consider A1 being non
empty set ,
d1 being
distance_function of
A1,
L,
Aq1 being non
empty set ,
dq1 being
distance_function of
Aq1,
L such that
Aq1,
dq1 is_extension_of A1,
d1
and A22:
S . j = [A1,d1]
and
S . (j + 1) = [Aq1,dq1]
by Def20;
[A1,d1] `2 = d1
;
hence
F . x is
set
by A17, A22;
verum
end;
then reconsider F = F as Function-yielding Function ;
A23:
rng (doms F) = { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
proof
thus
rng (doms F) c= { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
XBOOLE_0:def 10 { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } c= rng (doms F)proof
let x be
object ;
TARSKI:def 3 ( not x in rng (doms F) or x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } )
assume
x in rng (doms F)
;
x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
then consider j being
object such that A24:
j in dom (doms F)
and A25:
x = (doms F) . j
by FUNCT_1:def 3;
A26:
j in dom F
by A24, FUNCT_6:59;
reconsider j =
j as
Element of
NAT by A16, A24, FUNCT_6:59;
consider A1 being non
empty set ,
d1 being
distance_function of
A1,
L,
Aq1 being non
empty set ,
dq1 being
distance_function of
Aq1,
L such that
Aq1,
dq1 is_extension_of A1,
d1
and A27:
S . j = [A1,d1]
and
S . (j + 1) = [Aq1,dq1]
by Def20;
A28:
[A1,d1] `2 = d1
;
x =
dom (F . j)
by A25, A26, FUNCT_6:22
.=
dom d1
by A17, A28, A27
.=
[:((S . j) `1),((S . j) `1):]
by A27, FUNCT_2:def 1
;
hence
x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum } or x in rng (doms F) )
assume
x in { [:((S . i) `1),((S . i) `1):] where i is Element of NAT : verum }
;
x in rng (doms F)
then consider j being
Element of
NAT such that A29:
x = [:((S . j) `1),((S . j) `1):]
;
consider A1 being non
empty set ,
d1 being
distance_function of
A1,
L,
Aq1 being non
empty set ,
dq1 being
distance_function of
Aq1,
L such that
Aq1,
dq1 is_extension_of A1,
d1
and A30:
S . j = [A1,d1]
and
S . (j + 1) = [Aq1,dq1]
by Def20;
A31:
[A1,d1] `2 = d1
;
j in NAT
;
then A32:
j in dom (doms F)
by A16, FUNCT_6:59;
x =
dom d1
by A29, A30, FUNCT_2:def 1
.=
dom (F . j)
by A17, A31, A30
.=
(doms F) . j
by A16, FUNCT_6:22
;
hence
x in rng (doms F)
by A32, FUNCT_1:def 3;
verum
end;
then
X is c=-linear
;
then [:FS,FS:] =
union (rng (doms F))
by A1, A23, A11, Th3
.=
dom FD
by A18, Th1
;
then reconsider FD = FD as BiFunction of FS,L by A10, FUNCT_2:def 1, RELSET_1:4;
A37:
FD is symmetric
proof
let x,
y be
Element of
FS;
LATTICE5:def 5 FD . (x,y) = FD . (y,x)
consider x1 being
set such that A38:
x in x1
and A39:
x1 in X
by A1, TARSKI:def 4;
consider k being
Element of
NAT such that A40:
x1 = (S . k) `1
by A39;
consider A1 being non
empty set ,
d1 being
distance_function of
A1,
L,
Aq1 being non
empty set ,
dq1 being
distance_function of
Aq1,
L such that
Aq1,
dq1 is_extension_of A1,
d1
and A41:
S . k = [A1,d1]
and
S . (k + 1) = [Aq1,dq1]
by Def20;
A42:
[A1,d1] `1 = A1
;
A43:
x in A1
by A38, A40, A41;
[A1,d1] `2 = d1
;
then
d1 in { ((S . i) `2) where i is Element of NAT : verum }
by A41;
then A44:
d1 c= FD
by ZFMISC_1:74;
consider y1 being
set such that A45:
y in y1
and A46:
y1 in X
by A1, TARSKI:def 4;
consider l being
Element of
NAT such that A47:
y1 = (S . l) `1
by A46;
consider A2 being non
empty set ,
d2 being
distance_function of
A2,
L,
Aq2 being non
empty set ,
dq2 being
distance_function of
Aq2,
L such that
Aq2,
dq2 is_extension_of A2,
d2
and A48:
S . l = [A2,d2]
and
S . (l + 1) = [Aq2,dq2]
by Def20;
A49:
[A2,d2] `1 = A2
;
A50:
y in A2
by A45, A47, A48;
[A2,d2] `2 = d2
;
then
d2 in { ((S . i) `2) where i is Element of NAT : verum }
by A48;
then A51:
d2 c= FD
by ZFMISC_1:74;
per cases
( k <= l or l <= k )
;
suppose
k <= l
;
FD . (x,y) = FD . (y,x)then
A1 c= A2
by A42, A49, Th38, A41, A48;
then reconsider x9 =
x,
y9 =
y as
Element of
A2 by A43, A50;
A52:
dom d2 = [:A2,A2:]
by FUNCT_2:def 1;
hence FD . (
x,
y) =
d2 . [x9,y9]
by A51, GRFUNC_1:2
.=
d2 . (
x9,
y9)
.=
d2 . (
y9,
x9)
by Def5
.=
FD . [y9,x9]
by A51, A52, GRFUNC_1:2
.=
FD . (
y,
x)
;
verum end; suppose
l <= k
;
FD . (x,y) = FD . (y,x)then
A2 c= A1
by A42, A49, Th38, A48, A41;
then reconsider x9 =
x,
y9 =
y as
Element of
A1 by A38, A40, A41, A50;
A53:
dom d1 = [:A1,A1:]
by FUNCT_2:def 1;
hence FD . (
x,
y) =
d1 . [x9,y9]
by A44, GRFUNC_1:2
.=
d1 . (
x9,
y9)
.=
d1 . (
y9,
x9)
by Def5
.=
FD . [y9,x9]
by A44, A53, GRFUNC_1:2
.=
FD . (
y,
x)
;
verum end; end;
end;
A54:
FD is u.t.i.
proof
let x,
y,
z be
Element of
FS;
LATTICE5:def 7 (FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)
consider x1 being
set such that A55:
x in x1
and A56:
x1 in X
by A1, TARSKI:def 4;
consider k being
Element of
NAT such that A57:
x1 = (S . k) `1
by A56;
consider A1 being non
empty set ,
d1 being
distance_function of
A1,
L,
Aq1 being non
empty set ,
dq1 being
distance_function of
Aq1,
L such that
Aq1,
dq1 is_extension_of A1,
d1
and A58:
S . k = [A1,d1]
and
S . (k + 1) = [Aq1,dq1]
by Def20;
A59:
x in A1
by A55, A57, A58;
[A1,d1] `2 = d1
;
then
d1 in { ((S . i) `2) where i is Element of NAT : verum }
by A58;
then A60:
d1 c= FD
by ZFMISC_1:74;
A61:
dom d1 = [:A1,A1:]
by FUNCT_2:def 1;
A62:
(S . k) `1 = A1
by A58;
consider y1 being
set such that A63:
y in y1
and A64:
y1 in X
by A1, TARSKI:def 4;
consider l being
Element of
NAT such that A65:
y1 = (S . l) `1
by A64;
consider A2 being non
empty set ,
d2 being
distance_function of
A2,
L,
Aq2 being non
empty set ,
dq2 being
distance_function of
Aq2,
L such that
Aq2,
dq2 is_extension_of A2,
d2
and A66:
S . l = [A2,d2]
and
S . (l + 1) = [Aq2,dq2]
by Def20;
A67:
y in A2
by A63, A65, A66;
[A2,d2] `2 = d2
;
then
d2 in { ((S . i) `2) where i is Element of NAT : verum }
by A66;
then A68:
d2 c= FD
by ZFMISC_1:74;
A69:
dom d2 = [:A2,A2:]
by FUNCT_2:def 1;
A70:
[A2,d2] `1 = A2
;
consider z1 being
set such that A71:
z in z1
and A72:
z1 in X
by A1, TARSKI:def 4;
consider n being
Element of
NAT such that A73:
z1 = (S . n) `1
by A72;
consider A3 being non
empty set ,
d3 being
distance_function of
A3,
L,
Aq3 being non
empty set ,
dq3 being
distance_function of
Aq3,
L such that
Aq3,
dq3 is_extension_of A3,
d3
and A74:
S . n = [A3,d3]
and
S . (n + 1) = [Aq3,dq3]
by Def20;
A75:
[A3,d3] `1 = A3
;
A76:
z in A3
by A71, A73, A74;
[A3,d3] `2 = d3
;
then
d3 in { ((S . i) `2) where i is Element of NAT : verum }
by A74;
then A77:
d3 c= FD
by ZFMISC_1:74;
A78:
dom d3 = [:A3,A3:]
by FUNCT_2:def 1;
per cases
( k <= l or l <= k )
;
suppose
k <= l
;
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)then A79:
A1 c= A2
by A62, A70, Th38, A66;
thus
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (
x,
z)
verumproof
per cases
( l <= n or n <= l )
;
suppose
l <= n
;
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)then A80:
A2 c= A3
by A70, A75, Th38, A74, A66;
then
A1 c= A3
by A79;
then reconsider x9 =
x,
y9 =
y as
Element of
A3 by A59, A67, A80;
reconsider z9 =
z as
Element of
A3 by A76;
A81:
FD . (
y,
z) =
d3 . [y9,z9]
by A77, A78, GRFUNC_1:2
.=
d3 . (
y9,
z9)
;
A82:
FD . (
x,
z) =
d3 . [x9,z9]
by A77, A78, GRFUNC_1:2
.=
d3 . (
x9,
z9)
;
FD . (
x,
y) =
d3 . [x9,y9]
by A77, A78, GRFUNC_1:2
.=
d3 . (
x9,
y9)
;
hence
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (
x,
z)
by A81, A82, Def7;
verum end; suppose
n <= l
;
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)then A83:
A3 c= A2
by A70, A75, Th38, A74, A66;
reconsider y9 =
y as
Element of
A2 by A67;
reconsider x9 =
x as
Element of
A2 by A59, A79;
reconsider z9 =
z as
Element of
A2 by A76, A83;
A84:
FD . (
y,
z) =
d2 . [y9,z9]
by A68, A69, GRFUNC_1:2
.=
d2 . (
y9,
z9)
;
A85:
FD . (
x,
z) =
d2 . [x9,z9]
by A68, A69, GRFUNC_1:2
.=
d2 . (
x9,
z9)
;
FD . (
x,
y) =
d2 . [x9,y9]
by A68, A69, GRFUNC_1:2
.=
d2 . (
x9,
y9)
;
hence
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (
x,
z)
by A84, A85, Def7;
verum end; end;
end; end; suppose
l <= k
;
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)then A86:
A2 c= A1
by A62, A70, Th38, A66;
thus
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (
x,
z)
verumproof
per cases
( k <= n or n <= k )
;
suppose
k <= n
;
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)then A87:
A1 c= A3
by A62, A75, Th38, A74;
then A88:
A2 c= A3
by A86;
reconsider x9 =
x as
Element of
A3 by A59, A87;
reconsider z9 =
z as
Element of
A3 by A71, A73, A74;
reconsider y9 =
y as
Element of
A3 by A67, A88;
A89:
FD . (
y,
z) =
d3 . [y9,z9]
by A77, A78, GRFUNC_1:2
.=
d3 . (
y9,
z9)
;
A90:
FD . (
x,
z) =
d3 . [x9,z9]
by A77, A78, GRFUNC_1:2
.=
d3 . (
x9,
z9)
;
FD . (
x,
y) =
d3 . [x9,y9]
by A77, A78, GRFUNC_1:2
.=
d3 . (
x9,
y9)
;
hence
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (
x,
z)
by A89, A90, Def7;
verum end; suppose
n <= k
;
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (x,z)then
A3 c= A1
by A62, A75, Th38, A74;
then reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
A1 by A55, A57, A58, A67, A76, A86;
A91:
FD . (
y,
z) =
d1 . [y9,z9]
by A60, A61, GRFUNC_1:2
.=
d1 . (
y9,
z9)
;
A92:
FD . (
x,
z) =
d1 . [x9,z9]
by A60, A61, GRFUNC_1:2
.=
d1 . (
x9,
z9)
;
FD . (
x,
y) =
d1 . [x9,y9]
by A60, A61, GRFUNC_1:2
.=
d1 . (
x9,
y9)
;
hence
(FD . (x,y)) "\/" (FD . (y,z)) >= FD . (
x,
z)
by A91, A92, Def7;
verum end; end;
end; end; end;
end;
FD is zeroed
proof
let x be
Element of
FS;
LATTICE5:def 6 FD . (x,x) = Bottom L
consider y being
set such that A93:
x in y
and A94:
y in X
by A1, TARSKI:def 4;
consider j being
Element of
NAT such that A95:
y = (S . j) `1
by A94;
consider A1 being non
empty set ,
d1 being
distance_function of
A1,
L,
Aq1 being non
empty set ,
dq1 being
distance_function of
Aq1,
L such that
Aq1,
dq1 is_extension_of A1,
d1
and A96:
S . j = [A1,d1]
and
S . (j + 1) = [Aq1,dq1]
by Def20;
reconsider x9 =
x as
Element of
A1 by A93, A95, A96;
[A1,d1] `2 = d1
;
then
d1 in { ((S . i) `2) where i is Element of NAT : verum }
by A96;
then A97:
d1 c= FD
by ZFMISC_1:74;
dom d1 = [:A1,A1:]
by FUNCT_2:def 1;
hence FD . (
x,
x) =
d1 . [x9,x9]
by A97, GRFUNC_1:2
.=
d1 . (
x9,
x9)
.=
Bottom L
by Def6
;
verum
end;
hence
union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L
by A37, A54; verum