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