let A be non empty set ; for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i.
let L be lower-bounded LATTICE; for O being Ordinal
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i.
let O be Ordinal; for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i.
let d be BiFunction of A,L; ( d is symmetric & d is u.t.i. implies for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i. )
assume that
A1:
d is symmetric
and
A2:
d is u.t.i.
; for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i.
let q be QuadrSeq of d; ( O c= DistEsti d implies ConsecutiveDelta (q,O) is u.t.i. )
defpred S1[ Ordinal] means ( $1 c= DistEsti d implies ConsecutiveDelta (q,$1) is u.t.i. );
A3:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
( S1[O1] implies S1[ succ O1] )
assume that A4:
(
O1 c= DistEsti d implies
ConsecutiveDelta (
q,
O1) is
u.t.i. )
and A5:
succ O1 c= DistEsti d
;
ConsecutiveDelta (q,(succ O1)) is u.t.i.
A6:
O1 in DistEsti d
by A5, ORDINAL1:21;
then A7:
O1 in dom q
by Th25;
then
q . O1 in rng q
by FUNCT_1:def 3;
then A8:
q . O1 in { [u,v,a9,b9] where u, v is Element of A, a9, b9 is Element of L : d . (u,v) <= a9 "\/" b9 }
by Def13;
let x,
y,
z be
Element of
ConsecutiveSet (
A,
(succ O1));
LATTICE5:def 7 ((ConsecutiveDelta (q,(succ O1))) . (x,y)) "\/" ((ConsecutiveDelta (q,(succ O1))) . (y,z)) >= (ConsecutiveDelta (q,(succ O1))) . (x,z)
A9:
ConsecutiveDelta (
q,
O1) is
symmetric
by A1, Th34;
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
new_set (ConsecutiveSet (A,O1)) by Th22;
set f =
new_bi_fun (
(ConsecutiveDelta (q,O1)),
(Quadr (q,O1)));
set X =
(Quadr (q,O1)) `1_4 ;
set Y =
(Quadr (q,O1)) `2_4 ;
reconsider a =
(Quadr (q,O1)) `3_4 ,
b =
(Quadr (q,O1)) `4_4 as
Element of
L ;
A10:
(
dom d = [:A,A:] &
d c= ConsecutiveDelta (
q,
O1) )
by Th31, FUNCT_2:def 1;
consider u,
v being
Element of
A,
a9,
b9 being
Element of
L such that A11:
q . O1 = [u,v,a9,b9]
and A12:
d . (
u,
v)
<= a9 "\/" b9
by A8;
A13:
Quadr (
q,
O1)
= [u,v,a9,b9]
by A7, A11, Def14;
then A14:
(
u = (Quadr (q,O1)) `1_4 &
v = (Quadr (q,O1)) `2_4 )
;
A15:
(
a9 = a &
b9 = b )
by A13;
d . (
u,
v) =
d . [u,v]
.=
(ConsecutiveDelta (q,O1)) . (
((Quadr (q,O1)) `1_4),
((Quadr (q,O1)) `2_4))
by A14, A10, GRFUNC_1:2
;
then
new_bi_fun (
(ConsecutiveDelta (q,O1)),
(Quadr (q,O1))) is
u.t.i.
by A4, A6, A9, A12, A15, Th18, ORDINAL1:def 2;
then A16:
(new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (
x9,
z9)
<= ((new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (x9,y9)) "\/" ((new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (y9,z9))
;
ConsecutiveDelta (
q,
(succ O1)) =
new_bi_fun (
(BiFun ((ConsecutiveDelta (q,O1)),(ConsecutiveSet (A,O1)),L)),
(Quadr (q,O1)))
by Th27
.=
new_bi_fun (
(ConsecutiveDelta (q,O1)),
(Quadr (q,O1)))
by Def15
;
hence
(ConsecutiveDelta (q,(succ O1))) . (
x,
z)
<= ((ConsecutiveDelta (q,(succ O1))) . (x,y)) "\/" ((ConsecutiveDelta (q,(succ O1))) . (y,z))
by A16;
verum
end;
A17:
for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) holds
S1[O2]
proof
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet (A,$1)),
L =
ConsecutiveDelta (
q,$1);
let O2 be
Ordinal;
( O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) implies S1[O2] )
assume that A18:
(
O2 <> 0 &
O2 is
limit_ordinal )
and A19:
for
O1 being
Ordinal st
O1 in O2 &
O1 c= DistEsti d holds
ConsecutiveDelta (
q,
O1) is
u.t.i.
and A20:
O2 c= DistEsti d
;
ConsecutiveDelta (q,O2) is u.t.i.
set CS =
ConsecutiveSet (
A,
O2);
consider Ls being
Sequence such that A21:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
ConsecutiveDelta (
q,
O2)
= union (rng Ls)
by A18, A21, Th28;
then reconsider f =
union (rng Ls) as
BiFunction of
(ConsecutiveSet (A,O2)),
L ;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet (
A,$1);
consider Ts being
Sequence such that A22:
(
dom Ts = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ts . O1 = H2(
O1) ) )
from ORDINAL2:sch 2();
A23:
ConsecutiveSet (
A,
O2)
= union (rng Ts)
by A18, A22, Th23;
f is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet (
A,
O2);
LATTICE5:def 7 (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)
consider X being
set such that A24:
x in X
and A25:
X in rng Ts
by A23, TARSKI:def 4;
consider o1 being
object such that A26:
o1 in dom Ts
and A27:
X = Ts . o1
by A25, FUNCT_1:def 3;
consider Y being
set such that A28:
y in Y
and A29:
Y in rng Ts
by A23, TARSKI:def 4;
consider o2 being
object such that A30:
o2 in dom Ts
and A31:
Y = Ts . o2
by A29, FUNCT_1:def 3;
consider Z being
set such that A32:
z in Z
and A33:
Z in rng Ts
by A23, TARSKI:def 4;
consider o3 being
object such that A34:
o3 in dom Ts
and A35:
Z = Ts . o3
by A33, FUNCT_1:def 3;
reconsider o1 =
o1,
o2 =
o2,
o3 =
o3 as
Ordinal by A26, A30, A34;
A36:
x in ConsecutiveSet (
A,
o1)
by A22, A24, A26, A27;
A37:
Ls . o3 = ConsecutiveDelta (
q,
o3)
by A21, A22, A34;
then reconsider h3 =
Ls . o3 as
BiFunction of
(ConsecutiveSet (A,o3)),
L ;
A38:
h3 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet (
A,
o3);
LATTICE5:def 7 (h3 . (x,y)) "\/" (h3 . (y,z)) >= h3 . (x,z)
o3 c= DistEsti d
by A20, A22, A34, ORDINAL1:def 2;
then A39:
ConsecutiveDelta (
q,
o3) is
u.t.i.
by A19, A22, A34;
ConsecutiveDelta (
q,
o3)
= h3
by A21, A22, A34;
hence
h3 . (
x,
z)
<= (h3 . (x,y)) "\/" (h3 . (y,z))
by A39;
verum
end;
A40:
dom h3 = [:(ConsecutiveSet (A,o3)),(ConsecutiveSet (A,o3)):]
by FUNCT_2:def 1;
A41:
z in ConsecutiveSet (
A,
o3)
by A22, A32, A34, A35;
A42:
Ls . o2 = ConsecutiveDelta (
q,
o2)
by A21, A22, A30;
then reconsider h2 =
Ls . o2 as
BiFunction of
(ConsecutiveSet (A,o2)),
L ;
A43:
h2 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet (
A,
o2);
LATTICE5:def 7 (h2 . (x,y)) "\/" (h2 . (y,z)) >= h2 . (x,z)
o2 c= DistEsti d
by A20, A22, A30, ORDINAL1:def 2;
then A44:
ConsecutiveDelta (
q,
o2) is
u.t.i.
by A19, A22, A30;
ConsecutiveDelta (
q,
o2)
= h2
by A21, A22, A30;
hence
h2 . (
x,
z)
<= (h2 . (x,y)) "\/" (h2 . (y,z))
by A44;
verum
end;
A45:
dom h2 = [:(ConsecutiveSet (A,o2)),(ConsecutiveSet (A,o2)):]
by FUNCT_2:def 1;
A46:
Ls . o1 = ConsecutiveDelta (
q,
o1)
by A21, A22, A26;
then reconsider h1 =
Ls . o1 as
BiFunction of
(ConsecutiveSet (A,o1)),
L ;
A47:
h1 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet (
A,
o1);
LATTICE5:def 7 (h1 . (x,y)) "\/" (h1 . (y,z)) >= h1 . (x,z)
o1 c= DistEsti d
by A20, A22, A26, ORDINAL1:def 2;
then A48:
ConsecutiveDelta (
q,
o1) is
u.t.i.
by A19, A22, A26;
ConsecutiveDelta (
q,
o1)
= h1
by A21, A22, A26;
hence
h1 . (
x,
z)
<= (h1 . (x,y)) "\/" (h1 . (y,z))
by A48;
verum
end;
A49:
dom h1 = [:(ConsecutiveSet (A,o1)),(ConsecutiveSet (A,o1)):]
by FUNCT_2:def 1;
A50:
y in ConsecutiveSet (
A,
o2)
by A22, A28, A30, A31;
per cases
( o1 c= o3 or o3 c= o1 )
;
suppose A51:
o1 c= o3
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)then A52:
ConsecutiveSet (
A,
o1)
c= ConsecutiveSet (
A,
o3)
by Th29;
thus
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
verumproof
per cases
( o2 c= o3 or o3 c= o2 )
;
suppose A53:
o2 c= o3
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)reconsider z9 =
z as
Element of
ConsecutiveSet (
A,
o3)
by A22, A32, A34, A35;
reconsider x9 =
x as
Element of
ConsecutiveSet (
A,
o3)
by A36, A52;
ConsecutiveDelta (
q,
o3)
in rng Ls
by A21, A22, A34, A37, FUNCT_1:def 3;
then A54:
h3 c= f
by A37, ZFMISC_1:74;
A55:
ConsecutiveSet (
A,
o2)
c= ConsecutiveSet (
A,
o3)
by A53, Th29;
then reconsider y9 =
y as
Element of
ConsecutiveSet (
A,
o3)
by A50;
[y,z] in dom h3
by A50, A41, A40, A55, ZFMISC_1:87;
then A56:
f . (
y,
z)
= h3 . (
y9,
z9)
by A54, GRFUNC_1:2;
[x,z] in dom h3
by A36, A41, A40, A52, ZFMISC_1:87;
then A57:
f . (
x,
z)
= h3 . (
x9,
z9)
by A54, GRFUNC_1:2;
[x,y] in dom h3
by A36, A50, A40, A52, A55, ZFMISC_1:87;
then
f . (
x,
y)
= h3 . (
x9,
y9)
by A54, GRFUNC_1:2;
hence
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A38, A56, A57;
verum end; suppose A58:
o3 c= o2
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)reconsider y9 =
y as
Element of
ConsecutiveSet (
A,
o2)
by A22, A28, A30, A31;
ConsecutiveDelta (
q,
o2)
in rng Ls
by A21, A22, A30, A42, FUNCT_1:def 3;
then A59:
h2 c= f
by A42, ZFMISC_1:74;
A60:
ConsecutiveSet (
A,
o3)
c= ConsecutiveSet (
A,
o2)
by A58, Th29;
then reconsider z9 =
z as
Element of
ConsecutiveSet (
A,
o2)
by A41;
[y,z] in dom h2
by A50, A41, A45, A60, ZFMISC_1:87;
then A61:
f . (
y,
z)
= h2 . (
y9,
z9)
by A59, GRFUNC_1:2;
ConsecutiveSet (
A,
o1)
c= ConsecutiveSet (
A,
o3)
by A51, Th29;
then A62:
ConsecutiveSet (
A,
o1)
c= ConsecutiveSet (
A,
o2)
by A60;
then reconsider x9 =
x as
Element of
ConsecutiveSet (
A,
o2)
by A36;
[x,y] in dom h2
by A36, A50, A45, A62, ZFMISC_1:87;
then A63:
f . (
x,
y)
= h2 . (
x9,
y9)
by A59, GRFUNC_1:2;
[x,z] in dom h2
by A36, A41, A45, A60, A62, ZFMISC_1:87;
then
f . (
x,
z)
= h2 . (
x9,
z9)
by A59, GRFUNC_1:2;
hence
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A43, A63, A61;
verum end;
end; end; suppose A64:
o3 c= o1
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)then A65:
ConsecutiveSet (
A,
o3)
c= ConsecutiveSet (
A,
o1)
by Th29;
thus
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
verumproof
per cases
( o1 c= o2 or o2 c= o1 )
;
suppose A66:
o1 c= o2
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)reconsider y9 =
y as
Element of
ConsecutiveSet (
A,
o2)
by A22, A28, A30, A31;
ConsecutiveDelta (
q,
o2)
in rng Ls
by A21, A22, A30, A42, FUNCT_1:def 3;
then A67:
h2 c= f
by A42, ZFMISC_1:74;
A68:
ConsecutiveSet (
A,
o1)
c= ConsecutiveSet (
A,
o2)
by A66, Th29;
then reconsider x9 =
x as
Element of
ConsecutiveSet (
A,
o2)
by A36;
[x,y] in dom h2
by A36, A50, A45, A68, ZFMISC_1:87;
then A69:
f . (
x,
y)
= h2 . (
x9,
y9)
by A67, GRFUNC_1:2;
ConsecutiveSet (
A,
o3)
c= ConsecutiveSet (
A,
o1)
by A64, Th29;
then A70:
ConsecutiveSet (
A,
o3)
c= ConsecutiveSet (
A,
o2)
by A68;
then reconsider z9 =
z as
Element of
ConsecutiveSet (
A,
o2)
by A41;
[y,z] in dom h2
by A50, A41, A45, A70, ZFMISC_1:87;
then A71:
f . (
y,
z)
= h2 . (
y9,
z9)
by A67, GRFUNC_1:2;
[x,z] in dom h2
by A36, A41, A45, A68, A70, ZFMISC_1:87;
then
f . (
x,
z)
= h2 . (
x9,
z9)
by A67, GRFUNC_1:2;
hence
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A43, A69, A71;
verum end; suppose A72:
o2 c= o1
;
(f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)reconsider x9 =
x as
Element of
ConsecutiveSet (
A,
o1)
by A22, A24, A26, A27;
reconsider z9 =
z as
Element of
ConsecutiveSet (
A,
o1)
by A41, A65;
ConsecutiveDelta (
q,
o1)
in rng Ls
by A21, A22, A26, A46, FUNCT_1:def 3;
then A73:
h1 c= f
by A46, ZFMISC_1:74;
A74:
ConsecutiveSet (
A,
o2)
c= ConsecutiveSet (
A,
o1)
by A72, Th29;
then reconsider y9 =
y as
Element of
ConsecutiveSet (
A,
o1)
by A50;
[x,y] in dom h1
by A36, A50, A49, A74, ZFMISC_1:87;
then A75:
f . (
x,
y)
= h1 . (
x9,
y9)
by A73, GRFUNC_1:2;
[x,z] in dom h1
by A36, A41, A49, A65, ZFMISC_1:87;
then A76:
f . (
x,
z)
= h1 . (
x9,
z9)
by A73, GRFUNC_1:2;
[y,z] in dom h1
by A50, A41, A49, A65, A74, ZFMISC_1:87;
then
f . (
y,
z)
= h1 . (
y9,
z9)
by A73, GRFUNC_1:2;
hence
(f . (x,y)) "\/" (f . (y,z)) >= f . (
x,
z)
by A47, A75, A76;
verum end;
end; end;
end;
hence
ConsecutiveDelta (
q,
O2) is
u.t.i.
by A18, A21, Th28;
verum
end;
A77:
S1[ 0 ]
proof
assume
0 c= DistEsti d
;
ConsecutiveDelta (q,0) is u.t.i.
let x,
y,
z be
Element of
ConsecutiveSet (
A,
0);
LATTICE5:def 7 ((ConsecutiveDelta (q,0)) . (x,y)) "\/" ((ConsecutiveDelta (q,0)) . (y,z)) >= (ConsecutiveDelta (q,0)) . (x,z)
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
A by Th21;
(
ConsecutiveDelta (
q,
0)
= d &
d . (
x9,
z9)
<= (d . (x9,y9)) "\/" (d . (y9,z9)) )
by A2, Th26;
hence
(ConsecutiveDelta (q,0)) . (
x,
z)
<= ((ConsecutiveDelta (q,0)) . (x,y)) "\/" ((ConsecutiveDelta (q,0)) . (y,z))
;
verum
end;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A77, A3, A17);
hence
( O c= DistEsti d implies ConsecutiveDelta (q,O) is u.t.i. )
; verum