Copyright (c) 1997 Association of Mizar Users
environ
vocabulary FUNCT_1, RELAT_1, ORDINAL1, CLASSES1, ORDINAL2, MCART_1, PRALG_1,
TARSKI, FUNCT_6, HAHNBAN, ZFMISC_1, ORDERS_1, LATTICE3, MSUALG_5,
EQREL_1, LATTICES, BOOLE, WAYBEL_0, BHSP_3, SETFAM_1, CANTOR_1, RELAT_2,
PRE_TOPC, GROUP_6, YELLOW_0, FILTER_2, CAT_1, FINSEQ_1, MATRIX_2,
FINSEQ_2, ARYTM_1, SQUARE_1, REALSET1, SGRAPH1, CARD_1, PARTFUN1,
LATTICE5;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2,
RELSET_1, FUNCT_1, FUNCT_2, FUNCT_6, NUMBERS, XCMPLX_0, XREAL_0,
BINARITH, CANTOR_1, NAT_1, SETFAM_1, ORDINAL1, ORDINAL2, CARD_1, MCART_1,
DOMAIN_1, PARTFUN1, PRALG_1, PRE_TOPC, STRUCT_0, ORDERS_1, EQREL_1,
MSUALG_5, FINSEQ_1, FINSEQ_2, CLASSES1, CQC_SIM1, LATTICES, LATTICE3,
BINOP_1, YELLOW_0, WAYBEL_0, YELLOW_2, ABIAN, FINSOP_1;
constructors BINARITH, DOMAIN_1, RFUNCT_3, CANTOR_1, MSUALG_5, CQC_SIM1,
BINOP_1, CLASSES1, WAYBEL_1, LATTICE3, ABIAN, FINSOP_1, MEMBERED;
clusters SUBSET_1, RELSET_1, STRUCT_0, INT_1, YELLOW_0, YELLOW_1, CARD_1,
ORDINAL1, PRALG_1, LATTICE3, ABIAN, GOBOARD4, ARYTM_3, LATTICES,
MEMBERED, NUMBERS, ORDINAL2, PARTFUN1, EQREL_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, LATTICE3, PRALG_1, WAYBEL_0, XBOOLE_0;
theorems EQREL_1, CQC_SIM1, CQC_THE1, BINARITH, RELAT_1, RELAT_2, FINSEQ_1,
FINSEQ_2, MSUALG_5, MSUALG_7, ORDERS_1, TARSKI, ENUMSET1, ORDINAL1,
ORDINAL2, ORDINAL3, WELLORD2, HAHNBAN, PARTFUN1, GRFUNC_1, FUNCT_6,
EXTENS_1, MCART_1, FINSEQ_5, NAT_1, AXIOMS, REAL_1, INT_1, BINOP_1,
ZFMISC_1, FUNCT_1, FUNCT_2, FILTER_0, LATTICES, LATTICE3, YELLOW_0,
YELLOW_2, YELLOW_3, YELLOW_5, WAYBEL_0, WAYBEL_1, WAYBEL_6, CANTOR_1,
RELSET_1, CARD_1, CLASSES1, FINSEQ_3, SCMFSA_7, SETFAM_1, XBOOLE_0,
XBOOLE_1, SQUARE_1, XCMPLX_1;
schemes DOMAIN_1, FUNCT_1, FUNCT_2, YELLOW_2, RELSET_1, RECDEF_1, ORDINAL1,
ORDINAL2, NAT_1, FINSEQ_1, ZFREFLE1;
begin :: Preliminaries
scheme RecChoice{A() -> set,P[set,set,set]}:
ex f being Function st dom f = NAT & f.0 = A() &
for n being Element of NAT holds P[n,f.n,f.(n+1)]
provided
A1: for n being Nat for x being set ex y being set st P[n,x,y]
proof
defpred Q[set,set,set] means
ex O2 being Ordinal st O2 = $3 &
(for X being set, n being Nat st X c= Rank the_rank_of $2
ex Y being set st Y c= Rank O2 & P[n,X,Y]) &
(for O being Ordinal st
for X being set, n being Nat st X c= Rank the_rank_of $2
ex Y being set st Y c= Rank O & P[n,X,Y]
holds O2 c= O);
A2: for n being Nat for x being set ex y being set st Q[n,x,y]
proof
let n be Nat; let x be set;
defpred Y[set,set] means for m being Nat ex y being set st
$2 is Ordinal & y c= Rank the_rank_of $2 & P[m,$1,y];
A3: for x' being set st x' in bool Rank the_rank_of x
ex o being set st Y[x',o]
proof
let x' be set; assume
x' in bool Rank the_rank_of x;
defpred X[set,set] means
ex y being set st $2 is Ordinal & y c= Rank the_rank_of $2 & P[$1,x',y];
A4: for e being set st e in NAT ex u being set st X[e,u]
proof let i be set; assume i in NAT;
then reconsider i' = i as Nat;
thus ex o being set, y being set st
o is Ordinal & y c= Rank the_rank_of o & P[i,x',y]
proof
consider y being set such that
A5: P[i',x',y] by A1;
take o = the_rank_of y, y;
thus o is Ordinal;
the_rank_of the_rank_of y = the_rank_of y by CLASSES1:81;
hence y c= Rank the_rank_of o by CLASSES1:73;
thus P[i,x',y] by A5;
end;
end;
consider h being Function such that
A6: dom h = NAT and
A7: for i being set st i in NAT holds X[i,h.i]
from NonUniqFuncEx(A4);
take o = sup rng h;
thus for m being Nat ex y being set st
o is Ordinal & y c= Rank the_rank_of o & P[m,x',y]
proof
let m be Nat;
consider y being set such that
A8: h.m is Ordinal and
A9: y c= Rank the_rank_of (h.m) and
A10: P[m,x',y] by A7;
take y;
thus o is Ordinal;
h.m in rng h by A6,FUNCT_1:def 5;
then h.m in sup rng h by A8,ORDINAL2:27;
then A11: h.m c= o by ORDINAL1:def 2;
reconsider O = h.m as Ordinal by A8;
A12: Rank O c= Rank o by A11,CLASSES1:43;
y c= Rank O by A9,CLASSES1:81;
then y c= Rank o by A12,XBOOLE_1:1;
hence y c= Rank the_rank_of o by CLASSES1:81;
thus P[m,x',y] by A10;
end;
end;
consider f being Function such that
A13: dom f = bool Rank the_rank_of x and
A14: for x' being set st x' in bool Rank the_rank_of x holds Y[x',f.x']
from NonUniqFuncEx(A3);
defpred X[Ordinal] means
for X being set, n being Nat st X c= Rank the_rank_of x
ex Y being set st Y c= Rank $1 & P[n,X,Y];
A15: ex O being Ordinal st X[O]
proof take O2 = sup rng f;
thus (for X being set, m being Nat st X c= Rank the_rank_of x
ex Y being set st Y c= Rank O2 & P[m,X,Y])
proof
let X be set; let m be Nat; assume
A16: X c= Rank the_rank_of x;
then consider Y being set such that
A17: f.X is Ordinal and
A18: Y c= Rank the_rank_of (f.X) and
A19: P[m,X,Y] by A14;
take Y;
f.X in rng f by A13,A16,FUNCT_1:def 5;
then f.X in sup rng f by A17,ORDINAL2:27;
then A20:f.X c= O2 by ORDINAL1:def 2;
reconsider O = f.X as Ordinal by A17;
A21:Rank O c= Rank O2 by A20,CLASSES1:43;
the_rank_of O = O by CLASSES1:81;
hence Y c= Rank O2 by A18,A21,XBOOLE_1:1;
thus P[m,X,Y] by A19;
end;
end;
consider O2 being Ordinal such that
A22: X[O2] &
(for O being Ordinal st X[O] holds O2 c= O) from Ordinal_Min(A15);
take O2;
thus Q[n,x,O2] by A22;
end;
A23: for n being Nat for x,y1,y2 being set st Q[n,x,y1] & Q[n,x,y2]
holds y1 = y2
proof
let n be Nat; let x,y1,y2 be set; assume that
A24: Q[n,x,y1] and
A25: Q[n,x,y2];
consider O1 being Ordinal such that
A26: O1 = y1 and
A27: for X being set, n being Nat st X c= Rank the_rank_of x
ex Y being set st Y c= Rank O1 & P[n,X,Y] and
A28: for O being Ordinal st
for X being set, n being Nat st X c= Rank the_rank_of x
ex Y being set st Y c= Rank O & P[n,X,Y] holds O1 c= O by A24;
consider O2 being Ordinal such that
A29: O2 = y2 and
A30: for X being set, n being Nat st X c= Rank the_rank_of x
ex Y being set st Y c= Rank O2 & P[n,X,Y] and
A31: for O being Ordinal st
for X being set, n being Nat st X c= Rank the_rank_of x
ex Y being set st Y c= Rank O & P[n,X,Y] holds O2 c= O by A25;
A32: O1 c= O2 by A28,A30;
O2 c= O1 by A27,A31;
hence y1 = y2 by A26,A29,A32,XBOOLE_0:def 10;
end;
consider g being Function such that
A33: dom g = NAT and
A34: g.0 = the_rank_of A() and
A35: for n being Element of NAT holds Q[n,g.n,g.(n+1)] from RecEx(A2,A23);
set beta = sup rng g;
defpred X[set,set] means ex i being Nat st i = $1`2 &
P[$1`2,$1`1,$2`1] & $2`2 = i+1 &
not ex y being set st P[$1`2,$1`1,y] & the_rank_of y in the_rank_of $2`1;
A36: for x being set st x in [:Rank beta, NAT:] ex u being set st X[x,u]
proof
let x be set; assume x in [:Rank beta, NAT:];
then consider a,b being set such that
A37: a in Rank beta and
A38: b in NAT and
A39: x = [a,b] by ZFMISC_1:def 2;
reconsider b as Nat by A38;
the_rank_of a in beta by A37,CLASSES1:74;
then consider alfa being Ordinal such that
A40: alfa in rng g and
A41: the_rank_of a c= alfa by ORDINAL2:29;
A42: a c= Rank alfa by A41,CLASSES1:73;
consider k being set such that
A43: k in dom g and
A44: alfa = g.k by A40,FUNCT_1:def 5;
reconsider k as Nat by A33,A43;
A45: Q[k,alfa,g.(k+1)] by A35,A44;
then reconsider O2 = g.(k+1) as Ordinal;
A46: x`2 = b & x`1 = a by A39,MCART_1:7;
defpred X[Ordinal] means ex y being set st y c= Rank $1 & P[x`2,x`1,y];
a c= Rank the_rank_of alfa by A42,CLASSES1:81;
then ex y being set st y c= Rank O2 & P[x`2,x`1,y] by A45,A46;
then A47: ex O being Ordinal st X[O];
consider O being Ordinal such that
A48: X[O] and
A49: for O' being Ordinal st X[O'] holds O c= O' from Ordinal_Min(A47);
consider Y being set such that
A50: Y c= Rank O and
A51: P[b,a,Y] by A46,A48;
take u = [Y,b+1], i = b;
thus i = x`2 by A39,MCART_1:7;
thus P[x`2,x`1,u`1] by A46,A51,MCART_1:7;
thus u`2 = i+1 by MCART_1:7;
given y being set such that
A52: P[x`2,x`1,y] and
A53: the_rank_of y in the_rank_of u`1;
A54: the_rank_of y in the_rank_of Y by A53,MCART_1:7;
A55: the_rank_of Y c= O by A50,CLASSES1:73;
y c= Rank the_rank_of y by CLASSES1:def 8;
then O c= the_rank_of y by A49,A52;
hence contradiction by A54,A55,ORDINAL1:7;
end;
consider F being Function such that
dom F = [:Rank beta, NAT:] and
A56: for x being set st x in [:Rank beta, NAT:] holds X[x,F.x]
from NonUniqFuncEx(A36);
deffunc U(Nat,set) = (F.[$2,$1])`1;
consider f being Function such that
A57: dom f = NAT and
A58: f.0 = A() and
A59: for n being Element of NAT holds f.(n+1) = U(n,f.n) from LambdaRecEx;
take f;
thus dom f = NAT by A57;
thus f.0 = A() by A58;
defpred X[Nat] means the_rank_of (f.$1) in sup rng g;
g.0 in rng g by A33,FUNCT_1:def 5;
then A60: X[0] by A34,A58,ORDINAL2:27;
A61: for n being Element of NAT st X[n] holds X[n+1]
proof
let n be Element of NAT; assume
A62: the_rank_of (f.n) in sup rng g;
then f.n in Rank sup rng g by CLASSES1:74;
then A63: [f.n,n] in [:Rank beta, NAT:] by ZFMISC_1:106;
[f.n,n]`1 = f.n & [f.n,n]`2 = n by MCART_1:7;
then consider i being Nat such that
i = n and
P[n,f.n,(F.[f.n,n])`1] and
(F.[f.n,n])`2 = i+1 and
A64: not ex y being set st P[n,f.n,y] &
the_rank_of y in the_rank_of (F.[f.n,n])`1 by A56,A63;
A65: f.(n+1) = (F.[f.n,n])`1 by A59;
consider o1 being Ordinal such that
A66: o1 in rng g and
A67: the_rank_of (f.n) c= o1 by A62,ORDINAL2:29;
consider m being set such that
A68: m in dom g and
A69: g.m = o1 by A66,FUNCT_1:def 5;
reconsider m as Nat by A33,A68;
consider o2 being Ordinal such that
A70: o2 = g.(m+1) and
A71: for X being set, n being Nat st X c= Rank the_rank_of (g.m)
ex Y being set st Y c= Rank o2 & P[n,X,Y] and
for o being Ordinal st
for X being set, n being Nat st X c= Rank the_rank_of (g.m)
ex Y being set st Y c= Rank o & P[n,X,Y]
holds o2 c= o by A35;
the_rank_of (f.n) c= the_rank_of (g.m) by A67,A69,CLASSES1:81;
then f.n c= Rank the_rank_of (g.m) by CLASSES1:73;
then consider YY being set such that
A72: YY c= Rank o2 and
A73: P[n,f.n,YY] by A71;
not P[n,f.n,YY] or
not the_rank_of YY in the_rank_of (F.[f.n,n])`1 by A64;
then A74: the_rank_of (F.[f.n,n])`1 c= the_rank_of YY by A73,ORDINAL1:26;
the_rank_of YY c= o2 by A72,CLASSES1:73;
then A75: the_rank_of (f.(n+1)) c= o2 by A65,A74,XBOOLE_1:1;
g.(m+1) in rng g by A33,FUNCT_1:def 5;
then o2 in sup rng g by A70,ORDINAL2:27;
hence the_rank_of (f.(n+1)) in sup rng g by A75,ORDINAL1:22;
end;
A76: for n being Element of NAT holds X[n] from Ind(A60,A61);
A77: [A(),0]`1 = A() & [A(),0]`2 = 0 by MCART_1:7;
the_rank_of A() in sup rng g by A58,A76;
then A() in Rank sup rng g by CLASSES1:74;
then [A(),0] in [:Rank beta, NAT:] by ZFMISC_1:106;
then consider i being Nat such that
i = [A(),0]`2 and
A78: P[0,A(),(F.[A(),0])`1] and
(F.[A(),0])`2 = i+1 and not ex y being set st P[0,A(),y] &
the_rank_of y in the_rank_of (F.[A(),0])`1 by A56,A77;
defpred X[Nat] means P[$1,f.$1,f.($1+1)];
A79: X[0] by A58,A59,A78;
A80: for n being Element of NAT st X[n] holds X[n+1]
proof
let n be Element of NAT; assume P[n,f.n,f.(n+1)];
A81: [f.(n+1),n+1]`1 = f.(n+1) & [f.(n+1),n+1]`2 = n+1 by MCART_1:7;
the_rank_of (f.(n+1)) in sup rng g by A76;
then f.(n+1) in Rank sup rng g by CLASSES1:74;
then [f.(n+1),n+1] in [:Rank beta, NAT:] by ZFMISC_1:106;
then consider i being Nat such that i = n+1 and
A82: P[n+1,f.(n+1),(F.[f.(n+1),n+1])`1] and
(F.[f.(n+1),n+1])`2 = i+1 and
not ex y being set st P[(n+1),f.(n+1),y] &
the_rank_of y in the_rank_of (F.[f.(n+1),n+1])`1 by A56,A81;
thus P[(n+1),f.(n+1),f.((n+1)+1)] by A59,A82;
end;
thus for n being Element of NAT holds X[n] from Ind(A79,A80);
end;
theorem Th1:
for f being Function, F being Function-yielding Function
st f = union rng F holds dom f = union rng doms F
proof
let f be Function; let F be Function-yielding Function;
assume
A1: f = union rng F;
thus dom f c= union rng doms F
proof let x be set; assume
x in dom f;
then [x,f.x] in union rng F by A1,FUNCT_1:def 4;
then consider g being set such that
A2: [x,f.x] in g & g in rng F by TARSKI:def 4;
consider u being set such that
A3: u in dom F & g = F.u by A2,FUNCT_1:def 5;
x in dom (F.u) by A2,A3,FUNCT_1:8;
then A4: x in (doms F).u by A3,FUNCT_6:31;
u in dom doms F by A3,FUNCT_6:31;
then (doms F).u in rng doms F by FUNCT_1:def 5;
hence x in union rng doms F by A4,TARSKI:def 4;
end;
let x be set; assume x in union rng doms F;
then consider A be set such that
A5: x in A & A in rng doms F by TARSKI:def 4;
consider u being set such that
A6: u in dom doms F & A = (doms F).u by A5,FUNCT_1:def 5;
A7: u in dom F by A6,EXTENS_1:3;
then A8: F.u in rng F by FUNCT_1:def 5;
consider g being Function such that
A9: g = F.u;
A = dom (F.u) by A6,A7,FUNCT_6:31;
then [x,g.x] in F.u by A5,A9,FUNCT_1:def 4;
then [x,g.x] in f by A1,A8,TARSKI:def 4;
hence x in dom f by FUNCT_1:8;
end;
theorem Th2:
for A,B being non empty set holds [:union A, union B:] = union { [:a,b:]
where a is Element of A, b is Element of B : a in A & b in B }
proof let A,B be non empty set;
set Y = { [:a,b:]
where a is Element of A, b is Element of B : a in A & b in B };
thus [:union A, union B:] c= union Y
proof let z be set; assume
A1: z in [:union A, union B:];
then consider x,y being set such that
A2: z = [x,y] by ZFMISC_1:102;
x in union A by A1,A2,ZFMISC_1:106;
then consider a' being set such that
A3: x in a' & a' in A by TARSKI:def 4;
y in union B by A1,A2,ZFMISC_1:106;
then consider b' being set such that
A4: y in b' & b' in B by TARSKI:def 4;
reconsider a' as Element of A by A3;
reconsider b' as Element of B by A4;
A5: z in [:a',b':] by A2,A3,A4,ZFMISC_1:def 2;
[:a',b':] in Y;
hence z in union Y by A5,TARSKI:def 4;
end;
let z be set; assume z in union Y;
then consider e being set such that
A6: z in e & e in Y by TARSKI:def 4;
consider a' being Element of A, b' being Element of B such that
A7: [:a',b':] = e & a' in A & b' in B by A6;
consider x,y being set such that
A8: x in a' & y in b' & z = [x,y] by A6,A7,ZFMISC_1:def 2;
x in union A & y in union B by A8,TARSKI:def 4;
hence z in [:union A, union B:] by A8,ZFMISC_1:def 2;
end;
theorem Th3:
for A being non empty set st A is c=-linear holds
[:union A, union A:] = union { [:a,a:] where a is Element of A : a in A }
proof let A be non empty set; assume
A1: A is c=-linear;
set X = { [:a,a:] where a is Element of A : a in A },
Y = { [:a,b:] where a is Element of A, b is Element of A
: a in A & b in A };
X c= Y
proof let Z be set; assume
Z in X;
then consider a being Element of A such that
A2: Z = [:a,a:] & a in A;
thus Z in Y by A2;
end;
then A3: union X c= union Y by ZFMISC_1:95;
union Y c= union X
proof let Z be set; assume
Z in union Y;
then consider z being set such that
A4: Z in z & z in Y by TARSKI:def 4;
consider a,b being Element of A such that
A5: z = [:a,b:] & a in A & b in A by A4;
A6: a,b are_c=-comparable by A1,ORDINAL1:def 9;
per cases by A6,XBOOLE_0:def 9;
suppose a c= b;
then [:a,b:] c= [:b,b:] by ZFMISC_1:118;
then Z in [:b,b:] & [:b,b:] in X by A4,A5;
hence Z in union X by TARSKI:def 4;
suppose b c= a;
then [:a,b:] c= [:a,a:] by ZFMISC_1:118;
then Z in [:a,a:] & [:a,a:] in X by A4,A5;
hence Z in union X by TARSKI:def 4;
end;
then union X = union Y by A3,XBOOLE_0:def 10;
hence thesis by Th2;
end;
begin :: An equivalence lattice of a set
reserve X for non empty set;
definition let A be set;
func EqRelLATT A -> Poset equals :Def1:
LattPOSet EqRelLatt A;
correctness;
end;
definition let A be set;
cluster EqRelLATT A -> with_infima with_suprema;
coherence
proof
LattPOSet EqRelLatt A is with_suprema with_infima;
hence thesis by Def1;
end;
end;
theorem Th4:
for A, x being set holds
x in the carrier of EqRelLATT A iff x is Equivalence_Relation of A
proof let A, x be set;
hereby assume
x in the carrier of EqRelLATT A;
then reconsider e = x as Element of LattPOSet EqRelLatt A by
Def1;
%e = e &
%e is Element of EqRelLatt A by LATTICE3:def 4;
then A1: x in the carrier of EqRelLatt A;
the carrier of EqRelLatt A = {r where r is Relation of A,A :
r is Equivalence_Relation of A} by MSUALG_5:def 2;
then ex x' being Relation of A,A
st x' = x & x' is Equivalence_Relation of A by A1;
hence x is Equivalence_Relation of A;
end; assume
A2: x is Equivalence_Relation of A;
the carrier of EqRelLatt A = {r where r is Relation of A,A :
r is Equivalence_Relation of A} by MSUALG_5:def 2;
then x in the carrier of EqRelLatt A by A2;
then reconsider e = x as Element of EqRelLatt A;
e% = e & e% is Element of LattPOSet EqRelLatt A by LATTICE3:def 3;
then reconsider e as Element of EqRelLATT A by Def1;
e in the carrier of EqRelLATT A;
hence x in the carrier of EqRelLATT A;
end;
theorem Th5:
for A being set, x,y being Element of EqRelLatt A
holds x [= y iff x c= y
proof let A be set, x,y be Element of EqRelLatt A;
reconsider x' = x,y' = y as Equivalence_Relation of A by MSUALG_7:1;
A1: x "/\" y = (the L_meet of EqRelLatt A).(x',y') by LATTICES:def 2
.= x' /\ y' by MSUALG_5:def 2;
x' /\ y' = x' iff x' c= y' by XBOOLE_1:17,28;
hence thesis by A1,LATTICES:21;
end;
theorem Th6:
for A being set, a,b being Element of EqRelLATT A
holds a <= b iff a c= b
proof let A be set, a,b be Element of EqRelLATT A;
set EL = EqRelLATT A, El = EqRelLatt A;
a is Equivalence_Relation of A by Th4;
then reconsider a' = a as Element of El by MSUALG_7:1;
b is Equivalence_Relation of A by Th4;
then reconsider b' = b as Element of El by MSUALG_7:1;
A1: a'% = a & b'% = b by LATTICE3:def 3;
A2: the InternalRel of EL = the InternalRel of LattPOSet El by Def1;
thus a <= b implies a c= b
proof assume
a <= b;
then [a,b] in the InternalRel of EL by ORDERS_1:def 9;
then a'% <= b'% by A1,A2,ORDERS_1:def 9;
then a' [= b' by LATTICE3:7;
hence a c= b by Th5;
end;
thus a c= b implies a <= b
proof assume a c= b;
then a' [= b' by Th5;
then a'% <= b'% by LATTICE3:7;
hence a <= b by A1,Def1;
end;
end;
theorem Th7:
for L being Lattice, a,b being Element of LattPOSet L
holds a "/\" b = %a "/\" %b
proof let L be Lattice, a,b be Element of LattPOSet L;
a = %a & b = %b by LATTICE3:def 4;
then reconsider x = a, y = b as Element of L;
set c = x "/\" y;
A1:c [= x & c [= y by LATTICES:23;
A2:c% = c & x% = x & y% = y & %(c%) = c% & %(x%) = x% & %(y%) = y%
by LATTICE3:def 3,def 4;
then reconsider c as Element of LattPOSet L;
A3:c <= a & c <= b by A1,A2,LATTICE3:7;
for d being Element of LattPOSet L st d <= a & d <= b holds d <= c
proof let d be Element of LattPOSet L; assume
A4: d <= a & d <= b;
d = %d by LATTICE3:def 4;
then reconsider z = d as Element of L;
A5: z% = z & %(z%) = z% by LATTICE3:def 3,def 4;
then z [= x & z [= y by A2,A4,LATTICE3:7;
then z [= x "/\" y by FILTER_0:7;
hence d <= c by A2,A5,LATTICE3:7;
end;
hence a "/\" b = %a "/\" %b by A2,A3,YELLOW_0:23;
end;
theorem Th8:
for A being set, a,b being Element of EqRelLATT A
holds a "/\" b = a /\ b
proof let A be set, a,b be Element of EqRelLATT A;
A1: now let x,y be Element of EqRelLatt A;
reconsider e1 = x as Equivalence_Relation of A by MSUALG_7:1;
reconsider e2 = y as Equivalence_Relation of A by MSUALG_7:1;
thus x "/\" y = (the L_meet of EqRelLatt A).(e1,e2) by LATTICES:def 2
.= x /\ y by MSUALG_5:def 2;
end;
reconsider x = a as Element of LattPOSet EqRelLatt A by Def1;
%x = x & %x is Element of EqRelLatt A by LATTICE3:def 4;
then reconsider x as Element of EqRelLatt A;
reconsider y = b as Element of LattPOSet EqRelLatt A by Def1;
%y = y & %y is Element of EqRelLatt A by LATTICE3:def 4;
then reconsider y as Element of EqRelLatt A;
reconsider a1 = a,b1 = b as Element of LattPOSet EqRelLatt A by Def1;
A2: x% = x & y% = y & %(x%) = x% & %(y%) = y% &
%a1 = a1 & %b1 = b1 & (%a1)% = %a1 & (%b1)% = %b1
by LATTICE3:def 3,def 4;
thus a "/\" b = a1 "/\" b1 by Def1
.= x "/\" y by A2,Th7
.= a /\ b by A1;
end;
theorem Th9:
for L being Lattice, a,b being Element of LattPOSet L
holds a "\/" b = %a "\/" %b
proof let L be Lattice, a,b be Element of LattPOSet L;
a = %a & b = %b by LATTICE3:def 4;
then reconsider x = a, y = b as Element of L;
set c = x "\/" y;
A1: x [= c & y [= c by LATTICES:22;
A2: c% = c & x% = x & y% = y & %(c%) = c% & %(x%) = x% & %(y%) = y%
by LATTICE3:def 3,def 4;
then reconsider c as Element of LattPOSet L;
A3: a <= c & b <= c by A1,A2,LATTICE3:7;
for d being Element of LattPOSet L st a <= d & b <= d holds c <= d
proof let d be Element of LattPOSet L; assume
A4: a <= d & b <= d;
d = %d by LATTICE3:def 4;
then reconsider z = d as Element of L;
x% <= z% & y% <= z% by A2,A4,LATTICE3:def 3;
then x [= z & y [= z by LATTICE3:7;
then x "\/" y [= z by FILTER_0:6;
then (x "\/" y)% <= z% by LATTICE3:7;
hence c <= d by A2,LATTICE3:def 3;
end;
hence a "\/" b = %a "\/" %b by A2,A3,YELLOW_0:22;
end;
theorem Th10:
for A being set, a,b being Element of EqRelLATT A
for E1,E2 being Equivalence_Relation of A st a = E1 & b = E2
holds a "\/" b = E1 "\/" E2
proof let A be set, a,b be Element of EqRelLATT A,
E1,E2 be Equivalence_Relation of A; assume that
A1: a = E1 and
A2: b = E2;
reconsider x = a as Element of LattPOSet EqRelLatt A by Def1;
%x = x & %x is Element of EqRelLatt A by LATTICE3:def 4;
then
reconsider x as Element of EqRelLatt A;
reconsider y = b as Element of LattPOSet EqRelLatt A by Def1;
%y = y & %y is Element of EqRelLatt A by LATTICE3:def 4;
then
reconsider y as Element of EqRelLatt A;
reconsider a1 = a,b1 = b as Element of LattPOSet EqRelLatt A by Def1;
A3: x% = x & y% = y & %(x%) = x% & %(y%) = y% &
%a1 = a1 & %b1 = b1 & (%a1)% = %a1 & (%b1)% = %b1
by LATTICE3:def 3,def 4;
thus a "\/" b = a1 "\/" b1 by Def1 .= x "\/" y by A3,Th9
.= (the L_join of EqRelLatt A).(x,y) by LATTICES:def 1
.= E1 "\/" E2 by A1,A2,MSUALG_5:def 2;
end;
definition let L be non empty RelStr;
redefine attr L is complete means
for X being Subset of L
ex a being Element of L st a is_<=_than X &
for b being Element of L st b is_<=_than X holds b <= a;
compatibility
proof
hereby assume
A1: L is complete;
let X be Subset of L;
set Y = { c where c is Element of L: c is_<=_than X };
consider p being Element of L such that
A2: Y is_<=_than p and
A3: for r being Element of L st Y is_<=_than r holds p <= r
by A1,LATTICE3:def 12;
take p;
thus p is_<=_than X
proof let q be Element of L;
assume
A4: q in X;
Y is_<=_than q
proof let s be Element of L;
assume s in Y;
then ex t being Element of L st s = t & t is_<=_than X;
hence s <= q by A4,LATTICE3:def 8;
end;
hence p <= q by A3;
end;
let b be Element of L;
assume b is_<=_than X;
then b in Y;
hence b <= p by A2,LATTICE3:def 9;
end;
assume
A5: for X being Subset of L
ex a being Element of L st a is_<=_than X &
for b being Element of L st b is_<=_than X holds b <= a;
let X be set;
set Y = { c where c is Element of L: X is_<=_than c };
Y c= the carrier of L
proof
let x be set; assume x in Y;
then ex c being Element of L st x = c & X is_<=_than c;
hence x in the carrier of L;
end;
then consider p being Element of L such that
A6: p is_<=_than Y and
A7: for r being Element of L st r is_<=_than Y holds r <= p by A5;
take p;
thus X is_<=_than p
proof let q be Element of L;
assume
A8: q in X;
q is_<=_than Y
proof let s be Element of L;
assume s in Y;
then ex t being Element of L st
s = t & X is_<=_than t;
hence q <= s by A8,LATTICE3:def 9;
end;
hence q <= p by A7;
end;
let r be Element of L;
assume X is_<=_than r;
then r in Y;
hence p <= r by A6,LATTICE3:def 8;
end;
end;
definition let A be set;
cluster EqRelLATT A -> complete;
coherence
proof
let X be Subset of EqRelLATT A;
set B = X /\ the carrier of EqRelLATT A;
B c= bool [:A,A:]
proof
let x be set; assume x in B;
then x in the carrier of EqRelLATT A by XBOOLE_0:def 3;
then x is Equivalence_Relation of A by Th4;
hence x in bool [:A,A:];
end;
then reconsider B as Subset-Family of [:A,A:] by SETFAM_1:def 7;
consider b being Subset of [:A,A:] such that A1:b = Intersect(B);
A2:for Y being set st Y in B holds Y is Equivalence_Relation of A
proof
let Y be set; assume Y in B;
then Y in the carrier of EqRelLATT A by XBOOLE_0:def 3;
hence Y is Equivalence_Relation of A by Th4;
end;
for x being set holds x in A implies [x,x] in b
proof
let x be set; assume A3:x in A;
then A4:[x,x] in [:A,A:] by ZFMISC_1:def 2;
for Y being set st Y in B holds [x,x] in Y
proof
let Y be set; assume Y in B;
then Y is Equivalence_Relation of A by A2;
hence [x,x] in Y by A3,EQREL_1:11;
end;
hence [x,x] in b by A1,A4,CANTOR_1:10;
end;
then A5:b is_reflexive_in A by RELAT_2:def 1;
reconsider b as Relation of A by RELSET_1:def 1;
A6: dom b = A & field b = A by A5,ORDERS_1:98;
for x,y being set st x in A & y in A & [x,y] in b holds [y,x] in b
proof
let x,y be set; assume A8:x in A & y in A & [x,y] in b;
then A9:[y,x] in [:A,A:] by ZFMISC_1:def 2;
for Y being set st Y in B holds [y,x] in Y
proof
let Y be set; assume Y in B;
then [x,y] in Y & Y is Equivalence_Relation of A by A1,A2,A8,CANTOR_1:10
;
hence [y,x] in Y by EQREL_1:12;
end;
hence [y,x] in b by A1,A9,CANTOR_1:10;
end;
then A10:b is_symmetric_in A by RELAT_2:def 3;
for x,y,z being set holds x in A & y in A & z in A &
[x,y] in b & [y,z] in b implies [x,z] in b
proof
let x,y,z be set; assume that A11:x in A & y in A & z in A and
A12:[x,y] in b & [y,z] in b;
A13:[x,z] in [:A,A:] by A11,ZFMISC_1:def 2;
for Y being set st Y in B holds [x,z] in Y
proof
let Y be set; assume Y in B; then [x,y] in Y & [y,z] in Y &
Y is Equivalence_Relation of A by A1,A2,A12,CANTOR_1:10;
hence [x,z] in Y by EQREL_1:13;
end;
hence [x,z] in b by A1,A13,CANTOR_1:10;
end;
then b is_transitive_in A by RELAT_2:def 8;
then reconsider b as Equivalence_Relation of A
by A6,PARTFUN1:def 4,A10,RELAT_2:def 11,def 16;
reconsider b as Element of EqRelLATT A by Th4;
take b;
now let a be Element of EqRelLATT A; assume
A14: a in X /\ the carrier of EqRelLATT A;
reconsider a' = a as Equivalence_Relation of A by Th4;
reconsider b' = b as Equivalence_Relation of A;
for x,y being set holds [x,y] in b' implies [x,y] in a'
by A1,A14,CANTOR_1:10;
then b' c= a' by RELAT_1:def 3;
hence b <= a by Th6;
end;
then b is_<=_than X /\ the carrier of EqRelLATT A by LATTICE3:def 8;
hence b is_<=_than X by YELLOW_0:5;
let a be Element of EqRelLATT A; assume a is_<=_than X;
then A15: a is_<=_than X /\ the carrier of EqRelLATT A by YELLOW_0:5;
reconsider a' = a as Equivalence_Relation of A by Th4;
A16: for d being Element of EqRelLATT A st d in B holds a' c= d
proof
let d be Element of EqRelLATT A;
assume d in B; then a <= d by A15,LATTICE3:def 8;
hence a' c= d by Th6;
end;
a' c= Intersect(B)
proof
let x be set; assume A17:x in a';
for Y being set st Y in B holds x in Y
proof
let Y be set; assume A18:Y in B;
then Y in the carrier of EqRelLATT A by XBOOLE_0:def 3;
then a' c= Y by A16,A18;
hence x in Y by A17;
end;
hence x in Intersect(B) by A17,CANTOR_1:10;
end;
hence a <= b by A1,Th6;
end;
end;
begin :: A type of a sublattice of equivalence lattice of a set
definition let L1,L2 be LATTICE;
cluster meet-preserving join-preserving map of L1,L2;
existence
proof
consider z being Element of L2;
deffunc U(set) = z;
consider f being map of L1,L2 such that
A1: for x being Element of L1 holds f.x = U(x) from LambdaMD;
take f;
for x,y being Element of L1 holds f.(x "/\" y) = f.x "/\" f.y
proof
let x,y be Element of L1;
thus f.(x "/\" y) = z by A1 .= z "/\" z by YELLOW_5:2 .= f.x "/\" z by A1
.= f.x "/\" f.y by A1;
end;
hence f is meet-preserving by WAYBEL_6:1;
for x,y being Element of L1 holds f.(x "\/" y) = f.x "\/" f.y
proof
let x,y be Element of L1;
thus f.(x "\/" y) = z by A1 .= z "\/" z by YELLOW_5:1 .= f.x "\/" z by A1
.= f.x "\/" f.y by A1;
end;
hence f is join-preserving by WAYBEL_6:2;
end;
end;
definition let L1,L2 be LATTICE;
mode Homomorphism of L1,L2 is meet-preserving join-preserving map of L1,L2;
end;
definition let L be LATTICE;
cluster meet-inheriting join-inheriting strict SubRelStr of L;
existence
proof
consider a being Element of L;
consider r be Relation of {a};
A1: {a} c= the carrier of L
proof let x be set; assume
x in {a};
then x = a by TARSKI:def 1;
hence x in the carrier of L;
end;
r c= the InternalRel of L
proof let z be set; assume z in r;
then consider x,y be set such that
A2: z = [x,y] & x in {a} & y in {a} by RELSET_1:6;
x = a & y = a by A2,TARSKI:def 1;
then z = [a,a] & a <= a by A2;
hence z in the InternalRel of L by ORDERS_1:def 9;
end;
then reconsider S=RelStr(# {a}, r#) as strict SubRelStr of L
by A1,YELLOW_0:def 13;
take S;
A3: for x,y being Element of L st x in {a} & y in {a} & ex_inf_of {x,y},L
holds inf {x,y} in {a}
proof let x,y be Element of L; assume
x in {a} & y in {a} & ex_inf_of {x,y},L;
then x = a & y = a by TARSKI:def 1;
then inf {x,y} = a"/\"a by YELLOW_0:40 .= a by YELLOW_5:2;
hence inf {x,y} in {a} by TARSKI:def 1;
end;
for x,y being Element of L st x in {a} & y in {a} & ex_sup_of {x,y},L
holds sup {x,y} in {a}
proof let x,y be Element of L; assume
x in {a} & y in {a} & ex_sup_of {x,y},L;
then x = a & y = a by TARSKI:def 1;
then sup {x,y} = a"\/"a by YELLOW_0:41 .= a by YELLOW_5:1;
hence sup {x,y} in {a} by TARSKI:def 1;
end;
hence thesis by A3,YELLOW_0:def 16,def 17;
end;
end;
definition
let L be non empty RelStr;
mode Sublattice of L is meet-inheriting join-inheriting SubRelStr of L;
end;
definition
let L1, L2 be LATTICE;
let f be Homomorphism of L1,L2;
redefine func Image f -> strict full Sublattice of L2;
coherence
proof
set S = subrelstr rng f;
A1: the carrier of S = rng f by YELLOW_0:def 15;
A2: dom f = the carrier of L1 by FUNCT_2:def 1;
for x,y being Element of L2 st
x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L2
holds inf {x,y} in the carrier of S
proof
let x,y be Element of L2; assume
A3: x in the carrier of S & y in the carrier of S & ex_inf_of {x,y},L2;
then consider a being set such that
A4: a in dom f & x = f.a by A1,FUNCT_1:def 5;
consider b being set such that
A5: b in dom f & y = f.b by A1,A3,FUNCT_1:def 5;
reconsider a' = a, b' = b as Element of L1 by A4,A5;
A6: f preserves_inf_of {a',b'} by WAYBEL_0:def 34;
A7: ex_inf_of {a',b'},L1 by YELLOW_0:21;
inf {x,y} = inf (f.:{a',b'}) by A4,A5,FUNCT_1:118
.= f.inf {a',b'} by A6,A7,WAYBEL_0:def 30;
hence inf {x,y} in the carrier of S by A1,A2,FUNCT_1:def 5;
end;
then A8: S is meet-inheriting by YELLOW_0:def 16;
for x,y being Element of L2 st
x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L2
holds sup {x,y} in the carrier of S
proof
let x,y be Element of L2; assume
A9: x in the carrier of S & y in the carrier of S & ex_sup_of {x,y},L2;
then consider a being set such that
A10: a in dom f & x = f.a by A1,FUNCT_1:def 5;
consider b being set such that
A11: b in dom f & y = f.b by A1,A9,FUNCT_1:def 5;
reconsider a' = a, b' = b as Element of L1 by A10,A11;
A12: f preserves_sup_of {a',b'} by WAYBEL_0:def 35;
A13: ex_sup_of {a',b'},L1 by YELLOW_0:20;
sup {x,y} = sup (f.:{a',b'}) by A10,A11,FUNCT_1:118
.= f.sup {a',b'} by A12,A13,WAYBEL_0:def 31;
hence sup {x,y} in the carrier of S by A1,A2,FUNCT_1:def 5;
end;
then S is join-inheriting by YELLOW_0:def 17;
hence Image f is strict full Sublattice of L2 by A8,YELLOW_2:def 2;
end;
end;
reserve e,e1,e2,e1',e2' for Equivalence_Relation of X,
x,y,x',y' for set;
definition let X; let f be non empty FinSequence of X; let x,y;
let R1, R2 be Relation;
pred x,y are_joint_by f,R1,R2 means :Def3:
f.1 = x & f.(len f) = y &
for i being Nat st 1 <= i & i < len f holds
(i is odd implies [f.i,f.(i+1)] in R1) &
(i is even implies [f.i,f.(i+1)] in R2);
end;
canceled;
theorem Th12:
for x being set, o being Nat, R1,R2 being Relation,
f being non empty FinSequence of X st
R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x
holds x,x are_joint_by f,R1,R2
proof
let x be set, o be Nat, R1,R2 be Relation,
f be non empty FinSequence of X; assume that
A1:R1 is_reflexive_in X & R2 is_reflexive_in X and
A2:f = o |-> x;
A3: dom f = Seg(o) by A2,FINSEQ_2:68;
then A4: 1 in Seg(o) & len f in Seg(o) by FINSEQ_5:6;
then A5:f.1 = x by A2,FINSEQ_2:70;
A6:f.(len f) = x by A2,A4,FINSEQ_2:70;
for i being Nat st 1 <= i & i < len f holds
(i is odd implies [f.i,f.(i+1)] in R1) &
(i is even implies [f.i,f.(i+1)] in R2)
proof
let i be Nat; assume
A7: 1 <= i & i < len f;
A8: i is odd implies [f.i,f.(i+1)] in R1
proof
assume i is odd;
1 <= i+1 & i+1 <= len f by A7,NAT_1:38;
then i+1 in Seg(len f) by FINSEQ_1:3;
then i+1 in Seg(o) by A2,FINSEQ_2:69;
then A9: f.(i+1) = x by A2,FINSEQ_2:70;
1 <= i & i <= o by A2,A7,FINSEQ_2:69;
then i in Seg(o) by FINSEQ_1:3;
then A10: f.i = x by A2,FINSEQ_2:70;
x in X by A3,A4,A5,FINSEQ_2:13;
hence [f.i,f.(i+1)] in R1 by A1,A9,A10,RELAT_2:def 1;
end;
i is even implies [f.i,f.(i+1)] in R2
proof
assume i is even;
1 <= i+1 & i+1 <= len f by A7,NAT_1:38;
then i+1 in Seg(len f) by FINSEQ_1:3;
then i+1 in Seg(o) by A2,FINSEQ_2:69;
then A11: f.(i+1) = x by A2,FINSEQ_2:70;
1 <= i & i <= o by A2,A7,FINSEQ_2:69;
then i in Seg(o) by FINSEQ_1:3;
then A12: f.i = x by A2,FINSEQ_2:70;
x in X by A3,A4,A5,FINSEQ_2:13;
hence [f.i,f.(i+1)] in R2 by A1,A11,A12,RELAT_2:def 1;
end;
hence (i is odd implies [f.i,f.(i+1)] in R1) &
(i is even implies [f.i,f.(i+1)] in R2) by A8;
end;
hence x,x are_joint_by f,R1,R2 by A5,A6,Def3;
end;
Lm1:
now
let i,n,m be Nat; assume 1 <= i & i < n+m;
then 1 <= i & i < n or n = i & i < n+m or n < i & i < n+m by REAL_1:def 5;
hence 1 <= i & i < n or n = i & i < n+m or n+1 <= i & i < n+m by NAT_1:38;
end;
canceled;
theorem Th14:
for x,y being set, R1,R2 being Relation, n,m being Nat st
(n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X &
ex f being non empty FinSequence of X st
len f = n & x,y are_joint_by f,R1,R2)
ex h being non empty FinSequence of X st
len h = m & x,y are_joint_by h,R1,R2
proof
let x,y be set, R1,R2 be Relation, n,m be Nat; assume that
A1: n <= m and
A2: R1 is_reflexive_in X & R2 is_reflexive_in X;
given f being non empty FinSequence of X such that
A3: len f = n & x,y are_joint_by f,R1,R2;
A4: f.(len f) = y by A3,Def3;
per cases by A1,REAL_1:def 5;
suppose
A5:n < m;
reconsider i = m - n as Nat by A1,INT_1:18;
A6: i > 0 by A5,SQUARE_1:11;
len f in dom f by SCMFSA_7:12;
then A7: y in rng f by A4,FUNCT_1:def 5;
rng f c= X by FINSEQ_1:def 4;
then reconsider y' = y as Element of X by A7;
reconsider g = i |-> y' as FinSequence of X;
len g <> 0 by A6,FINSEQ_2:69;
then reconsider g as non empty FinSequence of X by FINSEQ_1:25;
A8: 1 in dom g & len g in dom g by FINSEQ_5:6;
A9: y,y are_joint_by g,R1,R2 by A2,Th12;
reconsider h = f^g as non empty FinSequence of X;
take h;
thus
len h = len f + len g by FINSEQ_1:35
.= n+(m-n) by A3,FINSEQ_2:69 .= n+m-n by XCMPLX_1:29
.= m+(n-n) by XCMPLX_1:29 .= m+0 by XCMPLX_1:14
.= m;
A10: len g = m-n by FINSEQ_2:69;
thus x,y are_joint_by h,R1,R2
proof
rng f <> {} by RELAT_1:64;
then 1 in dom f by FINSEQ_3:34;
hence h.1 = f.1 by FINSEQ_1:def 7 .= x by A3,Def3;
thus h.(len h) = h.(len f + len g) by FINSEQ_1:35
.= g.(len g) by A8,FINSEQ_1:def 7
.= y by A9,Def3;
let j be Nat;
assume
A11: 1 <= j & j < len h;
A12: dom f = Seg(len f) by FINSEQ_1:def 3;
thus j is odd implies [h.j,h.(j+1)] in R1
proof
assume
A13: j is odd;
per cases by A11,Lm1,FINSEQ_1:35;
suppose
A14: 1 <= j & j < len f;
then 1 <= j+1 & j+1 <= len f by NAT_1:38;
then j+1 in dom f by A12,FINSEQ_1:3;
then A15: f.(j+1) = h.(j+1) by FINSEQ_1:def 7;
j in dom f by A12,A14,FINSEQ_1:3;
then f.j = h.j by FINSEQ_1:def 7;
hence [h.j,h.(j+1)] in R1 by A3,A13,A14,A15,Def3;
suppose
A16: j = len f;
then j in dom f by FINSEQ_5:6;
then A17: h.j = y by A4,A16,FINSEQ_1:def 7;
h.(j+1) = g.1 by A8,A16,FINSEQ_1:def 7
.= y by A9,Def3;
hence [h.j,h.(j+1)] in R1 by A2,A17,RELAT_2:def 1;
suppose
A18: len f + 1 <= j & j < len f + len g;
then A19: 1 <= j - len f by REAL_1:84;
j - len f < len f + len g - len f by A18,REAL_1:54;
then j - len f < len f - len f + len g by XCMPLX_1:29;
then A20: j - len f < 0+len g by XCMPLX_1:14;
0 < j - len f by A19,AXIOMS:22;
then 0 + len f < j -len f + len f by REAL_1:53;
then len f < j + len f - len f by XCMPLX_1:29;
then len f < j + (len f - len f) by XCMPLX_1:29;
then A21: len f < j+0 by XCMPLX_1:14;
then reconsider k = j - len f as Nat by INT_1:18;
A22: 1 <= k+1 & k+1 <= len g by A19,A20,NAT_1:38;
k in Seg (len g) by A19,A20,FINSEQ_1:3;
then A23: g.k = y by A10,FINSEQ_2:70;
k+1 in Seg (len g) by A22,FINSEQ_1:3;
then A24: g.(k+1) = y by A10,FINSEQ_2:70;
A25: j < j+1 by REAL_1:69;
j+1 <= len f + len g by A18,NAT_1:38;
then len f < j+1 & j+1 <= len h by A21,A25,AXIOMS:22,FINSEQ_1:35;
then A26: h.(j+1) = g.(j+1-len f) by FINSEQ_1:37
.= g.(k+1) by XCMPLX_1:29;
h.j = y by A18,A23,FINSEQ_1:36;
hence [h.j,h.(j+1)] in R1 by A2,A24,A26,RELAT_2:def 1;
end;
assume
A27: j is even;
per cases by A11,Lm1,FINSEQ_1:35;
suppose
A28: 1 <= j & j < len f;
then 1 <= j+1 & j+1 <= len f by NAT_1:38;
then j+1 in dom f by A12,FINSEQ_1:3;
then A29: f.(j+1) = h.(j+1) by FINSEQ_1:def 7;
j in dom f by A12,A28,FINSEQ_1:3;
then f.j = h.j by FINSEQ_1:def 7;
hence [h.j,h.(j+1)] in R2 by A3,A27,A28,A29,Def3;
suppose
A30: j = len f;
then j in dom f by FINSEQ_5:6;
then A31: h.j = y by A4,A30,FINSEQ_1:def 7;
h.(j+1) = g.1 by A8,A30,FINSEQ_1:def 7
.= y by A9,Def3;
hence [h.j,h.(j+1)] in R2 by A2,A31,RELAT_2:def 1;
suppose
A32: len f + 1 <= j & j < len f + len g;
then A33: 1 <= j - len f by REAL_1:84;
j - len f < len f + len g - len f by A32,REAL_1:54;
then j - len f < len f - len f + len g by XCMPLX_1:29;
then A34: j - len f < 0+len g by XCMPLX_1:14;
0 < j - len f by A33,AXIOMS:22;
then 0 + len f < j -len f + len f by REAL_1:53;
then len f < j + len f - len f by XCMPLX_1:29;
then len f < j + (len f - len f) by XCMPLX_1:29;
then A35: len f < j+0 by XCMPLX_1:14;
then reconsider k = j - len f as Nat by INT_1:18;
A36: 1 <= k+1 & k+1 <= len g by A33,A34,NAT_1:38;
k in Seg (len g) by A33,A34,FINSEQ_1:3;
then A37: g.k = y by A10,FINSEQ_2:70;
k+1 in Seg (len g) by A36,FINSEQ_1:3;
then A38: g.(k+1) = y by A10,FINSEQ_2:70;
A39: j < j+1 by REAL_1:69;
j+1 <= len f + len g by A32,NAT_1:38;
then len f < j+1 & j+1 <= len h by A35,A39,AXIOMS:22,FINSEQ_1:35;
then A40: h.(j+1) = g.(j+1-len f) by FINSEQ_1:37
.= g.(k+1) by XCMPLX_1:29;
h.j = y by A32,A37,FINSEQ_1:36;
hence [h.j,h.(j+1)] in R2 by A2,A38,A40,RELAT_2:def 1;
end;
suppose n = m;
hence thesis by A3;
end;
definition
let X;let Y be Sublattice of EqRelLATT X;
given e such that
A1: e in the carrier of Y and
A2: e <> id X;
given o being Nat such that
A3: for e1,e2,x,y 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 -> Nat means :Def4:
(for e1,e2,x,y 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,x,y st e1 in the carrier of Y & e2 in the carrier of Y &
[x,y] in e1 "\/" e2 &
not (ex F being non empty FinSequence of X st
len F = it+1 & x,y are_joint_by F,e1,e2));
existence
proof
defpred X[Nat] means
for e1,e2,x,y 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 = $1+2 & x,y are_joint_by F,e1,e2;
set A = { n where n is Nat : X[n] };
A4: field e = X by EQREL_1:16;
id X c= e by A4,RELAT_2:17;
then not e c= id X by A2,XBOOLE_0:def 10;
then consider x,y such that
A5: [x,y] in e and
A6: not [x,y] in id X by RELAT_1:def 3;
A7: not x in X or x <> y by A6,RELAT_1:def 10;
consider e1,e2 such that
A8: e1 = e & e2 = e;
A9: [x,y] in e1 "\/" e2 by A5,A8,EQREL_1:22;
then consider F being non empty FinSequence of X such that
A10: len F = o and
A11: x,y are_joint_by F,e1,e2 by A1,A3,A8;
A12: F.1 = x & F.(len F) = y &
for i being Nat st 1 <= i & i < len F holds
(i is odd implies [F.i,F.(i+1)] in e1) &
(i is even implies [F.i,F.(i+1)] in e2) by A11,Def3;
o >= 2
proof assume
A13: not thesis;
A14: 0 <= len F by NAT_1:18;
len F < 1 + 1 by A10,A13;
then len F <= 0 + 1 by NAT_1:38;
then 0 = len F or len F = 1 by A14,NAT_1:27;
hence contradiction by A4,A5,A7,A12,FINSEQ_1:25,RELAT_1:30;
end;
then consider o' being Nat such that
A15: o = 2 + o' by NAT_1:28;
consider k being Nat such that
A16: k = o' &
for e1,e2,x,y 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 = k+2 & x,y are_joint_by F,e1,e2 by A3,A15;
A17: k in A by A16;
A is Subset of NAT from SubsetD;
then reconsider A as non empty Subset of NAT by A17;
set m = min A;
m in A by CQC_SIM1:def 8;
then consider m' being Nat such that
A18: m' = m &
for e1,e2,x,y 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 = m'+2 & x,y are_joint_by F,e1,e2);
ex e1,e2,x,y st e1 in the carrier of Y & e2 in the carrier of Y &
[x,y] in e1 "\/" e2 &
not (ex F being non empty FinSequence of X st
len F = m+1 & x,y are_joint_by F,e1,e2)
proof assume A19: not thesis;
then consider F being non empty FinSequence of X such that
A20: len F = m+1 & x,y are_joint_by F,e1,e2 by A1,A8,A9;
A21: F.1 = x & F.(len F) = y by A20,Def3;
len F >= 2
proof assume A22: not thesis;
A23: 0 <= len F by NAT_1:18;
len F < 1 + 1 by A22;
then len F <= 0 + 1 by NAT_1:38;
then 0 = len F or len F = 1 by A23,NAT_1:27;
hence contradiction by A4,A5,A7,A21,FINSEQ_1:25,RELAT_1:30;
end;
then m + 1 >= 1 + 1 by A20;
then A24: m >= 1 by REAL_1:53;
then A25: m - 1 >= 0 by SQUARE_1:12;
m < m + 1 by REAL_1:69;
then m - 1 < m + 1 - 1 by REAL_1:54;
then A26: m - 1 < m + (1 - 1) by XCMPLX_1:29;
A27: m + 1 = (m + 1) + 1 - 1 by XCMPLX_1:26 .= m + (1 + 1) - 1 by XCMPLX_1:1
.= m - 1 + 2 by XCMPLX_1:29;
m - 1 = m -' 1 by A24,SCMFSA_7:3;
then A28: m -' 1 in A by A19,A27;
m -' 1 < m by A25,A26,BINARITH:def 3;
hence contradiction by A28,CQC_SIM1:def 8;
end;
hence thesis by A18;
end;
uniqueness
proof let n1,n2 be Nat; assume
A29: (for e1,e2,x,y 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 = n1+2 & x,y are_joint_by F,e1,e2));
given e1',e2',x',y' such that
A30: e1' in the carrier of Y & e2' in the carrier of Y &
[x',y'] in e1' "\/" e2' and
A31: not (ex F being non empty FinSequence of X st
len F = n1+1 & x',y' are_joint_by F,e1',e2'); assume
A32: (for e1,e2,x,y 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 = n2+2 & x,y are_joint_by F,e1,e2));
given e1,e2,x,y such that
A33: e1 in the carrier of Y & e2 in the carrier of Y &
[x,y] in e1 "\/" e2 and
A34: not (ex F being non empty FinSequence of X st
len F = n2+1 & x,y are_joint_by F,e1,e2);
consider F1 being non empty FinSequence of X such that
A35: len F1 = n1+2 & x,y are_joint_by F1,e1,e2 by A29,A33;
consider F2 being non empty FinSequence of X such that
A36: len F2 = n2+2 & x',y' are_joint_by F2,e1',e2' by A30,A32;
A37: field e1 = X & field e2 = X by EQREL_1:16;
A38: e1 is_reflexive_in X & e2 is_reflexive_in X
by A37,RELAT_2:def 9;
A39: field e1' = X & field e2' = X by EQREL_1:16;
A40: e1' is_reflexive_in X & e2' is_reflexive_in X
by A39,RELAT_2:def 9;
assume A41:not thesis;
per cases by A41,REAL_1:def 5;
suppose n1 < n2;
then n1+2 < n2+(1+1) by REAL_1:53;
then n1+2 < (n2+1)+1 by XCMPLX_1:1;
then n1+2 <= n2+1 by NAT_1:38;
hence contradiction by A34,A35,A38,Th14;
suppose n2 < n1;
then n2+2 < n1+(1+1) by REAL_1:53;
then n2+2 < (n1+1)+1 by XCMPLX_1:1;
then n2+2 <= n1+1 by NAT_1:38;
hence contradiction by A31,A36,A40,Th14;
end;
end;
theorem Th15:
for Y being Sublattice of EqRelLATT X, n being Nat st
(ex e st e in the carrier of Y & e <> id X) &
(for e1,e2,x,y 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 = n+2 & x,y are_joint_by F,e1,e2))
holds type_of Y <= n
proof
let Y be Sublattice of EqRelLATT X, n be Nat; assume that
A1: (ex e st e in the carrier of Y & e <> id X) and
A2: for e1,e2,x,y 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 = n+2 & x,y are_joint_by F,e1,e2 and
A3: n < type_of Y;
n+1 <= type_of Y by A3,NAT_1:38;
then consider m being Nat such that
A4: type_of Y = (n+1)+m by NAT_1:28;
n+1+m+1 = n+m+1+1 by XCMPLX_1:1
.= (n+m)+(1+1) by XCMPLX_1:1 .= n+m+2;
then consider e1,e2,x,y such that
A5: e1 in the carrier of Y &
e2 in the carrier of Y & [x,y] in e1 "\/" e2 and
A6: not (ex F being non empty FinSequence of X st
len F = (n+m)+2 & x,y are_joint_by F,e1,e2) by A1,A4,Def4;
consider F1 being non empty FinSequence of X such that
A7: len F1 = n+2 & x,y are_joint_by F1,e1,e2 by A2,A5;
A8: field e1 = X & field e2 = X by EQREL_1:16;
A9: e1 is_reflexive_in X & e2 is_reflexive_in X
by A8,RELAT_2:def 9;
n+2+m = (n+m)+2 by XCMPLX_1:1;
then n+2 <= (n+m)+2 by NAT_1:29;
hence contradiction by A6,A7,A9,Th14;
end;
begin :: A meet-representation of a lattice
reserve A for non empty set,
L for lower-bounded LATTICE;
definition let A, L;
mode BiFunction of A,L is Function of [:A,A:],the carrier of L;
canceled;
end;
definition let A, L;
let f be BiFunction of A,L;let x,y be Element of A;
redefine func f.(x,y) -> Element of L;
coherence
proof
reconsider xy = [x,y] as Element of [:A,A:];
f.xy is Element of L;
hence thesis by BINOP_1:def 1;
end;
end;
definition let A, L; let f be BiFunction of A,L;
attr f is symmetric means :Def6:
for x,y being Element of A holds f.(x,y) = f.(y,x);
attr f is zeroed means :Def7:
for x being Element of A holds f.(x,x) = Bottom L;
attr f is u.t.i. means :Def8:
for x,y,z being Element of A holds f.(x,y) "\/" f.(y,z) >= f.(x,z);
end;
:: f is u.t.i. means that f satisfies the triangle inequality
definition let A, L;
cluster symmetric zeroed u.t.i. BiFunction of A,L;
existence
proof
deffunc U(Element of A,Element of A) = Bottom L;
consider f being Function of [:A,A:],the carrier of L such that
A1:for x,y being Element of A holds f.[x,y] = U(x,y) from Lambda2D;
reconsider f as BiFunction of A,L;
A2:for x,y being Element of A holds f.(x,y) = Bottom L
proof
let x,y be Element of A;
reconsider x' = x as set; reconsider y' = y as set;
Bottom L = f.[x,y] by A1 .= f.(x',y') by BINOP_1:def 1;
hence thesis;
end;
for x,y being Element of A holds f.(x,y) = f.(y,x)
proof
let x,y be Element of A;
thus f.(x,y) = Bottom L by A2 .= f.(y,x) by A2;
end;
then A3:f is symmetric by Def6;
for x being Element of A holds f.(x,x) = Bottom L by A2;
then A4:f is zeroed by Def7;
for x,y,z being Element of A holds f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
let x,y,z be Element of A;
A5: f.(x,y) = Bottom L & f.(y,z) = Bottom L by A2;
f.(x,z) <= Bottom L by A2;
hence thesis by A5,YELLOW_5:1;
end;
then f is u.t.i. by Def8;
hence thesis by A3,A4;
end;
end;
definition let A, L;
mode distance_function of A,L is symmetric zeroed u.t.i. BiFunction of A,L;
end;
definition let A, L; let d be distance_function of A,L;
func alpha d -> map 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 be Element of A holds [x,y] in E iff d.(x,y) <= e;
existence
proof
defpred X[Element of L,Element of EqRelLATT A] means
ex E being Equivalence_Relation of A st E = $2 &
for x,y be Element of A holds [x,y] in E iff d.(x,y) <= $1;
A1:for e being Element of L ex r being Element of EqRelLATT A st X[e,r]
proof
let e be Element of L;
defpred X[Element of A,Element of A] means d.($1,$2) <= e;
consider E being Relation of A,A such that A2:
for x,y being Element of A holds [x,y] in E iff X[x,y]
from Rel_On_Dom_Ex;
for x be set holds x in A implies [x,x] in E
proof
let x be set; assume x in A;
then reconsider x' = x as Element of A;
Bottom L <= e by YELLOW_0:44;
then d.(x',x') <= e by Def7;
hence [x,x] in E by A2;
end;
then E is_reflexive_in A by RELAT_2:def 1;
then
A3: dom E = A & field E = A by ORDERS_1:98;
for x,y being set holds x in A & y in A & [x,y] in E implies [y,x] in E
proof
let x,y be set; assume that A5: x in A & y in A and
A6: [x,y] in E;
reconsider x' = x as Element of A by A5;
reconsider y' = y as Element of A by A5;
d.(x',y') <= e by A2,A6;
then d.(y',x') <= e by Def6;
hence [y,x] in E by A2;
end;
then A7: E is_symmetric_in A by RELAT_2:def 3;
for x,y,z being set holds x in A & y in A & z in A &
[x,y] in E & [y,z] in E implies [x,z] in E
proof
let x,y,z be set; assume that A8: x in A & y in A & z in A and
A9: [x,y] in E & [y,z] in E;
reconsider x' = x, y' = y, z' = z as Element of A by A8;
d.(x',y') <= e & d.(y',z') <= e by A2,A9;
then A10: d.(x',y') "\/" d.(y',z') <= e by YELLOW_0:22;
d.(x',z') <= d.(x',y') "\/" d.(y',z') by Def8;
then d.(x',z') <= e by A10,ORDERS_1:26;
hence [x,z] in E by A2;
end;
then E is_transitive_in A by RELAT_2:def 8;
then reconsider E as Equivalence_Relation of A
by A3,PARTFUN1:def 4,A7,RELAT_2:def 11,def 16;
reconsider E as Element of EqRelLATT A by Th4;
consider r being Element of EqRelLATT A such that A11: r = E;
thus thesis by A2,A11;
end;
consider f being map of L,EqRelLATT A such that A12:
for e being Element of L holds X[e,f.e] from NonUniqExMD(A1);
thus thesis by A12;
end;
uniqueness
proof
let f1,f2 be map of L,EqRelLATT A such that
A13: for e being Element of L
ex E being Equivalence_Relation of A st E = f1.e &
for x,y be Element of A holds [x,y] in E iff d.(x,y) <= e and
A14: for e being Element of L
ex E being Equivalence_Relation of A st E = f2.e &
for x,y be Element of A holds [x,y] in E iff d.(x,y) <= e;
A15:for e being Element of L holds f1.e = f2.e
proof
let e be Element of L;
consider E1 being Equivalence_Relation of A such that A16:E1 = f1.e &
for x,y being Element of A holds [x,y] in E1 iff d.(x,y) <= e by A13;
consider E2 being Equivalence_Relation of A such that A17:E2 = f2.e &
for x,y being Element of A holds [x,y] in E2 iff d.(x,y) <= e by A14;
A18:for x,y being Element of A holds [x,y] in E1 iff [x,y] in E2
proof
let x,y be Element of A;
[x,y] in E1 iff d.(x,y) <= e by A16;
hence thesis by A17;
end;
for x,y being set holds [x,y] in E1 iff [x,y] in E2
proof
let x,y be set;
A19: field E1 = A & field E2 = A by EQREL_1:16;
hereby assume A20:[x,y] in E1;
then reconsider x' = x, y' = y as Element of A by A19,RELAT_1:30;
[x',y'] in E2 by A18,A20;
hence [x,y] in E2;
end;
assume A21:[x,y] in E2;
then reconsider x' = x, y' = y as Element of A by A19,RELAT_1:30;
[x',y'] in E1 by A18,A21;
hence [x,y] in E1;
end;
hence thesis by A16,A17,RELAT_1:def 2;
end;
reconsider f1'=f1, f2'=f2 as Function of the carrier of L,
the carrier of EqRelLATT A;
for e be set st e in the carrier of L holds f1'.e = f2'.e by A15;
hence f1 = f2 by FUNCT_2:18;
end;
end;
theorem Th16:
for d being distance_function of A,L holds alpha d is meet-preserving
proof let d be distance_function of A,L; let a,b be Element of L;
set f = alpha d;
A1: ex_inf_of f.:{a,b},EqRelLATT A by YELLOW_0:17;
A2: dom f = the carrier of L by FUNCT_2:def 1;
consider E1 being Equivalence_Relation of A such that
A3: E1 = f.a &
for x,y being Element of A holds [x,y] in E1 iff d.(x,y) <= a by Def9;
consider E2 being Equivalence_Relation of A such that
A4: E2 = f.b &
for x,y being Element of A holds [x,y] in E2 iff d.(x,y) <= b by Def9;
consider E3 being Equivalence_Relation of A such that
A5: E3 = f.(a "/\" b) &
for x,y being Element of A holds [x,y] in E3 iff d.(x,y) <= a "/\"
b by Def9;
A6: for x,y being Element of A holds [x,y] in E1 /\ E2 iff [x,y] in E3
proof let x,y be Element of A;
hereby assume
[x,y] in E1 /\ E2;
then [x,y] in E1 & [x,y] in E2 by XBOOLE_0:def 3;
then d.(x,y) <= a & d.(x,y) <= b by A3,A4;
then d.(x,y) <= a "/\" b by YELLOW_0:23;
hence [x,y] in E3 by A5;
end; assume [x,y] in E3;
then A7: d.(x,y) <= a "/\" b by A5;
a "/\" b <= a by YELLOW_0:23;
then d.(x,y) <= a by A7,ORDERS_1:26;
then A8: [x,y] in E1 by A3;
a "/\" b <= b by YELLOW_0:23;
then d.(x,y) <= b by A7,ORDERS_1:26;
then [x,y] in E2 by A4;
hence [x,y] in E1 /\ E2 by A8,XBOOLE_0:def 3;
end;
A9: for x,y being set holds [x,y] in E1 /\ E2 iff [x,y] in E3
proof let x,y be set;
A10: field E3 = A by EQREL_1:16;
field E1 /\ field E2 = A /\ field E2 by EQREL_1:16
.= A /\ A by EQREL_1:16 .= A;
then A11: field (E1 /\ E2) c= A by RELAT_1:34;
hereby
assume A12:[x,y] in E1 /\ E2;
then x in field (E1 /\ E2) & y in field (E1 /\ E2) by RELAT_1:30;
then reconsider x' = x, y' = y as Element of A by A11;
[x',y'] in E3 by A6,A12;
hence [x,y] in E3;
end;
assume A13:[x,y] in E3;
then reconsider x' = x, y' = y as Element of A by A10,RELAT_1:30;
[x',y'] in E1 /\ E2 by A6,A13;
hence [x,y] in E1 /\ E2;
end;
inf (f.:{a,b}) = inf {f.a,f.b} by A2,FUNCT_1:118
.= f.a "/\" f.b by YELLOW_0:40 .= E1 /\ E2 by A3,A4,Th8
.= f.(a "/\" b) by A5,A9,RELAT_1:def 2
.= f.inf {a,b} by YELLOW_0:40;
hence f preserves_inf_of {a,b} by A1,WAYBEL_0:def 30;
end;
theorem Th17:
for d being distance_function of A,L st d is onto holds alpha d is one-to-one
proof let d be distance_function of A,L; assume
d is onto;
then A1: rng d = the carrier of L by FUNCT_2:def 3;
set f = alpha d;
for a,b being Element of L st f.a = f.b holds a = b
proof
let a,b be Element of L; assume A2:f.a = f.b;
consider z1 be set such that A3: z1 in [:A,A:] & d.z1 = a by A1,FUNCT_2:17;
consider x1,y1 being set such that
A4: x1 in A & y1 in A & z1 = [x1,y1] by A3,ZFMISC_1:def 2;
consider z2 be set such that A5: z2 in [:A,A:] & d.z2 = b by A1,FUNCT_2:17;
consider x2,y2 being set such that
A6: x2 in A & y2 in A & z2 = [x2,y2] by A5,ZFMISC_1:def 2;
reconsider x1,y1 as Element of A by A4;
reconsider x2,y2 as Element of A by A6;
A7: d.(x1,y1) = a by A3,A4,BINOP_1:def 1;
A8: d.(x2,y2) = b by A5,A6,BINOP_1:def 1;
consider E1 being Equivalence_Relation of A such that A9:E1 = f.a &
for x,y be Element of A holds [x,y] in E1 iff d.(x,y) <= a by Def9;
consider E2 being Equivalence_Relation of A such that A10:E2 = f.b &
for x,y be Element of A holds [x,y] in E2 iff d.(x,y) <= b by Def9;
E1 = E2 & [x1,y1] in E1 by A2,A7,A9,A10;
then A11: a <= b by A7,A10;
E1 = E2 & [x2,y2] in E2 by A2,A8,A9,A10;
then b <= a by A8,A9;
hence a = b by A11,ORDERS_1:25;
end;
hence alpha d is one-to-one by WAYBEL_1:def 1;
end;
begin :: J\'onsson theorem
definition let A be set;
func new_set A equals :Def10:
A \/ {{A}, {{A}}, {{{A}}} };
correctness;
end;
definition let A be set;
cluster new_set A -> non empty;
coherence
proof
{A} in {{A}, {{A}}, {{{A}}}} by ENUMSET1:14;
then {A} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2;
hence new_set A is non empty by Def10;
end;
end;
definition let A,L; 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
proof
set x = q`1, y = q`2;
reconsider a = q`3, b = q`4 as Element of L;
A1:{A} in new_set A & {{A}} in new_set A & {{{A}}} in new_set A
proof
{A} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14;
then {A} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2;
hence {A} in new_set A by Def10;
{{A}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14;
then {{A}} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2;
hence {{A}} in new_set A by Def10;
{{{A}}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14;
then {{{A}}} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2;
hence {{{A}}} in new_set A by Def10;
end;
defpred
X[Element of new_set A,Element of new_set A,Element of L]
means ($1 in A & $2 in A implies $3 = d.($1,$2)) &
($1 = {{A}} & $2 = {{{A}}} or $2 = {{A}} & $1 = {{{A}}} implies $3 = a) &
($1 = {A} & $2 = {{A}} or $2 = {A} & $1 = {{A}} implies $3 = b) &
($1 = {A} & $2 = {{{A}}} or $2 = {A} & $1 = {{{A}}} implies $3 = a"\/"b) &
(($1 = {A} or $1 = {{A}} or $1 = {{{A}}}) & $2 = $1 implies $3 = Bottom L) &
($1 in A & $2 = {A} implies
ex p' being Element of A st p' = $1 & $3 = d.(p',x)"\/"a) &
($1 in A & $2 = {{A}} implies
ex p' being Element of A st p' = $1 & $3 = d.(p',x)"\/"a"\/"b) &
($1 in A & $2 = {{{A}}} implies
ex p' being Element of A st p' = $1 & $3 = d.(p',y)"\/"b) &
($2 in A & $1 = {A} implies ex q' being Element of A st
q' = $2 & $3 = d.(q',x)"\/"a) &
($2 in A & $1 = {{A}} implies ex q' being Element of A st
q' = $2 & $3 = d.(q',x)"\/"a"\/"b) &
($2 in A & $1 = {{{A}}} implies ex q' being Element of A st
q' = $2 & $3 = d.(q',y)"\/"b);
A2: for p,q being Element of new_set A
ex r being Element of L st X[p,q,r]
proof
let p,q be Element of new_set A; p in new_set A & q in new_set A;
then p in A \/ {{A},{{A}},{{{A}}}} & q in A \/ {{A},{{A}},{{{A}}}} by Def10;
then A3: (p in A or p in {{A},{{A}},{{{A}}}}) &
(q in A or q in {{A},{{A}},{{{A}}}}) by XBOOLE_0:def 2;
A4:{{A}} <> {{{A}}}
proof
assume {{A}} = {{{A}}}; then {{A}} in {{A}} by TARSKI:def 1;
hence contradiction;
end;
A5: {A} <> {{{A}}}
proof
assume {A} = {{{A}}}; then {{A}} in {A} by TARSKI:def 1;
hence contradiction by TARSKI:def 1;
end;
A6: not {A} in A by TARSKI:def 1;
A7:not {{A}} in A
proof assume
A8: {{A}} in A;
A in {A} & {A} in {{A}} by TARSKI:def 1;
hence contradiction by A8,ORDINAL1:3;
end;
A9:not {{{A}}} in A
proof assume
A10: {{{A}}} in A;
A in {A} & {A} in {{A}} & {{A}} in {{{A}}} by TARSKI:def 1;
hence contradiction by A10,ORDINAL1:4;
end;
A11:(p = {A} or p = {{A}} or p = {{{A}}}) & p = q iff
p = {A} & q = {A} or p = {{A}} & q = {{A}} or p = {{{A}}} & q = {{{A}}};
per cases by A3,A11,ENUMSET1:13;
suppose p in A & q in A; then reconsider p'=p,q'=q as Element of A;
take d.(p',q');
thus thesis by A6,A7,A9;
suppose A12:p = {{A}} & q = {{{A}}} or q = {{A}} & p = {{{A}}};
take a; thus thesis by A4,A5,A7,A9,A12;
suppose A13:p = {A} & q = {{A}} or q = {A} & p = {{A}};
take b; thus thesis by A4,A5,A7,A13,TARSKI:def 1;
suppose A14:p = {A} & q = {{{A}}} or q = {A} & p = {{{A}}};
take a"\/"b; thus thesis by A4,A5,A9,A14,TARSKI:def 1;
suppose A15: (p = {A} or p = {{A}} or p = {{{A}}}) & q = p;
take Bottom L; thus thesis by A4,A5,A7,A9,A15,TARSKI:def 1;
suppose A16:p in A & q = {A}; then reconsider p' = p as Element of A;
take d.(p',x)"\/"a;
thus thesis by A5,A7,A9,A16,TARSKI:def 1;
suppose A17:p in A & q = {{A}}; then reconsider p' = p as Element of A;
take d.(p',x)"\/"a"\/"b;
thus thesis by A4,A7,A9,A17,TARSKI:def 1;
suppose A18:p in A & q = {{{A}}}; then reconsider p' = p as Element of A;
take d.(p',y)"\/"b;
thus thesis by A4,A5,A7,A9,A18,TARSKI:def 1;
suppose A19:q in A & p = {A}; then reconsider q' = q as Element of A;
take d.(q',x)"\/"a;
thus thesis by A5,A7,A9,A19,TARSKI:def 1;
suppose A20:q in A & p = {{A}}; then reconsider q' = q as Element of A;
take d.(q',x)"\/"a"\/"b;
thus thesis by A4,A7,A9,A20,TARSKI:def 1;
suppose A21:q in A & p = {{{A}}}; then reconsider q' = q as Element of A;
take d.(q',y)"\/"b;
thus thesis by A4,A5,A7,A9,A21,TARSKI:def 1;
end;
consider f being Function of [:new_set A,new_set A:],the carrier of L
such that A22: for p,q being Element of new_set A holds X[p,q,f.[p,q]]
from FuncEx2D(A2);
reconsider f as BiFunction of new_set A,L;
take f;
A23: for u,v being Element of A holds f.(u,v) = d.(u,v)
proof
let u,v be Element of A;
u in A \/ {{A}, {{A}}, {{{A}}}} & v in A \/ {{A}, {{A}}, {{{A}}}}
by XBOOLE_0:def 2;
then reconsider u' = u, v' = v as Element of new_set A by Def10;
thus f.(u,v) = f.[u',v'] by BINOP_1:def 1 .= d.(u,v) by A22;
end;
A24: f.({{A}},{{{A}}}) = f.[{{A}},{{{A}}}] by BINOP_1:def 1 .= a by A1,A22;
A25:f.({{{A}}},{{A}}) = f.[{{{A}}},{{A}}] by BINOP_1:def 1 .= a by A1,A22;
A26: f.({A},{{A}}) = f.[{A},{{A}}] by BINOP_1:def 1 .= b by A1,A22;
A27:f.({{A}},{A}) = f.[{{A}},{A}] by BINOP_1:def 1 .= b by A1,A22;
A28: f.({A},{{{A}}}) = f.[{A},{{{A}}}] by BINOP_1:def 1 .= a"\/"b by A1,A22;
A29:f.({{{A}}},{A}) = f.[{{{A}}},{A}] by BINOP_1:def 1 .= a"\/"b by A1,A22;
A30: f.({A},{A}) = f.[{A},{A}] by BINOP_1:def 1 .= Bottom L by A1,A22;
A31: f.({{A}},{{A}}) = f.[{{A}},{{A}}] by BINOP_1:def 1 .= Bottom L by A1,A22;
A32: f.({{{A}}},{{{A}}}) = f.[{{{A}}},{{{A}}}] by BINOP_1:def 1 .= Bottom
L by A1,A22
;
A33:for u being Element of A holds (f.(u,{A}) = d.(u,x)"\/"a &
f.(u,{{A}}) = d.(u,x)"\/"a"\/"b & f.(u,{{{A}}}) = d.(u,y)"\/"b)
proof
let u be Element of A; u in
A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2;
then reconsider u' = u as Element of new_set A by Def10;
consider u1 being Element of A such that
A34: u1 = u' & f.[u',{A}] = d.(u1,x)"\/"a by A1,A22;
thus f.(u,{A}) = d.(u,x)"\/"a by A34,BINOP_1:def 1;
consider u2 being Element of A such that
A35: u2 = u' & f.[u',{{A}}] = d.(u2,x)"\/"a"\/"b by A1,A22;
thus f.(u,{{A}}) = d.(u,x)"\/"a"\/"b by A35,BINOP_1:def 1;
consider u3 being Element of A such that
A36: u3 = u' & f.[u',{{{A}}}] = d.(u3,y)"\/"b by A1,A22;
thus f.(u,{{{A}}}) = d.(u,y)"\/"b by A36,BINOP_1:def 1;
end;
for u being Element of A holds (f.({A},u) = d.(u,x)"\/"a &
f.({{A}},u) = d.(u,x)"\/"a"\/"b & f.({{{A}}},u) = d.(u,y)"\/"b)
proof
let u be Element of A; u in
A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2;
then reconsider u' = u as Element of new_set A by Def10;
consider u1 being Element of A such that
A37: u1 = u' & f.[{A},u'] = d.(u1,x)"\/"a by A1,A22;
thus f.({A},u) = d.(u,x)"\/"a by A37,BINOP_1:def 1;
consider u2 being Element of A such that
A38: u2 = u' & f.[{{A}},u'] = d.(u2,x)"\/"a"\/"b by A1,A22;
thus f.({{A}},u) = d.(u,x)"\/"a"\/"b by A38,BINOP_1:def 1;
consider u3 being Element of A such that
A39: u3 = u' & f.[{{{A}}},u'] = d.(u3,y)"\/"b by A1,A22;
thus f.({{{A}}},u) = d.(u,y)"\/"b by A39,BINOP_1:def 1;
end;
hence thesis by A23,A24,A25,A26,A27,A28,A29,A30,A31,A32,A33;
end;
uniqueness
proof
set x = q`1, y = q`2, a = q`3, b = q`4;
let f1,f2 be BiFunction of new_set A,L such that
A40:
(for u,v being Element of A holds f1.(u,v) = d.(u,v) ) &
f1.({A},{A}) = Bottom L & f1.({{A}},{{A}}) = Bottom
L & f1.({{{A}}},{{{A}}}) = Bottom L &
f1.({{A}},{{{A}}}) = a & f1.({{{A}}},{{A}}) = a &
f1.({A},{{A}}) = b & f1.({{A}},{A}) = b &
f1.({A},{{{A}}}) = a"\/"b & f1.({{{A}}},{A}) = a"\/"b &
for u being Element of A holds
(f1.(u,{A}) = d.(u,x)"\/"a & f1.({A},u) = d.(u,x)"\/"a &
f1.(u,{{A}}) = d.(u,x)"\/"a"\/"b & f1.({{A}},u) = d.(u,x)"\/"a"\/"b &
f1.(u,{{{A}}}) = d.(u,y)"\/"b & f1.({{{A}}},u) = d.(u,y)"\/"b) and
A41: (for u,v being Element of A holds f2.(u,v) = d.(u,v) ) &
f2.({A},{A}) = Bottom L & f2.({{A}},{{A}}) = Bottom
L & f2.({{{A}}},{{{A}}}) = Bottom L &
f2.({{A}},{{{A}}}) = a & f2.({{{A}}},{{A}}) = a &
f2.({A},{{A}}) = b & f2.({{A}},{A}) = b &
f2.({A},{{{A}}}) = a"\/"b & f2.({{{A}}},{A}) = a"\/"b &
for u being Element of A holds
(f2.(u,{A}) = d.(u,x)"\/"a & f2.({A},u) = d.(u,x)"\/"a &
f2.(u,{{A}}) = d.(u,x)"\/"a"\/"b & f2.({{A}},u) = d.(u,x)"\/"a"\/"b &
f2.(u,{{{A}}}) = d.(u,y)"\/"b & f2.({{{A}}},u) = d.(u,y)"\/"b);
now
let p,q be Element of new_set A;
p in new_set A & q in new_set A;
then p in A \/ {{A},{{A}},{{{A}}}} & q in A \/ {{A},{{A}},{{{A}}}} by Def10;
then A42: (p in A or p in {{A},{{A}},{{{A}}}}) &
(q in A or q in {{A},{{A}},{{{A}}}}) by XBOOLE_0:def 2;
per cases by A42,ENUMSET1:13;
suppose A43:p in A & q in A;
hence f1.(p,q) = d.(p,q) by A40 .= f2.(p,q) by A41,A43;
suppose A44:p in A & q = {A}; then reconsider p' = p as Element of A;
thus f1.(p,q) = d.(p',x)"\/"a by A40,A44
.= f2.(p,q) by A41,A44;
suppose A45:p in A & q = {{A}}; then reconsider p' = p as Element of A;
thus f1.(p,q) = d.(p',x)"\/"a"\/"b by A40,A45
.= f2.(p,q) by A41,A45;
suppose A46:p in A & q = {{{A}}}; then reconsider p' = p as Element of A;
thus f1.(p,q) = d.(p',y)"\/"b by A40,A46
.= f2.(p,q) by A41,A46;
suppose A47:p = {A} & q in A; then reconsider q' = q as Element of A;
thus f1.(p,q) = d.(q',x)"\/"a by A40,A47
.= f2.(p,q) by A41,A47;
suppose p = {A} & q = {A};
hence f1.(p,q) = f2.(p,q) by A40,A41;
suppose p = {A} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A40,A41;
suppose p = {A} & q = {{{A}}};
hence f1.(p,q) = f2.(p,q) by A40,A41;
suppose A48:p = {{A}} & q in A; then reconsider q' = q as Element of A;
thus f1.(p,q) = d.(q',x)"\/"a"\/"b by A40,A48
.= f2.(p,q) by A41,A48;
suppose p = {{A}} & q = {A};
hence f1.(p,q) = f2.(p,q) by A40,A41;
suppose p = {{A}} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A40,A41;
suppose p = {{A}} & q = {{{A}}};
hence f1.(p,q) = f2.(p,q) by A40,A41;
suppose A49:p = {{{A}}} & q in A; then reconsider q' = q as Element of A;
thus f1.(p,q) = d.(q',y)"\/"b by A40,A49
.= f2.(p,q) by A41,A49;
suppose p = {{{A}}} & q = {A};
hence f1.(p,q) = f2.(p,q) by A40,A41;
suppose p = {{{A}}} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A40,A41;
suppose p = {{{A}}} & q = {{{A}}};
hence f1.(p,q) = f2.(p,q) by A40,A41;
end;
hence f1 = f2 by BINOP_1:2;
end;
end;
theorem Th18:
for d being BiFunction of A,L st d is zeroed
for q being Element of [:A,A,the carrier of L,the carrier of L:]
holds new_bi_fun(d,q) is zeroed
proof let d be BiFunction of A,L; assume
A1: d is zeroed;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set f = new_bi_fun(d,q);
for u being Element of new_set A holds f.(u,u) = Bottom L
proof
let u be Element of new_set A; u in new_set A;
then u in A \/ {{A},{{A}},{{{A}}}} by Def10;
then A2:u in A or u in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 2;
per cases by A2,ENUMSET1:13;
suppose u in A; then reconsider u' = u as Element of A;
thus f.(u,u) = d.(u',u') by Def11 .= Bottom L by A1,Def7;
suppose u = {A} or u = {{A}} or u = {{{A}}};
hence f.(u,u) = Bottom L by Def11;
end;
hence thesis by Def7;
end;
theorem Th19:
for d being BiFunction of A,L st d is symmetric
for q being Element of [:A,A,the carrier of L,the carrier of L:]
holds new_bi_fun(d,q) is symmetric
proof let d be BiFunction of A,L; assume
A1: d is symmetric;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set f = new_bi_fun(d,q),
x = q`1, y = q`2, a = q`3, b = q`4;
let p,q be Element of new_set A; p in new_set A & q in new_set A;
then p in A \/ {{A},{{A}},{{{A}}}} & q in A \/ {{A},{{A}},{{{A}}}} by Def10;
then A2: (p in A or p in {{A},{{A}},{{{A}}}}) &
(q in A or q in {{A},{{A}},{{{A}}}}) by XBOOLE_0:def 2;
per cases by A2,ENUMSET1:13;
suppose p in A & q in A; then reconsider p' = p, q' = q as Element of A;
thus f.(p,q) = d.(p',q') by Def11 .= d.(q',p') by A1,Def6 .= f.(q,p) by Def11;
suppose A3:p in A & q = {A}; then reconsider p' = p as Element of A;
thus f.(p,q) = d.(p',x)"\/"a by A3,Def11 .= f.(q,p) by A3,Def11;
suppose A4:p in A & q = {{A}}; then reconsider p' = p as Element of A;
thus f.(p,q) = d.(p',x)"\/"a"\/"b by A4,Def11 .= f.(q,p) by A4,Def11;
suppose A5:p in A & q = {{{A}}}; then reconsider p' = p as Element of A;
thus f.(p,q) = d.(p',y)"\/"b by A5,Def11 .= f.(q,p) by A5,Def11;
suppose A6:p = {A} & q in A; then reconsider q' = q as Element of A;
thus f.(p,q) = d.(q',x)"\/"a by A6,Def11 .= f.(q,p) by A6,Def11;
suppose p = {A} & q = {A};
hence f.(p,q) = f.(q,p);
suppose A7:p = {A} & q = {{A}};
hence f.(p,q) = b by Def11 .= f.(q,p) by A7,Def11;
suppose A8:p = {A} & q = {{{A}}};
hence f.(p,q) = a"\/"b by Def11 .= f.(q,p) by A8,Def11;
suppose A9:p = {{A}} & q in A; then reconsider q' = q as Element of A;
thus f.(p,q) = d.(q',x)"\/"a"\/"b by A9,Def11 .= f.(q,p) by A9,Def11;
suppose A10:p = {{A}} & q = {A};
hence f.(p,q) = b by Def11 .= f.(q,p) by A10,Def11;
suppose p = {{A}} & q = {{A}};
hence f.(p,q) = f.(q,p);
suppose A11:p = {{A}} & q = {{{A}}};
hence f.(p,q) = a by Def11 .= f.(q,p) by A11,Def11;
suppose A12:p = {{{A}}} & q in A; then reconsider q' = q as Element of A;
thus f.(p,q) = d.(q',y)"\/"b by A12,Def11 .= f.(q,p) by A12,Def11;
suppose A13:p = {{{A}}} & q = {A};
hence f.(p,q) = a"\/"b by Def11 .= f.(q,p) by A13,Def11;
suppose A14:p = {{{A}}} & q = {{A}};
hence f.(p,q) = a by Def11 .= f.(q,p) by A14,Def11;
suppose p = {{{A}}} & q = {{{A}}};
hence f.(p,q) = f.(q,p);
end;
theorem Th20:
for d being BiFunction of A,L st d is symmetric & d is u.t.i.
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_fun(d,q) is u.t.i.
proof
let d be BiFunction of A,L; assume that
A1: d is symmetric and
A2: d is u.t.i.;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
assume
A3: d.(q`1,q`2) <= q`3"\/"q`4;
set x = q`1, y = q`2, f = new_bi_fun(d,q);
reconsider B = {{A}, {{A}}, {{{A}}}} as non empty set by ENUMSET1:14;
reconsider a = q`3,b = q`4 as Element of L;
A4: for p,q,u being Element of new_set A st p in A & q in A & u in A
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A; assume
p in A & q in A & u in A;
then reconsider p' = p, q' = q, u' = u as Element of A;
A5:f.(p,u) = d.(p',u') by Def11;
A6:f.(p,q) = d.(p',q') by Def11;
f.(q,u) = d.(q',u') by Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A2,A5,A6,Def8;
end;
A7: for p,q,u being Element of new_set A st p in A & q in A & u in B
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A; assume
A8: p in A & q in A & u in B;
per cases by A8,ENUMSET1:13;
suppose A9:p in A & q in A & u = {A};
then reconsider p' = p, q' = q as Element of A;
A10:f.(p,u) = d.(p',x)"\/"a by A9,Def11;
A11:f.(q,u) = d.(q',x)"\/"a by A9,Def11;
A12:f.(p,q) = d.(p',q') by Def11;
d.(p',x) <= d.(p',q') "\/" d.(q',x) by A2,Def8;
then d.(p',x)"\/"a <= (d.(p',q') "\/" d.(q',x))"\/"a by WAYBEL_1:3;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A10,A11,A12,LATTICE3:14;
suppose A13:p in A & q in A & u = {{A}};
then reconsider p' = p, q' = q as Element of A;
A14:f.(p,u) = d.(p',x)"\/"a"\/"b by A13,Def11;
A15:f.(q,u) = d.(q',x)"\/"a"\/"b by A13,Def11;
A16:f.(p,q) = d.(p',q') by Def11;
d.(p',x) <= d.(p',q') "\/" d.(q',x) by A2,Def8;
then d.(p',x)"\/"a <= (d.(p',q') "\/" d.(q',x))"\/"a by WAYBEL_1:3;
then (d.(p',x)"\/"a)"\/"b <= ((d.(p',q') "\/" d.(q',x))"\/"a)"\/"
b by WAYBEL_1:3;
then d.(p',x)"\/"a"\/"b <= (d.(p',q') "\/" (d.(q',x)"\/"a))"\/"b by LATTICE3
:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A14,A15,A16,LATTICE3:14;
suppose A17:p in A & q in A & u = {{{A}}};
then reconsider p' = p, q' = q as Element of A;
A18:f.(p,u) = d.(p',y)"\/"b by A17,Def11;
A19:f.(q,u) = d.(q',y)"\/"b by A17,Def11;
A20:f.(p,q) = d.(p',q') by Def11;
d.(p',y) <= d.(p',q') "\/" d.(q',y) by A2,Def8;
then d.(p',y)"\/"b <= (d.(p',q') "\/" d.(q',y))"\/"b by WAYBEL_1:3;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A18,A19,A20,LATTICE3:14;
end;
A21: for p,q,u being Element of new_set A st p in A & q in B & u in A
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A; assume A22:p in A & q in B & u in A;
per cases by A22,ENUMSET1:13;
suppose A23:p in A & u in A & q = {A};
then reconsider p' = p, u' = u as Element of A;
A24:f.(p,q) = d.(p',x)"\/"a by A23,Def11;
A25:f.(q,u) = d.(u',x)"\/"a by A23,Def11;
A26:d.(p',x) "\/" d.(u',x) <= (d.(p',x) "\/" d.(u',x))"\/"a by YELLOW_0:22;
A27:(d.(p',x)"\/"d.(u',x))"\/"a = d.(p',x)"\/"(d.(u',x)"\/"a) by LATTICE3:14
.= d.(p',x)"\/"(d.(u',x)"\/"(a"\/"a)) by YELLOW_5:1
.= d.(p',x)"\/"((d.(u',x)"\/"a)"\/"a) by LATTICE3:14
.= (d.(p',x)"\/"a) "\/" (d.(u',x)"\/"a) by LATTICE3:14;
d.(p',u') <= d.(p',x) "\/" d.(x,u') by A2,Def8;
then d.(p',u') <= d.(p',x) "\/" d.(u',x) by A1,Def6;
then d.(p',u') <= (d.(p',x)"\/"a) "\/" (d.(u',x)"\/"a) by A26,A27,ORDERS_1:
26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A24,A25,Def11;
suppose A28:p in A & u in A & q = {{A}};
then reconsider p' = p, u' = u as Element of A;
A29:f.(p,q) = d.(p',x)"\/"a"\/"b by A28,Def11;
A30:f.(q,u) = d.(u',x)"\/"a"\/"b by A28,Def11;
A31:d.(p',x) "\/" d.(u',x) <= (d.(p',x) "\/" d.(u',x))"\/"(a"\/"
b) by YELLOW_0:22;
A32:(d.(p',x)"\/"d.(u',x))"\/"(a"\/"b) = d.(p',x)"\/"(d.(u',x)"\/"(a"\/"
b)) by LATTICE3:14
.= d.(p',x)"\/"(d.(u',x)"\/"((a"\/"b)"\/"(a"\/"b))) by YELLOW_5:1
.= d.(p',x)"\/"((d.(u',x)"\/"(a"\/"b))"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p',x)"\/"(a"\/"b))"\/"(d.(u',x)"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p',x)"\/"a"\/"b) "\/" (d.(u',x)"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p',x)"\/"a"\/"b) "\/" (d.(u',x)"\/"a"\/"b) by LATTICE3:14;
d.(p',u') <= d.(p',x) "\/" d.(x,u') by A2,Def8;
then d.(p',u') <= d.(p',x) "\/" d.(u',x) by A1,Def6;
then d.(p',u') <= (d.(p',x)"\/"a"\/"b) "\/" (d.(u',x)"\/"a"\/"
b) by A31,A32,ORDERS_1:26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A29,A30,Def11;
suppose A33:p in A & u in A & q = {{{A}}};
then reconsider p' = p, u' = u as Element of A;
A34:f.(p,q) = d.(p',y)"\/"b by A33,Def11;
A35:f.(q,u) = d.(u',y)"\/"b by A33,Def11;
A36:d.(p',y) "\/" d.(u',y) <= (d.(p',y) "\/" d.(u',y))"\/"b by YELLOW_0:22;
A37:(d.(p',y)"\/"d.(u',y))"\/"b = d.(p',y)"\/"(d.(u',y)"\/"b) by LATTICE3:14
.= d.(p',y)"\/"(d.(u',y)"\/"(b"\/"b)) by YELLOW_5:1
.= d.(p',y)"\/"((d.(u',y)"\/"b)"\/"b) by LATTICE3:14
.= (d.(p',y)"\/"b) "\/" (d.(u',y)"\/"b) by LATTICE3:14;
d.(p',u') <= d.(p',y) "\/" d.(y,u') by A2,Def8;
then d.(p',u') <= d.(p',y) "\/" d.(u',y) by A1,Def6;
then d.(p',u') <= (d.(p',y)"\/"b) "\/" (d.(u',y)"\/"b) by A36,A37,ORDERS_1:
26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A34,A35,Def11;
end;
A38: for p,q,u being Element of new_set A st p in A & q in B & u in B
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A; assume A39: p in A & q in B & u in B;
then reconsider p' = p as Element of A;
per cases by A39,ENUMSET1:13;
suppose A40:p in A & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def11
.= f.(p,q) by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A40;
suppose A41: p in A & q = {A} & u = {{A}};
then f.(p,u) = d.(p',x)"\/"a"\/"b by Def11 .= f.(p,q)"\/"b by A41,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A41,Def11;
suppose A42:p in A & q = {A} & u = {{{A}}};
then A43:f.(p,q) = d.(p',x)"\/"a by Def11;
d.(p',y) <= d.(p',x)"\/"d.(x,y) by A2,Def8;
then A44: d.(p',y)"\/"b <= (d.(p',x)"\/"d.(x,y))"\/"b by WAYBEL_1:3;
A45: (d.(p',x)"\/"d.(x,y))"\/"b = (d.(p',x)"\/"b)"\/"d.(x,y) by LATTICE3:14;
d.(p',x)"\/"b <= d.(p',x)"\/"b;
then A46: (d.(p',x)"\/"b)"\/"d.(x,y) <= (d.(p',x)"\/"b)"\/"(a"\/"
b) by A3,YELLOW_3:3;
f.(p,u) <= (d.(p',x)"\/"d.(x,y))"\/"b by A42,A44,Def11;
then A47: f.(p,u) <= (d.(p',x)"\/"b)"\/"(a"\/"b) by A45,A46,ORDERS_1:26;
(d.(p',x)"\/"b)"\/"(a"\/"b) = d.(p',x)"\/"((b"\/"a)"\/"b) by LATTICE3:14
.= d.(p',x)"\/"(a"\/"(b"\/"b)) by LATTICE3:14
.= d.(p',x)"\/"(a"\/"b) by YELLOW_5:1
.= d.(p',x)"\/"((a"\/"a)"\/"b) by YELLOW_5:1
.= d.(p',x)"\/"(a"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p',x)"\/"a)"\/"(a"\/"b) by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A42,A43,A47,Def11;
suppose A48:p in A & q = {{A}} & u = {A};
then f.(p,q) = d.(p',x)"\/"a"\/"b by Def11 .= f.(p,u)"\/"b by A48,Def11;
then f.(p,q) "\/" f.(q,u) = (f.(p,u)"\/"b)"\/"b by A48,Def11
.= f.(p,u)"\/"(b"\/"b) by LATTICE3:14 .= f.(p,u)"\/"b by YELLOW_5:1;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:22;
suppose A49:p in A & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def11
.= f.(p,q) by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A49;
suppose A50:p in A & q = {{A}} & u = {{{A}}};
then A51:f.(p,q) = d.(p',x)"\/"a"\/"b by Def11;
d.(p',y) <= d.(p',x)"\/"d.(x,y) by A2,Def8;
then A52: d.(p',y)"\/"b <= (d.(p',x)"\/"d.(x,y))"\/"b by WAYBEL_1:3;
A53: (d.(p',x)"\/"d.(x,y))"\/"b = (d.(p',x)"\/"b)"\/"d.(x,y) by LATTICE3:14;
d.(p',x)"\/"b <= d.(p',x)"\/"b;
then A54: (d.(p',x)"\/"b)"\/"d.(x,y) <= (d.(p',x)"\/"b)"\/"(a"\/"
b) by A3,YELLOW_3:3;
f.(p,u) <= (d.(p',x)"\/"d.(x,y))"\/"b by A50,A52,Def11;
then A55: f.(p,u) <= (d.(p',x)"\/"b)"\/"(a"\/"b) by A53,A54,ORDERS_1:26;
(d.(p',x)"\/"b)"\/"(a"\/"b) = d.(p',x)"\/"((b"\/"a)"\/"b) by LATTICE3:14
.= d.(p',x)"\/"(a"\/"(b"\/"b)) by LATTICE3:14
.= d.(p',x)"\/"(a"\/"b) by YELLOW_5:1
.= d.(p',x)"\/"((a"\/"a)"\/"b) by YELLOW_5:1
.= d.(p',x)"\/"(a"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p',x)"\/"(a"\/"b))"\/"a by LATTICE3:14
.= (d.(p',x)"\/"a"\/"b)"\/"a by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A50,A51,A55,Def11;
suppose A56:p in A & q = {{{A}}} & u = {A};
then A57:f.(p,q) = d.(p',y)"\/"b by Def11;
d.(p',x) <= d.(p',y)"\/"d.(y,x) by A2,Def8;
then A58: d.(p',x)"\/"a <= (d.(p',y)"\/"d.(y,x))"\/"a by WAYBEL_1:3;
A59: (d.(p',y)"\/"d.(y,x))"\/"a = (d.(p',y)"\/"a)"\/"d.(y,x) by LATTICE3:14;
A60:d.(y,x) <= a"\/"b by A1,A3,Def6;
d.(p',y)"\/"a <= d.(p',y)"\/"a;
then A61: (d.(p',y)"\/"a)"\/"d.(y,x) <= (d.(p',y)"\/"a)"\/"(a"\/"
b) by A60,YELLOW_3:3;
f.(p,u) <= (d.(p',y)"\/"d.(y,x))"\/"a by A56,A58,Def11;
then A62: f.(p,u) <= (d.(p',y)"\/"a)"\/"(a"\/"b) by A59,A61,ORDERS_1:26;
(d.(p',y)"\/"a)"\/"(a"\/"b) =
(d.(p',y)"\/"a"\/"a)"\/"b by LATTICE3:14 .=(d.(p',y)"\/"(a"\/"a))"\/"
b by LATTICE3:14
.= (d.(p',y)"\/"a)"\/"b by YELLOW_5:1 .= d.(p',y)"\/"(a"\/"b) by LATTICE3:14
.= d.(p',y)"\/"(a"\/"(b"\/"b)) by YELLOW_5:1
.= d.(p',y)"\/"((a"\/"b)"\/"b) by LATTICE3:14
.= (d.(p',y)"\/"b)"\/"(a"\/"b) by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A56,A57,A62,Def11;
suppose A63:p in A & q = {{{A}}} & u = {{A}};
then A64:f.(p,u) = d.(p',x)"\/"a"\/"b by Def11;
A65:f.(p,q) = d.(p',y)"\/"b by A63,Def11;
d.(p',x) <= d.(p',y)"\/"d.(y,x) by A2,Def8;
then A66: d.(p',x)"\/"(a"\/"b) <= (d.(p',y)"\/"d.(y,x))"\/"(a"\/"b) by
WAYBEL_1:3;
A67: (d.(p',y)"\/"a)"\/"(a"\/"b) = (d.(p',y)"\/"a)"\/"((a"\/"b)"\/"(a"\/"
b)) by YELLOW_5:1
.= d.(p',y)"\/"(a"\/"((a"\/"b)"\/"(a"\/"b))) by LATTICE3:14
.= d.(p',y)"\/"((a"\/"(a"\/"b))"\/"(a"\/"b)) by LATTICE3:14
.= d.(p',y)"\/"(((a"\/"a)"\/"b)"\/"(a"\/"b)) by LATTICE3:14
.= d.(p',y)"\/"((a"\/"b)"\/"(a"\/"b)) by YELLOW_5:1
.= (d.(p',y)"\/"(a"\/"b))"\/"(a"\/"b) by LATTICE3:14;
A68:d.(y,x) <= a"\/"b by A1,A3,Def6;
A69:(d.(p',y)"\/"d.(y,x))"\/"(a"\/"b) = (d.(p',y)"\/"(a"\/"b))"\/"
d.(y,x) by LATTICE3:14;
d.(p',y)"\/"(a"\/"b) <= d.(p',y)"\/"(a"\/"b);
then A70:(d.(p',y)"\/"d.(y,x))"\/"(a"\/"b)<=(d.(p',y)"\/"(a"\/"b))"\/"(a"\/"
b) by A68,A69,YELLOW_3:3;
f.(p,u) <= (d.(p',y)"\/"d.(y,x))"\/"(a"\/"b) by A64,A66,LATTICE3:14;
then A71: f.(p,u) <= (d.(p',y)"\/"a)"\/"(a"\/"b) by A67,A70,ORDERS_1:26;
(d.(p',y)"\/"a)"\/"(a"\/"b) =
(d.(p',y)"\/"a"\/"a)"\/"b by LATTICE3:14 .=(d.(p',y)"\/"(a"\/"a))"\/"
b by LATTICE3:14
.= (d.(p',y)"\/"a)"\/"b by YELLOW_5:1 .= (d.(p',y)"\/"b)"\/"
a by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A63,A65,A71,Def11;
suppose A72:p in A & q = {{{A}}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def11
.= f.(p,q) by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A72;
end;
A73: for p,q,u being Element of new_set A st p in B & q in A & u in A
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A; assume A74:p in B & q in A & u in A;
then reconsider q' = q, u' = u as Element of A;
per cases by A74,ENUMSET1:13;
suppose A75:p = {A} & q in A & u in A;
then A76:f.(p,q) = d.(q',x)"\/"a by Def11;
A77:f.(q,u) = d.(q',u') by Def11;
d.(u',x) <= d.(u',q') "\/" d.(q',x) by A2,Def8;
then d.(u',x) <= d.(q',u') "\/" d.(q',x) by A1,Def6;
then d.(u',x)"\/"a <= (d.(q',x)"\/"d.(q',u'))"\/"a by WAYBEL_1:3;
then d.(u',x)"\/"a <= (d.(q',x)"\/"a)"\/"d.(q',u') by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A75,A76,A77,Def11;
suppose A78:p = {{A}} & q in A & u in A;
then A79:f.(p,q) = d.(q',x)"\/"a"\/"b by Def11;
A80:f.(q,u) = d.(q',u') by Def11;
d.(u',x) <= d.(u',q') "\/" d.(q',x) by A2,Def8;
then d.(u',x) <= d.(q',u') "\/" d.(q',x) by A1,Def6;
then d.(u',x)"\/"(a"\/"b) <= (d.(q',x)"\/"d.(q',u'))"\/"(a"\/"
b) by WAYBEL_1:3;
then d.(u',x)"\/"a"\/"b <= (d.(q',x)"\/"d.(q',u'))"\/"(a"\/"
b) by LATTICE3:14;
then d.(u',x)"\/"a"\/"b <= (d.(q',x)"\/"(a"\/"b))"\/"
d.(q',u') by LATTICE3:14;
then d.(u',x)"\/"a"\/"b <= (d.(q',x)"\/"a"\/"b)"\/"d.(q',u') by LATTICE3:14
;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A78,A79,A80,Def11;
suppose A81:p = {{{A}}} & q in A & u in A;
then A82:f.(p,q) = d.(q',y)"\/"b by Def11;
A83:f.(q,u) = d.(q',u') by Def11;
d.(u',y) <= d.(u',q') "\/" d.(q',y) by A2,Def8;
then d.(u',y) <= d.(q',u') "\/" d.(q',y) by A1,Def6;
then d.(u',y)"\/"b <= (d.(q',y)"\/"d.(q',u'))"\/"b by WAYBEL_1:3;
then d.(u',y)"\/"b <= (d.(q',y)"\/"b)"\/"d.(q',u') by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A81,A82,A83,Def11;
end;
A84: for p,q,u being Element of new_set A st p in B & q in A & u in B
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A; assume A85: p in B & q in A & u in B;
then reconsider q' = q as Element of A;
per cases by A85,ENUMSET1:13;
suppose q in A & p = {A} & u = {A};
then f.(p,u) = Bottom L by Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
suppose A86:q in A & p = {A} & u = {{A}};
then A87:f.(p,u) = b by Def11;
f.(p,q) "\/" f.(q,u) = f.(p,q)"\/"(d.(q',x)"\/"a"\/"b) by A86,Def11
.= f.(p,q)"\/"(d.(q',x)"\/"(a"\/"b)) by LATTICE3:14
.= (f.(p,q)"\/"d.(q',x))"\/"(a"\/"b) by LATTICE3:14
.= ((f.(p,q)"\/"d.(q',x))"\/"a)"\/"b by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A87,YELLOW_0:22;
suppose A88:q in A & p = {A} & u = {{{A}}};
then A89:f.(p,u) = a"\/"b by Def11;
f.(p,q) "\/" f.(q,u) = (d.(q',x)"\/"a)"\/"f.(q,u) by A88,Def11
.= (d.(q',x)"\/"a)"\/"(d.(q',y)"\/"b) by A88,Def11
.= d.(q',x)"\/"(a"\/"(d.(q',y)"\/"b)) by LATTICE3:14
.= d.(q',x)"\/"(d.(q',y)"\/"(a"\/"b)) by LATTICE3:14
.= (d.(q',x)"\/"d.(q',y))"\/"(a"\/"b) by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A89,YELLOW_0:22;
suppose A90:q in A & p = {{A}} & u = {A};
then A91:f.(p,u) = b by Def11;
f.(p,q) "\/" f.(q,u) = (d.(q',x)"\/"a"\/"b)"\/"f.(q,u) by A90,Def11
.= f.(q,u)"\/"(d.(q',x)"\/"(a"\/"b)) by LATTICE3:14
.= (f.(q,u)"\/"d.(q',x))"\/"(a"\/"b) by LATTICE3:14
.= ((f.(q,u)"\/"d.(q',x))"\/"a)"\/"b by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A91,YELLOW_0:22;
suppose q in A & p = {{A}} & u = {{A}};
then f.(p,u) = Bottom L by Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
suppose A92:q in A & p = {{A}} & u = {{{A}}};
then A93:f.(p,u) = a by Def11;
f.(p,q) "\/" f.(q,u) = (d.(q',x)"\/"a"\/"b)"\/"f.(q,u) by A92,Def11
.= (a"\/"(d.(q',x)"\/"b))"\/"f.(q,u) by LATTICE3:14
.= a"\/"((d.(q',x)"\/"b)"\/"f.(q,u)) by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A93,YELLOW_0:22;
suppose A94:q in A & p = {{{A}}} & u = {A};
then A95:f.(p,u) = a"\/"b by Def11;
f.(p,q) "\/" f.(q,u) = (d.(q',y)"\/"b)"\/"f.(q,u) by A94,Def11
.= (d.(q',y)"\/"b)"\/"(d.(q',x)"\/"a) by A94,Def11
.= d.(q',y)"\/"(b"\/"(d.(q',x)"\/"a)) by LATTICE3:14
.= d.(q',y)"\/"(d.(q',x)"\/"(b"\/"a)) by LATTICE3:14
.= (d.(q',y)"\/"d.(q',x))"\/"(a"\/"b) by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A95,YELLOW_0:22;
suppose A96:q in A & p = {{{A}}} & u = {{A}};
then A97:f.(p,u) = a by Def11;
f.(p,q) "\/" f.(q,u) = f.(p,q)"\/"(d.(q',x)"\/"a"\/"b) by A96,Def11
.= f.(p,q)"\/"(d.(q',x)"\/"(a"\/"b)) by LATTICE3:14
.= (f.(p,q)"\/"d.(q',x))"\/"(a"\/"b) by LATTICE3:14
.= ((f.(p,q)"\/"d.(q',x))"\/"b)"\/"a by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A97,YELLOW_0:22;
suppose q in A & p = {{{A}}} & u = {{{A}}};
then f.(p,u) = Bottom L by Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
end;
A98: for p,q,u being Element of new_set A st p in B & q in B & u in A
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A; assume A99: p in B & q in B & u in A;
then reconsider u' = u as Element of A;
per cases by A99,ENUMSET1:13;
suppose A100:u in A & q = {A} & p = {A};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/"
f.(q,u) by Def11 .= f.(p,u) by A100,WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u);
suppose A101:u in A & q = {A} & p = {{A}};
then f.(p,q)"\/"f.(q,u) = b"\/"f.(q,u) by Def11 .= d.(u',x)"\/"a"\/"
b by A101,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A101,Def11;
suppose A102:u in A & q = {A} & p = {{{A}}};
then A103:f.(p,u) = d.(u',y)"\/"b by Def11;
d.(u',y) <= d.(u',x)"\/"d.(x,y) by A2,Def8;
then A104:d.(u',y)"\/"b <= (d.(u',x)"\/"d.(x,y))"\/"b by WAYBEL_1:3;
A105:(d.(u',x)"\/"d.(x,y))"\/"b = (d.(u',x)"\/"b)"\/"d.(x,y) by LATTICE3:14;
d.(u',x)"\/"b <= d.(u',x)"\/"b;
then (d.(u',x)"\/"b)"\/"d.(x,y) <= (d.(u',x)"\/"b)"\/"(a"\/"
b) by A3,YELLOW_3:3;
then A106:f.(p,u) <= (d.(u',x)"\/"b)"\/"(a"\/"b) by A103,A104,A105,ORDERS_1:26;
b"\/"(a"\/"b) = (b"\/"b)"\/"a by LATTICE3:14
.= b"\/"a by YELLOW_5:1 .= b"\/"(a"\/"a) by YELLOW_5:1
.= a"\/"(a"\/"b) by LATTICE3:14;
then (d.(u',x)"\/"b)"\/"(a"\/"b) = d.(u',x)"\/"(a"\/"(a"\/"
b)) by LATTICE3:14 .=
(a"\/"b)"\/"(d.(u',x)"\/"a) by LATTICE3:14 .= f.(p,q)"\/"(d.(u',x)"\/"
a) by A102,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A102,A106,Def11;
suppose A107:u in A & q = {{A}} & p = {A};
then f.(p,q)"\/"f.(q,u) = b"\/"f.(q,u) by Def11 .= b"\/"(d.(u',x)"\/"a"\/"
b) by A107,Def11
.= b"\/"(b"\/"f.(p,u)) by A107,Def11
.= (b"\/"b)"\/"f.(p,u) by LATTICE3:14 .= b"\/"f.(p,u) by YELLOW_5:1;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:22;
suppose A108:u in A & q = {{A}} & p = {{A}};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/"
f.(q,u) by Def11 .= f.(p,u) by A108,WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u);
suppose A109:u in A & q = {{A}} & p = {{{A}}};
then A110:f.(p,u) = d.(u',y)"\/"b by Def11;
d.(u',y) <= d.(u',x)"\/"d.(x,y) by A2,Def8;
then A111:d.(u',y)"\/"b <= (d.(u',x)"\/"d.(x,y))"\/"b by WAYBEL_1:3;
A112:(d.(u',x)"\/"d.(x,y))"\/"b = (d.(u',x)"\/"b)"\/"d.(x,y) by LATTICE3:14;
A113:b"\/"(a"\/"b) = (b"\/"b)"\/"a by LATTICE3:14
.= b"\/"a by YELLOW_5:1 .= b"\/"(a"\/"a) by YELLOW_5:1
.= (a"\/"b)"\/"a by LATTICE3:14;
d.(u',x)"\/"b <= d.(u',x)"\/"b;
then (d.(u',x)"\/"b)"\/"d.(x,y) <= (d.(u',x)"\/"b)"\/"(a"\/"
b) by A3,YELLOW_3:3;
then A114:f.(p,u) <= (d.(u',x)"\/"b)"\/"(a"\/"b) by A110,A111,A112,ORDERS_1:26;
(d.(u',x)"\/"b)"\/"(a"\/"b) = d.(u',x)"\/"((a"\/"b)"\/"a) by A113,LATTICE3
:14 .= (d.(u',x)"\/"(a"\/"b))"\/"a by LATTICE3:14
.= (d.(u',x)"\/"a"\/"b)"\/"a by LATTICE3:14
.= f.(p,q)"\/"(d.(u',x)"\/"a"\/"b) by A109,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A109,A114,Def11;
suppose A115:u in A & q = {{{A}}} & p = {A};
then A116:f.(p,u) = d.(u',x)"\/"a by Def11;
d.(u',x) <= d.(u',y)"\/"d.(y,x) by A2,Def8;
then A117:d.(u',x)"\/"a <= (d.(u',y)"\/"d.(y,x))"\/"a by WAYBEL_1:3;
A118:(d.(u',y)"\/"d.(y,x))"\/"a = d.(y,x)"\/"(d.(u',y)"\/"a) by LATTICE3:14
.= (a"\/"d.(u',y))"\/"d.(x,y) by A1,Def6;
A119:a"\/"(a"\/"b) = (a"\/"a)"\/"b by LATTICE3:14 .= a"\/"b by YELLOW_5:1
.= a"\/"(b"\/"b) by YELLOW_5:1 .= b"\/"(a"\/"b) by LATTICE3:14;
a"\/"d.(u',y) <= a"\/"d.(u',y);
then (a"\/"d.(u',y))"\/"d.(x,y) <= (a"\/"d.(u',y))"\/"(a"\/"
b) by A3,YELLOW_3:3;
then A120:f.(p,u) <= (a"\/"d.(u',y))"\/"(a"\/"b) by A116,A117,A118,ORDERS_1:26;
(a"\/"d.(u',y))"\/"(a"\/"b) = d.(u',y)"\/"(a"\/"(a"\/"b)) by LATTICE3:14
.= (d.(u',y)"\/"b)"\/"(a"\/"b) by A119,LATTICE3:14
.= f.(p,q)"\/"(d.(u',y)"\/"b) by A115,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A115,A120,Def11;
suppose A121:u in A & q = {{{A}}} & p = {{A}};
then A122:f.(p,u) = d.(u',x)"\/"a"\/"b by Def11 .= d.(u',x)"\/"(a"\/"
b) by LATTICE3:14;
d.(u',x) <= d.(u',y)"\/"d.(y,x) by A2,Def8;
then A123:d.(u',x)"\/"(a"\/"b) <= (d.(u',y)"\/"d.(y,x))"\/"(a"\/"b) by WAYBEL_1
:3;
A124:(d.(u',y)"\/"d.(y,x))"\/"(a"\/"b) = ((a"\/"b)"\/"d.(u',y))"\/"
d.(y,x) by LATTICE3:14
.= ((a"\/"b)"\/"d.(u',y))"\/"d.(x,y) by A1,Def6;
(a"\/"b)"\/"d.(u',y) <= (a"\/"b)"\/"d.(u',y);
then A125:((a"\/"b)"\/"d.(u',y))"\/"d.(x,y) <=
((a"\/"b)"\/"d.(u',y))"\/"(a"\/"b) by A3,YELLOW_3:3;
f.(p,q)"\/"f.(q,u) = a"\/"f.(q,u) by A121,Def11 .= a"\/"(b"\/"
d.(u',y)) by A121,Def11 .= (a"\/"b)"\/"d.(u',y) by LATTICE3:14
.= ((a"\/"b)"\/"(a"\/"b))"\/"d.(u',y) by YELLOW_5:1
.= (a"\/"b)"\/"(d.(u',y)"\/"(a"\/"b)) by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A122,A123,A124,A125,ORDERS_1:26;
suppose A126:u in A & q = {{{A}}} & p = {{{A}}};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/"
f.(q,u) by Def11 .= f.(p,u) by A126,WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u);
end;
A127: for p,q,u being Element of new_set A st p in B & q in B & u in B
holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A; assume A128:p in B & q in B & u in B;
per cases by A128,ENUMSET1:13;
suppose A129: p = {A} & q = {A} & u = {A};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A129,Def11;
suppose A130: p = {A} & q = {A} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,u) by Def11
.= Bottom L"\/"b by A130,Def11 .= b by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A130,Def11;
suppose A131: p = {A} & q = {A} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,u) by Def11
.= Bottom
L"\/"(a"\/"b) by A131,Def11 .= a"\/"b by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A131,Def11;
suppose A132: p = {A} & q = {{A}} & u = {A};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A132,Def11;
suppose A133: p = {A} & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = b"\/"f.(q,u) by Def11 .= Bottom L"\/"b by A133,
Def11
.= b by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A133,Def11;
suppose A134: p = {A} & q = {{A}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = b"\/"f.(q,u) by Def11 .= a"\/"b by A134,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A134,Def11;
suppose A135: p = {A} & q = {{{A}}} & u = {A};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A135,Def11;
suppose A136: p = {A} & q = {{{A}}} & u = {{A}};
then A137:f.(p,u) = b by Def11;
f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by A136,Def11 .= (b"\/"a)"\/"
a by A136,Def11 .= b"\/"(a"\/"a) by LATTICE3:14
.= b"\/"a by YELLOW_5:1;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A137,YELLOW_0:22;
suppose A138: p = {A} & q = {{{A}}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by Def11 .= Bottom L"\/"(a
"\/"
b) by A138,Def11
.= a"\/"b by WAYBEL_1:4 .= f.(p,q) by A138,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A138;
suppose A139: p = {{A}} & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = b"\/" f.(q,u) by Def11 .= Bottom L"\/"b by A139,
Def11
.= b by WAYBEL_1:4 .= f.(p,q) by A139,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A139;
suppose A140: p = {{A}} & q = {A} & u = {{A}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A140,Def11;
suppose A141: p = {{A}} & q = {A} & u = {{{A}}};
then A142:f.(p,u) = a by Def11;
f.(p,q) "\/" f.(q,u) = b"\/" f.(q,u) by A141,Def11 .= b"\/"(b"\/"
a) by A141,Def11
.= (b"\/"b)"\/"a by LATTICE3:14
.= b"\/"a by YELLOW_5:1;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A142,YELLOW_0:22;
suppose A143: p = {{A}} & q = {{A}} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def11
.= Bottom L"\/"b by A143,Def11 .= b by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A143,Def11;
suppose A144: p = {{A}} & q = {{A}} & u = {{A}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A144,Def11;
suppose A145: p = {{A}} & q = {{A}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def11
.= Bottom L"\/"a by A145,Def11 .= a by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A145,Def11;
suppose A146: p = {{A}} & q = {{{A}}} & u = {A};
then A147:f.(p,u) = b by Def11;
f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by A146,Def11 .= a"\/"(a"\/"
b) by A146,Def11
.= (a"\/"a)"\/"b by LATTICE3:14 .= a"\/"b by YELLOW_5:1;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A147,YELLOW_0:22;
suppose A148: p = {{A}} & q = {{{A}}} & u = {{A}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A148,Def11;
suppose A149: p = {{A}} & q = {{{A}}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def11 .= Bottom L"\/"a by A149,
Def11
.= a by WAYBEL_1:4 .= f.(p,q) by A149,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A149;
suppose A150: p = {{{A}}} & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by Def11 .= Bottom L"\/"(a
"\/"
b) by A150,Def11
.= a"\/"b by WAYBEL_1:4 .= f.(p,q) by A150,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A150;
suppose A151: p = {{{A}}} & q = {A} & u = {{A}};
then A152:f.(p,u) = a by Def11;
f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by A151,Def11 .= (a"\/"b)"\/"
b by A151,Def11
.= a"\/"(b"\/"b) by LATTICE3:14 .= a"\/"b by YELLOW_5:1;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u)by A152,YELLOW_0:22;
suppose A153: p = {{{A}}} & q = {A} & u = {{{A}}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A153,Def11;
suppose A154: p = {{{A}}} & q = {{A}} & u = {A};
then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def11 .= a"\/"b by A154,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A154,Def11;
suppose A155: p = {{{A}}} & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def11 .= Bottom L"\/"a by A155,
Def11
.= a by WAYBEL_1:4 .= f.(p,q) by A155,Def11;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A155;
suppose A156: p = {{{A}}} & q = {{A}} & u = {{{A}}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A156,Def11;
suppose A157: p = {{{A}}} & q = {{{A}}} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def11
.= Bottom
L"\/"(a"\/"b) by A157,Def11 .= a"\/"b by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A157,Def11;
suppose A158: p = {{{A}}} & q = {{{A}}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def11
.= Bottom L"\/"a by A158,Def11 .= a by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A158,Def11;
suppose A159: p = {{{A}}} & q = {{{A}}} & u = {{{A}}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A159,Def11;
end;
for p,q,u being Element of new_set A holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
p in new_set A & q in new_set A & u in new_set A;
then A160: p in A \/ B & q in A \/ B & u in A \/ B by Def10;
per cases by A160,XBOOLE_0:def 2;
suppose p in A & q in A & u in A;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A4;
suppose p in A & q in A & u in B;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A7;
suppose p in A & q in B & u in A;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A21;
suppose p in A & q in B & u in B;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A38;
suppose p in B & q in A & u in A;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A73;
suppose p in B & q in A & u in B;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A84;
suppose p in B & q in B & u in A;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A98;
suppose p in B & q in B & u in B;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A127;
end;
hence f is u.t.i. by Def8;
end;
theorem Th21:
for A be set holds A c= new_set A
proof let A be set;
A c= A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_1:7;
hence thesis by Def10;
end;
theorem Th22:
for d be BiFunction of A,L
for q be Element of [:A,A,the carrier of L,the carrier of L:]
holds d c= new_bi_fun(d,q)
proof
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set g = new_bi_fun(d,q);
A1: dom d = [:A,A:] & dom g = [:new_set A,new_set A:] by FUNCT_2:def 1;
A c= new_set A by Th21;
then A2: dom d c= dom g by A1,ZFMISC_1:119;
for z being set st z in dom d holds d.z = g.z
proof let z be set; assume
A3: z in dom d;
then consider x,y such that
A4: [x,y] = z by ZFMISC_1:102;
reconsider x' = x, y' = y as Element of A by A3,A4,ZFMISC_1:106;
d.[x,y] = d.(x',y') by BINOP_1:def 1 .= g.(x',y') by Def11
.= g.[x,y] by BINOP_1:def 1;
hence d.z = g.z by A4;
end;
hence d c= new_bi_fun(d,q) by A2,GRFUNC_1:8;
end;
definition let A,L; let d be BiFunction of A,L;
func DistEsti(d) -> Cardinal means :Def12:
it,{ [x,y,a,b] where x is Element of A, y is Element of A,
a is Element of L, b is Element of L: d.(x,y) <= a"\/"b} are_equipotent;
existence
proof
set D = { [x,y,a,b] where x is Element of A, y is Element of A,
a is Element of L, b is Element of L: d.(x,y) <= a"\/"b};
take Card D;
thus Card D,D are_equipotent by CARD_1:def 5;
end;
uniqueness
proof
set D = { [x,y,a,b] where x is Element of A, y is Element of A,
a is Element of L, b is Element of L: d.(x,y) <= a"\/"b};
let c1,c2 be Cardinal such that
A1: c1,D are_equipotent and
A2: c2,D are_equipotent;
c1,c2 are_equipotent by A1,A2,WELLORD2:22;
hence c1 = c2 by CARD_1:8;
end;
end;
theorem Th23:
for d be distance_function of A,L holds DistEsti(d) <> {}
proof
let d be distance_function of A,L;
set X = { [x,y,a,b] where x is Element of A, y is Element of A,
a is Element of L, b is Element of L: d.(x,y) <= a"\/"b};
consider x' being Element of A;
consider z being set such that
A1: z = [x',x',Bottom L,Bottom L];
d.(x',x') = Bottom L by Def7 .= Bottom L "\/" Bottom L by YELLOW_5:1;
then A2: z in X by A1;
DistEsti(d),X are_equipotent by Def12;
hence DistEsti(d) <> {} by A2,CARD_1:46;
end;
reserve T,L1,LL for T-Sequence, O,O1,O2,O3,C for Ordinal;
definition let A; let O;
func ConsecutiveSet(A,O) means :Def13:
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_set 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
deffunc C(Ordinal,set) = new_set $2;
deffunc D(Ordinal,T-Sequence) = union rng $2;
thus (ex x,L1 st x = last L1 & dom L1 = succ O & L1.{} = A &
(for C being Ordinal st succ C in succ O
holds L1.succ C = C(C,L1.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L1.C = D(C,L1|C) ) &
for x1,x2 being set st
(ex L1 st x1 = last L1 & dom L1 = succ O & L1.{} = A &
(for C st succ C in succ O holds L1.succ C = C(C,L1.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L1.C = D(C,L1|C) ) &
(ex L1 st x2 = last L1 & dom L1 = succ O & L1.{} = A &
(for C st succ C in succ O holds L1.succ C = C(C,L1.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L1.C = D(C,L1|C) )
holds x1 = x2 from TS_Def;
end;
end;
theorem Th24:
ConsecutiveSet(A,{}) = A
proof
deffunc U(Ordinal,set) = new_set $2;
deffunc V(Ordinal,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveSet(A,$1);
A1: for O being Ordinal, x being set holds
x = F(O) iff
ex L0 being T-Sequence st x = last L0 & dom L0 = succ O &
L0.{} = A &
(for C being Ordinal st succ C in succ O holds L0.succ C = U(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = V(C,L0|C) by Def13;
thus F({}) = A from TS_Result0(A1);
end;
theorem Th25:
ConsecutiveSet(A,succ O) = new_set ConsecutiveSet(A,O)
proof
deffunc U(Ordinal,set) = new_set $2;
deffunc V(Ordinal,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveSet(A,$1);
A1: for O being Ordinal, It being set holds It = F(O) iff
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 = U(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = V(C,L0|C) by Def13;
for O holds F(succ O) = U(O,F(O)) from TS_ResultS(A1);
hence thesis;
end;
theorem Th26:
O <> {} & O is_limit_ordinal & dom T = O &
(for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveSet(A,O1))
implies ConsecutiveSet(A,O) = union rng T
proof
deffunc U(Ordinal,set) = new_set $2;
deffunc V(Ordinal,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveSet(A,$1);
assume that
A1: O <> {} & O is_limit_ordinal and
A2: dom T = O and
A3: for O1 being Ordinal st O1 in O holds T.O1 = F(O1);
A4: for O being Ordinal, x being set holds x = F(O) iff
ex L0 being T-Sequence st x = last L0 & dom L0 = succ O &
L0.{} = A &
(for C being Ordinal st succ C in succ O holds L0.succ C = U(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = V(C,L0|C) by Def13;
thus F(O) = V(O,T) from TS_ResultL(A4,A1,A2,A3);
end;
definition let A; let O;
cluster ConsecutiveSet(A,O) -> non empty;
coherence proof
defpred X[Ordinal] means ConsecutiveSet(A,$1) is non empty;
A1: X[{}] by Th24;
A2: for O st X[O] holds X[succ O]
proof let O1; assume ConsecutiveSet(A,O1) is non empty;
ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th25;
hence ConsecutiveSet(A,succ O1) is non empty;
end;
A3: for O st O <> {} & O is_limit_ordinal &
for B being Ordinal st B in O holds X[B] holds X[O]
proof let O1; assume
A4: O1 <> {} & O1 is_limit_ordinal &
for O2 st O2 in O1 holds ConsecutiveSet(A,O2) is non empty;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ls being T-Sequence such that
A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds
Ls.O2 = U(O2) from TS_Lambda;
A6: ConsecutiveSet(A,O1) = union rng Ls by A4,A5,Th26;
A7: {} in O1 by A4,ORDINAL3:10;
then Ls.{} = ConsecutiveSet(A,{}) by A5 .= A by Th24;
then A in rng Ls by A5,A7,FUNCT_1:def 5;
then A8: A c= ConsecutiveSet(A,O1) by A6,ZFMISC_1:92;
consider x being set such that A9:x in A by XBOOLE_0:def 1;
thus ConsecutiveSet(A,O1) is non empty by A8,A9;
end;
for O holds X[O] from Ordinal_Ind(A1,A2,A3);
hence thesis;
end;
end;
theorem Th27:
A c= ConsecutiveSet(A,O)
proof
defpred X[Ordinal] means A c= ConsecutiveSet(A,$1);
A1: X[{}] by Th24;
A2: for O1 st X[O1] holds X[succ O1]
proof
let O1; assume
A3: A c= ConsecutiveSet(A,O1);
ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th25;
then ConsecutiveSet(A,O1) c= ConsecutiveSet(A,succ O1) by Th21;
hence A c= ConsecutiveSet(A,succ O1) by A3,XBOOLE_1:1;
end;
A4: for O2 st O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds X[O1] holds X[O2]
proof
let O2; assume
A5: O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds A c= ConsecutiveSet(A,O1);
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ls being T-Sequence such that
A6: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A7: ConsecutiveSet(A,O2) = union rng Ls by A5,A6,Th26;
A8: {} in O2 by A5,ORDINAL3:10;
then Ls.{} = ConsecutiveSet(A,{}) by A6 .= A by Th24;
then A in rng Ls by A6,A8,FUNCT_1:def 5;
hence A c= ConsecutiveSet(A,O2) by A7,ZFMISC_1:92;
end;
for O holds X[O] from Ordinal_Ind(A1,A2,A4);
hence thesis;
end;
definition let A,L; 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 is Element of A, y is Element of A,
a is Element of L, b is Element of L: d.(x,y) <= a"\/"b};
existence
proof
set X = {[x,y,a,b] where x is Element of A, y is Element of A,
a is Element of L, b is Element of L: d.(x,y) <= a"\/"b};
Card X,X are_equipotent by CARD_1:def 5;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = Card X and
A3: rng f = X by WELLORD2:def 4;
reconsider f as T-Sequence by A2,ORDINAL1:def 7;
rng f c= [:A,A,the carrier of L,the carrier of L:]
proof
let z be set; assume
z in rng f;
then consider x,y being Element of A, a,b being Element of L such that
A4: z = [x,y,a,b] & d.(x,y) <= a"\/"b by A3;
thus z in [:A,A,the carrier of L,the carrier of L:] by A4;
end;
then reconsider f as T-Sequence of
[:A,A,the carrier of L,the carrier of L:] by ORDINAL1:def 8;
take f;
thus dom f is Cardinal by A2;
thus f is one-to-one by A1;
thus rng f = X by A3;
end;
end;
definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d;
let O;
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
proof
q.O in rng q by A1,FUNCT_1:def 5;
then q.O in {[x,y,a,b] where x is Element of A, y is Element of A,
a is Element of L, b is Element of L: d.(x,y) <= a"\/"b} by Def14;
then consider x,y be Element of A, a,b be Element of L such that
A2: q.O = [x,y,a,b] & d.(x,y) <= a"\/"b;
A3: x in A & y in A;
A c= ConsecutiveSet(A,O) by Th27;
then reconsider x,y as Element of ConsecutiveSet(A,O) by A3;
reconsider a,b as Element of L;
reconsider z = [x,y,a,b] as Element of
[:ConsecutiveSet(A,O),ConsecutiveSet(A,O),
the carrier of L,the carrier of L:];
z = q.O by A2;
hence thesis;
end;
end;
theorem Th28:
for d being BiFunction of A,L, q being QuadrSeq of d holds
O in DistEsti(d) iff O in dom q
proof
let d be BiFunction of A,L;
let q be QuadrSeq of d;
DistEsti(d),{[x,y,a,b] where x is Element of A, y is Element of A,
a is Element of L, b is Element of L: d.(x,y) <= a"\/"b} are_equipotent
by Def12;
then A1: DistEsti(d),rng q are_equipotent by Def14;
q is one-to-one by Def14;
then dom q,rng q are_equipotent by WELLORD2:def 4;
then A2: DistEsti(d),dom q are_equipotent by A1,WELLORD2:22;
reconsider M = DistEsti(d) as Cardinal;
reconsider N = dom q as Cardinal by Def14;
A3: M = N by A2,CARD_1:8;
hence O in DistEsti(d) implies O in dom q;
assume O in dom q;
hence O in DistEsti(d) by A3;
end;
definition let A,L;
let z be set;
assume
A1: z is BiFunction of A,L;
func BiFun(z,A,L) -> BiFunction of A,L equals :Def16:
z;
coherence by A1;
end;
definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d;
let O;
func ConsecutiveDelta(q,O) 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
proof
deffunc C(Ordinal,set) =
new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q,$1));
deffunc D(Ordinal,T-Sequence) = union rng $2;
thus (ex x,L1 st x = last L1 & dom L1 = succ O & L1.{} = d &
(for C being Ordinal st succ C in succ O holds L1.succ C = C(C,L1.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L1.C = D(C,L1|C) ) &
for x1,x2 being set st
(ex L1 st x1 = last L1 & dom L1 = succ O & L1.{} = d &
(for C st succ C in succ O holds L1.succ C = C(C,L1.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L1.C = D(C,L1|C) ) &
(ex L1 st x2 = last L1 & dom L1 = succ O & L1.{} = d &
(for C st succ C in succ O holds L1.succ C = C(C,L1.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L1.C = D(C,L1|C) )
holds x1 = x2 from TS_Def;
end;
end;
theorem Th29:
for d being BiFunction of A,L for q being QuadrSeq of d
holds ConsecutiveDelta(q,{}) = d
proof let d be BiFunction of A,L, q be QuadrSeq of d;
deffunc C(Ordinal,set)
= new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q,$1));
deffunc D(Ordinal,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveDelta(q,$1);
A1: for O being Ordinal, It being set holds It = F(O) iff
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 = C(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def17;
thus F({}) = d from TS_Result0(A1);
end;
theorem Th30:
for d be BiFunction of A,L for q being QuadrSeq of d holds
ConsecutiveDelta(q,succ O) = new_bi_fun(BiFun(ConsecutiveDelta(q,O),
ConsecutiveSet(A,O),L),Quadr(q,O))
proof
let d be BiFunction of A,L; let q be QuadrSeq of d;
deffunc C(Ordinal,set)
= new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q,$1));
deffunc D(Ordinal,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveDelta(q,$1);
A1: for O being Ordinal, It being set holds It = F(O) iff
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 = C(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def17;
for O holds F(succ O) = C(O,F(O)) from TS_ResultS(A1);
hence thesis;
end;
theorem Th31:
for d be BiFunction of A,L for q being QuadrSeq of d holds
O <> {} & O is_limit_ordinal & dom T = O &
(for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveDelta(q,O1))
implies ConsecutiveDelta(q,O) = union rng T
proof
let d be BiFunction of A,L; let q be QuadrSeq of d;
deffunc C(Ordinal,set)
= new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q,$1));
deffunc D(Ordinal,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveDelta(q,$1);
assume that
A1: O <> {} & O is_limit_ordinal and
A2: dom T = O and
A3: for O1 being Ordinal st O1 in O holds T.O1 = F(O1);
A4: for O being Ordinal, It being set holds It = F(O) iff
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 = C(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def17;
thus F(O) = D(O,T) from TS_ResultL(A4,A1,A2,A3);
end;
theorem Th32:
O1 c= O2 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2)
proof
defpred X[Ordinal] means O1 c= $1 implies
ConsecutiveSet(A,O1) c= ConsecutiveSet(A,$1);
A1: X[{}] by XBOOLE_1:3;
A2: for O2 st X[O2] holds X[succ O2]
proof
let O2; assume
A3: O1 c= O2 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2);
assume
A4: O1 c= succ O2;
per cases;
suppose O1 = succ O2;
hence ConsecutiveSet(A,O1) c= ConsecutiveSet(A,succ O2);
suppose O1 <> succ O2;
then O1 c< succ O2 by A4,XBOOLE_0:def 8;
then A5: O1 in succ O2 by ORDINAL1:21;
ConsecutiveSet(A,O2) c= new_set ConsecutiveSet(A,O2) by Th21;
then ConsecutiveSet(A,O1) c=
new_set ConsecutiveSet(A,O2) by A3,A5,ORDINAL1:34,XBOOLE_1:1;
hence ConsecutiveSet(A,O1) c= ConsecutiveSet(A,succ O2) by Th25;
end;
A6: for O2 st O2 <> {} & O2 is_limit_ordinal &
for O3 st O3 in O2 holds X[O3] holds X[O2]
proof
let O2; assume
A7: O2 <> {} & O2 is_limit_ordinal &
for O3 st O3 in O2 holds O1 c= O3 implies
ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O3);
assume
A8: O1 c= O2;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider L being T-Sequence such that
A9: dom L = O2 & for O3 being Ordinal st O3 in O2 holds
L.O3 = U(O3) from TS_Lambda;
A10: ConsecutiveSet(A,O2) = union rng L by A7,A9,Th26;
per cases;
suppose O1 = O2;
hence ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2);
suppose O1 <> O2;
then O1 c< O2 by A8,XBOOLE_0:def 8;
then A11: O1 in O2 by ORDINAL1:21;
then A12: L.O1 = ConsecutiveSet(A,O1) by A9;
L.O1 in rng L by A9,A11,FUNCT_1:def 5;
hence ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2)
by A10,A12,ZFMISC_1:92;
end;
for O2 holds X[O2] from Ordinal_Ind(A1,A2,A6);
hence thesis;
end;
theorem Th33:
for d be BiFunction of A,L for q being QuadrSeq of d
holds ConsecutiveDelta(q,O) is BiFunction of ConsecutiveSet(A,O),L
proof
let d be BiFunction of A,L; let q be QuadrSeq of d;
defpred Y[Ordinal] means
ConsecutiveDelta(q,$1) is BiFunction of ConsecutiveSet(A,$1),L;
A1: Y[{}]
proof
ConsecutiveDelta(q,{}) = d & ConsecutiveSet(A,{}) = A by Th24,Th29;
hence ConsecutiveDelta(q,{}) is BiFunction of ConsecutiveSet(A,{}),L;
end;
A2: for O1 st Y[O1] holds Y[succ O1]
proof
let O1; assume
ConsecutiveDelta(q,O1) is BiFunction of ConsecutiveSet(A,O1),L;
then reconsider CD = ConsecutiveDelta(q,O1) as
BiFunction of ConsecutiveSet(A,O1),L;
X: ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th25;
ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30
.= new_bi_fun(CD,Quadr(q,O1)) by Def16;
hence ConsecutiveDelta(q,succ O1) is
BiFunction of ConsecutiveSet(A,succ O1),L by X;
end;
A3: for O1 st O1 <> {} & O1 is_limit_ordinal &
for O2 st O2 in O1 holds Y[O2] holds Y[O1]
proof
let O1; assume
A4: O1 <> {} & O1 is_limit_ordinal &
for O2 st O2 in O1 holds
ConsecutiveDelta(q,O2) is BiFunction of ConsecutiveSet(A,O2),L;
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
consider Ls being T-Sequence such that
A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds
Ls.O2 = U(O2) from TS_Lambda;
A6: ConsecutiveDelta(q,O1) = union rng Ls by A4,A5,Th31;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ts being T-Sequence such that
A7: dom Ts = O1 & for O2 being Ordinal st O2 in O1 holds
Ts.O2 = U(O2) from TS_Lambda;
set CS = ConsecutiveSet(A,O1),
Y = the carrier of L,
X = [:ConsecutiveSet(A,O1),ConsecutiveSet(A,O1):],
f = union rng Ls;
A8: for O,O2 st O c= O2 & O2 in dom Ls holds Ls.O c= Ls.O2
proof let O;
defpred X[Ordinal] means
O c= $1 & $1 in dom Ls implies Ls.O c= Ls.$1;
A9: X[{}] by XBOOLE_1:3;
A10: for O2 st X[O2] holds X[succ O2]
proof
let O2; assume
A11: O c= O2 & O2 in dom Ls implies Ls.O c= Ls.O2;
assume that
A12: O c= succ O2 and
A13: succ O2 in dom Ls;
per cases;
suppose O = succ O2;
hence Ls.O c= Ls.succ O2;
suppose O <> succ O2;
then O c< succ O2 by A12,XBOOLE_0:def 8;
then A14: O in succ O2 by ORDINAL1:21;
A15: O2 in succ O2 by ORDINAL1:10;
then A16: O2 in dom Ls by A13,ORDINAL1:19;
then reconsider cd2 = ConsecutiveDelta(q,O2) as
BiFunction of ConsecutiveSet(A,O2),L by A4,A5;
Ls.succ O2 = ConsecutiveDelta(q,succ O2) by A5,A13
.= new_bi_fun(BiFun(ConsecutiveDelta(q,O2),
ConsecutiveSet(A,O2),L),Quadr(q,O2)) by Th30
.= new_bi_fun(cd2,Quadr(q,O2)) by Def16;
then ConsecutiveDelta(q,O2) c= Ls.succ O2 by Th22;
then Ls.O2 c= Ls.succ O2 by A5,A16;
hence Ls.O c= Ls.succ O2 by A11,A13,A14,A15,ORDINAL1:19,34,XBOOLE_1:1
;
end;
A17: for O2 st O2 <> {} & O2 is_limit_ordinal &
for O3 st O3 in O2 holds X[O3] holds X[O2]
proof
let O2; assume that
A18: O2 <> {} & O2 is_limit_ordinal and
for O3 st O3 in O2 holds O c= O3 & O3 in dom Ls implies Ls.O c= Ls.O3;
assume that
A19: O c= O2 and
A20: O2 in dom Ls;
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
consider Lt being T-Sequence such that
A21: dom Lt = O2 & for O3 being Ordinal st O3 in O2 holds
Lt.O3 = U(O3) from TS_Lambda;
A22:Ls.O2 = ConsecutiveDelta(q,O2) by A5,A20 .= union rng Lt by A18,A21,Th31;
per cases;
suppose O = O2;
hence Ls.O c= Ls.O2;
suppose O <> O2;
then O c< O2 by A19,XBOOLE_0:def 8;
then A23: O in O2 by ORDINAL1:21;
then O in O1 by A5,A20,ORDINAL1:19;
then Ls.O = ConsecutiveDelta(q,O) by A5 .= Lt.O by A21,A23;
then Ls.O in rng Lt by A21,A23,FUNCT_1:def 5;
hence Ls.O c= Ls.O2 by A22,ZFMISC_1:92;
end;
thus for O2 holds X[O2] from Ordinal_Ind(A9,A10,A17);
end;
for x,y being set st x in rng Ls & y in rng Ls holds x,y are_c=-comparable
proof
let x,y be set; assume
A24: x in rng Ls & y in rng Ls;
then consider o1 being set such that
A25: o1 in dom Ls & Ls.o1 = x by FUNCT_1:def 5;
consider o2 being set such that
A26: o2 in dom Ls & Ls.o2 = y by A24,FUNCT_1:def 5;
reconsider o1' = o1, o2' = o2 as Ordinal by A25,A26,ORDINAL1:23;
o1' c= o2' or o2' c= o1';
then x c= y or y c= x by A8,A25,A26;
hence thesis by XBOOLE_0:def 9;
end;
then A27: rng Ls is c=-linear by ORDINAL1:def 9;
rng Ls c= PFuncs(X,Y)
proof
let z be set; assume
z in rng Ls;
then consider o being set such that
A28: o in dom Ls & z = Ls.o by FUNCT_1:def 5;
reconsider o as Ordinal by A28,ORDINAL1:23;
Ls.o = ConsecutiveDelta(q,o) by A5,A28;
then reconsider h = Ls.o as
BiFunction of ConsecutiveSet(A,o),L by A4,A5,A28;
A29: dom h = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):] by FUNCT_2:def 1;
A30: rng h c= Y;
o c= O1 by A5,A28,ORDINAL1:def 2;
then ConsecutiveSet(A,o) c= ConsecutiveSet(A,O1) by Th32;
then dom h c= X by A29,ZFMISC_1:119;
hence z in PFuncs(X,Y) by A28,A30,PARTFUN1:def 5;
end;
then f in PFuncs(X,Y) by A27,HAHNBAN:13;
then consider g being Function such that
A31: f = g & dom g c= X & rng g c= Y by PARTFUN1:def 5;
reconsider f as Function by A31;
Ls is Function-yielding
proof
let x be set; assume
A32: x in dom Ls;
then reconsider o = x as Ordinal by ORDINAL1:23;
Ls.o = ConsecutiveDelta(q,o) by A5,A32;
hence Ls.x is Function by A4,A5,A32;
end;
then reconsider LsF = Ls as Function-yielding Function;
A33: dom f = union rng doms LsF by Th1;
reconsider o1 = O1 as non empty Ordinal by A4;
set YY = { [:ConsecutiveSet(A,O2),ConsecutiveSet(A,O2):]
where O2 is Element of o1 : not contradiction };
A34: rng doms Ls = YY
proof
thus rng doms Ls c= YY
proof
let Z be set;
assume Z in rng doms Ls;
then consider o being set such that
A35: o in dom doms Ls & Z = (doms Ls).o by FUNCT_1:def 5;
A36: o in dom LsF by A35,EXTENS_1:3;
then reconsider o' = o as Element of o1 by A5;
Ls.o' = ConsecutiveDelta(q,o') by A5;
then reconsider ls = Ls.o' as
BiFunction of ConsecutiveSet(A,o'),L by A4;
Z = dom ls by A35,A36,FUNCT_6:31
.= [:ConsecutiveSet(A,o'),ConsecutiveSet(A,o'):]
by FUNCT_2:def 1;
hence Z in YY;
end;
let Z be set;
assume Z in YY;
then consider o being Element of o1 such that
A37: Z = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):];
o in dom LsF by A5;
then A38: o in dom doms LsF by EXTENS_1:3;
Ls.o = ConsecutiveDelta(q,o) by A5;
then reconsider ls = Ls.o as
BiFunction of ConsecutiveSet(A,o),L by A4;
Z = dom ls by A37,FUNCT_2:def 1 .= (doms Ls).o by A5,FUNCT_6:31;
hence Z in rng doms Ls by A38,FUNCT_1:def 5;
end;
{} in O1 by A4,ORDINAL3:10;
then reconsider RTs = rng Ts as non empty set by A7,FUNCT_1:12;
for x,y being set st x in RTs & y in RTs holds x,y are_c=-comparable
proof
let x,y be set; assume
A39: x in RTs & y in RTs;
then consider o1 being set such that
A40: o1 in dom Ts & Ts.o1 = x by FUNCT_1:def 5;
consider o2 being set such that
A41: o2 in dom Ts & Ts.o2 = y by A39,FUNCT_1:def 5;
reconsider o1' = o1, o2' = o2 as Ordinal by A40,A41,ORDINAL1:23;
A42: Ts.o1' = ConsecutiveSet(A,o1') by A7,A40;
A43: Ts.o2' = ConsecutiveSet(A,o2') by A7,A41;
o1' c= o2' or o2' c= o1';
then x c= y or y c= x by A40,A41,A42,A43,Th32;
hence thesis by XBOOLE_0:def 9;
end;
then A44: RTs is c=-linear by ORDINAL1:def 9;
A45: YY = { [:a,a:] where a is Element of RTs : a in RTs }
proof
set XX = { [:a,a:] where a is Element of RTs : a in RTs };
thus YY c= XX
proof
let Z be set; assume Z in YY;
then consider o being Element of o1 such that
A46: Z = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):];
Ts.o = ConsecutiveSet(A,o) by A7;
then reconsider CoS = ConsecutiveSet(A,o)
as Element of RTs by A7,FUNCT_1:def 5;
Z = [:CoS,CoS:] by A46;
hence Z in XX;
end;
let Z be set; assume Z in XX;
then consider a being Element of RTs such that
A47: Z = [:a,a:] & a in RTs;
consider o being set such that
A48: o in dom Ts & a = Ts.o by FUNCT_1:def 5;
reconsider o' = o as Ordinal by A48,ORDINAL1:23;
A49: a = ConsecutiveSet(A,o') by A7,A48;
consider O being Element of o1 such that
A50: O = o' by A7,A48;
thus Z in YY by A47,A49,A50;
end;
X = [:union rng Ts, ConsecutiveSet(A,O1):] by A4,A7,Th26
.= [:union RTs, union RTs :] by A4,A7,Th26
.= dom f by A33,A34,A44,A45,Th3;
hence ConsecutiveDelta(q,O1) is BiFunction of CS,L
by A6,A31,FUNCT_2:def 1,RELSET_1:11;
end;
for O holds Y[O] from Ordinal_Ind(A1,A2,A3);
hence thesis;
end;
definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d;
let O;
redefine func ConsecutiveDelta(q,O) -> BiFunction of ConsecutiveSet(A,O),L;
coherence by Th33;
end;
theorem Th34:
for d be BiFunction of A,L for q being QuadrSeq of d holds
d c= ConsecutiveDelta(q,O)
proof
let d be BiFunction of A,L; let q be QuadrSeq of d;
defpred X[Ordinal] means d c= ConsecutiveDelta(q,$1);
A1: X[{}] by Th29;
A2: for O1 st X[O1] holds X[succ O1]
proof
let O1; assume
A3: d c= ConsecutiveDelta(q,O1);
ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30
.= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def16;
then ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,succ O1) by Th22;
hence d c= ConsecutiveDelta(q,succ O1) by A3,XBOOLE_1:1;
end;
A4: for O2 st O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds X[O1] holds X[O2]
proof
let O2; assume
A5: O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds d c= ConsecutiveDelta(q,O1);
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
consider Ls being T-Sequence such that
A6: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A7: ConsecutiveDelta(q,O2) = union rng Ls by A5,A6,Th31;
A8: {} in O2 by A5,ORDINAL3:10;
then Ls.{} = ConsecutiveDelta(q,{}) by A6 .= d by Th29;
then d in rng Ls by A6,A8,FUNCT_1:def 5;
hence d c= ConsecutiveDelta(q,O2) by A7,ZFMISC_1:92;
end;
for O holds X[O] from Ordinal_Ind(A1,A2,A4);
hence thesis;
end;
theorem Th35:
for d being BiFunction of A,L for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2)
proof
let d be BiFunction of A,L; let q be QuadrSeq of d;
defpred X[Ordinal] means
O1 c= $1 implies ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,$1);
A1: X[{}] by XBOOLE_1:3;
A2: for O2 st X[O2] holds X[succ O2]
proof
let O2; assume
A3: O1 c= O2 implies ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2);
assume
A4: O1 c= succ O2;
per cases;
suppose O1 = succ O2;
hence ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,succ O2);
suppose O1 <> succ O2;
then O1 c< succ O2 by A4,XBOOLE_0:def 8;
then A5: O1 in succ O2 by ORDINAL1:21;
ConsecutiveDelta(q,succ O2)
= new_bi_fun(BiFun(ConsecutiveDelta(q,O2),
ConsecutiveSet(A,O2),L),Quadr(q,O2)) by Th30
.= new_bi_fun(ConsecutiveDelta(q,O2),Quadr(q,O2)) by Def16;
then ConsecutiveDelta(q,O2) c= ConsecutiveDelta(q,succ O2) by Th22;
hence ConsecutiveDelta(q,O1) c=
ConsecutiveDelta(q,succ O2) by A3,A5,ORDINAL1:34,XBOOLE_1:1;
end;
A6: for O2 st O2 <> {} & O2 is_limit_ordinal &
for O3 st O3 in O2 holds X[O3] holds X[O2]
proof
let O2; assume
A7: O2 <> {} & O2 is_limit_ordinal &
for O3 st O3 in O2 holds O1 c= O3 implies
ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O3);
assume
A8: O1 c= O2;
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
consider L being T-Sequence such that
A9: dom L = O2 & for O3 being Ordinal st O3 in O2 holds
L.O3 = U(O3) from TS_Lambda;
A10: ConsecutiveDelta(q,O2) = union rng L by A7,A9,Th31;
per cases;
suppose O1 = O2;
hence ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2);
suppose O1 <> O2;
then O1 c< O2 by A8,XBOOLE_0:def 8;
then A11: O1 in O2 by ORDINAL1:21;
then A12: L.O1 = ConsecutiveDelta(q,O1) by A9;
L.O1 in rng L by A9,A11,FUNCT_1:def 5;
hence ConsecutiveDelta(q,O1) c=
ConsecutiveDelta(q,O2) by A10,A12,ZFMISC_1:92;
end;
for O2 holds X[O2] from Ordinal_Ind(A1,A2,A6);
hence thesis;
end;
theorem Th36:
for d be BiFunction of A,L st d is zeroed
for q being QuadrSeq of d holds ConsecutiveDelta(q,O) is zeroed
proof
let d be BiFunction of A,L; assume
A1: d is zeroed;
let q be QuadrSeq of d;
defpred X[Ordinal] means ConsecutiveDelta(q,$1) is zeroed;
A2: X[{}]
proof
let z be Element of ConsecutiveSet(A,{});
reconsider z' = z as Element of A by Th24;
thus ConsecutiveDelta(q,{}).(z,z) = d.(z',z') by Th29 .= Bottom L by A1,Def7
;
end;
A3: for O1 st X[O1] holds X[succ O1]
proof
let O1; assume ConsecutiveDelta(q,O1) is zeroed;
then A4:new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is zeroed by Th18;
let z be Element of ConsecutiveSet(A,succ O1);
reconsider z' = z as Element of new_set ConsecutiveSet(A,O1) by Th25;
ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30
.= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def16;
hence ConsecutiveDelta(q,succ O1).(z,z) =
new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)).(z',z') .= Bottom
L by A4,Def7;
end;
A5: for O2 st O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds X[O1] holds X[O2]
proof
let O2; assume
A6: O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds ConsecutiveDelta(q,O1) is zeroed;
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
consider Ls being T-Sequence such that
A7: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A8: ConsecutiveDelta(q,O2) = union rng Ls by A6,A7,Th31;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ts being T-Sequence such that
A9: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds
Ts.O1 = U(O1) from TS_Lambda;
A10: ConsecutiveSet(A,O2) = union rng Ts by A6,A9,Th26;
set CS = ConsecutiveSet(A,O2);
reconsider f = union rng Ls as BiFunction of CS,L by A8;
f is zeroed
proof
let x be Element of CS;
consider y being set such that
A11: x in y & y in rng Ts by A10,TARSKI:def 4;
consider o being set such that
A12: o in dom Ts & y = Ts.o by A11,FUNCT_1:def 5;
reconsider o as Ordinal by A12,ORDINAL1:23;
A13: x in ConsecutiveSet(A,o) by A9,A11,A12;
A14: Ls.o = ConsecutiveDelta(q,o) by A7,A9,A12;
then reconsider h = Ls.o as BiFunction of ConsecutiveSet(A,o),L;
A15: h is zeroed
proof
let z be Element of ConsecutiveSet(A,o);
A16: ConsecutiveDelta(q,o) is zeroed by A6,A9,A12;
thus h.(z,z) = ConsecutiveDelta(q,o).(z,z) by A7,A9,A12
.= Bottom L by A16,Def7;
end;
ConsecutiveDelta(q,o) in rng Ls by A7,A9,A12,A14,FUNCT_1:def 5;
then A17: h c= f by A14,ZFMISC_1:92;
reconsider x' = x as Element of ConsecutiveSet(A,o) by A9,A11,A12;
dom h = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):]
by FUNCT_2:def 1;
then A18: [x,x] in dom h by A13,ZFMISC_1:106;
thus f.(x,x) = f.[x,x] by BINOP_1:def 1
.= h.[x,x] by A17,A18,GRFUNC_1:8 .= h.(x',x') by BINOP_1:def 1
.= Bottom L by A15,Def7;
end;
hence ConsecutiveDelta(q,O2) is zeroed by A6,A7,Th31;
end;
for O holds X[O] from Ordinal_Ind(A2,A3,A5);
hence thesis;
end;
theorem Th37:
for d be BiFunction of A,L st d is symmetric
for q being QuadrSeq of d holds ConsecutiveDelta(q,O) is symmetric
proof
let d be BiFunction of A,L; assume
A1: d is symmetric;
let q be QuadrSeq of d;
defpred X[Ordinal] means ConsecutiveDelta(q,$1) is symmetric;
A2: X[{}]
proof
let x,y be Element of ConsecutiveSet(A,{});
reconsider x' = x, y' = y as Element of A by Th24;
thus ConsecutiveDelta(q,{}).(x,y) = d.(x',y') by Th29 .= d.(y',x') by A1,Def6
.= ConsecutiveDelta(q,{}).(y,x) by Th29;
end;
A3: for O1 st X[O1] holds X[succ O1]
proof
let O1; assume
ConsecutiveDelta(q,O1) is symmetric;
then A4:new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is symmetric by Th19;
let x,y be Element of ConsecutiveSet(A,succ O1);
reconsider x'=x, y'=y as Element of new_set ConsecutiveSet(A,O1) by Th25;
A5:ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30
.= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def16;
hence ConsecutiveDelta(q,succ O1).(x,y) =
new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)).(y',x') by A4,Def6
.= ConsecutiveDelta(q,succ O1).(y,x) by A5;
end;
A6: for O2 st O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds X[O1] holds X[O2]
proof
let O2; assume
A7: O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds ConsecutiveDelta(q,O1) is symmetric;
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
consider Ls being T-Sequence such that
A8: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A9: ConsecutiveDelta(q,O2) = union rng Ls by A7,A8,Th31;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ts being T-Sequence such that
A10: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds
Ts.O1 = U(O1) from TS_Lambda;
A11: ConsecutiveSet(A,O2) = union rng Ts by A7,A10,Th26;
set CS = ConsecutiveSet(A,O2);
reconsider f = union rng Ls as BiFunction of CS,L by A9;
f is symmetric
proof
let x,y be Element of CS;
consider x1 being set such that
A12: x in x1 & x1 in rng Ts by A11,TARSKI:def 4;
consider o1 being set such that
A13: o1 in dom Ts & x1 = Ts.o1 by A12,FUNCT_1:def 5;
consider y1 being set such that
A14: y in y1 & y1 in rng Ts by A11,TARSKI:def 4;
consider o2 being set such that
A15: o2 in dom Ts & y1 = Ts.o2 by A14,FUNCT_1:def 5;
reconsider o1,o2 as Ordinal by A13,A15,ORDINAL1:23;
A16: x in ConsecutiveSet(A,o1) by A10,A12,A13;
A17: y in ConsecutiveSet(A,o2) by A10,A14,A15;
A18: Ls.o1 = ConsecutiveDelta(q,o1) by A8,A10,A13;
then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet(A,o1),L;
A19: h1 is symmetric
proof
let x,y be Element of ConsecutiveSet(A,o1);
A20: ConsecutiveDelta(q,o1) is symmetric by A7,A10,A13;
thus h1.(x,y) = ConsecutiveDelta(q,o1).(x,y) by A8,A10,A13 .=
ConsecutiveDelta(q,o1).(y,x) by A20,Def6 .= h1.(y,x) by A8,A10,A13;
end;
A21: dom h1 = [:ConsecutiveSet(A,o1),ConsecutiveSet(A,o1):]
by FUNCT_2:def 1;
A22: Ls.o2 = ConsecutiveDelta(q,o2) by A8,A10,A15;
then reconsider h2 = Ls.o2 as
BiFunction of ConsecutiveSet(A,o2),L;
A23: h2 is symmetric
proof
let x,y be Element of ConsecutiveSet(A,o2);
A24: ConsecutiveDelta(q,o2) is symmetric by A7,A10,A15;
thus h2.(x,y) = ConsecutiveDelta(q,o2).(x,y) by A8,A10,A15 .=
ConsecutiveDelta(q,o2).(y,x) by A24,Def6 .= h2.(y,x) by A8,A10,A15;
end;
A25: dom h2 = [:ConsecutiveSet(A,o2),ConsecutiveSet(A,o2):] by FUNCT_2:def 1;
per cases;
suppose o1 c= o2;
then A26: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by Th32;
then reconsider x'=x, y'=y as
Element of ConsecutiveSet(A,o2) by A10,A14,A15,A16;
ConsecutiveDelta(q,o2) in rng Ls by A8,A10,A15,A22,FUNCT_1:def 5
;
then A27: h2 c= f by A22,ZFMISC_1:92;
A28: [x,y] in dom h2 & [y,x] in dom h2 by A16,A17,A25,A26,ZFMISC_1:106;
thus f.(x,y) = f.[x,y] by BINOP_1:def 1
.= h2.[x,y] by A27,A28,GRFUNC_1:8 .= h2.(x',y') by BINOP_1:def 1
.= h2.(y',x') by A23,Def6 .= h2.[y,x] by BINOP_1:def 1
.= f.[y,x] by A27,A28,GRFUNC_1:8 .= f.(y,x) by BINOP_1:def 1;
suppose o2 c= o1;
then A29: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o1) by Th32;
then reconsider x'=x, y'=y as
Element of ConsecutiveSet(A,o1) by A10,A12,A13,A17;
ConsecutiveDelta(q,o1) in rng Ls by A8,A10,A13,A18,FUNCT_1:def 5
;
then A30: h1 c= f by A18,ZFMISC_1:92;
A31: [x,y] in dom h1 & [y,x] in dom h1 by A16,A17,A21,A29,ZFMISC_1:106;
thus f.(x,y) = f.[x,y] by BINOP_1:def 1
.= h1.[x,y] by A30,A31,GRFUNC_1:8 .= h1.(x',y') by BINOP_1:def 1
.= h1.(y',x') by A19,Def6 .= h1.[y,x] by BINOP_1:def 1
.= f.[y,x] by A30,A31,GRFUNC_1:8 .= f.(y,x) by BINOP_1:def 1;
end;
hence ConsecutiveDelta(q,O2) is symmetric by A7,A8,Th31;
end;
for O holds X[O] from Ordinal_Ind(A2,A3,A6);
hence thesis;
end;
theorem Th38:
for d be BiFunction of A,L st d is symmetric u.t.i.
for q being QuadrSeq of d st O c= DistEsti(d) holds
ConsecutiveDelta(q,O) is u.t.i.
proof
let d be BiFunction of A,L; assume that
A1: d is symmetric and
A2: d is u.t.i.;
let q be QuadrSeq of d;
defpred X[Ordinal] means
$1 c= DistEsti(d) implies ConsecutiveDelta(q,$1) is u.t.i.;
A3: X[{}]
proof
assume {} c= DistEsti(d);
let x,y,z be Element of ConsecutiveSet(A,{});
reconsider x' = x, y' = y, z' = z as Element of A by Th24;
A4:ConsecutiveDelta(q,{}) = d by Th29;
d.(x',z') <= d.(x',y') "\/" d.(y',z') by A2,Def8;
hence ConsecutiveDelta(q,{}).(x,z) <=
ConsecutiveDelta(q,{}).(x,y) "\/" ConsecutiveDelta(q,{}).(y,z) by A4;
end;
A5: for O1 st X[O1] holds X[succ O1]
proof
let O1; assume that
A6: O1 c= DistEsti(d) implies ConsecutiveDelta(q,O1) is u.t.i. and
A7: succ O1 c= DistEsti(d);
A8: O1 in DistEsti(d) by A7,ORDINAL1:33;
A9: ConsecutiveDelta(q,O1) is symmetric by A1,Th37;
let x,y,z be Element of ConsecutiveSet(A,succ O1);
set f = new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1));
reconsider x' = x, y' = y, z' = z as
Element of new_set ConsecutiveSet(A,O1) by Th25;
A10: O1 in dom q by A8,Th28;
then q.O1 in rng q by FUNCT_1:def 5;
then q.O1 in {[u,v,a',b'] where u is Element of A, v is Element of A,
a' is Element of L, b' is Element of L: d.(u,v) <=
a'"\/"b'} by Def14;
then consider u,v be Element of A, a',b' be Element of L such that
A11: q.O1 = [u,v,a',b'] & d.(u,v) <= a'"\/"b';
set X = Quadr(q,O1)`1, Y = Quadr(q,O1)`2;
reconsider a = Quadr(q,O1)`3, b = Quadr(q,O1)`4 as Element of L
;
A12: Quadr(q,O1) = [u,v,a',b'] by A10,A11,Def15;
then A13: u = X by MCART_1:def 8;
A14: v = Y by A12,MCART_1:def 9;
A15: a' = a by A12,MCART_1:def 10;
A16: b' = b by A12,MCART_1:def 11;
A17: dom d = [:A,A:] by FUNCT_2:def 1;
A18: d c= ConsecutiveDelta(q,O1) by Th34;
d.(u,v) = d.[u,v] by BINOP_1:def 1
.= ConsecutiveDelta(q,O1).[X,Y] by A13,A14,A17,A18,GRFUNC_1:8
.= ConsecutiveDelta(q,O1).(X,Y) by BINOP_1:def 1;
then A19:new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is u.t.i.
by A6,A8,A9,A11,A15,A16,Th20,ORDINAL1:def
2;
A20: ConsecutiveDelta(q,succ O1) =
new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th30 .=
new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def16;
f.(x',z') <= f.(x',y') "\/" f.(y',z') by A19,Def8;
hence ConsecutiveDelta(q,succ O1).(x,z) <= ConsecutiveDelta(q,succ O1).(x,y)
"\/" ConsecutiveDelta(q,succ O1).(y,z) by A20;
end;
A21: for O2 st O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds X[O1] holds X[O2]
proof
let O2; assume that
A22: O2 <> {} & O2 is_limit_ordinal &
for O1 st O1 in O2 holds
(O1 c= DistEsti(d) implies ConsecutiveDelta(q,O1) is u.t.i.) and
A23: O2 c= DistEsti(d);
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
consider Ls being T-Sequence such that
A24: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A25: ConsecutiveDelta(q,O2) = union rng Ls by A22,A24,Th31;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ts being T-Sequence such that
A26: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds
Ts.O1 = U(O1) from TS_Lambda;
A27: ConsecutiveSet(A,O2) = union rng Ts by A22,A26,Th26;
set CS = ConsecutiveSet(A,O2);
reconsider f = union rng Ls as BiFunction of CS,L by A25;
f is u.t.i.
proof
let x,y,z be Element of CS;
consider X being set such that
A28: x in X & X in rng Ts by A27,TARSKI:def 4;
consider o1 being set such that
A29: o1 in dom Ts & X = Ts.o1 by A28,FUNCT_1:def 5;
consider Y being set such that
A30: y in Y & Y in rng Ts by A27,TARSKI:def 4;
consider o2 being set such that
A31: o2 in dom Ts & Y = Ts.o2 by A30,FUNCT_1:def 5;
consider Z being set such that
A32: z in Z & Z in rng Ts by A27,TARSKI:def 4;
consider o3 being set such that
A33: o3 in dom Ts & Z = Ts.o3 by A32,FUNCT_1:def 5;
reconsider o1,o2,o3 as Ordinal by A29,A31,A33,ORDINAL1:23;
A34: x in ConsecutiveSet(A,o1) by A26,A28,A29;
A35: y in ConsecutiveSet(A,o2) by A26,A30,A31;
A36: z in ConsecutiveSet(A,o3) by A26,A32,A33;
A37: Ls.o1 = ConsecutiveDelta(q,o1) by A24,A26,A29;
then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet(A,o1),L;
A38: h1 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet(A,o1);
A39:ConsecutiveDelta(q,o1) = h1 by A24,A26,A29;
o1 c= DistEsti(d) by A23,A26,A29,ORDINAL1:def 2;
then ConsecutiveDelta(q,o1) is u.t.i. by A22,A26,A29;
hence h1.(x,z) <= h1.(x,y) "\/" h1.(y,z) by A39,Def8;
end;
A40: dom h1 = [:ConsecutiveSet(A,o1),ConsecutiveSet(A,o1):]
by FUNCT_2:def 1;
A41: Ls.o2 = ConsecutiveDelta(q,o2) by A24,A26,A31;
then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet(A,o2),L;
A42: h2 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet(A,o2);
A43:ConsecutiveDelta(q,o2) = h2 by A24,A26,A31;
o2 c= DistEsti(d) by A23,A26,A31,ORDINAL1:def 2;
then ConsecutiveDelta(q,o2) is u.t.i. by A22,A26,A31;
hence h2.(x,z) <= h2.(x,y) "\/" h2.(y,z) by A43,Def8;
end;
A44: dom h2 = [:ConsecutiveSet(A,o2),ConsecutiveSet(A,o2):]
by FUNCT_2:def 1;
A45: Ls.o3 = ConsecutiveDelta(q,o3) by A24,A26,A33;
then reconsider h3 = Ls.o3 as
BiFunction of ConsecutiveSet(A,o3),L;
A46: h3 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet(A,o3);
A47:ConsecutiveDelta(q,o3) = h3 by A24,A26,A33;
o3 c= DistEsti(d) by A23,A26,A33,ORDINAL1:def 2;
then ConsecutiveDelta(q,o3) is u.t.i. by A22,A26,A33;
hence h3.(x,z) <= h3.(x,y) "\/" h3.(y,z) by A47,Def8;
end;
A48: dom h3 = [:ConsecutiveSet(A,o3),ConsecutiveSet(A,o3):]
by FUNCT_2:def 1;
per cases;
suppose A49: o1 c= o3;
then A50: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o3) by Th32;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose o2 c= o3;
then A51: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o3) by Th32;
then reconsider y' = y as Element of ConsecutiveSet(A,o3) by A35;
reconsider x' = x as Element of ConsecutiveSet(A,o3) by A34,A50;
reconsider z' = z as Element of ConsecutiveSet(A,o3) by A26,A32,A33;
ConsecutiveDelta(q,o3) in rng Ls by A24,A26,A33,A45,FUNCT_1:def 5
;
then A52: h3 c= f by A45,ZFMISC_1:92;
A53: [x,y] in dom h3 by A34,A35,A48,A50,A51,ZFMISC_1:106;
A54: [y,z] in dom h3 by A35,A36,A48,A51,ZFMISC_1:106;
A55: [x,z] in dom h3 by A34,A36,A48,A50,ZFMISC_1:106;
A56: f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h3.[x,y] by A52,A53,GRFUNC_1:8
.= h3.(x',y') by BINOP_1:def 1;
A57: f.(y,z) = f.[y,z] by BINOP_1:def 1 .= h3.[y,z] by A52,A54,GRFUNC_1:8
.= h3.(y',z') by BINOP_1:def 1;
f.(x,z) = f.[x,z] by BINOP_1:def 1 .= h3.[x,z] by A52,A55,GRFUNC_1:8
.= h3.(x',z') by BINOP_1:def 1;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A46,A56,A57,Def8;
suppose o3 c= o2;
then A58: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o2) by Th32;
then reconsider z' = z as Element of ConsecutiveSet(A,o2) by A36;
ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o3) by A49,Th32;
then A59: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by A58,XBOOLE_1:1;
then reconsider x' = x as Element of ConsecutiveSet(A,o2) by A34;
reconsider y' = y as Element of ConsecutiveSet(A,o2) by A26,A30,A31;
ConsecutiveDelta(q,o2) in rng Ls by A24,A26,A31,A41,FUNCT_1:def 5
;
then A60: h2 c= f by A41,ZFMISC_1:92;
A61: [x,y] in dom h2 by A34,A35,A44,A59,ZFMISC_1:106;
A62: [y,z] in dom h2 by A35,A36,A44,A58,ZFMISC_1:106;
A63: [x,z] in dom h2 by A34,A36,A44,A58,A59,ZFMISC_1:106;
A64: f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h2.[x,y] by A60,A61,GRFUNC_1:8
.= h2.(x',y') by BINOP_1:def 1;
A65: f.(y,z) = f.[y,z] by BINOP_1:def 1 .= h2.[y,z] by A60,A62,GRFUNC_1:8
.= h2.(y',z') by BINOP_1:def 1;
f.(x,z) = f.[x,z] by BINOP_1:def 1 .= h2.[x,z] by A60,A63,GRFUNC_1:8
.= h2.(x',z') by BINOP_1:def 1;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A42,A64,A65,Def8;
end;
suppose A66: o3 c= o1;
then A67: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o1) by Th32;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose o1 c= o2;
then A68: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by Th32;
then reconsider x' = x as Element of ConsecutiveSet(A,o2) by A34;
ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o1) by A66,Th32;
then A69: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o2) by A68,XBOOLE_1:1;
then reconsider z' = z as Element of ConsecutiveSet(A,o2) by A36;
reconsider y' = y as Element of ConsecutiveSet(A,o2) by A26,A30,A31;
ConsecutiveDelta(q,o2) in rng Ls by A24,A26,A31,A41,FUNCT_1:def 5
;
then A70: h2 c= f by A41,ZFMISC_1:92;
A71: [x,y] in dom h2 by A34,A35,A44,A68,ZFMISC_1:106;
A72: [y,z] in dom h2 by A35,A36,A44,A69,ZFMISC_1:106;
A73: [x,z] in dom h2 by A34,A36,A44,A68,A69,ZFMISC_1:106;
A74: f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h2.[x,y] by A70,A71,GRFUNC_1:8
.= h2.(x',y') by BINOP_1:def 1;
A75: f.(y,z) = f.[y,z] by BINOP_1:def 1 .= h2.[y,z] by A70,A72,GRFUNC_1:8
.= h2.(y',z') by BINOP_1:def 1;
f.(x,z) = f.[x,z] by BINOP_1:def 1 .= h2.[x,z] by A70,A73,GRFUNC_1:8
.= h2.(x',z') by BINOP_1:def 1;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A42,A74,A75,Def8;
suppose o2 c= o1;
then A76: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o1) by Th32;
then reconsider y' = y as Element of ConsecutiveSet(A,o1) by A35;
reconsider z' = z as Element of ConsecutiveSet(A,o1) by A36,A67;
reconsider x' = x as Element of ConsecutiveSet(A,o1) by A26,A28,A29;
ConsecutiveDelta(q,o1) in rng Ls by A24,A26,A29,A37,FUNCT_1:def 5
;
then A77: h1 c= f by A37,ZFMISC_1:92;
A78: [x,y] in dom h1 by A34,A35,A40,A76,ZFMISC_1:106;
A79: [y,z] in dom h1 by A35,A36,A40,A67,A76,ZFMISC_1:106;
A80: [x,z] in dom h1 by A34,A36,A40,A67,ZFMISC_1:106;
A81: f.(x,y) = f.[x,y] by BINOP_1:def 1 .= h1.[x,y] by A77,A78,GRFUNC_1:8
.= h1.(x',y') by BINOP_1:def 1;
A82: f.(y,z) = f.[y,z] by BINOP_1:def 1 .= h1.[y,z] by A77,A79,GRFUNC_1:8
.= h1.(y',z') by BINOP_1:def 1;
f.(x,z) = f.[x,z] by BINOP_1:def 1 .= h1.[x,z] by A77,A80,GRFUNC_1:8
.= h1.(x',z') by BINOP_1:def 1;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A38,A81,A82,Def8;
end;
end;
hence ConsecutiveDelta(q,O2) is u.t.i. by A22,A24,Th31;
end;
for O holds X[O] from Ordinal_Ind(A3,A5,A21);
hence thesis;
end;
theorem
for d being distance_function of A,L
for q being QuadrSeq of d st O c= DistEsti(d) holds
ConsecutiveDelta(q,O) is distance_function of ConsecutiveSet(A,O),L
by Th36,Th37,Th38;
definition let A,L; let d be BiFunction of A,L;
func NextSet(d) equals :Def18:
ConsecutiveSet(A,DistEsti(d));
correctness;
end;
definition let A,L; let d be BiFunction of A,L;
cluster NextSet(d) -> non empty;
coherence proof
ConsecutiveSet(A,DistEsti(d)) is non empty;
hence thesis by Def18;
end;
end;
definition let A,L; let d be BiFunction of A,L; let q be QuadrSeq of d;
func NextDelta(q) equals :Def19:
ConsecutiveDelta(q,DistEsti(d));
correctness;
end;
definition let A,L; let d be distance_function of A,L; let q be QuadrSeq of d;
redefine func NextDelta(q) -> distance_function of NextSet(d),L;
coherence proof
A1: ConsecutiveDelta(q,DistEsti(d)) = NextDelta(q) by Def19;
ConsecutiveSet(A,DistEsti(d)) = NextSet(d) by Def18;
hence NextDelta(q) is distance_function of NextSet(d),L
by A1,Th36,Th37,Th38;
end;
end;
definition let A,L; let d be distance_function of A,L;
let Aq be non empty set, dq be distance_function of Aq,L;
pred Aq, dq is_extension_of A,d means :Def20:
ex q being QuadrSeq of d st Aq = NextSet(d) & dq = NextDelta(q);
end;
theorem Th40:
for d be distance_function of A,L
for Aq be non empty set, dq be distance_function of Aq,L
st Aq, dq is_extension_of A,d
for x,y being Element of A, a,b being Element of L st d.(x,y) <= a "\/" b
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
proof
let d be distance_function of A,L;
let Aq be non empty set, dq be distance_function of Aq,L; assume
Aq, dq is_extension_of A,d;
then consider q being QuadrSeq of d such that
A1: Aq = NextSet(d) and
A2: dq = NextDelta(q) by Def20;
let x,y be Element of A; let a,b be Element of L; assume
A3: d.(x,y) <= a "\/" b;
rng q = {[x',y',a',b'] where x' is Element of A, y' is Element of A,
a' is Element of L, b' is Element of L: d.(x',y') <=
a'"\/"b'} by Def14;
then [x,y,a,b] in rng q by A3;
then consider o being set such that
A4: o in dom q & q.o = [x,y,a,b] by FUNCT_1:def 5;
reconsider o as Ordinal by A4,ORDINAL1:23;
A5: q.o = Quadr(q,o) by A4,Def15;
then A6: x = Quadr(q,o)`1 by A4,MCART_1:78;
A7: y = Quadr(q,o)`2 by A4,A5,MCART_1:78;
A8: a = Quadr(q,o)`3 by A4,A5,MCART_1:78;
A9: b = Quadr(q,o)`4 by A4,A5,MCART_1:78;
reconsider B = ConsecutiveSet(A,o) as non empty set;
reconsider Q = Quadr(q,o)
as Element of [:B,B,the carrier of L,the carrier of L:];
reconsider cd = ConsecutiveDelta(q,o) as BiFunction of B,L;
x in A & y in A & A c= B by Th27;
then reconsider xo = x, yo = y as Element of B;
xo in B & yo in B & B c= new_set B by Th21;
then reconsider x1 = xo, y1 = yo as Element of new_set B;
A10: ConsecutiveSet(A,succ o) = new_set B by Th25;
o in DistEsti(d) by A4,Th28;
then A11: succ o c= DistEsti(d) by ORDINAL1:33;
then A12: ConsecutiveDelta(q,succ o) c= ConsecutiveDelta(q,DistEsti(d)) by Th35
;
ConsecutiveDelta(q,succ o)
= new_bi_fun(BiFun(ConsecutiveDelta(q,o),
ConsecutiveSet(A,o),L),Quadr(q,o)) by Th30
.= new_bi_fun(cd,Q) by Def16;
then A13: new_bi_fun(cd,Q) c= dq by A2,A12,Def19;
{B} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:14;
then {B} in B \/ {{B}, {{B}}, {{{B}}} } by XBOOLE_0:def 2;
then A14: {B} in new_set B by Def10;
{{B}} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:14;
then {{B}} in B \/ {{B}, {{B}}, {{{B}}} } by XBOOLE_0:def 2;
then A15: {{B}} in new_set B by Def10;
{{{B}}} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:14;
then {{{B}}} in B \/ {{B}, {{B}}, {{{B}}} } by XBOOLE_0:def 2;
then A16: {{{B}}} in new_set B by Def10;
A17: cd is zeroed by Th36;
A18: dom new_bi_fun(cd,Q) = [:new_set B,new_set B:] by FUNCT_2:def 1;
then A19: [x1,{B}] in dom new_bi_fun(cd,Q) by A14,ZFMISC_1:106;
A20: [{{B}},{{{B}}}] in dom new_bi_fun(cd,Q) by A15,A16,A18,ZFMISC_1:106;
A21: [{B},{{B}}] in dom new_bi_fun(cd,Q) by A14,A15,A18,ZFMISC_1:106;
A22: [{{{B}}},y1] in dom new_bi_fun(cd,Q) by A16,A18,ZFMISC_1:106;
new_set B c= ConsecutiveSet(A,DistEsti(d)) by A10,A11,Th32;
then reconsider z1={B},z2={{B}},z3={{{B}}} as Element of Aq by A1,A14,A15,
A16,Def18;
take z1,z2,z3;
thus dq.(x,z1) = dq.[x,z1] by BINOP_1:def 1
.= new_bi_fun(cd,Q).[x1,{B}] by A13,A19,GRFUNC_1:8
.= new_bi_fun(cd,Q).(x1,{B}) by BINOP_1:def 1
.= cd.(xo,xo)"\/"a by A6,A8,Def11 .= Bottom L"\/"
a by A17,Def7 .= a by WAYBEL_1:4;
thus dq.(z2,z3) = dq.[z2,z3] by BINOP_1:def 1
.= new_bi_fun(cd,Q).[{{B}},{{{B}}}] by A13,A20,GRFUNC_1:8
.= new_bi_fun(cd,Q).({{B}},{{{B}}}) by BINOP_1:def 1 .= a by A8,Def11;
thus dq.(z1,z2) = dq.[z1,z2] by BINOP_1:def 1
.= new_bi_fun(cd,Q).[{B},{{B}}] by A13,A21,GRFUNC_1:8
.= new_bi_fun(cd,Q).({B},{{B}}) by BINOP_1:def 1 .= b by A9,Def11;
thus dq.(z3,y) = dq.[z3,y] by BINOP_1:def 1
.= new_bi_fun(cd,Q).[{{{B}}},y1] by A13,A22,GRFUNC_1:8
.= new_bi_fun(cd,Q).({{{B}}},y1) by BINOP_1:def 1
.= cd.(yo,yo)"\/"b by A7,A9,Def11 .= Bottom L"\/"
b by A17,Def7 .= b by WAYBEL_1:4;
end;
definition let A,L; 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 Nat holds
ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, 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
proof
defpred P[set,set,set] means
(ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension_of A',d' & $2 = [A',d'] & $3 = [Aq,dq]) or
$3= 0 &
not ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension_of A',d' & $2 = [A',d'];
A1: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat; let x be set;
per cases;
suppose ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension_of A',d' & x = [A',d'];
then consider A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
A2: Aq, dq is_extension_of A',d' and
A3: x = [A',d'];
take [Aq,dq];
thus thesis by A2,A3;
suppose
A4: not ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension_of A',d' & x = [A',d'];
take 0;
thus thesis by A4;
end;
consider f being Function such that
A5: dom f = NAT and
A6: f.0 = [A,d] and
A7: for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecChoice(A1);
take f;
thus dom f = NAT by A5;
thus f.0 = [A,d] by A6;
defpred X[Nat] means ex A' being non empty set,
d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension_of A',d' &
f.$1 = [A',d'] & f.($1+1) = [Aq,dq];
ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension_of A',d' & f.0 = [A',d']
proof
take A,d;
consider q being QuadrSeq of d;
set Aq = NextSet(d);
consider dq being distance_function of Aq,L such that
A8: dq = NextDelta(q);
take Aq,dq;
thus Aq, dq is_extension_of A,d by A8,Def20;
thus f.0 = [A,d] by A6;
end;
then A9: X[0] by A7;
A10: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat; given
A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
Aq, dq is_extension_of A',d' and
f.k = [A',d'] and
A11: f.(k+1) = [Aq,dq];
ex A1 being non empty set, d1 being distance_function of A1,L,
AQ being non empty set, DQ being distance_function of AQ,L st
AQ, DQ is_extension_of A1,d1 & f.(k+1) = [A1,d1]
proof
take Aq,dq;
set AQ = NextSet(dq);
consider Q being QuadrSeq of dq;
set DQ = NextDelta(Q);
take AQ,DQ;
thus AQ, DQ is_extension_of Aq,dq by Def20;
thus f.(k+1) = [Aq,dq] by A11;
end;
hence thesis by A7;
end;
thus for k being Nat holds X[k] from Ind(A9,A10);
end;
end;
theorem Th41:
for d be distance_function of A,L for S being ExtensionSeq of A,d
for k,l being Nat st k <= l holds (S.k)`1 c= (S.l)`1
proof
let d be distance_function of A,L; let S be ExtensionSeq of A,d;
let k be Nat;
defpred X[Nat] means k <= $1 implies (S.k)`1 c= (S.$1)`1;
A1: X[0] by NAT_1:19;
A2: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat; assume that
A3: k <= i implies (S.k)`1 c= (S.i)`1 and
A4: k <= i+1;
per cases by A4,NAT_1:26;
suppose k = i+1;
hence (S.k)`1 c= (S.(i+1))`1;
suppose A5: k <= i;
consider A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
A6: Aq, dq is_extension_of A',d' and
A7: S.i = [A',d'] & S.(i+1) = [Aq,dq] by Def21;
consider q being QuadrSeq of d' such that
A8: Aq = NextSet(d') and
dq = NextDelta(q) by A6,Def20;
A9: (S.i)`1 = A' by A7,MCART_1:def 1;
A10: (S.(i+1))`1 = NextSet(d') by A7,A8,MCART_1:def 1
.= ConsecutiveSet(A',DistEsti(d')) by Def18;
(S.i)`1 c= ConsecutiveSet(A',DistEsti(d')) by A9,Th27;
hence (S.k)`1 c= (S.(i+1))`1 by A3,A5,A10,XBOOLE_1:1;
end;
thus for l being Nat holds X[l] from Ind(A1,A2);
end;
theorem Th42:
for d be distance_function of A,L for S being ExtensionSeq of A,d
for k,l being Nat st k <= l holds (S.k)`2 c= (S.l)`2
proof
let d be distance_function of A,L; let S be ExtensionSeq of A,d;
let k be Nat;
defpred X[Nat] means k <= $1 implies (S.k)`2 c= (S.$1)`2;
A1: X[0] by NAT_1:19;
A2: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat; assume that
A3: k <= i implies (S.k)`2 c= (S.i)`2 and
A4: k <= i+1;
per cases by A4,NAT_1:26;
suppose k = i+1;
hence (S.k)`2 c= (S.(i+1))`2;
suppose A5: k <= i;
consider A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
A6: Aq, dq is_extension_of A',d' and
A7: S.i = [A',d'] & S.(i+1) = [Aq,dq] by Def21;
consider q being QuadrSeq of d' such that
Aq = NextSet(d') and
A8: dq = NextDelta(q) by A6,Def20;
A9: (S.i)`2 = d' by A7,MCART_1:def 2;
A10: (S.(i+1))`2 = NextDelta(q) by A7,A8,MCART_1:def 2
.= ConsecutiveDelta(q,DistEsti(d')) by Def19;
(S.i)`2 c= ConsecutiveDelta(q,DistEsti(d')) by A9,Th34;
hence (S.k)`2 c= (S.(i+1))`2 by A3,A5,A10,XBOOLE_1:1;
end;
thus for l being Nat holds X[l] from Ind(A1,A2);
end;
definition let L;
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
proof
set A = the carrier of L;
defpred X[Element of L,Element of L,set]
means ($1 = $2 implies $3 = Bottom L) & ($1 <> $2 implies $3 = $1"\/"$2);
A1: for x,y being Element of L
ex z being Element of L st X[x,y,z]
proof
let x,y be Element of L;
per cases;
suppose A2: x = y;
take Bottom L;
thus thesis by A2;
suppose A3: x <> y;
take x"\/"y;
thus thesis by A3;
end;
consider f being Function of
[:the carrier of L,the carrier of L:],the carrier of L such that
A4: for x,y being Element of L holds X[x,y,f.[x,y]]
from FuncEx2D(A1);
A5:for x,y being Element of L holds
(x <> y implies f.(x,y) = x"\/"y) & (x = y implies f.(x,y) = Bottom L)
proof
let x,y be Element of L;
thus x <> y implies f.(x,y) = x"\/"y
proof
assume A6: x <> y;
thus f.(x,y) = f.[x,y] by BINOP_1:def 1 .= x"\/"y by A4,A6;
end;
thus x = y implies f.(x,y) = Bottom L
proof
assume A7: x = y;
thus f.(x,y) = f.[x,y] by BINOP_1:def 1 .= Bottom L by A4,A7;
end;
end;
reconsider f as BiFunction of A,L;
A8: f is zeroed
proof
let x be Element of A;
thus f.(x,x) = Bottom L by A5;
end;
A9: f is symmetric
proof
let x,y be Element of A;
reconsider x' = x, y' = y as Element of L;
per cases;
suppose x = y;
hence f.(x,y) = f.(y,x);
suppose A10: x <> y;
hence f.(x,y) = y' "\/" x' by A5
.= f.(y,x) by A5,A10;
end;
f is u.t.i.
proof
let x,y,z be Element of A;
reconsider x' = x, y' = y, z' = z as Element of L;
per cases;
suppose A11: x = z;
f.(x,y) "\/" f.(y,z) >= Bottom L by YELLOW_0:44;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A5,A11;
suppose A12: x <> z;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose A13: x = y;
x' "\/" z' >= x' "\/" z' by ORDERS_1:24;
then f.(x,z) >= x' "\/" z' by A5,A12;
then Bottom L "\/" f.(x,z) >= x' "\/" z' by WAYBEL_1:4;
then f.(x,y) "\/" f.(y,z) >= x' "\/" z' by A5,A13;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A5,A12;
suppose A14: x <> y;
(x' "\/" y') "\/" f.(y,z) >= x' "\/" z'
proof
per cases;
suppose A15: y = z;
(x' "\/" y') >= x' "\/" y' by ORDERS_1:24;
then Bottom L "\/" (x' "\/" y') >= x' "\/" z' by A15,WAYBEL_1:4
;
hence (x' "\/" y') "\/" f.(y,z) >= x' "\/" z' by A5,A15;
suppose A16: y <> z;
(x' "\/" z') "\/" y' = (x' "\/" z') "\/" (y' "\/" y') by YELLOW_5
:1
.= x' "\/" (z' "\/" (y' "\/" y')) by LATTICE3:14
.= x' "\/" (y' "\/" (y' "\/" z')) by LATTICE3:14
.= (x' "\/" y') "\/" (y' "\/"
z') by LATTICE3:14;
then (x' "\/" y') "\/" (y' "\/" z') >= x' "\/"
z' by YELLOW_0:22;
hence (x' "\/" y') "\/" f.(y,z) >= x' "\/" z' by A5,A16;
end;
then f.(x,y) "\/" f.(y,z) >= x' "\/" z' by A5,A14;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A5,A12;
end;
end;
then reconsider f as distance_function of A,L by A8,A9;
take f;
thus thesis by A5;
end;
uniqueness
proof
let f1,f2 be distance_function of the carrier of L,L such that
A17: for x,y being Element of L holds
(x <> y implies f1.(x,y) = x"\/"y) & (x = y implies f1.(x,y) = Bottom L) and
A18: for x,y being Element of L holds
(x <> y implies f2.(x,y) = x"\/"y) & (x = y implies f2.(x,y) = Bottom L);
A19: dom f1 = [:the carrier of L,the carrier of L:] by FUNCT_2:def 1
.= dom f2 by FUNCT_2:def 1;
for z being set st z in dom f1 holds f1.z = f2.z
proof
let z be set; assume A20: z in dom f1;
then consider x,y being set such that
A21: z = [x,y] by ZFMISC_1:102;
reconsider x,y as Element of L by A20,A21,ZFMISC_1:106;
per cases;
suppose A22: x = y;
thus f1.z = f1.(x,y) by A21,BINOP_1:def 1 .= Bottom L by A17,A22
.= f2.(x,y) by A18,A22 .= f2.z by A21,BINOP_1:def 1;
suppose A23: x <> y;
thus f1.z = f1.(x,y) by A21,BINOP_1:def 1 .= x"\/"y by A17,A23
.= f2.(x,y) by A18,A23 .= f2.z by A21,BINOP_1:def 1;
end;
hence f1 = f2 by A19,FUNCT_1:9;
end;
end;
theorem Th43:
BasicDF(L) is onto
proof
set X = the carrier of L, f = BasicDF(L);
for w being set st w in X ex z being set st z in [:X,X:] & w = f.z
proof
let w be set; assume
A1: w in X;
then reconsider w' = w as Element of L;
reconsider w'' = w as Element of L by A1;
per cases;
suppose A2: w = Bottom L;
take z = [w,w];
thus z in [:X,X:] by A1,ZFMISC_1:106;
thus f.z = f.(w',w') by BINOP_1:def 1.= w by A2,Def22;
suppose A3: w <> Bottom L;
take z = [Bottom L,w];
thus z in [:X,X:] by A1,ZFMISC_1:106;
thus f.z = f.(Bottom L,w') by BINOP_1:def 1
.= Bottom L "\/" w'' by A3,Def22 .= w by WAYBEL_1:4;
end;
then rng f = the carrier of L by FUNCT_2:16;
hence BasicDF(L) is onto by FUNCT_2:def 3;
end;
Lm2: now let j be Nat; assume
A1: 1 <= j & j < 5;
then j < 4+1;
then j <= 4 by NAT_1:38;
then j = 0 or j = 1 or j = 2 or j = 3 or j = 4 by CQC_THE1:5;
hence j = 1 or j = 2 or j = 3 or j = 4 by A1;
end;
Lm3: now let m be Nat; assume
A1: m in Seg 5;
then 1 <= m & m <= 5 by FINSEQ_1:3;
then m = 0 or m = 1 or m = 2 or m = 3 or m = 4 or m = 5 by CQC_THE1:6;
hence m = 1 or m = 2 or m = 3 or m = 4 or m = 5 by A1,FINSEQ_1:3;
end;
Lm4: now let A,L; let d be distance_function of A,L;
succ {} c= DistEsti(d) or DistEsti(d) in succ {} by ORDINAL1:26;
then succ {} c= DistEsti(d) or DistEsti(d) c= {} by ORDINAL1:34;
then succ {} c= DistEsti(d) or DistEsti(d) = {} by XBOOLE_1:3;
hence succ {} c= DistEsti(d) by Th23;
end;
theorem Th44:
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 Nat: not contradiction} holds
union { (S.i)`2 where i is Nat: not contradiction}
is distance_function of FS,L
proof
let S be ExtensionSeq of the carrier of L, BasicDF(L);
let FS be non empty set;
assume A1:FS = union { (S.i)`1 where i is Nat: not contradiction};
set FD = union { (S.i)`2 where i is Nat: not contradiction};
set A = the carrier of L;
(S.0)`1 in { (S.i)`1 where i is Nat: not contradiction};
then reconsider X = { (S.i)`1 where i is Nat: not contradiction}
as non empty set;
reconsider FS as non empty set;
A2: { (S.i)`2 where i is Nat: not contradiction} is c=-linear
proof
now let x,y be set; assume that
A3: x in { (S.i)`2 where i is Nat: not contradiction} and
A4: y in { (S.i)`2 where i is Nat: not contradiction};
consider k being Nat such that
A5: x = (S.k)`2 by A3;
consider l being Nat such that
A6: y = (S.l)`2 by A4;
k <= l or l <= k;
then x c= y or y c= x by A5,A6,Th42;
hence x,y are_c=-comparable by XBOOLE_0:def 9;
end; hence thesis by ORDINAL1:def 9;
end;
{ (S.i)`2 where i is Nat: not contradiction} c= PFuncs([:FS,FS:],A)
proof
let z be set;
assume z in { (S.i)`2 where i is Nat: not contradiction};
then consider j being Nat such that
A7: z = (S.j)`2;
consider A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
Aq, dq is_extension_of A',d' and
A8: S.j = [A',d'] & S.(j+1) = [Aq,dq] by Def21;
A9: z = d' by A7,A8,MCART_1:def 2;
A10: rng d' c= A;
A11: dom d' = [:A',A':] by FUNCT_2:def 1;
A' = (S.j)`1 by A8,MCART_1:def 1;
then A' in { (S.i)`1 where i is Nat: not contradiction};
then A' c= FS by A1,ZFMISC_1:92;
then dom d' c= [:FS,FS:] by A11,ZFMISC_1:119;
hence z in PFuncs([:FS,FS:],A) by A9,A10,PARTFUN1:def 5;
end;
then FD in PFuncs([:FS,FS:],A) by A2,HAHNBAN:13;
then consider g being Function such that
A12: FD = g and
dom g c= [:FS,FS:] and
A13: rng g c= A by PARTFUN1:def 5;
reconsider FD as Function by A12;
A14: X is c=-linear
proof
now let x,y be set; assume that
A15: x in X and
A16: y in X;
consider k being Nat such that
A17: x = (S.k)`1 by A15;
consider l being Nat such that
A18: y = (S.l)`1 by A16;
k <= l or l <= k;
then x c= y or y c= x by A17,A18,Th41;
hence x,y are_c=-comparable by XBOOLE_0:def 9;
end; hence thesis by ORDINAL1:def 9;
end;
defpred X[set,set] means $2 = (S.$1)`2;
A19: for x,y1,y2 being set st x in NAT & X[x,y1] & X[x,y2]
holds y1 = y2;
A20: for x being set st x in NAT ex y being set st X[x,y];
consider F being Function such that
A21: dom F = NAT and
A22: for x being set st x in NAT holds X[x,F.x] from FuncEx(A19,A20);
A23: rng F = { (S.i)`2 where i is Nat: not contradiction}
proof
thus rng F c= { (S.i)`2 where i is Nat: not contradiction}
proof
let x be set; assume x in rng F;
then consider j being set such that
A24: j in dom F & F.j = x by FUNCT_1:def 5;
reconsider j as Nat by A21,A24;
x = (S.j)`2 by A22,A24;
hence x in { (S.i)`2 where i is Nat: not contradiction};
end;
let x be set; assume
x in { (S.i)`2 where i is Nat: not contradiction};
then consider j being Nat such that
A25: x = (S.j)`2;
x = F.j by A22,A25;
hence x in rng F by A21,FUNCT_1:def 5;
end;
F is Function-yielding
proof
let x be set; assume x in dom F;
then reconsider j = x as Nat by A21;
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
A26: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def21;
(S.j)`2 = d1 by A26,MCART_1:def 2;
hence F.x is Function by A22;
end;
then reconsider F as Function-yielding Function;
set LL = { [:I,I:] where I is Element of X : I in X },
PP = { [:(S.i)`1,(S.i)`1:] where i is Nat: not contradiction };
A27: rng doms F = PP
proof
thus rng doms F c= PP
proof
let x be set; assume x in rng doms F;
then consider j being set such that
A28: j in dom doms F & x = (doms F).j by FUNCT_1:def 5;
A29: j in dom F by A28,EXTENS_1:3;
reconsider j as Nat by A21,A28,EXTENS_1:3;
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] & S.(j+1) = [Aq1,dq1] by Def21;
A31: (S.j)`2 = d1 by A30,MCART_1:def 2;
A32: (S.j)`1 = A1 by A30,MCART_1:def 1;
x = dom (F.j) by A28,A29,FUNCT_6:31 .= dom d1 by A22,A31
.= [:(S.j)`1,(S.j)`1:] by A32,FUNCT_2:def 1;
hence x in PP;
end;
let x be set; assume x in PP;
then consider j being Nat such that
A33: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
A34: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def21;
A35: (S.j)`2 = d1 by A34,MCART_1:def 2;
A36: (S.j)`1 = A1 by A34,MCART_1:def 1;
j in NAT;
then A37: j in dom doms F by A21,EXTENS_1:3;
x = dom d1 by A33,A36,FUNCT_2:def 1
.= dom (F.j) by A22,A35 .= (doms F).j by A21,FUNCT_6:31;
hence x in rng doms F by A37,FUNCT_1:def 5;
end;
LL = PP
proof
thus LL c= PP
proof
let x be set; assume x in LL;
then consider J being Element of X such that
A38:x = [:J,J:] and
A39:J in X;
consider j being Nat such that
A40:J = (S.j)`1 by A39;
thus x in PP by A38,A40;
end;
let x be set; assume x in PP;
then consider j being Nat such that
A41:x = [:(S.j)`1,(S.j)`1:];
(S.j)`1 in X;
hence x in LL by A41;
end;
then [:FS,FS:] = union rng doms F by A1,A14,A27,Th3
.= dom FD by A23,Th1;
then reconsider FD as BiFunction of FS,L
by A12,A13,FUNCT_2:def 1,RELSET_1:11;
A42: FD is zeroed
proof
let x be Element of FS;
consider y being set such that
A43: x in y & y in X by A1,TARSKI:def 4;
consider j being Nat such that
A44: y = (S.j)`1 by A43;
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
A45: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def21;
A46: (S.j)`2 = d1 by A45,MCART_1:def 2;
reconsider x' = x as Element of A1 by A43,A44,A45,MCART_1:def 1;
d1 in { (S.i)`2 where i is Nat: not contradiction} by A46;
then A47: d1 c= FD by ZFMISC_1:92;
A48: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
thus FD.(x,x) = FD.[x',x'] by BINOP_1:def 1
.= d1.[x',x'] by A47,A48,GRFUNC_1:8
.= d1.(x',x') by BINOP_1:def 1 .=Bottom L by Def7;
end;
A49: FD is symmetric
proof
let x,y be Element of FS;
consider x1 being set such that
A50: x in x1 & x1 in X by A1,TARSKI:def 4;
consider k being Nat such that
A51: x1 = (S.k)`1 by A50;
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
A52: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def21;
A53: (S.k)`2 = d1 by A52,MCART_1:def 2;
A54: (S.k)`1 = A1 by A52,MCART_1:def 1;
d1 in { (S.i)`2 where i is Nat: not contradiction} by A53;
then A55: d1 c= FD by ZFMISC_1:92;
A56: x in A1 by A50,A51,A52,MCART_1:def 1;
consider y1 being set such that
A57: y in y1 & y1 in X by A1,TARSKI:def 4;
consider l being Nat such that
A58: y1 = (S.l)`1 by A57;
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
A59: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def21;
A60: (S.l)`2 = d2 by A59,MCART_1:def 2;
A61: (S.l)`1 = A2 by A59,MCART_1:def 1;
d2 in { (S.i)`2 where i is Nat: not contradiction} by A60;
then A62: d2 c= FD by ZFMISC_1:92;
A63: y in A2 by A57,A58,A59,MCART_1:def 1;
per cases;
suppose k <= l;
then A1 c= A2 by A54,A61,Th41;
then reconsider x'=x,y'=y as Element of A2 by A56,A57,A58,A59,MCART_1:def
1;
A64: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
thus FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d2.[x',y'] by A62,A64,GRFUNC_1:8 .= d2.(x',y') by BINOP_1:def 1
.= d2.(y',x') by Def6 .= d2.[y',x'] by BINOP_1:def 1
.= FD.[y',x'] by A62,A64,GRFUNC_1:8 .= FD.(y,x) by BINOP_1:def 1;
suppose l <= k;
then A2 c= A1 by A54,A61,Th41;
then reconsider x'=x,y'=y as Element of A1 by A50,A51,A52,A63,MCART_1:def
1;
A65: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
thus FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d1.[x',y'] by A55,A65,GRFUNC_1:8 .= d1.(x',y') by BINOP_1:def 1
.= d1.(y',x') by Def6 .= d1.[y',x'] by BINOP_1:def 1
.= FD.[y',x'] by A55,A65,GRFUNC_1:8 .= FD.(y,x) by BINOP_1:def 1;
end;
FD is u.t.i.
proof
let x,y,z be Element of FS;
consider x1 being set such that
A66: x in x1 & x1 in X by A1,TARSKI:def 4;
consider k being Nat such that
A67: x1 = (S.k)`1 by A66;
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
A68: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def21;
A69: (S.k)`2 = d1 by A68,MCART_1:def 2;
A70: (S.k)`1 = A1 by A68,MCART_1:def 1;
d1 in { (S.i)`2 where i is Nat: not contradiction} by A69;
then A71: d1 c= FD by ZFMISC_1:92;
A72: x in A1 by A66,A67,A68,MCART_1:def 1;
A73: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
consider y1 being set such that
A74: y in y1 & y1 in X by A1,TARSKI:def 4;
consider l being Nat such that
A75: y1 = (S.l)`1 by A74;
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
A76: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def21;
A77: (S.l)`2 = d2 by A76,MCART_1:def 2;
A78: (S.l)`1 = A2 by A76,MCART_1:def 1;
d2 in { (S.i)`2 where i is Nat: not contradiction} by A77;
then A79: d2 c= FD by ZFMISC_1:92;
A80: y in A2 by A74,A75,A76,MCART_1:def 1;
A81: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
consider z1 being set such that
A82: z in z1 & z1 in X by A1,TARSKI:def 4;
consider n being Nat such that
A83: z1 = (S.n)`1 by A82;
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
A84: S.n = [A3,d3] & S.(n+1) = [Aq3,dq3] by Def21;
A85: (S.n)`2 = d3 by A84,MCART_1:def 2;
A86: (S.n)`1 = A3 by A84,MCART_1:def 1;
d3 in { (S.i)`2 where i is Nat: not contradiction} by A85;
then A87: d3 c= FD by ZFMISC_1:92;
A88: z in A3 by A82,A83,A84,MCART_1:def 1;
A89: dom d3 = [:A3,A3:] by FUNCT_2:def 1;
per cases;
suppose k <= l;
then A90: A1 c= A2 by A70,A78,Th41;
thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z)
proof
per cases;
suppose l <= n;
then A91: A2 c= A3 by A78,A86,Th41;
then A1 c= A3 by A90,XBOOLE_1:1;
then reconsider x' = x, y' = y, z' = z as Element of A3
by A72,A80,A82,A83,A84,A91,MCART_1:def
1;
A92: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d3.[x',y'] by A87,A89,GRFUNC_1:8
.= d3.(x',y') by BINOP_1:def 1;
A93: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1
.= d3.[y',z'] by A87,A89,GRFUNC_1:8
.= d3.(y',z') by BINOP_1:def 1;
FD.(x,z) = FD.[x',z'] by BINOP_1:def 1
.= d3.[x',z'] by A87,A89,GRFUNC_1:8
.= d3.(x',z') by BINOP_1:def 1;
hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A92,A93,Def8;
suppose n <= l;
then A3 c= A2 by A78,A86,Th41;
then reconsider x' = x, y' = y, z' = z as Element of A2
by A72,A74,A75,A76,A88,A90,MCART_1:def 1;
A94: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d2.[x',y'] by A79,A81,GRFUNC_1:8
.= d2.(x',y') by BINOP_1:def 1;
A95: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1
.= d2.[y',z'] by A79,A81,GRFUNC_1:8
.= d2.(y',z') by BINOP_1:def 1;
FD.(x,z) = FD.[x',z'] by BINOP_1:def 1
.= d2.[x',z'] by A79,A81,GRFUNC_1:8
.= d2.(x',z') by BINOP_1:def 1;
hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A94,A95,Def8;
end;
suppose l <= k;
then A96: A2 c= A1 by A70,A78,Th41;
thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z)
proof
per cases;
suppose k <= n;
then A97: A1 c= A3 by A70,A86,Th41;
then A2 c= A3 by A96,XBOOLE_1:1;
then reconsider x' = x, y' = y, z' = z as Element of A3
by A72,A80,A82,A83,A84,A97,MCART_1:def
1;
A98: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d3.[x',y'] by A87,A89,GRFUNC_1:8
.= d3.(x',y') by BINOP_1:def 1;
A99: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1
.= d3.[y',z'] by A87,A89,GRFUNC_1:8
.= d3.(y',z') by BINOP_1:def 1;
FD.(x,z) = FD.[x',z'] by BINOP_1:def 1
.= d3.[x',z'] by A87,A89,GRFUNC_1:8
.= d3.(x',z') by BINOP_1:def 1;
hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A98,A99,Def8;
suppose n <= k;
then A3 c= A1 by A70,A86,Th41;
then reconsider x' = x, y' = y, z' = z as Element of A1
by A66,A67,A68,A80,A88,A96,MCART_1:def 1;
A100: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d1.[x',y'] by A71,A73,GRFUNC_1:8
.= d1.(x',y') by BINOP_1:def 1;
A101: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1
.= d1.[y',z'] by A71,A73,GRFUNC_1:8
.= d1.(y',z') by BINOP_1:def 1;
FD.(x,z) = FD.[x',z'] by BINOP_1:def 1
.= d1.[x',z'] by A71,A73,GRFUNC_1:8
.= d1.(x',z') by BINOP_1:def 1;
hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A100,A101,Def8;
end;
end;
hence thesis by A42,A49;
end;
theorem Th45:
for S being ExtensionSeq of the carrier of L, BasicDF(L)
for FS being non empty set,
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: not contradiction} &
FD = union { (S.i)`2 where i is Nat: not contradiction} &
FD.(x,y) <= a"\/"b
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
proof
let S be ExtensionSeq of the carrier of L, BasicDF(L);
let FS be non empty set, FD be distance_function of FS,L;
let x,y be Element of FS; let a,b be Element of L; assume that
A1: FS = union { (S.i)`1 where i is Nat: not contradiction} &
FD = union { (S.i)`2 where i is Nat: not contradiction} and
A2: FD.(x,y) <= a"\/"b;
(S.0)`1 in { (S.i)`1 where i is Nat: not contradiction};
then reconsider X = { (S.i)`1 where i is Nat: not contradiction}
as non empty set;
consider x1 being set such that
A3: x in x1 & x1 in X by A1,TARSKI:def 4;
consider k being Nat such that
A4: x1 = (S.k)`1 by A3;
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
A5: Aq1, dq1 is_extension_of A1,d1 and
A6: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def21;
A7: (S.k)`2 = d1 by A6,MCART_1:def 2;
A8: (S.k)`1 = A1 by A6,MCART_1:def 1;
A9: (S.(k+1))`1 = Aq1 by A6,MCART_1:def 1;
A10: (S.(k+1))`2 = dq1 by A6,MCART_1:def 2;
d1 in { (S.i)`2 where i is Nat: not contradiction} by A7;
then A11: d1 c= FD by A1,ZFMISC_1:92;
dq1 in { (S.i)`2 where i is Nat: not contradiction} by A10;
then A12: dq1 c= FD by A1,ZFMISC_1:92;
Aq1 in { (S.i)`1 where i is Nat: not contradiction} by A9;
then A13: Aq1 c= FS by A1,ZFMISC_1:92;
A14: x in A1 by A3,A4,A6,MCART_1:def 1;
consider y1 being set such that
A15: y in y1 & y1 in X by A1,TARSKI:def 4;
consider l being Nat such that
A16: y1 = (S.l)`1 by A15;
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
A17: Aq2, dq2 is_extension_of A2,d2 and
A18: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def21;
A19: (S.l)`2 = d2 by A18,MCART_1:def 2;
A20: (S.l)`1 = A2 by A18,MCART_1:def 1;
A21: (S.(l+1))`1 = Aq2 by A18,MCART_1:def 1;
A22: (S.(l+1))`2 = dq2 by A18,MCART_1:def 2;
d2 in { (S.i)`2 where i is Nat: not contradiction} by A19;
then A23: d2 c= FD by A1,ZFMISC_1:92;
dq2 in { (S.i)`2 where i is Nat: not contradiction} by A22;
then A24: dq2 c= FD by A1,ZFMISC_1:92;
Aq2 in { (S.i)`1 where i is Nat: not contradiction} by A21;
then A25: Aq2 c= FS by A1,ZFMISC_1:92;
A26: y in A2 by A15,A16,A18,MCART_1:def 1;
per cases;
suppose k <= l;
then A1 c= A2 by A8,A20,Th41;
then reconsider x'=x,y'=y as Element of A2 by A14,A15,A16,A18,MCART_1:def
1;
A27: x' in A2 & y' in A2;
A28: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d2.[x',y'] by A23,A28,GRFUNC_1:8
.= d2.(x',y') by BINOP_1:def 1;
then consider z1,z2,z3 being Element of Aq2 such that
A29: dq2.(x,z1) = a and
A30: dq2.(z2,z3) = a and
A31: dq2.(z1,z2) = b and
A32: dq2.(z3,y) = b by A2,A17,Th40;
z1 in Aq2 & z2 in Aq2 & z3 in Aq2;
then reconsider z1' = z1, z2' = z2, z3' = z3 as Element of FS by A25;
l <= l+1 by NAT_1:29;
then A2 c= Aq2 by A20,A21,Th41;
then reconsider x'' = x',y'' = y' as Element of Aq2 by A27;
A33: dom dq2 = [:Aq2,Aq2:] by FUNCT_2:def 1;
take z1',z2',z3';
thus FD.(x,z1') = FD.[x'',z1] by BINOP_1:def 1
.= dq2.[x'',z1] by A24,A33,GRFUNC_1:8
.= a by A29,BINOP_1:def 1;
thus FD.(z2',z3') = FD.[z2,z3] by BINOP_1:def 1
.= dq2.[z2,z3] by A24,A33,GRFUNC_1:8
.= a by A30,BINOP_1:def 1;
thus FD.(z1',z2') = FD.[z1,z2] by BINOP_1:def 1
.= dq2.[z1,z2] by A24,A33,GRFUNC_1:8
.= b by A31,BINOP_1:def 1;
thus FD.(z3',y) = FD.[z3,y''] by BINOP_1:def 1
.= dq2.[z3,y''] by A24,A33,GRFUNC_1:8
.= b by A32,BINOP_1:def 1;
suppose l <= k;
then A2 c= A1 by A8,A20,Th41;
then reconsider x'=x,y'=y as Element of A1 by A3,A4,A6,A26,MCART_1:def 1;
A34: x' in A1 & y' in A1;
A35: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d1.[x',y'] by A11,A35,GRFUNC_1:8
.= d1.(x',y') by BINOP_1:def 1;
then consider z1,z2,z3 being Element of Aq1 such that
A36: dq1.(x,z1) = a and
A37: dq1.(z2,z3) = a and
A38: dq1.(z1,z2) = b and
A39: dq1.(z3,y) = b by A2,A5,Th40;
z1 in Aq1 & z2 in Aq1 & z3 in Aq1;
then reconsider z1' = z1, z2' = z2, z3' = z3 as Element of FS by A13;
k <= k+1 by NAT_1:29;
then A1 c= Aq1 by A8,A9,Th41;
then reconsider x'' = x',y'' = y' as Element of Aq1 by A34;
A40: dom dq1 = [:Aq1,Aq1:] by FUNCT_2:def 1;
take z1',z2',z3';
thus FD.(x,z1') = FD.[x'',z1] by BINOP_1:def 1 .= dq1.[x'',z1]
by A12,A40,GRFUNC_1:8 .= a by A36,BINOP_1:def 1;
thus FD.(z2',z3') = FD.[z2,z3] by BINOP_1:def 1 .= dq1.[z2,z3]
by A12,A40,GRFUNC_1:8 .= a by A37,BINOP_1:def 1;
thus FD.(z1',z2') = FD.[z1,z2] by BINOP_1:def 1 .= dq1.[z1,z2]
by A12,A40,GRFUNC_1:8 .= b by A38,BINOP_1:def 1;
thus FD.(z3',y) = FD.[z3,y''] by BINOP_1:def 1 .= dq1.[z3,y'']
by A12,A40,GRFUNC_1:8 .= b by A39,BINOP_1:def 1;
end;
theorem Th46:
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,x,y st f = alpha FD &
FS = union { (S.i)`1 where i is Nat: not contradiction} &
FD = union { (S.i)`2 where i is Nat: not contradiction} &
e1 in the carrier of Image f & e2 in the carrier of Image f &
[x,y] in e1 "\/" e2
ex F being non empty FinSequence of FS st
len F = 3+2 & x,y are_joint_by F,e1,e2
proof
let S be ExtensionSeq of the carrier of L, BasicDF(L);
let FS be non empty set;
let FD be distance_function of FS,L;
let f be Homomorphism of L,EqRelLATT FS;
let x, y be Element of FS;
let e1,e2 be Equivalence_Relation of FS,x,y; assume that
A1: f = alpha FD and
A2: FS = union { (S.i)`1 where i is Nat: not contradiction} &
FD = union { (S.i)`2 where i is Nat: not contradiction} and
A3: e1 in the carrier of Image f & e2 in the carrier of Image f and
A4: [x,y] in e1 "\/" e2;
Image f = subrelstr rng f by YELLOW_2:def 2;
then A5:the carrier of Image f = rng f by YELLOW_0:def 15;
then consider a being set such that
A6: a in dom f and
A7: e1 = f.a by A3,FUNCT_1:def 5;
consider b being set such that
A8: b in dom f and
A9: e2 = f.b by A3,A5,FUNCT_1:def 5;
reconsider a,b as Element of L by A6,A8;
field (e1 "\/" e2) = FS by EQREL_1:15;
then reconsider u = x, v = y as Element of FS by A4,RELAT_1:30;
reconsider a,b as Element of L;
consider e1' being Equivalence_Relation of FS such that
A10: e1' = f.a and
A11: for u,v being Element of FS holds [u,v] in e1' iff FD.(u,v) <= a
by A1,Def9;
consider e2' being Equivalence_Relation of FS such that
A12: e2' = f.b and
A13: for u,v being Element of FS holds [u,v] in e2' iff FD.(u,v) <= b
by A1,Def9;
consider e being Equivalence_Relation of FS such that
A14: e = f.(a"\/"b) and
A15: for u,v being Element of FS holds [u,v] in e iff FD.(u,v) <=
a"\/"b by A1,Def9;
e = f.a"\/"f.b by A14,WAYBEL_6:2
.= e1 "\/" e2 by A7,A9,Th10;
then FD.(u,v) <= a"\/"b by A4,A15;
then consider z1,z2,z3 being Element of FS such that
A16: FD.(u,z1) = a and
A17: FD.(z2,z3) = a and
A18: FD.(z1,z2) = b and
A19: FD.(z3,v) = b by A2,Th45;
defpred P[set,set] means
($1 = 1 implies $2 = u) & ($1 = 2 implies $2 = z1) &
($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = z3) &
($1 = 5 implies $2 = v);
A20: for m being Nat, w1,w2 being set st m in Seg 5 & P[m,w1] & P[m,w2]
holds w1 = w2 by Lm3;
A21: for m being Nat st m in Seg 5 ex w being set st P[m,w]
proof
let m be Nat; assume
A22:m in Seg 5;
per cases by A22,Lm3;
suppose A23: m = 1; take w = x; thus P[m,w] by A23;
suppose A24: m = 2; take w = z1; thus P[m,w] by A24;
suppose A25: m = 3; take w = z2; thus P[m,w] by A25;
suppose A26: m = 4; take w = z3; thus P[m,w] by A26;
suppose A27: m = 5; take w = y; thus P[m,w] by A27;
end;
ex p being FinSequence st dom p = Seg 5 &
for k being Nat st k in Seg 5 holds P[k,p.k] from SeqEx(A20,A21);
then consider h being FinSequence such that
A28: dom h = Seg 5 and
A29: for m being Nat st m in Seg 5 holds
(m = 1 implies h.m = u) & (m = 2 implies h.m = z1) &
(m = 3 implies h.m = z2) & (m = 4 implies h.m = z3) &
(m = 5 implies h.m = v);
Seg 5 = { n where n is Nat: 1 <= n & n <= 5 } by FINSEQ_1:def 1;
then A30: 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5;
A31: len h = 5 by A28,FINSEQ_1:def 3;
rng h c= FS
proof
let w be set; assume w in rng h;
then consider j be set such that
A32: j in dom h & w = h.j by FUNCT_1:def 5;
per cases by A28,A32,Lm3;
suppose j = 1; then h.j = u by A29,A30; hence w in FS by A32;
suppose j = 2; then h.j = z1 by A29,A30; hence w in FS by A32;
suppose j = 3; then h.j = z2 by A29,A30; hence w in FS by A32;
suppose j = 4; then h.j = z3 by A29,A30; hence w in FS by A32;
suppose j = 5; then h.j = v by A29,A30; hence w in FS by A32;
end;
then reconsider h as FinSequence of FS by FINSEQ_1:def 4;
len h <> 0 by A28,FINSEQ_1:def 3;
then reconsider h as non empty FinSequence of FS by FINSEQ_1:25;
take h;
thus len h = 3+2 by A28,FINSEQ_1:def 3;
A33: h.1 = x by A29,A30;
A34: h.(len h) = h.5 by A28,FINSEQ_1:def 3 .= y by A29,A30;
for j being Nat st 1 <= j & j < len h holds
(j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
proof
let j be Nat; assume
A35: 1 <= j & j < len h;
per cases by A31,A35,Lm2;
suppose j = 1;
then A36: 2*0+1 = j;
[u,z1] in e1' by A11,A16;
then [h.1,z1] in e1' by A29,A30;
hence (j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
by A7,A10,A29,A30,A36;
suppose j = 3;
then A37: 2*1+1 = j;
[z2,z3] in e1' by A11,A17;
then [h.3,z3] in e1' by A29,A30;
hence (j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
by A7,A10,A29,A30,A37;
suppose j = 2;
then A38: 2*1 = j;
[z1,z2] in e2' by A13,A18;
then [h.2,z2] in e2' by A29,A30;
hence (j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
by A9,A12,A29,A30,A38;
suppose j = 4;
then A39: 2*2 = j;
[z3,v] in e2' by A13,A19;
then [h.4,v] in e2' by A29,A30;
hence (j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
by A9,A12,A29,A30,A39;
end;
hence x,y are_joint_by h,e1,e2 by A33,A34,Def3;
end;
theorem
ex A being non empty set, f being Homomorphism of L,EqRelLATT A st
f is one-to-one & type_of Image f <= 3
proof
set A = the carrier of L, D = BasicDF(L);
A1: D is onto by Th43;
consider S being ExtensionSeq of A,D;
set FS = union { (S.i)`1 where i is Nat: not contradiction};
A2: S.0 = [A,D] by Def21;
then A3: (S.0)`1 = A by MCART_1:def 1;
(S.0)`1 in { (S.i)`1 where i is Nat: not contradiction};
then A4: A c= FS by A3,ZFMISC_1:92;
consider xx being set such that A5: xx in A by XBOOLE_0:def 1;
reconsider FS as non empty set by A4,A5;
reconsider FD = union { (S.i)`2 where i is Nat: not contradiction}
as distance_function of FS,L by Th44;
A6: FD is onto
proof
A7: rng D = A by A1,FUNCT_2:def 3;
for w being set st w in A ex z being set st z in [:FS,FS:] & w = FD.z
proof
let w be set; assume w in A;
then consider z being set such that
A8: z in [:A,A:] and
A9: D.z = w by A7,FUNCT_2:17;
take z;
A10: S.0 = [A,D] by Def21;
then A11: A = (S.0)`1 by MCART_1:def 1;
(S.0)`1 in { (S.i)`1 where i is Nat: not contradiction};
then A c= FS by A11,ZFMISC_1:92;
then [:A,A:] c= [:FS,FS:] by ZFMISC_1:119;
hence z in [:FS,FS:] by A8;
A12: z in dom D by A8,FUNCT_2:def 1;
A13: D = (S.0)`2 by A10,MCART_1:def 2;
(S.0)`2 in { (S.i)`2 where i is Nat: not contradiction};
then D c= FD by A13,ZFMISC_1:92;
hence w = FD.z by A9,A12,GRFUNC_1:8;
end;
then rng FD = A by FUNCT_2:16;
hence FD is onto by FUNCT_2:def 3;
end;
alpha FD is join-preserving
proof
let a,b be Element of L;
set f = alpha FD;
A14:ex_sup_of f.:{a,b},EqRelLATT FS by YELLOW_0:17;
A15: dom f = the carrier of L by FUNCT_2:def 1;
consider e1 being Equivalence_Relation of FS such that
A16: e1 = f.a and
A17: for x,y being Element of FS holds [x,y] in e1 iff FD.(x,y) <= a by Def9;
consider e2 being Equivalence_Relation of FS such that
A18: e2 = f.b and
A19: for x,y being Element of FS holds [x,y] in e2 iff FD.(x,y) <= b by Def9;
consider e3 being Equivalence_Relation of FS such that
A20: e3 = f.(a "\/" b) and
A21: for x,y being Element of FS holds [x,y] in e3 iff FD.(x,y) <=
a"\/"b by Def9;
A22: field e1 = FS by EQREL_1:15;
A23: field e2 = FS by EQREL_1:15;
A24: field e3 = FS by EQREL_1:15;
A25: e1 "\/" e2 c= e3
proof
now let x,y be set; assume
A26:[x,y] in e1;
then reconsider x' = x, y' = y as Element of FS by A22,RELAT_1:30;
A27:FD.(x',y') <= a by A17,A26;
a <= a "\/" b by YELLOW_0:22;
then FD.(x',y') <= a "\/" b by A27,ORDERS_1:26;
hence [x,y] in e3 by A21;
end;
then A28: e1 c= e3 by RELAT_1:def 3;
now
let x,y be set; assume
A29:[x,y] in e2;
then reconsider x' = x, y' = y as Element of FS by A23,RELAT_1:30;
A30:FD.(x',y') <= b by A19,A29;
b <= b "\/" a by YELLOW_0:22;
then FD.(x',y') <= b "\/" a by A30,ORDERS_1:26;
hence [x,y] in e3 by A21;
end;
then e2 c= e3 by RELAT_1:def 3;
then e1 \/ e2 c= e3 by A28,XBOOLE_1:8;
hence thesis by EQREL_1:def 3;
end;
A31: e3 c= e1 "\/" e2
proof
for u,v being set holds [u,v] in e3 implies [u,v] in e1 "\/" e2
proof
let u,v be set; assume
A32: [u,v] in e3;
then reconsider x = u, y = v as Element of FS by A24,RELAT_1:30;
A33: u in FS by A24,A32,RELAT_1:30;
FD.(x,y) <= a"\/"b by A21,A32;
then consider z1,z2,z3 being Element of FS such that
A34: FD.(x,z1) = a and
A35: FD.(z2,z3) = a and
A36: FD.(z1,z2) = b and
A37: FD.(z3,y) = b by Th45;
defpred P[set,set] means
($1 = 1 implies $2 = x) & ($1 = 2 implies $2 = z1) &
($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = z3) &
($1 = 5 implies $2 = y);
A38: for m being Nat, w1,w2 being set st m in Seg 5 & P[m,w1] & P[m,w2]
holds w1 = w2 by Lm3;
A39: for m being Nat st m in Seg 5 ex w being set st P[m,w]
proof
let m be Nat; assume
A40:m in Seg 5;
per cases by A40,Lm3;
suppose A41: m = 1; take w = x; thus P[m,w] by A41;
suppose A42: m = 2; take w = z1; thus P[m,w] by A42;
suppose A43: m = 3; take w = z2; thus P[m,w] by A43;
suppose A44: m = 4; take w = z3; thus P[m,w] by A44;
suppose A45: m = 5; take w = y; thus P[m,w] by A45;
end;
ex p being FinSequence
st dom p = Seg 5 & for k being Nat st k in Seg 5 holds P[k,p.k]
from SeqEx(A38,A39);
then consider h being FinSequence such that
A46: dom h = Seg 5 and
A47: for m being Nat st m in Seg 5 holds
(m = 1 implies h.m = x) & (m = 2 implies h.m = z1) &
(m = 3 implies h.m = z2) & (m = 4 implies h.m = z3) &
(m = 5 implies h.m = y);
Seg 5 = { n where n is Nat: 1 <= n & n <= 5 } by FINSEQ_1:def 1;
then A48: 1 in Seg 5 & 2 in Seg 5 & 3 in Seg 5 & 4 in Seg 5 & 5 in Seg 5;
A49: len h = 5 by A46,FINSEQ_1:def 3;
A50: u = h.1 by A47,A48;
A51: v = h.5 by A47,A48 .= h.(len h) by A46,FINSEQ_1:def 3;
for j being Nat st 1 <= j & j < len h holds [h.j,h.(j+1)] in e1 \/ e2
proof
let j be Nat; assume
A52: 1 <= j & j < len h;
per cases by A49,A52,Lm2;
suppose A53:j = 1;
[x,z1] in e1 by A17,A34;
then [h.1,z1] in e1 by A47,A48;
then [h.1,h.2] in e1 by A47,A48;
hence [h.j,h.(j+1)] in e1 \/ e2 by A53,XBOOLE_0:def 2;
suppose A54:j = 3;
[z2,z3] in e1 by A17,A35;
then [h.3,z3] in e1 by A47,A48;
then [h.3,h.4] in e1 by A47,A48;
hence [h.j,h.(j+1)] in e1 \/ e2 by A54,XBOOLE_0:def 2;
suppose A55:j = 2;
[z1,z2] in e2 by A19,A36;
then [h.2,z2] in e2 by A47,A48;
then [h.2,h.3] in e2 by A47,A48;
hence [h.j,h.(j+1)] in e1 \/ e2 by A55,XBOOLE_0:def 2;
suppose A56:j = 4;
[z3,y] in e2 by A19,A37;
then [h.4,y] in e2 by A47,A48;
then [h.4,h.5] in e2 by A47,A48;
hence [h.j,h.(j+1)] in e1 \/ e2 by A56,XBOOLE_0:def 2;
end;
hence [u,v] in e1 "\/" e2 by A33,A49,A50,A51,EQREL_1:36;
end;
hence thesis by RELAT_1:def 3;
end;
sup (f.:{a,b}) = sup {f.a,f.b} by A15,FUNCT_1:118
.= f.a "\/" f.b by YELLOW_0:41 .= e1 "\/" e2 by A16,A18,Th10
.= f.(a "\/" b) by A20,A25,A31,XBOOLE_0:def 10
.= f.sup {a,b} by YELLOW_0:41;
hence f preserves_sup_of {a,b} by A14,WAYBEL_0:def 31;
end;
then reconsider f = alpha FD as Homomorphism of L,EqRelLATT FS by Th16;
take FS,f;
thus f is one-to-one by A6,Th17;
A57: Image f = subrelstr rng f by YELLOW_2:def 2;
A58:dom f = the carrier of L by FUNCT_2:def 1;
A59: ex e being Equivalence_Relation of FS st
e in the carrier of Image f & e <> id FS
proof
consider A' being non empty set, d' being distance_function of A',L,
Aq' being non empty set, dq' being distance_function of Aq',L such that
A60: Aq', dq' is_extension_of A',d' and
A61: S.0 = [A',d'] & S.(0+1) = [Aq',dq'] by Def21;
A' = A & d' = D by A2,A61,ZFMISC_1:33;
then consider q being QuadrSeq of D such that
A62: Aq' = NextSet(D) and
A63: dq' = NextDelta(q) by A60,Def20;
A64: (S.1)`2 = NextDelta(q) by A61,A63,MCART_1:def 2;
(S.1)`2 in { (S.i)`2 where i is Nat: not contradiction};
then A65: NextDelta(q) c= FD by A64,ZFMISC_1:92;
A66: (S.1)`1 = NextSet(D) by A61,A62,MCART_1:def 1;
(S.1)`1 in { (S.i)`1 where i is Nat: not contradiction};
then A67: NextSet(D) c= FS by A66,ZFMISC_1:92;
succ {} c= DistEsti(D) by Lm4;
then {} in DistEsti(D) by ORDINAL1:33;
then A68: {} in dom q by Th28;
then q.{} in rng q by FUNCT_1:def 5;
then q.{} in {[u,v,a',b'] where u is Element of A, v is Element of A,
a' is Element of L, b' is Element of L: D.(u,v) <= a'"\/"b'} by Def14;
then consider u,v be Element of A, a,b be Element of L such that
A69: q.{} = [u,v,a,b] & D.(u,v) <= a"\/"b;
ConsecutiveSet(A,{}) = A by Th24;
then reconsider Q = Quadr(q,{}) as
Element of [:A,A,the carrier of L,the carrier of L:];
A70: Quadr(q,{}) = [u,v,a,b] by A68,A69,Def15;
consider e being Equivalence_Relation of FS such that
A71: e = f.b and
A72: for x,y being Element of FS holds [x,y] in e iff FD.(x,y) <= b by Def9;
take e;
e in rng f by A58,A71,FUNCT_1:def 5;
hence e in the carrier of Image f by A57,YELLOW_0:def 15;
A73: new_set A = new_set ConsecutiveSet(A,{}) by Th24
.= ConsecutiveSet(A,succ {}) by Th25;
A74: NextSet(D) = ConsecutiveSet(A,DistEsti(D)) by Def18;
A75: succ {} c= DistEsti(D) by Lm4;
then A76: new_set A c= NextSet(D) by A73,A74,Th32;
A77: ConsecutiveSet(A,{}) = A & ConsecutiveDelta(q,{}) = D by Th24,Th29;
A78: ConsecutiveDelta(q,succ {}) =
new_bi_fun(BiFun(ConsecutiveDelta(q,{}),
ConsecutiveSet(A,{}),L),Quadr(q,{})) by Th30
.= new_bi_fun(D,Q) by A77,Def16;
ConsecutiveDelta(q,DistEsti(D)) = NextDelta(q) by Def19;
then new_bi_fun(D,Q) c= NextDelta(q) by A75,A78,Th35;
then A79: new_bi_fun(D,Q) c= FD by A65,XBOOLE_1:1;
A80: new_set A c= FS by A67,A76,XBOOLE_1:1;
A81: dom new_bi_fun(D,Q) = [:new_set A,new_set A:] by FUNCT_2:def 1;
{A} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14;
then {A} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2;
then A82: {A} in new_set A by Def10;
{{A}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:14;
then {{A}} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 2;
then A83: {{A}} in new_set A by Def10;
then A84: [{A},{{A}}] in dom new_bi_fun(D,Q) by A81,A82,ZFMISC_1:106;
reconsider W = {A}, V = {{A}} as Element of FS by A80,A82,A83;
FD.(W,V) = FD.[{A},{{A}}] by BINOP_1:def 1
.= new_bi_fun(D,Q).[{A},{{A}}] by A79,A84,GRFUNC_1:8
.= new_bi_fun(D,Q).({A},{{A}}) by BINOP_1:def 1
.= Q`4 by Def11 .= b by A70,MCART_1:def 11;
then A85: [{A},{{A}}] in e by A72;
{A} <> {{A}}
proof assume {A} = {{A}}; then {A} in {A} by TARSKI:def 1;
hence contradiction; end;
hence e <> id FS by A85,RELAT_1:def 10;
end;
for e1,e2 being Equivalence_Relation of FS,x,y st
e1 in the carrier of Image f & e2 in the carrier of Image f &
[x,y] in e1 "\/" e2
ex F being non empty FinSequence of FS st
len F = 3+2 & x,y are_joint_by F,e1,e2 by Th46;
hence type_of Image f <= 3 by A59,Th15;
end;