Copyright (c) 2000 Association of Mizar Users
environ
vocabulary RELAT_1, ORDERS_1, EQREL_1, LATTICES, FINSEQ_1, LATTICE5, WAYBEL_0,
REALSET1, GROUP_6, FUNCT_1, FINSET_1, MATRIX_2, CAT_1, FILTER_2, BOOLE,
YELLOW_0, ORDINAL2, ORDINAL1, PRE_TOPC, WELLORD1, SEQM_3, LATTICE3,
WAYBEL_1, MCART_1, RELAT_2, TARSKI, ZFMISC_1, HAHNBAN, PARTFUN1, PRALG_1,
FUNCT_6, SGRAPH1, LATTICE8;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_2, FUNCT_6, NUMBERS, XREAL_0, NAT_1, ORDINAL1, ORDINAL2, MCART_1,
DOMAIN_1, PARTFUN1, PRALG_1, PRE_TOPC, STRUCT_0, GROUP_1, REALSET1,
ORDERS_1, EQREL_1, FINSEQ_1, LATTICE3, BINOP_1, YELLOW_0, YELLOW_2,
LATTICE5, YELLOW11, WAYBEL_1, WAYBEL_0, ABIAN;
constructors NAT_1, DOMAIN_1, RFUNCT_3, LATTICE5, YELLOW11, ORDERS_3,
YELLOW10, ABIAN, SCMPDS_1, MEMBERED, PRE_TOPC;
clusters SUBSET_1, RELSET_1, STRUCT_0, INT_1, YELLOW_0, YELLOW_2, YELLOW11,
CARD_1, ORDINAL1, PRALG_1, LATTICE3, LATTICE5, WAYBEL10, WAYBEL21,
REALSET1, EQREL_1, LATTICE7, FINSEQ_6, ABIAN, ARYTM_3, MEMBERED,
PARTFUN1, NUMBERS, ORDINAL2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, LATTICE3, PRALG_1, WAYBEL_0, YELLOW_0, YELLOW11, LATTICE5,
RELAT_1, XBOOLE_0;
theorems EQREL_1, CQC_THE1, RELAT_1, RELAT_2, FINSEQ_1, FINSEQ_2, ORDERS_1,
TARSKI, ORDINAL1, ORDINAL3, HAHNBAN, PARTFUN1, GRFUNC_1, FUNCT_6,
EXTENS_1, MCART_1, NAT_1, BINOP_1, ZFMISC_1, FUNCT_1, FUNCT_2, LATTICE3,
YELLOW_0, YELLOW_2, YELLOW_3, YELLOW_5, WAYBEL_0, WAYBEL_1, WAYBEL_6,
RELSET_1, LATTICE5, YELLOW11, WAYBEL13, REALSET1, ORDERS_3, TEX_1,
SYSREL, XBOOLE_0, XBOOLE_1;
schemes LATTICE5, FUNCT_1, FUNCT_2, ORDINAL2, NAT_1, FINSEQ_1;
begin :: Preliminaries
definition
let A be non empty set;
let P,R be Relation of A;
redefine pred P c= R means
for a,b being Element of A st [a,b] in P holds [a,b] in R;
compatibility
proof
thus P c= R implies
(for a,b being Element of A st [a,b] in P holds [a,b] in R);
thus (for a,b being Element of A st [a,b] in P holds [a,b] in R) implies
P c= R
proof
assume
A1: for a,b being Element of A st [a,b] in P holds [a,b] in R;
let x,y be set;
assume
A2: [x,y] in P;
then ex x1,y1 being set st
[x,y] = [x1,y1] & x1 in A & y1 in A by RELSET_1:6;
hence [x,y] in R by A1,A2;
end;
end;
end;
definition
let L be RelStr;
attr L is finitely_typed means :Def2:
ex A being non empty set
st (for e being set st e in the carrier of L
holds e is Equivalence_Relation of A) &
ex o being Nat
st for e1,e2 being Equivalence_Relation of A, x,y being set
st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2
holds ex F being non empty FinSequence of A
st len F = o & x,y are_joint_by F,e1,e2;
end;
definition
let L be lower-bounded LATTICE;
let n be Nat;
pred L has_a_representation_of_type<= n means :Def3:
ex A being non trivial set, f be Homomorphism of L,EqRelLATT A
st f is one-to-one & Image f is finitely_typed &
(ex e being Equivalence_Relation of A
st e in the carrier of Image f & e <> id A) & type_of Image f <= n;
end;
definition
cluster lower-bounded distributive finite LATTICE;
existence
proof
consider L being distributive finite LATTICE;
take L;
thus thesis;
end;
end;
Lm1:
1 is odd
proof
2*0+1 = 1;
hence thesis;
end;
Lm2:
2 is even
proof
2*1 = 2;
hence thesis;
end;
definition
let A be non trivial set;
cluster non trivial finitely_typed full (non empty Sublattice of EqRelLATT A);
existence
proof
consider a being Element of A;
consider b being Element of A\{a};
A\{a} is non empty set by REALSET1:32;
then A1: b in A & a <> b by ZFMISC_1:64;
A2: id A in the carrier of EqRelLATT A by LATTICE5:4;
nabla A in the carrier of EqRelLATT A by LATTICE5:4;
then reconsider e1 = nabla A, e2 = id A as Element of EqRelLATT A
by A2;
set Y = subrelstr {e1,e2};
A3: the carrier of Y = {e1,e2} by YELLOW_0:def 15;
e1 = [:A,A:] by EQREL_1:def 1;
then A4: e2 <= e1 by LATTICE5:6;
A5: Y is meet-inheriting
proof
thus for x,y being Element of EqRelLATT A st
x in the carrier of Y & y in the carrier of Y &
ex_inf_of {x,y},EqRelLATT A
holds inf {x,y} in the carrier of Y
proof
let x,y be Element of EqRelLATT A;
assume
A6: x in the carrier of Y & y in the carrier of Y &
ex_inf_of {x,y},EqRelLATT A;
per cases by A3,A6,TARSKI:def 2;
suppose
x = e1 & y = e1;
then inf {x,y} = e1"/\"e1 by YELLOW_0:40
.= e1 by YELLOW_5:2;
hence thesis by A3,TARSKI:def 2;
suppose
x = e1 & y = e2;
then inf {x,y} = e1"/\"e2 by YELLOW_0:40
.= e2 by A4,YELLOW_5:10;
hence thesis by A3,TARSKI:def 2;
suppose
x = e2 & y = e1;
then inf {x,y} = e2"/\"e1 by YELLOW_0:40
.= e2 by A4,YELLOW_5:10;
hence thesis by A3,TARSKI:def 2;
suppose
x = e2 & y = e2;
then inf {x,y} = e2"/\"e2 by YELLOW_0:40
.= e2 by YELLOW_5:2;
hence thesis by A3,TARSKI:def 2;
end;
thus thesis;
end;
A7: Y is join-inheriting
proof
thus for x,y being Element of EqRelLATT A st
x in the carrier of Y & y in the carrier of Y &
ex_sup_of {x,y},EqRelLATT A
holds sup {x,y} in the carrier of Y
proof
let x,y be Element of EqRelLATT A;
assume
A8: x in the carrier of Y & y in the carrier of Y &
ex_sup_of {x,y},EqRelLATT A;
per cases by A3,A8,TARSKI:def 2;
suppose
x = e1 & y = e1;
then sup {x,y} = e1"\/"e1 by YELLOW_0:41
.= e1 by YELLOW_5:1;
hence thesis by A3,TARSKI:def 2;
suppose
x = e1 & y = e2;
then sup {x,y} = e1"\/"e2 by YELLOW_0:41
.= e1 by A4,YELLOW_5:8;
hence thesis by A3,TARSKI:def 2;
suppose
x = e2 & y = e1;
then sup {x,y} = e2"\/"e1 by YELLOW_0:41
.= e1 by A4,YELLOW_5:8;
hence thesis by A3,TARSKI:def 2;
suppose
x = e2 & y = e2;
then sup {x,y} = e2"\/"e2 by YELLOW_0:41
.= e2 by YELLOW_5:1;
hence thesis by A3,TARSKI:def 2;
end;
thus thesis;
end;
A9: Y is non trivial
proof
assume Y is trivial;
then consider s being Element of Y such that
A10: the carrier of Y = {s} by TEX_1:def 1;
nabla A = id A by A3,A10,ZFMISC_1:9;
then [:A,A:] = id A by EQREL_1:def 1;
then [a,b] in id A by A1,ZFMISC_1:def 2;
hence contradiction by A1,RELAT_1:def 10;
end;
A11: Y is finitely_typed
proof
take A;
thus for e being set st e in the carrier of Y
holds e is Equivalence_Relation of A by A3,TARSKI:def 2;
take o = 3;
thus for eq1,eq2 being Equivalence_Relation of A, x1,y1 being set
st eq1 in the carrier of Y & eq2 in the carrier of Y &
[x1,y1] in eq1 "\/" eq2 holds
ex F being non empty FinSequence of A st
len F = o & x1,y1 are_joint_by F,eq1,eq2
proof
let eq1,eq2 be Equivalence_Relation of A;
let x1,y1 be set;
assume
A12: eq1 in the carrier of Y & eq2 in the carrier of Y &
[x1,y1] in eq1 "\/" eq2;
eq1 = e2 or eq1 <> e2;
then consider z being set such that
A13: eq1 = e2 & z = x1 or eq1 <> e2 & z = y1;
consider x2,y2 being set such that
A14: [x1,y1] = [x2,y2] & x2 in A & y2 in A by A12,RELSET_1:6;
x1 in A & y1 in A by A14,ZFMISC_1:33;
then reconsider F = <*x1,z,y1*> as non empty FinSequence of A
by A13,FINSEQ_2:16;
take F;
per cases by A13;
suppose
A15: eq1 = e2 & z = x1;
then A16: eq1 = e2 & len F = 3 & F.1 = x1 & F.2 = x1 & F.3 = y1 by FINSEQ_1:
62;
for i being Nat st 1 <= i & i < len F holds
(i is odd implies [F.i,F.(i+1)] in eq1) &
(i is even implies [F.i,F.(i+1)] in eq2)
proof
let i be Nat;
assume
A17: 1 <= i & i < len F;
then i < 2+1 by FINSEQ_1:62;
then i <= 2 by NAT_1:38;
then A18: i = 0 or i = 1 or i = 2 by CQC_THE1:3;
per cases by A3,A12,A15,A17,A18,Lm1,Lm2,TARSKI:def 2;
suppose
A19: i = 1 & i is odd & eq1 = e2 & eq2 = e1;
consider x2,y2 being set such that
A20: [x1,y1] = [x2,y2] & x2 in A & y2 in A by A12,RELSET_1:6;
x1 in A by A20,ZFMISC_1:33;
hence thesis by A16,A19,EQREL_1:11;
suppose
A21: i = 1 & i is odd & eq1 = e2 & eq2 = e2;
consider x2,y2 being set such that
A22: [x1,y1] = [x2,y2] & x2 in A & y2 in A by A12,RELSET_1:6;
x1 in A by A22,ZFMISC_1:33;
hence thesis by A16,A21,EQREL_1:11;
suppose
A23: i = 2 & i is even & eq1 = e2 & eq2 = e1;
then eq1 "\/" eq2 = e2 "\/" e1 by LATTICE5:10
.= eq2 by A4,A23,YELLOW_5:8;
hence thesis by A12,A16,A23;
suppose
A24: i = 2 & i is even & eq1 = e2 & eq2 = e2;
then eq1 "\/" eq2 = e2 "\/" e2 by LATTICE5:10
.= eq2 by A24,YELLOW_5:1;
hence thesis by A12,A16,A24;
end;
hence len F = o & x1,y1 are_joint_by F,eq1,eq2 by A16,LATTICE5:def 3;
suppose
A25: eq1 <> e2 & z = y1;
then A26: eq1 <> e2 & len F = 3 & F.1 = x1 & F.2 = y1 & F.3 = y1 by FINSEQ_1:
62;
for i being Nat st 1 <= i & i < len F holds
(i is odd implies [F.i,F.(i+1)] in eq1) &
(i is even implies [F.i,F.(i+1)] in eq2)
proof
let i be Nat;
assume
A27: 1 <= i & i < len F;
then i < 2+1 by FINSEQ_1:62;
then i <= 2 by NAT_1:38;
then A28: i = 0 or i = 1 or i = 2 by CQC_THE1:3;
per cases by A3,A12,A25,A27,A28,Lm1,Lm2,TARSKI:def 2;
suppose
A29: i = 1 & i is odd & eq1 = e1 & eq2 = e1;
then eq1 "\/" eq2 = e1 "\/" e1 by LATTICE5:10
.= eq1 by A29,YELLOW_5:8;
hence
(i is odd implies [F.i,F.(i+1)] in eq1) &
(i is even implies [F.i,F.(i+1)] in eq2) by A12,A26,A29;
suppose
A30: i = 1 & i is odd & eq1 = e1 & eq2 = e2;
then eq1 "\/" eq2 = e1 "\/" e2 by LATTICE5:10
.= eq1 by A4,A30,YELLOW_5:8;
hence
(i is odd implies [F.i,F.(i+1)] in eq1) &
(i is even implies [F.i,F.(i+1)] in eq2) by A12,A26,A30;
suppose
A31: i = 2 & i is even & eq1 = e1 & eq2 = e1;
consider x2,y2 being set such that
A32: [x1,y1] = [x2,y2] & x2 in A & y2 in A by A12,RELSET_1:6;
y1 in A by A32,ZFMISC_1:33;
hence
(i is odd implies [F.i,F.(i+1)] in eq1) &
(i is even implies [F.i,F.(i+1)] in eq2) by A26,A31,EQREL_1:11;
suppose
A33: i = 2 & i is even & eq1 = e1 & eq2 = e2;
consider x2,y2 being set such that
A34: [x1,y1] = [x2,y2] & x2 in A & y2 in A by A12,RELSET_1:6;
y1 in A by A34,ZFMISC_1:33;
hence
(i is odd implies [F.i,F.(i+1)] in eq1) &
(i is even implies [F.i,F.(i+1)] in eq2) by A26,A33,EQREL_1:11;
end;
hence len F = o & x1,y1 are_joint_by F,eq1,eq2 by A26,LATTICE5:def 3;
end;
end;
reconsider Y as full
(non empty Sublattice of EqRelLATT A) by A5,A7;
take Y; thus thesis by A9,A11;
end;
end;
theorem Th1:
for A be non empty set
for L be lower-bounded LATTICE
for d be distance_function of A,L
holds succ {} c= DistEsti(d)
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
succ {} c= DistEsti(d) or DistEsti(d) in succ {} by ORDINAL1:26;
then succ {} c= DistEsti(d) or DistEsti(d) c= {} by ORDINAL1:34;
then succ {} c= DistEsti(d) or DistEsti(d) = {} by XBOOLE_1:3;
hence succ {} c= DistEsti(d) by LATTICE5:23;
end;
theorem
for L being trivial Semilattice holds L is modular
proof
let L be trivial Semilattice;
let a,b,c be Element of L such that a <= c;
thus a"\/"(b"/\"c) = (a"\/"b)"/\"c by REALSET1:def 20;
end;
theorem
for A being non empty set
for L being non empty Sublattice of EqRelLATT A
holds L is trivial or ex e being Equivalence_Relation of A
st e in the carrier of L & e <> id A
proof
let A be non empty set;
let L be non empty Sublattice of EqRelLATT A;
now
assume
A1: not ex e being Equivalence_Relation of A st
e in the carrier of L & e <> id A;
thus L is trivial
proof
consider x be set such that
A2: x in the carrier of L by XBOOLE_0:def 1;
the carrier of L c= the carrier of EqRelLATT A by YELLOW_0:def 13;
then reconsider e=x as Equivalence_Relation of A by A2,LATTICE5:4;
the carrier of L = {x}
proof
thus the carrier of L c= {x}
proof
let a be set;
assume
A3: a in the carrier of L;
the carrier of L c= the carrier of EqRelLATT A by YELLOW_0:def 13;
then reconsider B=a as Equivalence_Relation of A by A3,LATTICE5:4;
B = id A by A1,A3
.= e by A1,A2;
hence a in {x} by TARSKI:def 1;
end;
let A be set;
assume A in {x};
hence A in the carrier of L by A2,TARSKI:def 1;
end;
then the carrier of L is trivial by REALSET1:def 12;
hence thesis by REALSET1:def 13;
end;
end;
hence thesis;
end;
theorem Th4:
for L1,L2 be lower-bounded LATTICE
for f being map of L1,L2 st f is infs-preserving sups-preserving
holds f is meet-preserving join-preserving
proof
let L1,L2 be lower-bounded LATTICE;
let f be map of L1,L2;
assume
A1: f is infs-preserving sups-preserving;
thus f is meet-preserving
proof
let x,y be Element of L1;
thus f preserves_inf_of {x,y} by A1,WAYBEL_0:def 32;
end;
thus f is join-preserving
proof
let x,y be Element of L1;
thus f preserves_sup_of {x,y} by A1,WAYBEL_0:def 33;
end;
end;
theorem Th5:
for L1,L2 be lower-bounded LATTICE
st L1,L2 are_isomorphic & L1 is modular holds L2 is modular
proof
let L1,L2 be lower-bounded LATTICE;
assume
A1: L1,L2 are_isomorphic & L1 is modular;
then consider f be map of L1,L2 such that
A2: f is isomorphic by WAYBEL_1:def 8;
f is infs-preserving sups-preserving by A2,WAYBEL13:20;
then A3: f is meet-preserving join-preserving by Th4;
let a,b,c be Element of L2;
assume
A4: a <= c;
set A = f".a;
set B = f".b;
set C = f".c;
A5: f is one-to-one & rng f = the carrier of L2 by A2,WAYBEL_0:66;
then A6: f is one-to-one & a in rng f & b in rng f & c in rng f &
a = f.A & b = f.B & c = f.C by FUNCT_1:57;
A in dom f & B in dom f & C in dom f by A5,FUNCT_1:54;
then reconsider A,B,C as Element of L1;
A <= C by A2,A4,A6,WAYBEL_0:66;
then A7: A"\/"(B"/\"C) = (A"\/"B)"/\"C by A1,YELLOW11:def 3;
thus a"\/"(b"/\"c) = f.A "\/" f.(B"/\"C) by A3,A6,WAYBEL_6:1
.= f.((A"\/"B)"/\"C) by A3,A7,WAYBEL_6:2
.= (f.(A"\/"B)"/\"f.C) by A3,WAYBEL_6:1
.= (a"\/"b)"/\"c by A3,A6,WAYBEL_6:2;
end;
theorem Th6:
for S being lower-bounded non empty Poset
for T being non empty Poset
for f being monotone map of S,T holds Image f is lower-bounded
proof
let S be lower-bounded non empty Poset;
let T be non empty Poset;
let f be monotone map of S,T;
thus Image f is lower-bounded
proof
consider x being Element of S such that
A1: x is_<=_than the carrier of S by YELLOW_0:def 4;
dom f = the carrier of S by FUNCT_2:def 1;
then x in dom f & f.x in rng f by FUNCT_1:def 5;
then f.x in the carrier of subrelstr (rng f) by YELLOW_0:def 15;
then f.x in the carrier of Image f by YELLOW_2:def 2;
then reconsider fx = f.x as Element of Image f;
take fx;
let b be Element of Image f;
assume
A2: b in the carrier of Image f;
then b in the carrier of subrelstr (rng f) by YELLOW_2:def 2;
then b in rng f by YELLOW_0:def 15;
then consider c be set such that
A3: c in dom f & f.c = b by FUNCT_1:def 5;
reconsider c as Element of S by A3;
the carrier of Image f c= the carrier of T by YELLOW_0:def 13;
then reconsider b1 = b as Element of T by A2;
x <= c by A1,LATTICE3:def 8;
then f.x <= b1 by A3,ORDERS_3:def 5;
hence fx <= b by YELLOW_0:61;
end;
end;
theorem Th7:
for L being lower-bounded LATTICE
for x,y being Element of L
for A being non empty set
for f be Homomorphism of L,EqRelLATT A st f is one-to-one
holds (corestr f).x <= (corestr f).y implies x <= y
proof
let L be lower-bounded LATTICE;
let x,y be Element of L;
let A be non empty set;
let f be Homomorphism of L,EqRelLATT A;
assume that
A1: f is one-to-one and
A2: (corestr f).x <= (corestr f).y;
now
assume
A3: not x <= y;
A4: corestr f = f & corestr f is one-to-one by A1,WAYBEL_1:32;
A5: Image f is Semilattice & L is Semilattice;
A6: Image f is strict full Sublattice of EqRelLATT A;
A7: for x,y being Element of L holds
(corestr f).(x "/\" y) = (corestr f).x "/\" (corestr f).y
proof
let x,y be Element of L;
thus (corestr f).(x "/\" y) = f.x "/\" f.y by A4,WAYBEL_6:1
.= (corestr f).x "/\" (corestr f).y by A4,A6,YELLOW_0:70;
end;
(corestr f).y "/\" (corestr f).x = (corestr f).x by A2,A5,YELLOW_5:10;
then (corestr f).x = (corestr f).(x "/\" y) by A7;
then x = x "/\" y by A4,WAYBEL_1:def 1;
hence contradiction by A3,YELLOW_0:25;
end;
hence thesis;
end;
begin :: J\'onsson theorem
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: => :: L has_a_representation_of_type<= 2 implies L is modular ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem Th8:
for A being non trivial set
for L being finitely_typed full (non empty Sublattice of EqRelLATT A)
for e being Equivalence_Relation of A st e in the carrier of L & e <> id A
holds type_of L <= 2 implies L is modular
proof
let A be non trivial set;
let L be finitely_typed full (non empty Sublattice of EqRelLATT A);
let e be Equivalence_Relation of A;
assume that
A1: e in the carrier of L and
A2: e <> id A;
assume
A3: type_of L <= 2;
let a,b,c be Element of L;
assume
A4: a <= c;
A5: the carrier of L c= the carrier of EqRelLATT A by YELLOW_0:def 13;
A6: a in the carrier of L;
then reconsider a' = a as Equivalence_Relation of A by A5,LATTICE5:4;
A7: b in the carrier of L;
then reconsider b' = b as Equivalence_Relation of A by A5,LATTICE5:4;
A8: c in the carrier of L;
then reconsider c' = c as Equivalence_Relation of A by A5,LATTICE5:4;
reconsider a'' = a' as Element of EqRelLATT A by A5,A6;
reconsider b'' = b' as Element of EqRelLATT A by A5,A7;
reconsider c'' = c' as Element of EqRelLATT A by A5,A8;
A9: a'' <= c'' by A4,YELLOW_0:60;
then A10: a' c= c' by LATTICE5:6;
A11: b' /\ c' = b''"/\"c'' & b''"/\"c'' = b"/\"c by LATTICE5:8,YELLOW_0:70;
A12: a' "\/" b' = a''"\/"b'' & a''"\/"b'' = a"\/"b by LATTICE5:10,YELLOW_0:71;
A13: a'"\/"(b' /\ c') = a''"\/"(b''"/\"c'') by A11,LATTICE5:10;
A14: a''"\/"(b''"/\"c'') <= (a''"\/"b'')"/\"c'' by A9,YELLOW11:8;
(a''"\/"b'')"/\"c'' = (a''"\/"b'') /\ c' by LATTICE5:8
.= (a'"\/"b') /\ c' by LATTICE5:10;
then A15: a'"\/"(b' /\ c') c= (a'"\/"b') /\ c' by A13,A14,LATTICE5:6;
consider AA being non empty set such that
A16: for e being set st e in the carrier of L
holds e is Equivalence_Relation of AA and
A17: ex i being Nat st
for e1,e2 being Equivalence_Relation of AA, x,y being set st
e1 in the carrier of L & e2 in the carrier of L &
[x,y] in e1 "\/" e2
holds
ex F being non empty FinSequence of AA st
len F = i & x,y are_joint_by F,e1,e2 by Def2;
e is Equivalence_Relation of AA by A1,A16;
then A18: field e = A & field e = AA by EQREL_1:16;
A19: (a'"\/"b') /\ c' c= a'"\/"(b' /\ c')
proof
let x,y be Element of A;
assume
A20: [x,y] in (a' "\/" b') /\ c';
then A21: [x,y] in a' "\/" b' & [x,y] in c' by XBOOLE_0:def 3;
per cases by A3,CQC_THE1:3;
suppose
type_of L = 2;
then consider F being non empty FinSequence of A such that
A22: len F = 2+2 & x,y are_joint_by F,a',b' by A1,A2,A17,A18,A21,LATTICE5:
def 4;
set z1 = F.2;
set z2 = F.3;
A23: F.1 = x & F.4 = y &
for i being Nat st 1 <= i & i < 4 holds
(i is odd implies [F.i,F.(i+1)] in a') &
(i is even implies [F.i,F.(i+1)] in b') by A22,LATTICE5:def 3;
consider j being Nat such that
A24: j = 0;
2*j+1 = 1 by A24;
then A25: 1 is odd & [F.1,F.(1+1)] in a' by A22,LATTICE5:def 3;
consider k being Nat such that
A26: k = 1;
2*k = 2 by A26;
then A27: 2 is even & [F.2,F.(2+1)] in b' by A22,LATTICE5:def 3;
consider l being Nat such that
A28: l = 1;
2*l+1 = 3 by A28;
then A29: 3 is odd & [F.3,F.(3+1)] in a' by A22,LATTICE5:def 3;
then [x,z1] in a' & [z2,y] in a' & [z1,z2] in b' & [y,x] in c' &
[x,z1] in c' & [z2,y] in c' & [x,y] in c' by A10,A21,A23,A25,A27,EQREL_1
:12;
then [z2,x] in c' by EQREL_1:13;
then [z2,z1] in c' by A10,A23,A25,EQREL_1:13;
then [z1,z2] in c' by EQREL_1:12;
then A30: [z1,z2] in b' /\ c' by A27,XBOOLE_0:def 3;
reconsider BC = b' /\ c' as Element of EqRelLATT A by A11;
A31: a'' <= a'' "\/" BC by YELLOW_0:22;
A32: a' "\/" (b' /\ c') = a''"\/" BC by LATTICE5:10;
then A33: a' c= a' "\/" (b' /\ c') by A31,LATTICE5:6;
BC <= BC "\/" a'' by YELLOW_0:22;
then b' /\ c' c= a' "\/" (b' /\ c') by A32,LATTICE5:6;
then [x,z2] in a' "\/" (b' /\ c') by A23,A25,A30,A33,EQREL_1:13;
hence thesis by A23,A29,A33,EQREL_1:13;
suppose
type_of L = 1;
then consider F being non empty FinSequence of A such that
A34: len F = 1+2 & x,y are_joint_by F,a',b' by A1,A2,A17,A18,A21,LATTICE5:
def 4;
set z1 = F.2;
A35: F.1 = x & F.3 = y &
for i being Nat st 1 <= i & i < 3 holds
(i is odd implies [F.i,F.(i+1)] in a') &
(i is even implies [F.i,F.(i+1)] in b') by A34,LATTICE5:def 3;
consider j being Nat such that
A36: j = 0;
2*j+1 = 1 by A36;
then A37: 1 is odd & [F.1,F.(1+1)] in a' by A34,LATTICE5:def 3;
consider k being Nat such that
A38: k = 1;
A39: 2*k = 2 by A38;
then A40: 2 is even & [F.2,F.(2+1)] in b' by A34,LATTICE5:def 3;
[x,z1] in a' & [x,z1] in c' & [x,y] in c' & [z1,y] in b' & [z1,x] in c'
by A10,A20,A34,A35,A37,A39,EQREL_1:12,XBOOLE_0:def 3;
then [z1,y] in c' by EQREL_1:13;
then A41: [z1,y] in b' /\ c' by A35,A40,XBOOLE_0:def 3;
reconsider BC = b' /\ c' as Element of EqRelLATT A by A11;
A42: a'' <= a'' "\/" BC by YELLOW_0:22;
A43: a' "\/" (b' /\ c') = a''"\/" BC by LATTICE5:10;
then A44: a' c= a' "\/" (b' /\ c') by A42,LATTICE5:6;
BC <= BC "\/" a'' by YELLOW_0:22;
then b' /\ c' c= a' "\/" (b' /\ c') by A43,LATTICE5:6;
hence thesis by A35,A37,A41,A44,EQREL_1:13;
suppose
type_of L = 0;
then consider F being non empty FinSequence of A such that
A45: len F = 0+2 & x,y are_joint_by F,a',b' by A1,A2,A17,A18,A21,LATTICE5:
def 4;
A46: F.1 = x & F.2 = y &
for i being Nat st 1 <= i & i < 2 holds
(i is odd implies [F.i,F.(i+1)] in a') &
(i is even implies [F.i,F.(i+1)] in b') by A45,LATTICE5:def 3;
consider j being Nat such that
A47: j = 0;
2*j+1 = 1 by A47;
then A48: 1 is odd & [F.1,F.(1+1)] in a' by A45,LATTICE5:def 3;
reconsider BC = b' /\ c' as Element of EqRelLATT A by A11;
A49: a'' <= a'' "\/" BC by YELLOW_0:22;
a' "\/" (b' /\ c') = a''"\/" BC by LATTICE5:10;
then a' c= a' "\/" (b' /\ c') by A49,LATTICE5:6;
hence thesis by A46,A48;
end;
A50: a'"\/"(b' /\ c') = a''"\/"(b''"/\"c'') by A11,LATTICE5:10
.= a"\/"(b"/\"c) by A11,YELLOW_0:71;
(a"\/"b)"/\"c = (a''"\/"b'')"/\"c'' by A12,YELLOW_0:70
.= (a''"\/"b'') /\ c' by LATTICE5:8
.= (a'"\/"b') /\ c' by LATTICE5:10;
hence thesis by A15,A19,A50,XBOOLE_0:def 10;
end;
theorem Th9:
for L be lower-bounded LATTICE
holds L has_a_representation_of_type<= 2 implies L is modular
proof
let L be lower-bounded LATTICE;
assume
L has_a_representation_of_type<= 2;
then consider A being non trivial set,
f being Homomorphism of L,EqRelLATT A such that
A1: f is one-to-one & Image f is finitely_typed &
(ex e being Equivalence_Relation of A st
e in the carrier of Image f & e <> id A) &
type_of Image f <= 2 by Def3;
A2: Image f is modular by A1,Th8;
A3: Image f is lower-bounded LATTICE &
corestr f is one-to-one by A1,Th6,WAYBEL_1:32;
A4: rng (corestr f) = the carrier of Image f by FUNCT_2:def 3;
A5: for x,y being Element of L holds
x <= y implies (corestr f).x <= (corestr f).y by WAYBEL_1:def 2;
for x,y being Element of L holds
(corestr f).x <= (corestr f).y implies x <= y by A1,Th7;
then corestr f is isomorphic by A3,A4,A5,WAYBEL_0:66;
then L, Image f are_isomorphic by WAYBEL_1:def 8;
then Image f, L are_isomorphic by WAYBEL_1:7;
hence thesis by A2,A3,Th5;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: <= :: L is modular implies L has_a_representation_of_type<= 2 ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let A be set;
func new_set2 A equals :Def4:
A \/ {{A}, {{A}}};
correctness;
end;
definition
let A be set;
cluster new_set2 A -> non empty;
coherence
proof
{A} in {{A}, {{A}}} by TARSKI:def 2;
then {A} in A \/ {{A}, {{A}}} by XBOOLE_0:def 2;
hence new_set2 A is non empty by Def4;
end;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
func new_bi_fun2(d,q) -> BiFunction of new_set2 A,L means :Def5:
(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}}) = (d.(q`1,q`2)"\/"q`3)"/\"q`4 &
it.({{A}},{A}) = (d.(q`1,q`2)"\/"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`2)"\/"q`3 &
it.({{A}},u) = d.(u,q`2)"\/"q`3);
existence
proof
set x = q`1, y = q`2;
reconsider a = q`3, b = q`4 as Element of L;
A1: {A} in new_set2 A & {{A}} in new_set2 A
proof
{A} in {{A}, {{A}} } by TARSKI:def 2;
then {A} in A \/ {{A}, {{A}}} by XBOOLE_0:def 2;
hence {A} in new_set2 A by Def4;
{{A}} in {{A}, {{A}} } by TARSKI:def 2;
then {{A}} in A \/ {{A}, {{A}}} by XBOOLE_0:def 2;
hence {{A}} in new_set2 A by Def4;
end;
defpred X[Element of new_set2 A,Element of new_set2 A,set] means
($1 in A & $2 in A implies $3 = d.($1,$2)) &
($1 = {A} & $2 = {{A}} or $2 = {A} & $1 = {{A}}
implies $3 = (d.(x,y)"\/"a)"/\"b) &
(($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',y)"\/"a) &
($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',y)"\/"a);
A2: for p,q being Element of new_set2 A
ex r being Element of L st X[p,q,r]
proof
let p,q be Element of new_set2 A;
p in new_set2 A & q in new_set2 A;
then p in A \/ {{A},{{A}}} & q in A \/ {{A},{{A}}} by Def4;
then A3: (p in A or p in {{A},{{A}}}) &
(q in A or q in {{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: not {A} in A by TARSKI:def 1;
A6: not {{A}} in A
proof
assume
A7: {{A}} in A;
A in {A} & {A} in {{A}} by TARSKI:def 1;
hence contradiction by A7,ORDINAL1:3;
end;
A8: (p = {A} or p = {{A}}) & p = q iff
p = {A} & q = {A} or p = {{A}} & q = {{A}};
per cases by A3,A8,TARSKI:def 2;
suppose
p in A & q in A;
then reconsider p'=p,q'=q as Element of A;
take d.(p',q');
thus thesis by A5,A6;
suppose
A9: p = {A} & q = {{A}} or q = {A} & p = {{A}};
take (d.(x,y)"\/"a)"/\"b;
thus thesis by A4,A6,A9,TARSKI:def 1;
suppose
A10: (p = {A} or p = {{A}}) & q = p;
take Bottom L;
thus thesis by A4,A6,A10,TARSKI:def 1;
suppose
A11: p in A & q = {A};
then reconsider p' = p as Element of A;
take d.(p',x)"\/"a;
thus thesis by A4,A6,A11,TARSKI:def 1;
suppose
A12: p in A & q = {{A}};
then reconsider p' = p as Element of A;
take d.(p',y)"\/"a;
thus thesis by A4,A6,A12,TARSKI:def 1;
suppose
A13: q in A & p = {A};
then reconsider q' = q as Element of A;
take d.(q',x)"\/"a;
thus thesis by A4,A6,A13,TARSKI:def 1;
suppose
A14: q in A & p = {{A}};
then reconsider q' = q as Element of A;
take d.(q',y)"\/"a;
thus thesis by A4,A6,A14,TARSKI:def 1;
end;
consider f being Function of [:new_set2 A,new_set2 A:],the carrier of L
such that
A15: for p,q being Element of new_set2 A holds X[p,q,f.[p,q]]
from FuncEx2D(A2);
reconsider f as BiFunction of new_set2 A,L;
take f;
A16: 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}}} & v in A \/ {{A}, {{A}}} by XBOOLE_0:def 2;
then reconsider u' = u, v' = v as Element of new_set2 A by Def4;
thus f.(u,v) = f.[u',v'] by BINOP_1:def 1
.= d.(u,v) by A15;
end;
A17: f.({A},{{A}}) = f.[{A},{{A}}] by BINOP_1:def 1
.= (d.(x,y)"\/"a)"/\"b by A1,A15;
A18: f.({{A}},{A}) = f.[{{A}},{A}] by BINOP_1:def 1
.= (d.(x,y)"\/"a)"/\"b by A1,A15;
A19: f.({A},{A}) = f.[{A},{A}] by BINOP_1:def 1
.= Bottom L by A1,A15;
A20: f.({{A}},{{A}}) = f.[{{A}},{{A}}] by BINOP_1:def 1
.= Bottom L by A1,A15;
A21: for u being Element of A
holds (f.(u,{A}) = d.(u,x)"\/"a & f.(u,{{A}}) = d.(u,y)"\/"a)
proof
let u be Element of A;
u in A \/ {{A}, {{A}}} by XBOOLE_0:def 2;
then reconsider u' = u as Element of new_set2 A by Def4;
consider u1 being Element of A such that
A22: u1 = u' & f.[u',{A}] = d.(u1,x)"\/"a by A1,A15;
thus f.(u,{A}) = d.(u,x)"\/"a by A22,BINOP_1:def 1;
consider u2 being Element of A such that
A23: u2 = u' & f.[u',{{A}}] = d.(u2,y)"\/"a by A1,A15;
thus f.(u,{{A}}) = d.(u,y)"\/"a by A23,BINOP_1:def 1;
end;
for u being Element of A holds (f.({A},u) = d.(u,x)"\/"a &
f.({{A}},u) = d.(u,y)"\/"a)
proof
let u be Element of A;
u in A \/ {{A}, {{A}}} by XBOOLE_0:def 2;
then reconsider u' = u as Element of new_set2 A by Def4;
consider u1 being Element of A such that
A24: u1 = u' & f.[{A},u'] = d.(u1,x)"\/"a by A1,A15;
thus f.({A},u) = d.(u,x)"\/"a by A24,BINOP_1:def 1;
consider u2 being Element of A such that
A25: u2 = u' & f.[{{A}},u'] = d.(u2,y)"\/"a by A1,A15;
thus f.({{A}},u) = d.(u,y)"\/"a by A25,BINOP_1:def 1;
end;
hence thesis by A16,A17,A18,A19,A20,A21;
end;
uniqueness
proof
set x = q`1, y = q`2, a = q`3;
let f1,f2 be BiFunction of new_set2 A,L such that
A26:(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}}) = (d.(q`1,q`2)"\/"q`3)"/\"q`4 &
f1.({{A}},{A}) = (d.(q`1,q`2)"\/"q`3)"/\"q`4 &
for u being Element of A holds
(f1.(u,{A}) = d.(u,q`1)"\/"q`3 &
f1.({A},u) = d.(u,q`1)"\/"q`3 &
f1.(u,{{A}}) = d.(u,q`2)"\/"q`3 &
f1.({{A}},u) = d.(u,q`2)"\/"q`3)
and
A27:(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}}) = (d.(q`1,q`2)"\/"q`3)"/\"q`4 &
f2.({{A}},{A}) = (d.(q`1,q`2)"\/"q`3)"/\"q`4 &
for u being Element of A holds
(f2.(u,{A}) = d.(u,q`1)"\/"q`3 &
f2.({A},u) = d.(u,q`1)"\/"q`3 &
f2.(u,{{A}}) = d.(u,q`2)"\/"q`3 &
f2.({{A}},u) = d.(u,q`2)"\/"q`3);
now
let p,q be Element of new_set2 A;
p in new_set2 A & q in new_set2 A;
then p in A \/ {{A},{{A}}} & q in A \/ {{A},{{A}}} by Def4;
then A28: (p in A or p in {{A},{{A}}}) &
(q in A or q in {{A},{{A}}}) by XBOOLE_0:def 2;
per cases by A28,TARSKI:def 2;
suppose
A29: p in A & q in A;
hence f1.(p,q) = d.(p,q) by A26
.= f2.(p,q) by A27,A29;
suppose
A30: p in A & q = {A};
then reconsider p' = p as Element of A;
thus f1.(p,q) = d.(p',x)"\/"a by A26,A30
.= f2.(p,q) by A27,A30;
suppose
A31: p in A & q = {{A}};
then reconsider p' = p as Element of A;
thus f1.(p,q) = d.(p',y)"\/"a by A26,A31
.= f2.(p,q) by A27,A31;
suppose
A32: p = {A} & q in A;
then reconsider q' = q as Element of A;
thus f1.(p,q) = d.(q',x)"\/"a by A26,A32
.= f2.(p,q) by A27,A32;
suppose p = {A} & q = {A};
hence f1.(p,q) = f2.(p,q) by A26,A27;
suppose p = {A} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A26,A27;
suppose
A33: p = {{A}} & q in A;
then reconsider q' = q as Element of A;
thus f1.(p,q) = d.(q',y)"\/"a by A26,A33
.= f2.(p,q) by A27,A33;
suppose p = {{A}} & q = {A};
hence f1.(p,q) = f2.(p,q) by A26,A27;
suppose p = {{A}} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A26,A27;
end;
hence f1 = f2 by BINOP_1:2;
end;
end;
theorem Th10:
for A being non empty set
for L being lower-bounded LATTICE
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_fun2(d,q) is zeroed
proof
let A be non empty set;
let L be lower-bounded LATTICE;
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_fun2(d,q);
for u being Element of new_set2 A holds f.(u,u) = Bottom L
proof
let u be Element of new_set2 A;
u in new_set2 A;
then u in A \/ {{A},{{A}}} by Def4;
then A2: u in A or u in {{A},{{A}}} by XBOOLE_0:def 2;
per cases by A2,TARSKI:def 2;
suppose u in A;
then reconsider u' = u as Element of A;
thus f.(u,u) = d.(u',u') by Def5 .= Bottom L by A1,LATTICE5:def 7;
suppose u = {A} or u = {{A}};
hence f.(u,u) = Bottom L by Def5;
end;
hence thesis by LATTICE5:def 7;
end;
theorem Th11:
for A being non empty set
for L being lower-bounded LATTICE
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_fun2(d,q) is symmetric
proof
let A be non empty set;
let L be lower-bounded LATTICE;
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_fun2(d,q), x = q`1, y = q`2, a = q`3, b = q`4;
let p,q be Element of new_set2 A;
p in new_set2 A & q in new_set2 A;
then p in A \/ {{A},{{A}}} & q in A \/ {{A},{{A}}} by Def4;
then A2: (p in A or p in {{A},{{A}}}) & (q in A or q in {{A},{{A}}}) by
XBOOLE_0:def 2;
per cases by A2,TARSKI:def 2;
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 Def5
.= d.(q',p') by A1,LATTICE5:def 6
.= f.(q,p) by Def5;
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,Def5
.= f.(q,p) by A3,Def5;
suppose
A4: p in A & q = {{A}};
then reconsider p' = p as Element of A;
thus f.(p,q) = d.(p',y)"\/"a by A4,Def5
.= f.(q,p) by A4,Def5;
suppose
A5: p = {A} & q in A;
then reconsider q' = q as Element of A;
thus f.(p,q) = d.(q',x)"\/"a by A5,Def5
.= f.(q,p) by A5,Def5;
suppose
p = {A} & q = {A};
hence f.(p,q) = f.(q,p);
suppose
A6: p = {A} & q = {{A}};
hence f.(p,q) = (d.(x,y)"\/"a)"/\"b by Def5
.= f.(q,p) by A6,Def5;
suppose
A7: p = {{A}} & q in A;
then reconsider q' = q as Element of A;
thus f.(p,q) = d.(q',y)"\/"a by A7,Def5
.= f.(q,p) by A7,Def5;
suppose
A8: p = {{A}} & q = {A};
hence f.(p,q) = (d.(x,y)"\/"a)"/\"b by Def5
.= f.(q,p) by A8,Def5;
suppose
p = {{A}} & q = {{A}};
hence f.(p,q) = f.(q,p);
end;
theorem Th12:
for A being non empty set
for L being lower-bounded LATTICE st L is modular
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_fun2(d,q) is u.t.i.
proof
let A be non empty set;
let L be lower-bounded LATTICE;
assume
A1: L is modular;
let d be BiFunction of A,L;
assume that
A2: d is symmetric and
A3: d is u.t.i.;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set x = q`1, y = q`2, a = q`3, b = q`4, f = new_bi_fun2(d,q);
assume
A4: d.(q`1,q`2) <= q`3"\/"q`4;
reconsider B = {{A}, {{A}}} as non empty set;
reconsider a,b as Element of L;
A5: for p,q,u being Element of new_set2 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_set2 A;
assume
p in A & q in A & u in A;
then reconsider p' = p, q' = q, u' = u as Element of A;
A6: f.(p,u) = d.(p',u') by Def5;
A7: f.(p,q) = d.(p',q') by Def5;
f.(q,u) = d.(q',u') by Def5;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A3,A6,A7,LATTICE5:def 8;
end;
A8: for p,q,u being Element of new_set2 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_set2 A;
assume
A9: p in A & q in A & u in B;
per cases by A9,TARSKI:def 2;
suppose
A10: p in A & q in A & u = {A};
then reconsider p' = p, q' = q as Element of A;
A11:f.(p,u) = d.(p',x)"\/"a by A10,Def5;
A12:f.(q,u) = d.(q',x)"\/"a by A10,Def5;
A13:f.(p,q) = d.(p',q') by Def5;
d.(p',x) <= d.(p',q') "\/" d.(q',x) by A3,LATTICE5:def 8;
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 A11,A12,A13,LATTICE3:14;
suppose
A14: p in A & q in A & u = {{A}};
then reconsider p' = p, q' = q as Element of A;
A15: f.(p,u) = d.(p',y)"\/"a by A14,Def5;
A16: f.(q,u) = d.(q',y)"\/"a by A14,Def5;
A17: f.(p,q) = d.(p',q') by Def5;
d.(p',y) <= d.(p',q') "\/" d.(q',y) by A3,LATTICE5:def 8;
then d.(p',y)"\/"a <= (d.(p',q') "\/" d.(q',y))"\/"a by WAYBEL_1:3;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A15,A16,A17,LATTICE3:14;
end;
A18: for p,q,u being Element of new_set2 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_set2 A;
assume
A19: p in A & q in B & u in A;
per cases by A19,TARSKI:def 2;
suppose
A20: p in A & u in A & q = {A};
then reconsider p' = p, u' = u as Element of A;
A21: f.(p,q) = d.(p',x)"\/"a by A20,Def5;
A22: f.(q,u) = d.(u',x)"\/"a by A20,Def5;
A23: d.(p',x) "\/" d.(u',x) <= (d.(p',x) "\/" d.(u',x))"\/"a by YELLOW_0:22;
A24: (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 A3,LATTICE5:def 8;
then d.(p',u') <= d.(p',x) "\/" d.(u',x) by A2,LATTICE5:def 6;
then d.(p',u') <= (d.(p',x)"\/"a) "\/" (d.(u',x)"\/"a) by A23,A24,ORDERS_1:
26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A21,A22,Def5;
suppose
A25: p in A & u in A & q = {{A}};
then reconsider p' = p, u' = u as Element of A;
A26: f.(p,q) = d.(p',y)"\/"a by A25,Def5;
A27: f.(q,u) = d.(u',y)"\/"a by A25,Def5;
A28: d.(p',y) "\/" d.(u',y) <= (d.(p',y) "\/" d.(u',y))"\/"a by YELLOW_0:22;
A29: (d.(p',y)"\/"d.(u',y))"\/"a = d.(p',y)"\/"(d.(u',y)"\/"a) by LATTICE3:14
.= d.(p',y)"\/"(d.(u',y)"\/"(a"\/"a)) by YELLOW_5:1
.= d.(p',y)"\/"((d.(u',y)"\/"a)"\/"a) by LATTICE3:14
.= (d.(p',y)"\/"a)"\/"(d.(u',y)"\/"a) by LATTICE3:14;
d.(p',u') <= d.(p',y) "\/" d.(y,u') by A3,LATTICE5:def 8;
then d.(p',u') <= d.(p',y) "\/" d.(u',y) by A2,LATTICE5:def 6;
then d.(p',u') <= (d.(p',y)"\/"a) "\/" (d.(u',y)"\/"a) by A28,A29,ORDERS_1:
26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A26,A27,Def5;
end;
A30: for p,q,u being Element of new_set2 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_set2 A;
assume
A31: p in A & q in B & u in B;
per cases by A31,TARSKI:def 2;
suppose
A32: p in A & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def5
.= f.(p,q) by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A32;
suppose
A33: p in A & q = {A} & u = {{A}};
then reconsider p' = p as Element of A;
A34: f.(p,q) = d.(p',x)"\/"a by A33,Def5;
A35: f.(q,u) = (d.(x,y)"\/"a)"/\"b by A33,Def5;
a <= a "\/" d.(x,y) by YELLOW_0:22;
then A36: a"\/"((d.(x,y)"\/"a)"/\"b) = (a"\/"b)"/\"(a"\/"
d.(x,y)) by A1,YELLOW11:def 3;
A37: d.(x,y)"\/"a = (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) by YELLOW_5:2;
a <= a;
then d.(x,y)"\/"a <= (a"\/"b)"\/"a by A4,YELLOW_3:3;
then (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a)
<= (d.(x,y)"\/"a)"/\"((a"\/"b)"\/"a) by YELLOW_5:6;
then A38: d.(p',x)"\/"((d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a))
<= d.(p',x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by WAYBEL_1:3;
f.(p,q) "\/" f.(q,u) = d.(p',x)"\/"((a"\/"b)"/\"(a"\/"
d.(x,y))) by A34,A35,A36,LATTICE3:14
.= d.(p',x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"a)"\/"b)) by YELLOW_5:1
.= d.(p',x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by LATTICE3:14;
then A39: (d.(p',x)"\/"d.(x,y))"\/"a <= f.(p,q) "\/" f.(q,u) by A37,A38,
LATTICE3:14;
d.(p',y) <= d.(p',x)"\/"d.(x,y) by A3,LATTICE5:def 8;
then d.(p',y)"\/"a <= (d.(p',x)"\/"d.(x,y))"\/"a by YELLOW_5:7;
then d.(p',y)"\/"a <= f.(p,q) "\/" f.(q,u) by A39,ORDERS_1:26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A33,Def5;
suppose
A40: p in A & q = {{A}} & u = {A};
then reconsider p' = p as Element of A;
A41: f.(p,q) = d.(p',y)"\/"a by A40,Def5;
A42: f.(q,u) = (d.(x,y)"\/"a)"/\"b by A40,Def5;
a <= a "\/" d.(x,y) by YELLOW_0:22;
then A43: a"\/"((d.(x,y)"\/"a)"/\"b) = (a"\/"b)"/\"(a"\/"
d.(x,y)) by A1,YELLOW11:def 3;
A44: d.(x,y)"\/"a = (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) by YELLOW_5:2;
a <= a;
then d.(x,y)"\/"a <= (a"\/"b)"\/"a by A4,YELLOW_3:3;
then (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a)
<= (d.(x,y)"\/"a)"/\"((a"\/"b)"\/"a) by YELLOW_5:6;
then A45: d.(p',y)"\/"((d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a))
<= d.(p',y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by WAYBEL_1:3;
f.(p,q) "\/" f.(q,u) = d.(p',y)"\/"((a"\/"b)"/\"(a"\/"
d.(x,y))) by A41,A42,A43,LATTICE3:14
.= d.(p',y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"a)"\/"b)) by YELLOW_5:1
.= d.(p',y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by LATTICE3:14;
then A46: (d.(p',y)"\/"d.(x,y))"\/"a <= f.(p,q) "\/" f.(q,u) by A44,A45,
LATTICE3:14;
d.(y,x) = d.(x,y) by A2,LATTICE5:def 6;
then d.(p',x) <= d.(p',y)"\/"d.(x,y) by A3,LATTICE5:def 8;
then d.(p',x)"\/"a <= (d.(p',y)"\/"d.(x,y))"\/"a by YELLOW_5:7;
then d.(p',x)"\/"a <= f.(p,q) "\/" f.(q,u) by A46,ORDERS_1:26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A40,Def5;
suppose
A47: p in A & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def5
.= f.(p,q) by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A47;
end;
A48: for p,q,u being Element of new_set2 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_set2 A;
assume
A49: p in B & q in A & u in A;
then reconsider q' = q, u' = u as Element of A;
per cases by A49,TARSKI:def 2;
suppose
A50: p = {A} & q in A & u in A;
then A51: f.(p,q) = d.(q',x)"\/"a by Def5;
A52: f.(q,u) = d.(q',u') by Def5;
d.(u',x) <= d.(u',q') "\/" d.(q',x) by A3,LATTICE5:def 8;
then d.(u',x) <= d.(q',u') "\/" d.(q',x) by A2,LATTICE5:def 6;
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 A50,A51,A52,Def5;
suppose
A53: p = {{A}} & q in A & u in A;
then A54: f.(p,q) = d.(q',y)"\/"a by Def5;
A55: f.(q,u) = d.(q',u') by Def5;
d.(u',y) <= d.(u',q') "\/" d.(q',y) by A3,LATTICE5:def 8;
then d.(u',y) <= d.(q',u') "\/" d.(q',y) by A2,LATTICE5:def 6;
then d.(u',y)"\/"a <= (d.(q',y)"\/"d.(q',u'))"\/"a by WAYBEL_1:3;
then d.(u',y)"\/"a <= (d.(q',y)"\/"a)"\/"d.(q',u') by LATTICE3:14;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A53,A54,A55,Def5;
end;
A56: for p,q,u being Element of new_set2 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_set2 A;
assume
A57: p in B & q in A & u in B;
per cases by A57,TARSKI:def 2;
suppose
q in A & p = {A} & u = {A};
then f.(p,u) = Bottom L by Def5;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
suppose
A58: q in A & p = {A} & u = {{A}};
then reconsider q' = q as Element of A;
A59: f.(p,u) = (d.(x,y)"\/"a)"/\"b by A58,Def5;
f.(p,q) = d.(q',x)"\/"a by A58,Def5;
then A60: f.(p,q) "\/" f.(q,u) = d.(q',x)"\/"a"\/"(d.(q',y)"\/"a) by A58,Def5
.= d.(q',x)"\/"(d.(q',y)"\/"a)"\/"a by LATTICE3:14
.= d.(q',x)"\/"d.(q',y)"\/"a"\/"a by LATTICE3:14
.= d.(q',x)"\/"d.(q',y)"\/"(a"\/"a) by LATTICE3:14
.= d.(q',x)"\/"d.(q',y)"\/"a by YELLOW_5:1;
d.(q',x) = d.(x,q') by A2,LATTICE5:def 6;
then d.(x,y) <= d.(q',x)"\/"d.(q',y) by A3,LATTICE5:def 8;
then A61: d.(x,y)"\/"a <= f.(p,q) "\/" f.(q,u) by A60,YELLOW_5:7;
(d.(x,y)"\/"a)"/\"b <= d.(x,y)"\/"a by YELLOW_0:23;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A59,A61,ORDERS_1:26;
suppose
A62: q in A & p = {{A}} & u = {A};
then reconsider q' = q as Element of A;
A63: f.(p,u) = (d.(x,y)"\/"a)"/\"b by A62,Def5;
f.(p,q) = d.(q',y)"\/"a by A62,Def5;
then A64: f.(p,q) "\/" f.(q,u) = d.(q',x)"\/"a"\/"(d.(q',y)"\/"a) by A62,Def5
.= d.(q',x)"\/"(d.(q',y)"\/"a)"\/"a by LATTICE3:14
.= d.(q',x)"\/"d.(q',y)"\/"a"\/"a by LATTICE3:14
.= d.(q',x)"\/"d.(q',y)"\/"(a"\/"a) by LATTICE3:14
.= d.(q',x)"\/"d.(q',y)"\/"a by YELLOW_5:1;
d.(q',x) = d.(x,q') by A2,LATTICE5:def 6;
then d.(x,y) <= d.(q',x)"\/"d.(q',y) by A3,LATTICE5:def 8;
then A65: d.(x,y)"\/"a <= f.(p,q) "\/" f.(q,u) by A64,YELLOW_5:7;
(d.(x,y)"\/"a)"/\"b <= d.(x,y)"\/"a by YELLOW_0:23;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A63,A65,ORDERS_1:26;
suppose
q in A & p = {{A}} & u = {{A}};
then f.(p,u) = Bottom L by Def5;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
end;
A66: for p,q,u being Element of new_set2 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_set2 A;
assume
A67: p in B & q in B & u in A;
per cases by A67,TARSKI:def 2;
suppose
A68: u in A & q = {A} & p = {A};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/"f.(q,u) by Def5
.= f.(p,u) by A68,WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u);
suppose
A69: u in A & q = {A} & p = {{A}};
then reconsider u' = u as Element of A;
A70: f.(p,q) = (d.(x,y)"\/"a)"/\"b by A69,Def5;
A71: f.(q,u) = d.(u',x)"\/"a by A69,Def5;
a <= a "\/" d.(x,y) by YELLOW_0:22;
then A72: a"\/"((d.(x,y)"\/"a)"/\"b) = (a"\/"b)"/\"(a"\/"
d.(x,y)) by A1,YELLOW11:def 3;
A73: d.(x,y)"\/"a = (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) by YELLOW_5:2;
a <= a;
then d.(x,y)"\/"a <= (a"\/"b)"\/"a by A4,YELLOW_3:3;
then (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a)
<= (d.(x,y)"\/"a)"/\"((a"\/"b)"\/"a) by YELLOW_5:6;
then A74: d.(u',x)"\/"((d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a))
<= d.(u',x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by WAYBEL_1:3;
f.(p,q) "\/" f.(q,u) = d.(u',x)"\/"((a"\/"b)"/\"(a"\/"
d.(x,y))) by A70,A71,A72,LATTICE3:14
.= d.(u',x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"a)"\/"b)) by YELLOW_5:1
.= d.(u',x)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by LATTICE3:14;
then A75: (d.(u',x)"\/"d.(x,y))"\/"a <= f.(p,q) "\/" f.(q,u) by A73,A74,
LATTICE3:14;
d.(u',y) <= d.(u',x)"\/"d.(x,y) by A3,LATTICE5:def 8;
then d.(u',y)"\/"a <= (d.(u',x)"\/"d.(x,y))"\/"a by YELLOW_5:7;
then d.(u',y)"\/"a <= f.(p,q) "\/" f.(q,u) by A75,ORDERS_1:26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A69,Def5;
suppose
A76: u in A & q = {{A}} & p = {A};
then reconsider u' = u as Element of A;
A77: f.(p,q) = (d.(x,y)"\/"a)"/\"b by A76,Def5;
A78: f.(q,u) = d.(u',y)"\/"a by A76,Def5;
a <= a "\/" d.(x,y) by YELLOW_0:22;
then A79: a"\/"((d.(x,y)"\/"a)"/\"b) = (a"\/"b)"/\"(a"\/"
d.(x,y)) by A1,YELLOW11:def 3;
A80: d.(x,y)"\/"a = (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a) by YELLOW_5:2;
a <= a;
then d.(x,y)"\/"a <= (a"\/"b)"\/"a by A4,YELLOW_3:3;
then (d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a)
<= (d.(x,y)"\/"a)"/\"((a"\/"b)"\/"a) by YELLOW_5:6;
then A81: d.(u',y)"\/"((d.(x,y)"\/"a)"/\"(d.(x,y)"\/"a))
<= d.(u',y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by WAYBEL_1:3;
f.(p,q) "\/" f.(q,u) = d.(u',y)"\/"((a"\/"b)"/\"(a"\/"
d.(x,y))) by A77,A78,A79,LATTICE3:14
.= d.(u',y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"a)"\/"b)) by YELLOW_5:1
.= d.(u',y)"\/"((d.(x,y)"\/"a)"/\"((a"\/"b)"\/"
a)) by LATTICE3:14;
then A82: (d.(u',y)"\/"d.(x,y))"\/"a <= f.(p,q) "\/" f.(q,u) by A80,A81,
LATTICE3:14;
d.(y,x) = d.(x,y) by A2,LATTICE5:def 6;
then d.(u',x) <= d.(u',y)"\/"d.(x,y) by A3,LATTICE5:def 8;
then d.(u',x)"\/"a <= (d.(u',y)"\/"d.(x,y))"\/"a by YELLOW_5:7;
then d.(u',x)"\/"a <= f.(p,q) "\/" f.(q,u) by A82,ORDERS_1:26;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A76,Def5;
suppose
A83: u in A & q = {{A}} & p = {{A}};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/"f.(q,u) by Def5
.= f.(p,u) by A83,WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u);
end;
A84: for p,q,u being Element of new_set2 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_set2 A;
assume
A85:p in B & q in B & u in B;
per cases by A85,TARSKI:def 2;
suppose
A86: 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 A86,Def5;
suppose
A87: p = {A} & q = {A} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L "\/" f.(p,u) by Def5
.= Bottom L "\/" ((d.(x,y)"\/"a)"/\"b) by A87,Def5
.= ((d.(x,y)"\/"a)"/\"b) by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A87,Def5;
suppose
A88: 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 A88,Def5;
suppose
A89: p = {A} & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = ((d.(x,y)"\/"a)"/\"b)"\/"f.(q,u) by Def5
.= Bottom L"\/"((d.(x,y)"\/"a)"/\"b) by A89,Def5
.= ((d.(x,y)"\/"a)"/\"b) by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A89,Def5;
suppose
A90: p = {{A}} & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = ((d.(x,y)"\/"a)"/\"b)"\/" f.(q,u) by Def5
.= Bottom L"\/"((d.(x,y)"\/"a)"/\"b) by A90,Def5
.= ((d.(x,y)"\/"a)"/\"b) by WAYBEL_1:4
.= f.(p,q) by A90,Def5;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A90;
suppose
A91: 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 A91,Def5;
suppose
A92: p = {{A}} & q = {{A}} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def5
.= Bottom L"\/"((d.(x,y)"\/"a)"/\"b) by A92,Def5
.= ((d.(x,y)"\/"a)"/\"b) by WAYBEL_1:4;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A92,Def5;
suppose
A93: 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 A93,Def5;
end;
for p,q,u being Element of new_set2 A holds f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set2 A;
p in new_set2 A & q in new_set2 A & u in new_set2 A;
then A94: p in A \/ B & q in A \/ B & u in A \/ B by Def4;
per cases by A94,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 A5;
suppose p in A & q in A & u in B;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A8;
suppose p in A & q in B & u in A;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A18;
suppose p in A & q in B & u in B;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A30;
suppose p in B & q in A & u in A;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A48;
suppose p in B & q in A & u in B;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A56;
suppose p in B & q in B & u in A;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A66;
suppose p in B & q in B & u in B;
hence f.(p,u) <= f.(p,q) "\/" f.(q,u) by A84;
end;
hence f is u.t.i. by LATTICE5:def 8;
end;
theorem Th13:
for A be set holds A c= new_set2 A
proof
let A be set;
A c= A \/ {{A}, {{A}}} by XBOOLE_1:7;
hence thesis by Def4;
end;
theorem Th14:
for A being non empty set
for L being lower-bounded LATTICE
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_fun2(d,q)
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set g = new_bi_fun2(d,q);
A1: dom d = [:A,A:] & dom g = [:new_set2 A,new_set2 A:] by FUNCT_2:def 1;
A c= new_set2 A by Th13;
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 being set 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 Def5
.= g.[x,y] by BINOP_1:def 1;
hence d.z = g.z by A4;
end;
hence d c= new_bi_fun2(d,q) by A2,GRFUNC_1:8;
end;
reserve x,y for set, C for Ordinal, L0,L1 for T-Sequence;
definition
let A be non empty set;
let O be Ordinal;
func ConsecutiveSet2(A,O) means :Def6:
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_set2(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_set2 $2;
deffunc D(set,T-Sequence) = union rng $2;
thus (ex x,L0 st x = last L0 & dom L0 = succ O & L0.{} = A &
(for C st succ C in succ O holds L0.succ C = C(C,L0.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) ) &
for x1,x2 being set st
(ex L0 st x1 = last L0 & dom L0 = succ O & L0.{} = A &
(for C st succ C in succ O holds L0.succ C = C(C,L0.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) ) &
(ex L0 st x2 = last L0 & dom L0 = succ O & L0.{} = A &
(for C st succ C in succ O holds L0.succ C = C(C,L0.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) )
holds x1 = x2 from TS_Def;
end;
end;
theorem Th15:
for A being non empty set holds ConsecutiveSet2(A,{}) = A
proof
let A be non empty set;
deffunc C(Ordinal,set) = new_set2 $2;
deffunc D(set,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveSet2(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 = C(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def6;
thus F({}) = A from TS_Result0(A1);
end;
theorem Th16:
for A being non empty set
for O being Ordinal
holds ConsecutiveSet2(A,succ O) = new_set2 ConsecutiveSet2(A,O)
proof
let A be non empty set;
let O be Ordinal;
deffunc C(Ordinal,set) = new_set2 $2;
deffunc D(set,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveSet2(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 = C(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def6;
for O being Ordinal holds F(succ O) = C(O,F(O)) from TS_ResultS(A1);
hence thesis;
end;
theorem Th17:
for A being non empty set
for O being Ordinal
for T being T-Sequence
holds O <> {} & O is_limit_ordinal & dom T = O & (for O1 being Ordinal
st O1 in O holds T.O1 = ConsecutiveSet2(A,O1))
implies ConsecutiveSet2(A,O) = union rng T
proof
let A be non empty set;
let O be Ordinal;
let T be T-Sequence;
deffunc C(Ordinal,set) = new_set2 $2;
deffunc D(set,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveSet2(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, 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 = C(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def6;
thus F(O) = D(O,T) from TS_ResultL(A4,A1,A2,A3);
end;
reserve O1,O2 for Ordinal;
definition
let A be non empty set;
let O be Ordinal;
cluster ConsecutiveSet2(A,O) -> non empty;
coherence
proof
defpred X[Ordinal] means ConsecutiveSet2(A,$1) is non empty;
A1: X[{}] by Th15;
A2: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume ConsecutiveSet2(A,O1) is non empty;
ConsecutiveSet2(A,succ O1) = new_set2 ConsecutiveSet2(A,O1) by Th16;
hence ConsecutiveSet2(A,succ O1) is non empty;
end;
A3: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof let O1 be Ordinal;
assume
A4: O1 <> {} & O1 is_limit_ordinal &
for O2 being Ordinal st O2 in O1
holds ConsecutiveSet2(A,O2) is non empty;
deffunc U(Ordinal) = ConsecutiveSet2(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: ConsecutiveSet2(A,O1) = union rng Ls by A4,A5,Th17;
A7: {} in O1 by A4,ORDINAL3:10;
then Ls.{} = ConsecutiveSet2(A,{}) by A5
.= A by Th15;
then A in rng Ls by A5,A7,FUNCT_1:def 5;
then A8: A c= ConsecutiveSet2(A,O1) by A6,ZFMISC_1:92;
consider x being set such that A9:x in A by XBOOLE_0:def 1;
thus ConsecutiveSet2(A,O1) is non empty by A8,A9;
end;
for O being Ordinal holds X[O]
from Ordinal_Ind(A1,A2,A3);
hence thesis;
end;
end;
theorem Th18:
for A being non empty set
for O being Ordinal holds A c= ConsecutiveSet2(A,O)
proof
let A be non empty set;
let O be Ordinal;
defpred X[Ordinal] means A c= ConsecutiveSet2(A,$1);
A1: X[{}] by Th15;
A2: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume
A3: A c= ConsecutiveSet2(A,O1);
ConsecutiveSet2(A,succ O1) = new_set2 ConsecutiveSet2(A,O1) by Th16;
then ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,succ O1) by Th13;
hence A c= ConsecutiveSet2(A,succ O1) by A3,XBOOLE_1:1;
end;
A4: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof
let O2 be Ordinal;
assume
A5: O2 <> {} & O2 is_limit_ordinal &
for O1 be Ordinal st O1 in O2 holds A c= ConsecutiveSet2(A,O1);
deffunc U(Ordinal) = ConsecutiveSet2(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: ConsecutiveSet2(A,O2) = union rng Ls by A5,A6,Th17;
A8: {} in O2 by A5,ORDINAL3:10;
then Ls.{} = ConsecutiveSet2(A,{}) by A6 .= A by Th15;
then A in rng Ls by A6,A8,FUNCT_1:def 5;
hence A c= ConsecutiveSet2(A,O2) by A7,ZFMISC_1:92;
end;
for O being Ordinal holds X[O]
from Ordinal_Ind(A1,A2,A4);
hence thesis;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
assume A1: O in dom q;
func Quadr2(q,O) -> Element of [:ConsecutiveSet2(A,O),ConsecutiveSet2(A,O),
the carrier of L,the carrier of L:] equals :Def7:
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 LATTICE5:def 14;
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= ConsecutiveSet2(A,O) by Th18;
then reconsider x,y as Element of ConsecutiveSet2(A,O) by A3;
reconsider a,b as Element of L;
reconsider z = [x,y,a,b] as Element of
[:ConsecutiveSet2(A,O),ConsecutiveSet2(A,O),
the carrier of L,the carrier of L:];
z = q.O by A2;
hence thesis;
end;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
func ConsecutiveDelta2(q,O) means :Def8:
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_fun2(BiFun(L0.C,ConsecutiveSet2(A,C),L),Quadr2(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_fun2(BiFun($2,ConsecutiveSet2(A,$1),L),Quadr2(q,$1));
deffunc D(set,T-Sequence) = union rng $2;
thus (ex x,L0 st x = last L0 & dom L0 = succ O & L0.{} = d &
(for C st succ C in succ O holds L0.succ C = C(C,L0.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C)) &
for x1,x2 being set st
(ex L0 st x1 = last L0 & dom L0 = succ O & L0.{} = d &
(for C st succ C in succ O holds L0.succ C = C(C,L0.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) ) &
(ex L0 st x2 = last L0 & dom L0 = succ O & L0.{} = d &
(for C st succ C in succ O holds L0.succ C = C(C,L0.C)) &
for C st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) )
holds x1 = x2 from TS_Def;
end;
end;
theorem Th19:
for A being non empty set
for L be lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta2(q,{}) = d
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
deffunc C(Ordinal,set) =
new_bi_fun2(BiFun($2,ConsecutiveSet2(A,$1),L),Quadr2(q,$1));
deffunc D(set,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveDelta2(q,$1);
A1: for O being Ordinal, It being set holds It = F(O) iff
ex L0 being T-Sequence st It = last L0 & dom L0 = succ O &
L0.{} = d &
(for C being Ordinal st succ C in succ O holds L0.succ C = C(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def8;
thus F({}) = d from TS_Result0(A1);
end;
theorem Th20:
for A being non empty set
for L be lower-bounded LATTICE
for d be BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds
ConsecutiveDelta2(q,succ O) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O),
ConsecutiveSet2(A,O),L),Quadr2(q,O))
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
deffunc C(Ordinal,set) =
new_bi_fun2(BiFun($2,ConsecutiveSet2(A,$1),L),Quadr2(q,$1));
deffunc D(set,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveDelta2(q,$1);
A1: for O being Ordinal, It being set holds It = F(O) iff
ex L0 being T-Sequence st It = last L0 & dom L0 = succ O &
L0.{} = d &
(for C being Ordinal st succ C in succ O holds L0.succ C = C(C,L0.C)) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def8;
for O being Ordinal holds F(succ O) = C(O,F(O)) from TS_ResultS(A1);
hence thesis;
end;
theorem Th21:
for A being non empty set
for L be lower-bounded LATTICE
for d be BiFunction of A,L
for q being QuadrSeq of d
for T being T-Sequence
for O being Ordinal holds O <> {} & O is_limit_ordinal & dom T = O &
(for O1 being Ordinal st O1 in O holds T.O1 = ConsecutiveDelta2(q,O1))
implies ConsecutiveDelta2(q,O) = union rng T
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let T be T-Sequence;
let O be Ordinal;
deffunc C(Ordinal,set) =
new_bi_fun2(BiFun($2,ConsecutiveSet2(A,$1),L),Quadr2(q,$1));
deffunc D(set,T-Sequence) = union rng $2;
deffunc F(Ordinal) = ConsecutiveDelta2(q,$1);
assume that
A1: O <> {} & O is_limit_ordinal and
A2: dom T = O and
A3: for O1 being Ordinal st O1 in O holds T.O1 = F(O1);
A4: for O being Ordinal, It being set holds It = F(O) iff
ex L0 being T-Sequence st It = last L0 & dom L0 = succ O & L0.{} = d &
(for C being Ordinal st succ C in succ O holds L0.succ C = C(C,L0.C) ) &
for C being Ordinal st C in succ O & C <> {} & C is_limit_ordinal
holds L0.C = D(C,L0|C) by Def8;
thus F(O) = D(O,T) from TS_ResultL(A4,A1,A2,A3);
end;
theorem Th22:
for A being non empty set
for O,O1,O2 being Ordinal
holds O1 c= O2 implies ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2)
proof
let A be non empty set;
let O,O1,02 be Ordinal;
defpred X[Ordinal] means O1 c= $1 implies
ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,$1);
A1: X[{}] by XBOOLE_1:3;
A2: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O2 be Ordinal;
assume
A3: O1 c= O2 implies ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2);
assume
A4: O1 c= succ O2;
per cases;
suppose O1 = succ O2;
hence ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,succ O2);
suppose O1 <> succ O2;
then O1 c< succ O2 by A4,XBOOLE_0:def 8;
then A5: O1 in succ O2 by ORDINAL1:21;
ConsecutiveSet2(A,O2) c= new_set2 ConsecutiveSet2(A,O2) by Th13;
then ConsecutiveSet2(A,O1) c=
new_set2 ConsecutiveSet2(A,O2) by A3,A5,ORDINAL1:34,XBOOLE_1:1;
hence ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,succ O2) by Th16;
end;
A6: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof
let O2 be Ordinal;
assume
A7: O2 <> {} & O2 is_limit_ordinal &
for O3 being Ordinal st O3 in O2 holds O1 c= O3 implies
ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O3);
assume
A8: O1 c= O2;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider L being T-Sequence such that
A9: dom L = O2 & for O3 being Ordinal st O3 in O2 holds
L.O3 = U(O3) from TS_Lambda;
A10: ConsecutiveSet2(A,O2) = union rng L by A7,A9,Th17;
per cases;
suppose O1 = O2;
hence ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2);
suppose O1 <> O2;
then O1 c< O2 by A8,XBOOLE_0:def 8;
then A11: O1 in O2 by ORDINAL1:21;
then A12: L.O1 = ConsecutiveSet2(A,O1) by A9;
L.O1 in rng L by A9,A11,FUNCT_1:def 5;
hence ConsecutiveSet2(A,O1) c= ConsecutiveSet2(A,O2)
by A10,A12,ZFMISC_1:92;
end;
for O being Ordinal holds X[O]
from Ordinal_Ind(A1,A2,A6);
hence thesis;
end;
theorem Th23:
for A being non empty set
for L be lower-bounded LATTICE
for d be BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal
holds ConsecutiveDelta2(q,O) is BiFunction of ConsecutiveSet2(A,O),L
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
defpred X[Ordinal] means
ConsecutiveDelta2(q,$1) is BiFunction of ConsecutiveSet2(A,$1),L;
A1: X[{}]
proof
ConsecutiveDelta2(q,{}) = d & ConsecutiveSet2(A,{}) = A by Th15,Th19;
hence ConsecutiveDelta2(q,{}) is BiFunction of ConsecutiveSet2(A,{}),L;
end;
A2: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume
ConsecutiveDelta2(q,O1) is BiFunction of ConsecutiveSet2(A,O1),L;
then reconsider CD = ConsecutiveDelta2(q,O1) as
BiFunction of ConsecutiveSet2(A,O1),L;
X: ConsecutiveSet2(A,succ O1) = new_set2 ConsecutiveSet2(A,O1) by Th16;
ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O1)
,
ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th20
.= new_bi_fun2(CD,Quadr2(q,O1)) by LATTICE5:def 16;
hence ConsecutiveDelta2(q,succ O1) is
BiFunction of ConsecutiveSet2(A,succ O1),L by X;
end;
A3: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof
let O1 be Ordinal;
assume
A4: O1 <> {} & O1 is_limit_ordinal &
for O2 be Ordinal st O2 in O1 holds
ConsecutiveDelta2(q,O2) is BiFunction of ConsecutiveSet2(A,O2),L;
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
consider Ls being T-Sequence such that
A5: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds
Ls.O2 = U(O2) from TS_Lambda;
A6: ConsecutiveDelta2(q,O1) = union rng Ls by A4,A5,Th21;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider Ts being T-Sequence such that
A7: dom Ts = O1 & for O2 being Ordinal st O2 in O1 holds
Ts.O2 = U(O2) from TS_Lambda;
set CS = ConsecutiveSet2(A,O1),
Y = the carrier of L,
X = [:ConsecutiveSet2(A,O1),ConsecutiveSet2(A,O1):],
f = union rng Ls;
A8: for O,O2 being Ordinal st O c= O2 & O2 in dom Ls holds Ls.O c= Ls.O2
proof
let O be Ordinal;
defpred X[Ordinal] means O c= $1 & $1 in dom Ls implies Ls.O c= Ls.$1;
A9: X[{}] by XBOOLE_1:3;
A10: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O2 be Ordinal;
assume
A11: O c= O2 & O2 in dom Ls implies Ls.O c= Ls.O2;
assume that
A12: O c= succ O2 and
A13: succ O2 in dom Ls;
per cases;
suppose O = succ O2;
hence Ls.O c= Ls.succ O2;
suppose O <> succ O2;
then O c< succ O2 by A12,XBOOLE_0:def 8;
then A14: O in succ O2 by ORDINAL1:21;
A15: O2 in succ O2 by ORDINAL1:10;
then A16: O2 in dom Ls by A13,ORDINAL1:19;
then reconsider Def8 = ConsecutiveDelta2(q,O2) as
BiFunction of ConsecutiveSet2(A,O2),L by A4,A5;
Ls.succ O2 = ConsecutiveDelta2(q,succ O2) by A5,A13
.= new_bi_fun2(BiFun(ConsecutiveDelta2(q,O2),
ConsecutiveSet2(A,O2),L),Quadr2(q,O2)) by Th20
.= new_bi_fun2(Def8,Quadr2(q,O2)) by LATTICE5:def 16;
then ConsecutiveDelta2(q,O2) c= Ls.succ O2 by Th14;
then Ls.O2 c= Ls.succ O2 by A5,A16;
hence Ls.O c= Ls.succ O2 by A11,A13,A14,A15,ORDINAL1:19,34,XBOOLE_1:
1;
end;
A17: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1
holds X[O2]
holds X[O1]
proof
let O2 be Ordinal;
assume that
A18: O2 <> {} & O2 is_limit_ordinal and
for O3 be Ordinal st O3 in O2 holds O c= O3 & O3 in dom Ls
implies Ls.O c= Ls.O3;
assume that
A19: O c= O2 and
A20: O2 in dom Ls;
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
consider Lt being T-Sequence such that
A21: dom Lt = O2 & for O3 being Ordinal st O3 in O2 holds
Lt.O3 = U(O3) from TS_Lambda;
A22: Ls.O2 = ConsecutiveDelta2(q,O2) by A5,A20
.= union rng Lt by A18,A21,Th21;
per cases;
suppose O = O2;
hence Ls.O c= Ls.O2;
suppose O <> O2;
then O c< O2 by A19,XBOOLE_0:def 8;
then A23: O in O2 by ORDINAL1:21;
then O in O1 by A5,A20,ORDINAL1:19;
then Ls.O = ConsecutiveDelta2(q,O) by A5
.= Lt.O by A21,A23;
then Ls.O in rng Lt by A21,A23,FUNCT_1:def 5;
hence Ls.O c= Ls.O2 by A22,ZFMISC_1:92;
end;
thus for O being Ordinal holds X[O]
from Ordinal_Ind(A9,A10,A17);
end;
for x,y being set st x in rng Ls & y in rng Ls holds x,y are_c=-comparable
proof
let x,y be set;
assume
A24: x in rng Ls & y in rng Ls;
then consider o1 being set such that
A25: o1 in dom Ls & Ls.o1 = x by FUNCT_1:def 5;
consider o2 being set such that
A26: o2 in dom Ls & Ls.o2 = y by A24,FUNCT_1:def 5;
reconsider o1' = o1, o2' = o2 as Ordinal by A25,A26,ORDINAL1:23;
o1' c= o2' or o2' c= o1';
then x c= y or y c= x by A8,A25,A26;
hence thesis by XBOOLE_0:def 9;
end;
then A27: rng Ls is c=-linear by ORDINAL1:def 9;
rng Ls c= PFuncs(X,Y)
proof
let z be set;
assume z in rng Ls;
then consider o being set such that
A28: o in dom Ls & z = Ls.o by FUNCT_1:def 5;
reconsider o as Ordinal by A28,ORDINAL1:23;
Ls.o = ConsecutiveDelta2(q,o) by A5,A28;
then reconsider h = Ls.o as
BiFunction of ConsecutiveSet2(A,o),L by A4,A5,A28;
A29: dom h = [:ConsecutiveSet2(A,o),ConsecutiveSet2(A,o):]
by FUNCT_2:def 1;
A30: rng h c= Y;
o c= O1 by A5,A28,ORDINAL1:def 2;
then ConsecutiveSet2(A,o) c= ConsecutiveSet2(A,O1) by Th22;
then dom h c= X by A29,ZFMISC_1:119;
hence z in PFuncs(X,Y) by A28,A30,PARTFUN1:def 5;
end;
then f in PFuncs(X,Y) by A27,HAHNBAN:13;
then consider g being Function such that
A31: f = g & dom g c= X & rng g c= Y by PARTFUN1:def 5;
reconsider f as Function by A31;
Ls is Function-yielding
proof
let x be set;
assume
A32: x in dom Ls;
then reconsider o = x as Ordinal by ORDINAL1:23;
Ls.o = ConsecutiveDelta2(q,o) by A5,A32;
hence Ls.x is Function by A4,A5,A32;
end;
then reconsider LsF = Ls as Function-yielding Function;
A33: dom f = union rng doms LsF by LATTICE5:1;
reconsider o1 = O1 as non empty Ordinal by A4;
set YY = { [:ConsecutiveSet2(A,O2),ConsecutiveSet2(A,O2):]
where O2 is Element of o1 : not contradiction };
A34: rng doms Ls = YY
proof
thus rng doms Ls c= YY
proof
let Z be set;
assume Z in rng doms Ls;
then consider o being set such that
A35: o in dom doms Ls & Z = (doms Ls).o by FUNCT_1:def 5;
A36: o in dom LsF by A35,EXTENS_1:3;
then reconsider o' = o as Element of o1 by A5;
Ls.o' = ConsecutiveDelta2(q,o') by A5;
then reconsider ls = Ls.o' as
BiFunction of ConsecutiveSet2(A,o'),L by A4;
Z = dom ls by A35,A36,FUNCT_6:31
.= [:ConsecutiveSet2(A,o'),ConsecutiveSet2(A,o'):]
by FUNCT_2:def 1;
hence Z in YY;
end;
let Z be set;
assume Z in YY;
then consider o being Element of o1 such that
A37: Z = [:ConsecutiveSet2(A,o),ConsecutiveSet2(A,o):];
o in dom LsF by A5;
then A38: o in dom doms LsF by EXTENS_1:3;
Ls.o = ConsecutiveDelta2(q,o) by A5;
then reconsider ls = Ls.o as
BiFunction of ConsecutiveSet2(A,o),L by A4;
Z = dom ls by A37,FUNCT_2:def 1
.= (doms Ls).o by A5,FUNCT_6:31;
hence Z in rng doms Ls by A38,FUNCT_1:def 5;
end;
{} in O1 by A4,ORDINAL3:10;
then reconsider RTs = rng Ts as non empty set by A7,FUNCT_1:12;
for x,y being set st x in RTs & y in RTs holds x,y are_c=-comparable
proof
let x,y be set;
assume
A39: x in RTs & y in RTs;
then consider o1 being set such that
A40: o1 in dom Ts & Ts.o1 = x by FUNCT_1:def 5;
consider o2 being set such that
A41: o2 in dom Ts & Ts.o2 = y by A39,FUNCT_1:def 5;
reconsider o1' = o1, o2' = o2 as Ordinal by A40,A41,ORDINAL1:23;
A42: Ts.o1' = ConsecutiveSet2(A,o1') by A7,A40;
A43: Ts.o2' = ConsecutiveSet2(A,o2') by A7,A41;
o1' c= o2' or o2' c= o1';
then x c= y or y c= x by A40,A41,A42,A43,Th22;
hence thesis by XBOOLE_0:def 9;
end;
then A44: RTs is c=-linear by ORDINAL1:def 9;
A45: YY = { [:a,a:] where a is Element of RTs : a in RTs }
proof
set XX = { [:a,a:] where a is Element of RTs : a in RTs };
thus YY c= XX
proof
let Z be set;
assume Z in YY;
then consider o being Element of o1 such that
A46: Z = [:ConsecutiveSet2(A,o),ConsecutiveSet2(A,o):];
Ts.o = ConsecutiveSet2(A,o) by A7;
then reconsider CoS = ConsecutiveSet2(A,o)
as Element of RTs by A7,FUNCT_1:def 5;
Z = [:CoS,CoS:] by A46;
hence Z in XX;
end;
let Z be set; assume Z in XX;
then consider a being Element of RTs such that
A47: Z = [:a,a:] & a in RTs;
consider o being set such that
A48: o in dom Ts & a = Ts.o by FUNCT_1:def 5;
reconsider o' = o as Ordinal by A48,ORDINAL1:23;
A49: a = ConsecutiveSet2(A,o') by A7,A48;
consider O being Element of o1 such that
A50: O = o' by A7,A48;
thus Z in YY by A47,A49,A50;
end;
X = [:union rng Ts, ConsecutiveSet2(A,O1):] by A4,A7,Th17
.= [:union RTs, union RTs :] by A4,A7,Th17
.= dom f by A33,A34,A44,A45,LATTICE5:3;
then f is Function of X,Y by A31,FUNCT_2:def 1,RELSET_1:11;
hence ConsecutiveDelta2(q,O1) is BiFunction of CS,L by A6;
end;
for O being Ordinal holds X[O]
from Ordinal_Ind(A1,A2,A3);
hence thesis;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
redefine func ConsecutiveDelta2(q,O) -> BiFunction of
ConsecutiveSet2(A,O),L;
coherence by Th23;
end;
theorem Th24:
for A being non empty set
for L be lower-bounded LATTICE
for d be BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal holds d c= ConsecutiveDelta2(q,O)
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
defpred X[Ordinal] means d c= ConsecutiveDelta2(q,$1);
A1: X[{}] by Th19;
A2: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume
A3: d c= ConsecutiveDelta2(q,O1);
ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O1)
,
ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th20
.= new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1))
by LATTICE5:def 16;
then ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,succ O1) by Th14;
hence d c= ConsecutiveDelta2(q,succ O1) by A3,XBOOLE_1:1;
end;
A4: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof
let O2 be Ordinal;
assume
A5: O2 <> {} & O2 is_limit_ordinal &
for O1 be Ordinal st O1 in O2 holds d c= ConsecutiveDelta2(q,O1);
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
consider Ls being T-Sequence such that
A6: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A7: ConsecutiveDelta2(q,O2) = union rng Ls by A5,A6,Th21;
A8: {} in O2 by A5,ORDINAL3:10;
then Ls.{} = ConsecutiveDelta2(q,{}) by A6
.= d by Th19;
then d in rng Ls by A6,A8,FUNCT_1:def 5;
hence d c= ConsecutiveDelta2(q,O2) by A7,ZFMISC_1:92;
end;
for O being Ordinal holds X[O]
from Ordinal_Ind(A1,A2,A4);
hence thesis;
end;
theorem Th25:
for A being non empty set
for L be lower-bounded LATTICE
for d being BiFunction of A,L
for O1,O2 being Ordinal
for q being QuadrSeq of d st O1 c= O2
holds ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O2)
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let O1,O2 be Ordinal;
let q be QuadrSeq of d;
defpred X[Ordinal] means
O1 c= $1 implies ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,$1);
A1: X[{}] by XBOOLE_1:3;
A2: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O2 be Ordinal;
assume
A3: O1 c= O2 implies ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O2);
assume
A4: O1 c= succ O2;
per cases;
suppose O1 = succ O2;
hence ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,succ O2);
suppose O1 <> succ O2;
then O1 c< succ O2 by A4,XBOOLE_0:def 8;
then A5: O1 in succ O2 by ORDINAL1:21;
ConsecutiveDelta2(q,succ O2)
= new_bi_fun2(BiFun(ConsecutiveDelta2(q,O2),
ConsecutiveSet2(A,O2),L),Quadr2(q,O2)) by Th20
.= new_bi_fun2(ConsecutiveDelta2(q,O2),Quadr2(q,O2))
by LATTICE5:def 16;
then ConsecutiveDelta2(q,O2) c= ConsecutiveDelta2(q,succ O2) by Th14;
hence ConsecutiveDelta2(q,O1) c=
ConsecutiveDelta2(q,succ O2) by A3,A5,ORDINAL1:34,XBOOLE_1:1
;
end;
A6: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof
let O2 be Ordinal;
assume
A7: O2 <> {} & O2 is_limit_ordinal &
for O3 be Ordinal st O3 in O2 holds O1 c= O3 implies
ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O3);
assume
A8: O1 c= O2;
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
consider L being T-Sequence such that
A9: dom L = O2 & for O3 being Ordinal st O3 in O2 holds
L.O3 = U(O3) from TS_Lambda;
A10: ConsecutiveDelta2(q,O2) = union rng L by A7,A9,Th21;
per cases;
suppose O1 = O2;
hence ConsecutiveDelta2(q,O1) c= ConsecutiveDelta2(q,O2);
suppose O1 <> O2;
then O1 c< O2 by A8,XBOOLE_0:def 8;
then A11: O1 in O2 by ORDINAL1:21;
then A12: L.O1 = ConsecutiveDelta2(q,O1) by A9;
L.O1 in rng L by A9,A11,FUNCT_1:def 5;
hence ConsecutiveDelta2(q,O1) c=
ConsecutiveDelta2(q,O2) by A10,A12,ZFMISC_1:92;
end;
for O being Ordinal holds X[O]
from Ordinal_Ind(A1,A2,A6);
hence thesis;
end;
theorem Th26:
for A being non empty set
for L be lower-bounded LATTICE
for d be BiFunction of A,L st d is zeroed
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2(q,O) is zeroed
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L; assume
A1: d is zeroed;
let q be QuadrSeq of d;
let O be Ordinal;
defpred X[Ordinal] means ConsecutiveDelta2(q,$1) is zeroed;
A2: X[{}]
proof
let z be Element of ConsecutiveSet2(A,{});
reconsider z' = z as Element of A by Th15;
thus ConsecutiveDelta2(q,{}).(z,z) = d.(z',z') by Th19
.= Bottom L by A1,LATTICE5:def 7;
end;
A3: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume ConsecutiveDelta2(q,O1) is zeroed;
then A4: new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) is zeroed by Th10;
let z be Element of ConsecutiveSet2(A,succ O1);
reconsider z' = z as Element of new_set2 ConsecutiveSet2(A,O1) by Th16;
ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O1),
ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th20
.= new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) by LATTICE5:def 16;
hence ConsecutiveDelta2(q,succ O1).(z,z) =
new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)).(z',z')
.= Bottom L by A4,LATTICE5:def 7;
end;
A5: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof
let O2 be Ordinal;
assume
A6: O2 <> {} & O2 is_limit_ordinal &
for O1 be Ordinal st O1 in O2 holds ConsecutiveDelta2(q,O1) is zeroed;
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
consider Ls being T-Sequence such that
A7: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A8: ConsecutiveDelta2(q,O2) = union rng Ls by A6,A7,Th21;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider Ts being T-Sequence such that
A9: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds
Ts.O1 = U(O1) from TS_Lambda;
A10: ConsecutiveSet2(A,O2) = union rng Ts by A6,A9,Th17;
set CS = ConsecutiveSet2(A,O2);
reconsider f = union rng Ls as BiFunction of CS,L by A8;
f is zeroed
proof
let x be Element of CS;
consider y being set such that
A11: x in y & y in rng Ts by A10,TARSKI:def 4;
consider o being set such that
A12: o in dom Ts & y = Ts.o by A11,FUNCT_1:def 5;
reconsider o as Ordinal by A12,ORDINAL1:23;
A13: x in ConsecutiveSet2(A,o) by A9,A11,A12;
A14: Ls.o = ConsecutiveDelta2(q,o) by A7,A9,A12;
then reconsider h = Ls.o as BiFunction of ConsecutiveSet2(A,o),L;
A15: h is zeroed
proof
let z be Element of ConsecutiveSet2(A,o);
A16: ConsecutiveDelta2(q,o) is zeroed by A6,A9,A12;
thus h.(z,z) = ConsecutiveDelta2(q,o).(z,z) by A7,A9,A12
.= Bottom L by A16,LATTICE5:def 7;
end;
ConsecutiveDelta2(q,o) in rng Ls by A7,A9,A12,A14,FUNCT_1:def 5;
then A17: h c= f by A14,ZFMISC_1:92;
reconsider x' = x as Element of ConsecutiveSet2(A,o) by A9,A11,A12;
dom h = [:ConsecutiveSet2(A,o),ConsecutiveSet2(A,o):]
by FUNCT_2:def 1;
then A18: [x,x] in dom h by A13,ZFMISC_1:106;
thus f.(x,x) = f.[x,x] by BINOP_1:def 1
.= h.[x,x] by A17,A18,GRFUNC_1:8
.= h.(x',x') by BINOP_1:def 1
.= Bottom L by A15,LATTICE5:def 7;
end;
hence ConsecutiveDelta2(q,O2) is zeroed by A6,A7,Th21;
end;
for O being Ordinal holds X[O]
from Ordinal_Ind(A2,A3,A5);
hence thesis;
end;
theorem Th27:
for A being non empty set
for L be lower-bounded LATTICE
for d be BiFunction of A,L st d is symmetric
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2(q,O) is symmetric
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L; assume
A1: d is symmetric;
let q be QuadrSeq of d;
let O be Ordinal;
defpred X[Ordinal] means ConsecutiveDelta2(q,$1) is symmetric;
A2: X[{}]
proof
let x,y be Element of ConsecutiveSet2(A,{});
reconsider x' = x, y' = y as Element of A by Th15;
thus ConsecutiveDelta2(q,{}).(x,y) = d.(x',y') by Th19
.= d.(y',x') by A1,LATTICE5:def 6
.= ConsecutiveDelta2(q,{}).(y,x) by Th19;
end;
A3: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume ConsecutiveDelta2(q,O1) is symmetric;
then A4: new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) is symmetric by
Th11;
let x,y be Element of ConsecutiveSet2(A,succ O1);
reconsider x'=x, y'=y as Element of new_set2 ConsecutiveSet2(A,O1)
by Th16;
A5: ConsecutiveDelta2(q,succ O1) = new_bi_fun2(BiFun(ConsecutiveDelta2(q,O1),
ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th20
.= new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) by LATTICE5:def 16;
hence ConsecutiveDelta2(q,succ O1).(x,y) =
new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)).(y',x')
by A4,LATTICE5:def 6
.= ConsecutiveDelta2(q,succ O1).(y,x) by A5;
end;
A6: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof
let O2 be Ordinal;
assume
A7: O2 <> {} & O2 is_limit_ordinal &
for O1 being Ordinal st O1 in O2
holds ConsecutiveDelta2(q,O1) is symmetric;
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
consider Ls being T-Sequence such that
A8: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A9: ConsecutiveDelta2(q,O2) = union rng Ls by A7,A8,Th21;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider Ts being T-Sequence such that
A10: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds
Ts.O1 = U(O1) from TS_Lambda;
A11: ConsecutiveSet2(A,O2) = union rng Ts by A7,A10,Th17;
set CS = ConsecutiveSet2(A,O2);
reconsider f = union rng Ls as BiFunction of CS,L by A9;
f is symmetric
proof
let x,y be Element of CS;
consider x1 being set such that
A12: x in x1 & x1 in rng Ts by A11,TARSKI:def 4;
consider o1 being set such that
A13: o1 in dom Ts & x1 = Ts.o1 by A12,FUNCT_1:def 5;
consider y1 being set such that
A14: y in y1 & y1 in rng Ts by A11,TARSKI:def 4;
consider o2 being set such that
A15: o2 in dom Ts & y1 = Ts.o2 by A14,FUNCT_1:def 5;
reconsider o1,o2 as Ordinal by A13,A15,ORDINAL1:23;
A16: x in ConsecutiveSet2(A,o1) by A10,A12,A13;
A17: y in ConsecutiveSet2(A,o2) by A10,A14,A15;
A18: Ls.o1 = ConsecutiveDelta2(q,o1) by A8,A10,A13;
then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet2(A,o1),L;
A19: h1 is symmetric
proof
let x,y be Element of ConsecutiveSet2(A,o1);
A20: ConsecutiveDelta2(q,o1) is symmetric by A7,A10,A13;
thus h1.(x,y) = ConsecutiveDelta2(q,o1).(x,y) by A8,A10,A13 .=
ConsecutiveDelta2(q,o1).(y,x) by A20,LATTICE5:def 6
.= h1.(y,x) by A8,A10,A13;
end;
A21: dom h1 = [:ConsecutiveSet2(A,o1),ConsecutiveSet2(A,o1):]
by FUNCT_2:def 1;
A22: Ls.o2 = ConsecutiveDelta2(q,o2) by A8,A10,A15;
then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet2(A,o2),L;
A23: h2 is symmetric
proof
let x,y be Element of ConsecutiveSet2(A,o2);
A24: ConsecutiveDelta2(q,o2) is symmetric by A7,A10,A15;
thus h2.(x,y) = ConsecutiveDelta2(q,o2).(x,y) by A8,A10,A15
.= ConsecutiveDelta2(q,o2).(y,x) by A24,LATTICE5:def 6
.= h2.(y,x) by A8,A10,A15;
end;
A25: dom h2 = [:ConsecutiveSet2(A,o2),ConsecutiveSet2(A,o2):]
by FUNCT_2:def 1;
per cases;
suppose o1 c= o2;
then A26: ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o2) by Th22;
then reconsider x'=x, y'=y as Element of ConsecutiveSet2(A,o2)
by A10,A14,A15,A16;
ConsecutiveDelta2(q,o2) in rng Ls by A8,A10,A15,A22,FUNCT_1:def 5
;
then A27: h2 c= f by A22,ZFMISC_1:92;
A28: [x,y] in dom h2 & [y,x] in dom h2 by A16,A17,A25,A26,ZFMISC_1:106;
thus f.(x,y) = f.[x,y] by BINOP_1:def 1
.= h2.[x,y] by A27,A28,GRFUNC_1:8
.= h2.(x',y') by BINOP_1:def 1
.= h2.(y',x') by A23,LATTICE5:def 6
.= h2.[y,x] by BINOP_1:def 1
.= f.[y,x] by A27,A28,GRFUNC_1:8
.= f.(y,x) by BINOP_1:def 1;
suppose o2 c= o1;
then A29: ConsecutiveSet2(A,o2) c= ConsecutiveSet2(A,o1) by Th22;
then reconsider x'=x, y'=y as Element of ConsecutiveSet2(A,o1)
by A10,A12,A13,A17;
ConsecutiveDelta2(q,o1) in rng Ls by A8,A10,A13,A18,FUNCT_1:def 5
;
then A30: h1 c= f by A18,ZFMISC_1:92;
A31: [x,y] in dom h1 & [y,x] in dom h1 by A16,A17,A21,A29,ZFMISC_1:106;
thus f.(x,y) = f.[x,y] by BINOP_1:def 1
.= h1.[x,y] by A30,A31,GRFUNC_1:8
.= h1.(x',y') by BINOP_1:def 1
.= h1.(y',x') by A19,LATTICE5:def 6
.= h1.[y,x] by BINOP_1:def 1
.= f.[y,x] by A30,A31,GRFUNC_1:8
.= f.(y,x) by BINOP_1:def 1;
end;
hence ConsecutiveDelta2(q,O2) is symmetric by A7,A8,Th21;
end;
for O being Ordinal holds X[O]
from Ordinal_Ind(A2,A3,A6);
hence thesis;
end;
theorem Th28:
for A being non empty set
for L being lower-bounded LATTICE st
L is modular
for d be BiFunction of A,L st d is symmetric u.t.i.
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti(d)
holds ConsecutiveDelta2(q,O) is u.t.i.
proof
let A be non empty set;
let L be lower-bounded LATTICE;
assume
A1: L is modular;
let d be BiFunction of A,L;
assume that
A2: d is symmetric and
A3: d is u.t.i.;
let O be Ordinal;
let q be QuadrSeq of d;
defpred X[Ordinal] means
$1 c= DistEsti(d) implies ConsecutiveDelta2(q,$1) is u.t.i.;
A4: X[{}]
proof
assume {} c= DistEsti(d);
let x,y,z be Element of ConsecutiveSet2(A,{});
reconsider x' = x, y' = y, z' = z as Element of A by Th15;
A5: ConsecutiveDelta2(q,{}) = d by Th19;
d.(x',z') <= d.(x',y') "\/" d.(y',z') by A3,LATTICE5:def 8;
hence ConsecutiveDelta2(q,{}).(x,z) <=
ConsecutiveDelta2(q,{}).(x,y) "\/" ConsecutiveDelta2(q,{}).(y,z) by A5;
end;
A6: for O1 being Ordinal st X[O1] holds X[succ O1]
proof
let O1 be Ordinal;
assume that
A7: O1 c= DistEsti(d) implies ConsecutiveDelta2(q,O1) is u.t.i. and
A8: succ O1 c= DistEsti(d);
A9: O1 in DistEsti(d) by A8,ORDINAL1:33;
A10: ConsecutiveDelta2(q,O1) is symmetric by A2,Th27;
let x,y,z be Element of ConsecutiveSet2(A,succ O1);
set f = new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1));
reconsider x' = x, y' = y, z' = z as
Element of new_set2 ConsecutiveSet2(A,O1) by Th16;
A11: O1 in dom q by A9,LATTICE5:28;
then q.O1 in rng q by FUNCT_1:def 5;
then q.O1 in {[u,v,a',b'] where u is Element of A, v is Element of A,
a' is Element of L, b' is Element of L: d.(u,v) <=
a'"\/"b'} by LATTICE5:def 14;
then consider u,v be Element of A, a',b' be Element of L such that
A12: q.O1 = [u,v,a',b'] & d.(u,v) <= a'"\/"b';
set X = Quadr2(q,O1)`1, Y = Quadr2(q,O1)`2;
reconsider a = Quadr2(q,O1)`3, b = Quadr2(q,O1)`4 as Element of L
;
A13: Quadr2(q,O1) = [u,v,a',b'] by A11,A12,Def7;
then A14: u = X by MCART_1:def 8;
A15: v = Y by A13,MCART_1:def 9;
A16: a' = a by A13,MCART_1:def 10;
A17: b' = b by A13,MCART_1:def 11;
A18: dom d = [:A,A:] by FUNCT_2:def 1;
A19: d c= ConsecutiveDelta2(q,O1) by Th24;
d.(u,v) = d.[u,v] by BINOP_1:def 1
.= ConsecutiveDelta2(q,O1).[X,Y] by A14,A15,A18,A19,GRFUNC_1:8
.= ConsecutiveDelta2(q,O1).(X,Y) by BINOP_1:def 1;
then A20: new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) is u.t.i.
by A1,A7,A9,A10,A12,A16,A17,Th12,ORDINAL1:def 2;
A21: ConsecutiveDelta2(q,succ O1) =
new_bi_fun2(BiFun(ConsecutiveDelta2(q,O1),
ConsecutiveSet2(A,O1),L),Quadr2(q,O1)) by Th20
.= new_bi_fun2(ConsecutiveDelta2(q,O1),Quadr2(q,O1)) by LATTICE5:def 16;
f.(x',z') <= f.(x',y') "\/" f.(y',z') by A20,LATTICE5:def 8;
hence ConsecutiveDelta2(q,succ O1).(x,z) <=
ConsecutiveDelta2(q,succ O1).(x,y) "\/" ConsecutiveDelta2(q,succ O1).(y,z)
by A21;
end;
A22: for O1 st O1 <> {} & O1 is_limit_ordinal & for O2 st O2 in O1 holds X[O2]
holds X[O1]
proof
let O2 be Ordinal;
assume that
A23: O2 <> {} & O2 is_limit_ordinal &
for O1 be Ordinal st O1 in O2 holds
(O1 c= DistEsti(d) implies ConsecutiveDelta2(q,O1) is u.t.i.) and
A24: O2 c= DistEsti(d);
deffunc U(Ordinal) = ConsecutiveDelta2(q,$1);
consider Ls being T-Sequence such that
A25: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds
Ls.O1 = U(O1) from TS_Lambda;
A26: ConsecutiveDelta2(q,O2) = union rng Ls by A23,A25,Th21;
deffunc U(Ordinal) = ConsecutiveSet2(A,$1);
consider Ts being T-Sequence such that
A27: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds
Ts.O1 = U(O1) from TS_Lambda;
A28: ConsecutiveSet2(A,O2) = union rng Ts by A23,A27,Th17;
set CS = ConsecutiveSet2(A,O2);
reconsider f = union rng Ls as BiFunction of CS,L by A26;
f is u.t.i.
proof
let x,y,z be Element of CS;
consider X being set such that
A29: x in X & X in rng Ts by A28,TARSKI:def 4;
consider o1 being set such that
A30: o1 in dom Ts & X = Ts.o1 by A29,FUNCT_1:def 5;
consider Y being set such that
A31: y in Y & Y in rng Ts by A28,TARSKI:def 4;
consider o2 being set such that
A32: o2 in dom Ts & Y = Ts.o2 by A31,FUNCT_1:def 5;
consider Z being set such that
A33: z in Z & Z in rng Ts by A28,TARSKI:def 4;
consider o3 being set such that
A34: o3 in dom Ts & Z = Ts.o3 by A33,FUNCT_1:def 5;
reconsider o1,o2,o3 as Ordinal by A30,A32,A34,ORDINAL1:23;
A35: x in ConsecutiveSet2(A,o1) by A27,A29,A30;
A36: y in ConsecutiveSet2(A,o2) by A27,A31,A32;
A37: z in ConsecutiveSet2(A,o3) by A27,A33,A34;
A38: Ls.o1 = ConsecutiveDelta2(q,o1) by A25,A27,A30;
then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet2(A,o1),L;
A39: h1 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet2(A,o1);
A40: ConsecutiveDelta2(q,o1) = h1 by A25,A27,A30;
o1 c= DistEsti(d) by A24,A27,A30,ORDINAL1:def 2;
then ConsecutiveDelta2(q,o1) is u.t.i. by A23,A27,A30;
hence h1.(x,z) <= h1.(x,y) "\/" h1.(y,z) by A40,LATTICE5:def 8;
end;
A41: dom h1 = [:ConsecutiveSet2(A,o1),ConsecutiveSet2(A,o1):]
by FUNCT_2:def 1;
A42: Ls.o2 = ConsecutiveDelta2(q,o2) by A25,A27,A32;
then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet2(A,o2),L;
A43: h2 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet2(A,o2);
A44: ConsecutiveDelta2(q,o2) = h2 by A25,A27,A32;
o2 c= DistEsti(d) by A24,A27,A32,ORDINAL1:def 2;
then ConsecutiveDelta2(q,o2) is u.t.i. by A23,A27,A32;
hence h2.(x,z) <= h2.(x,y) "\/" h2.(y,z) by A44,LATTICE5:def 8;
end;
A45: dom h2 = [:ConsecutiveSet2(A,o2),ConsecutiveSet2(A,o2):]
by FUNCT_2:def 1;
A46: Ls.o3 = ConsecutiveDelta2(q,o3) by A25,A27,A34;
then reconsider h3 = Ls.o3 as BiFunction of ConsecutiveSet2(A,o3),L;
A47: h3 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet2(A,o3);
A48: ConsecutiveDelta2(q,o3) = h3 by A25,A27,A34;
o3 c= DistEsti(d) by A24,A27,A34,ORDINAL1:def 2;
then ConsecutiveDelta2(q,o3) is u.t.i. by A23,A27,A34;
hence h3.(x,z) <= h3.(x,y) "\/" h3.(y,z) by A48,LATTICE5:def 8;
end;
A49: dom h3 = [:ConsecutiveSet2(A,o3),ConsecutiveSet2(A,o3):]
by FUNCT_2:def 1;
per cases;
suppose
A50: o1 c= o3;
then A51: ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o3) by Th22;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose o2 c= o3;
then A52: ConsecutiveSet2(A,o2) c= ConsecutiveSet2(A,o3) by Th22;
then reconsider y' = y as Element of ConsecutiveSet2(A,o3) by A36;
reconsider x' = x as Element of ConsecutiveSet2(A,o3) by A35,A51;
reconsider z' = z as Element of ConsecutiveSet2(A,o3) by A27,A33,A34;
ConsecutiveDelta2(q,o3) in rng Ls by A25,A27,A34,A46,FUNCT_1:def 5
;
then A53: h3 c= f by A46,ZFMISC_1:92;
A54: [x,y] in dom h3 by A35,A36,A49,A51,A52,ZFMISC_1:106;
A55: [y,z] in dom h3 by A36,A37,A49,A52,ZFMISC_1:106;
A56: [x,z] in dom h3 by A35,A37,A49,A51,ZFMISC_1:106;
A57: f.(x,y) = f.[x,y] by BINOP_1:def 1
.= h3.[x,y] by A53,A54,GRFUNC_1:8
.= h3.(x',y') by BINOP_1:def 1;
A58: f.(y,z) = f.[y,z] by BINOP_1:def 1
.= h3.[y,z] by A53,A55,GRFUNC_1:8
.= h3.(y',z') by BINOP_1:def 1;
f.(x,z) = f.[x,z] by BINOP_1:def 1
.= h3.[x,z] by A53,A56,GRFUNC_1:8
.= h3.(x',z') by BINOP_1:def 1;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A47,A57,A58,LATTICE5:def 8;
suppose o3 c= o2;
then A59: ConsecutiveSet2(A,o3) c= ConsecutiveSet2(A,o2) by Th22;
then reconsider z' = z as Element of ConsecutiveSet2(A,o2) by A37;
ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o3) by A50,Th22;
then A60: ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o2) by A59,XBOOLE_1:1
;
then reconsider x' = x as Element of ConsecutiveSet2(A,o2) by A35;
reconsider y' = y as Element of ConsecutiveSet2(A,o2) by A27,A31,A32;
ConsecutiveDelta2(q,o2) in rng Ls by A25,A27,A32,A42,FUNCT_1:def 5
;
then A61: h2 c= f by A42,ZFMISC_1:92;
A62: [x,y] in dom h2 by A35,A36,A45,A60,ZFMISC_1:106;
A63: [y,z] in dom h2 by A36,A37,A45,A59,ZFMISC_1:106;
A64: [x,z] in dom h2 by A35,A37,A45,A59,A60,ZFMISC_1:106;
A65: f.(x,y) = f.[x,y] by BINOP_1:def 1
.= h2.[x,y] by A61,A62,GRFUNC_1:8
.= h2.(x',y') by BINOP_1:def 1;
A66: f.(y,z) = f.[y,z] by BINOP_1:def 1
.= h2.[y,z] by A61,A63,GRFUNC_1:8
.= h2.(y',z') by BINOP_1:def 1;
f.(x,z) = f.[x,z] by BINOP_1:def 1
.= h2.[x,z] by A61,A64,GRFUNC_1:8
.= h2.(x',z') by BINOP_1:def 1;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A43,A65,A66,LATTICE5:def 8;
end;
suppose A67: o3 c= o1;
then A68: ConsecutiveSet2(A,o3) c= ConsecutiveSet2(A,o1) by Th22;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose o1 c= o2;
then A69: ConsecutiveSet2(A,o1) c= ConsecutiveSet2(A,o2) by Th22;
then reconsider x' = x as Element of ConsecutiveSet2(A,o2) by A35;
ConsecutiveSet2(A,o3) c= ConsecutiveSet2(A,o1) by A67,Th22;
then A70: ConsecutiveSet2(A,o3) c= ConsecutiveSet2(A,o2) by A69,XBOOLE_1:1;
then reconsider z' = z as Element of ConsecutiveSet2(A,o2) by A37;
reconsider y' = y as Element of ConsecutiveSet2(A,o2) by A27,A31,A32;
ConsecutiveDelta2(q,o2) in rng Ls by A25,A27,A32,A42,FUNCT_1:def 5
;
then A71: h2 c= f by A42,ZFMISC_1:92;
A72: [x,y] in dom h2 by A35,A36,A45,A69,ZFMISC_1:106;
A73: [y,z] in dom h2 by A36,A37,A45,A70,ZFMISC_1:106;
A74: [x,z] in dom h2 by A35,A37,A45,A69,A70,ZFMISC_1:106;
A75: f.(x,y) = f.[x,y] by BINOP_1:def 1
.= h2.[x,y] by A71,A72,GRFUNC_1:8
.= h2.(x',y') by BINOP_1:def 1;
A76: f.(y,z) = f.[y,z] by BINOP_1:def 1
.= h2.[y,z] by A71,A73,GRFUNC_1:8
.= h2.(y',z') by BINOP_1:def 1;
f.(x,z) = f.[x,z] by BINOP_1:def 1
.= h2.[x,z] by A71,A74,GRFUNC_1:8
.= h2.(x',z') by BINOP_1:def 1;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A43,A75,A76,LATTICE5:def 8;
suppose o2 c= o1;
then A77: ConsecutiveSet2(A,o2) c= ConsecutiveSet2(A,o1) by Th22;
then reconsider y' = y as Element of ConsecutiveSet2(A,o1) by A36;
reconsider z' = z as Element of ConsecutiveSet2(A,o1) by A37,A68;
reconsider x' = x as Element of ConsecutiveSet2(A,o1) by A27,A29,A30;
ConsecutiveDelta2(q,o1) in rng Ls by A25,A27,A30,A38,FUNCT_1:def 5
;
then A78: h1 c= f by A38,ZFMISC_1:92;
A79: [x,y] in dom h1 by A35,A36,A41,A77,ZFMISC_1:106;
A80: [y,z] in dom h1 by A36,A37,A41,A68,A77,ZFMISC_1:106;
A81: [x,z] in dom h1 by A35,A37,A41,A68,ZFMISC_1:106;
A82: f.(x,y) = f.[x,y] by BINOP_1:def 1
.= h1.[x,y] by A78,A79,GRFUNC_1:8
.= h1.(x',y') by BINOP_1:def 1;
A83: f.(y,z) = f.[y,z] by BINOP_1:def 1
.= h1.[y,z] by A78,A80,GRFUNC_1:8
.= h1.(y',z') by BINOP_1:def 1;
f.(x,z) = f.[x,z] by BINOP_1:def 1
.= h1.[x,z] by A78,A81,GRFUNC_1:8
.= h1.(x',z') by BINOP_1:def 1;
hence f.(x,y) "\/" f.(y,z) >= f.(x,z) by A39,A82,A83,LATTICE5:def 8;
end;
end;
hence ConsecutiveDelta2(q,O2) is u.t.i. by A23,A25,Th21;
end;
for O being Ordinal holds X[O] from Ordinal_Ind(A4,A6,A22);
hence thesis;
end;
theorem
for A being non empty set
for L being lower-bounded modular LATTICE
for d being distance_function of A,L
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti(d)
holds ConsecutiveDelta2(q,O) is distance_function of ConsecutiveSet2(A,O),L
by Th26,Th27,Th28;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
func NextSet2(d) equals :Def9:
ConsecutiveSet2(A,DistEsti(d));
correctness;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
cluster NextSet2(d) -> non empty;
coherence
proof
ConsecutiveSet2(A,DistEsti(d)) is non empty;
hence thesis by Def9;
end;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
func NextDelta2(q) equals :Def10:
ConsecutiveDelta2(q,DistEsti(d));
correctness;
end;
definition
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let q be QuadrSeq of d;
redefine func NextDelta2(q) -> distance_function of NextSet2(d),L;
coherence
proof
A1: ConsecutiveDelta2(q,DistEsti(d)) = NextDelta2(q) by Def10;
ConsecutiveSet2(A,DistEsti(d)) = NextSet2(d) by Def9;
hence thesis by A1,Th26,Th27,Th28;
end;
end;
definition
let A be non empty set;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set;
let dq be distance_function of Aq,L;
pred Aq, dq is_extension2_of A,d means :Def11:
ex q being QuadrSeq of d st Aq = NextSet2(d) & dq = NextDelta2(q);
end;
theorem Th30:
for A being non empty set
for L be lower-bounded LATTICE
for d be distance_function of A,L
for Aq be non empty set
for dq be distance_function of Aq,L st Aq, dq is_extension2_of A,d
for x,y being Element of A, a,b being Element of L st d.(x,y) <= a "\/" b
ex z1,z2 being Element of Aq
st dq.(x,z1) = a & dq.(z1,z2) = (d.(x,y) "\/" a) "/\" b & dq.(z2,y) = a
proof
let A be non empty set;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set;
let dq be distance_function of Aq,L;
assume Aq, dq is_extension2_of A,d;
then consider q being QuadrSeq of d such that
A1: Aq = NextSet2(d) and
A2: dq = NextDelta2(q) by Def11;
let x,y be Element of A;
let a,b be Element of L; assume
A3: d.(x,y) <= a "\/" b;
rng q = {[x',y',a',b'] where x' is Element of A, y' is Element of A,
a' is Element of L, b' is Element of L: d.(x',y')
<= a'"\/"b'} by LATTICE5:def 14;
then [x,y,a,b] in rng q by A3;
then consider o being set such that
A4: o in dom q & q.o = [x,y,a,b] by FUNCT_1:def 5;
reconsider o as Ordinal by A4,ORDINAL1:23;
A5: q.o = Quadr2(q,o) by A4,Def7;
then A6: x = Quadr2(q,o)`1 by A4,MCART_1:78;
A7: y = Quadr2(q,o)`2 by A4,A5,MCART_1:78;
A8: a = Quadr2(q,o)`3 by A4,A5,MCART_1:78;
A9: b = Quadr2(q,o)`4 by A4,A5,MCART_1:78;
reconsider B = ConsecutiveSet2(A,o) as non empty set;
reconsider Q = Quadr2(q,o)
as Element of [:B,B,the carrier of L,the carrier of L:];
reconsider cd = ConsecutiveDelta2(q,o) as BiFunction of B,L;
x in A & y in A & A c= B by Th18;
then reconsider xo = x, yo = y as Element of B;
xo in B & yo in B & B c= new_set2 B by Th13;
then reconsider x1 = xo, y1 = yo as Element of new_set2 B;
A10: ConsecutiveSet2(A,succ o) = new_set2 B by Th16;
o in DistEsti(d) by A4,LATTICE5:28;
then A11: succ o c= DistEsti(d) by ORDINAL1:33;
then A12: ConsecutiveDelta2(q,succ o) c= ConsecutiveDelta2(q,DistEsti(d)) by
Th25;
ConsecutiveDelta2(q,succ o)
= new_bi_fun2(BiFun(ConsecutiveDelta2(q,o),
ConsecutiveSet2(A,o),L),Quadr2(q,o)) by Th20
.= new_bi_fun2(cd,Q) by LATTICE5:def 16;
then A13: new_bi_fun2(cd,Q) c= dq by A2,A12,Def10;
{B} in {{B}, {{B}} } by TARSKI:def 2;
then {B} in B \/ {{B}, {{B}} } by XBOOLE_0:def 2;
then A14: {B} in new_set2 B by Def4;
{{B}} in {{B}, {{B}} } by TARSKI:def 2;
then {{B}} in B \/ {{B}, {{B}} } by XBOOLE_0:def 2;
then A15: {{B}} in new_set2 B by Def4;
A16: cd is zeroed by Th26;
A17: dom new_bi_fun2(cd,Q) = [:new_set2 B,new_set2 B:] by FUNCT_2:def 1;
then A18: [x1,{B}] in dom new_bi_fun2(cd,Q) by A14,ZFMISC_1:106;
A19: [{B},{{B}}] in dom new_bi_fun2(cd,Q) by A14,A15,A17,ZFMISC_1:106;
A20: [{{B}},y1] in dom new_bi_fun2(cd,Q) by A15,A17,ZFMISC_1:106;
A21: d c= cd by Th24;
dom d = [:A,A:] by FUNCT_2:def 1;
then A22: [xo,yo] in dom d by ZFMISC_1:106;
A23: cd.(xo,yo) = cd.[xo,yo] by BINOP_1:def 1
.= d.[xo,yo] by A21,A22,GRFUNC_1:8
.= d.(x,y) by BINOP_1:def 1;
new_set2 B c= ConsecutiveSet2(A,DistEsti(d)) by A10,A11,Th22;
then reconsider z1={B},z2={{B}} as Element of Aq by A1,A14,A15,Def9;
take z1,z2;
thus dq.(x,z1) = dq.[x,z1] by BINOP_1:def 1
.= new_bi_fun2(cd,Q).[x1,{B}] by A13,A18,GRFUNC_1:8
.= new_bi_fun2(cd,Q).(x1,{B}) by BINOP_1:def 1
.= cd.(xo,xo)"\/"a by A6,A8,Def5
.= Bottom L"\/"a by A16,LATTICE5:def 7
.= a by WAYBEL_1:4;
thus dq.(z1,z2) = dq.[z1,z2] by BINOP_1:def 1
.= new_bi_fun2(cd,Q).[{B},{{B}}] by A13,A19,GRFUNC_1:8
.= new_bi_fun2(cd,Q).({B},{{B}}) by BINOP_1:def 1
.= (d.(x,y)"\/"a)"/\"b by A6,A7,A8,A9,A23,Def5;
thus dq.(z2,y) = dq.[z2,y] by BINOP_1:def 1
.= new_bi_fun2(cd,Q).[{{B}},y1] by A13,A20,GRFUNC_1:8
.= new_bi_fun2(cd,Q).({{B}},y1) by BINOP_1:def 1
.= cd.(yo,yo)"\/"a by A7,A8,Def5
.= Bottom L"\/"a by A16,LATTICE5:def 7
.= a by WAYBEL_1:4;
end;
definition
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
mode ExtensionSeq2 of A,d -> Function means :Def12:
dom it = NAT & it.0 = [A,d] & for n being Nat holds
ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L
st Aq, dq is_extension2_of A',d' & it.n = [A',d'] & it.(n+1) = [Aq,dq];
existence
proof
defpred P[set,set,set] means
(ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension2_of A',d' & $2 = [A',d'] & $3 = [Aq,dq]) or
$3= 0 &
not ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension2_of A',d' & $2 = [A',d'];
A1: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat; let x be set;
per cases;
suppose ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension2_of A',d' & x = [A',d'];
then consider A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
A2: Aq, dq is_extension2_of A',d' and
A3: x = [A',d'];
take [Aq,dq];
thus thesis by A2,A3;
suppose
A4: not ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension2_of A',d' & x = [A',d'];
take 0;
thus thesis by A4;
end;
consider f being Function such that
A5: dom f = NAT and
A6: f.0 = [A,d] and
A7: for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecChoice(A1);
take f;
thus dom f = NAT by A5;
thus f.0 = [A,d] by A6;
defpred X[Nat] means
ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension2_of A',d' &
f.$1 = [A',d'] & f.($1+1) = [Aq,dq];
ex A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L st
Aq, dq is_extension2_of A',d' & f.0 = [A',d']
proof
take A,d;
consider q being QuadrSeq of d;
set Aq = NextSet2(d);
consider dq being distance_function of Aq,L such that
A8: dq = NextDelta2(q);
take Aq,dq;
thus Aq, dq is_extension2_of A,d by A8,Def11;
thus f.0 = [A,d] by A6;
end;
then A9: X[0] by A7;
A10: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat; given
A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
Aq, dq is_extension2_of A',d' and
f.k = [A',d'] and
A11: f.(k+1) = [Aq,dq];
ex A1 being non empty set, d1 being distance_function of A1,L,
AQ being non empty set, DQ being distance_function of AQ,L st
AQ, DQ is_extension2_of A1,d1 & f.(k+1) = [A1,d1]
proof
take Aq,dq;
set AQ = NextSet2(dq);
consider Q being QuadrSeq of dq;
set DQ = NextDelta2(Q);
take AQ,DQ;
thus AQ, DQ is_extension2_of Aq,dq by Def11;
thus f.(k+1) = [Aq,dq] by A11;
end;
hence thesis by A7;
end;
thus for k being Nat holds X[k] from Ind(A9,A10);
end;
end;
theorem Th31:
for A being non empty set
for L be lower-bounded modular LATTICE
for d be distance_function of A,L
for S being ExtensionSeq2 of A,d
for k,l being Nat st k <= l holds (S.k)`1 c= (S.l)`1
proof
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let S be ExtensionSeq2 of A,d;
let k be Nat;
defpred X[Nat] means k <= $1 implies (S.k)`1 c= (S.$1)`1;
A1: X[0] by NAT_1:19;
A2: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat;
assume that
A3: k <= i implies (S.k)`1 c= (S.i)`1 and
A4: k <= i+1;
per cases by A4,NAT_1:26;
suppose k = i+1;
hence (S.k)`1 c= (S.(i+1))`1;
suppose A5: k <= i;
consider A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
A6: Aq, dq is_extension2_of A',d' and
A7: S.i = [A',d'] & S.(i+1) = [Aq,dq] by Def12;
consider q being QuadrSeq of d' such that
A8: Aq = NextSet2(d') and
dq = NextDelta2(q) by A6,Def11;
A9: (S.i)`1 = A' by A7,MCART_1:def 1;
A10: (S.(i+1))`1 = NextSet2(d') by A7,A8,MCART_1:def 1
.= ConsecutiveSet2(A',DistEsti(d')) by Def9;
(S.i)`1 c= ConsecutiveSet2(A',DistEsti(d')) by A9,Th18;
hence (S.k)`1 c= (S.(i+1))`1 by A3,A5,A10,XBOOLE_1:1;
end;
thus for l being Nat holds X[l] from Ind(A1,A2);
end;
theorem Th32:
for A being non empty set
for L be lower-bounded modular LATTICE
for d be distance_function of A,L
for S being ExtensionSeq2 of A,d
for k,l being Nat st k <= l holds (S.k)`2 c= (S.l)`2
proof
let A be non empty set;
let L be lower-bounded modular LATTICE;
let d be distance_function of A,L;
let S be ExtensionSeq2 of A,d;
let k be Nat;
defpred X[Nat] means k <= $1 implies (S.k)`2 c= (S.$1)`2;
A1: X[0] by NAT_1:19;
A2: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat;
assume that
A3: k <= i implies (S.k)`2 c= (S.i)`2 and
A4: k <= i+1;
per cases by A4,NAT_1:26;
suppose k = i+1;
hence (S.k)`2 c= (S.(i+1))`2;
suppose A5: k <= i;
consider A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
A6: Aq, dq is_extension2_of A',d' and
A7: S.i = [A',d'] & S.(i+1) = [Aq,dq] by Def12;
consider q being QuadrSeq of d' such that
Aq = NextSet2(d') and
A8: dq = NextDelta2(q) by A6,Def11;
A9: (S.i)`2 = d' by A7,MCART_1:def 2;
A10: (S.(i+1))`2 = NextDelta2(q) by A7,A8,MCART_1:def 2
.= ConsecutiveDelta2(q,DistEsti(d')) by Def10;
(S.i)`2 c= ConsecutiveDelta2(q,DistEsti(d')) by A9,Th24;
hence (S.k)`2 c= (S.(i+1))`2 by A3,A5,A10,XBOOLE_1:1;
end;
thus for l being Nat holds X[l] from Ind(A1,A2);
end;
theorem Th33:
for L be lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF(L)
for FS being non empty set
st FS = union { (S.i)`1 where i is Nat: not contradiction}
holds union { (S.i)`2 where i is Nat: not contradiction}
is distance_function of FS,L
proof
let L be lower-bounded modular LATTICE;
let S be ExtensionSeq2 of the carrier of L, BasicDF(L);
let FS be non empty set;
assume
A1: FS = union { (S.i)`1 where i is Nat: not contradiction};
set FD = union { (S.i)`2 where i is Nat: not contradiction};
set A = the carrier of L;
(S.0)`1 in { (S.i)`1 where i is Nat: not contradiction};
then reconsider X = { (S.i)`1 where i is Nat: not contradiction}
as non empty set;
reconsider FS as non empty set;
A2: { (S.i)`2 where i is Nat: not contradiction} is c=-linear
proof
now
let x,y be set;
assume that
A3: x in { (S.i)`2 where i is Nat: not contradiction} and
A4: y in { (S.i)`2 where i is Nat: not contradiction};
consider k being Nat such that
A5: x = (S.k)`2 by A3;
consider l being Nat such that
A6: y = (S.l)`2 by A4;
k <= l or l <= k;
then x c= y or y c= x by A5,A6,Th32;
hence x,y are_c=-comparable by XBOOLE_0:def 9;
end;
hence thesis by ORDINAL1:def 9;
end;
{ (S.i)`2 where i is Nat: not contradiction} c= PFuncs([:FS,FS:],A)
proof
let z be set;
assume z in { (S.i)`2 where i is Nat: not contradiction};
then consider j being Nat such that
A7: z = (S.j)`2;
consider A' being non empty set, d' being distance_function of A',L,
Aq being non empty set, dq being distance_function of Aq,L such that
Aq, dq is_extension2_of A',d' and
A8: S.j = [A',d'] & S.(j+1) = [Aq,dq] by Def12;
A9: z = d' by A7,A8,MCART_1:def 2;
A10: rng d' c= A;
A11: dom d' = [:A',A':] by FUNCT_2:def 1;
A' = (S.j)`1 by A8,MCART_1:def 1;
then A' in { (S.i)`1 where i is Nat: not contradiction};
then A' c= FS by A1,ZFMISC_1:92;
then dom d' c= [:FS,FS:] by A11,ZFMISC_1:119;
hence z in PFuncs([:FS,FS:],A) by A9,A10,PARTFUN1:def 5;
end;
then FD in PFuncs([:FS,FS:],A) by A2,HAHNBAN:13;
then consider g being Function such that
A12: FD = g and
dom g c= [:FS,FS:] and
A13: rng g c= A by PARTFUN1:def 5;
reconsider FD as Function by A12;
A14: X is c=-linear
proof
now
let x,y be set;
assume that
A15: x in X and
A16: y in X;
consider k being Nat such that
A17: x = (S.k)`1 by A15;
consider l being Nat such that
A18: y = (S.l)`1 by A16;
k <= l or l <= k;
then x c= y or y c= x by A17,A18,Th31;
hence x,y are_c=-comparable by XBOOLE_0:def 9;
end;
hence thesis by ORDINAL1:def 9;
end;
defpred X[set,set] means $2 = (S.$1)`2;
A19: for x,y1,y2 being set st x in NAT & X[x,y1] & X[x,y2]
holds y1 = y2;
A20: for x being set st x in NAT ex y being set st X[x,y];
consider F being Function such that
A21: dom F = NAT and
A22: for x being set st x in NAT holds X[x,F.x] from FuncEx(A19,A20);
A23: rng F = { (S.i)`2 where i is Nat: not contradiction}
proof
thus rng F c= { (S.i)`2 where i is Nat: not contradiction}
proof
let x be set;
assume x in rng F;
then consider j being set such that
A24: j in dom F & F.j = x by FUNCT_1:def 5;
reconsider j as Nat by A21,A24;
x = (S.j)`2 by A22,A24;
hence x in { (S.i)`2 where i is Nat: not contradiction};
end;
let x be set;
assume x in { (S.i)`2 where i is Nat: not contradiction};
then consider j being Nat such that
A25: x = (S.j)`2;
x = F.j by A22,A25;
hence x in rng F by A21,FUNCT_1:def 5;
end;
F is Function-yielding
proof
let x be set;
assume x in dom F;
then reconsider j = x as Nat by A21;
consider A1 being non empty set, d1 being distance_function of A1,L,
Aq1 being non empty set, dq1 being distance_function of Aq1,L
such that
Aq1, dq1 is_extension2_of A1,d1 and
A26: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def12;
(S.j)`2 = d1 by A26,MCART_1:def 2;
hence F.x is Function by A22;
end;
then reconsider F as Function-yielding Function;
set LL = { [:I,I:] where I is Element of X : I in X },
PP = { [:(S.i)`1,(S.i)`1:] where i is Nat: not contradiction };
A27: rng doms F = PP
proof
thus rng doms F c= PP
proof
let x be set;
assume x in rng doms F;
then consider j being set such that
A28: j in dom doms F & x = (doms F).j by FUNCT_1:def 5;
A29: j in dom F by A28,EXTENS_1:3;
reconsider j as Nat by A21,A28,EXTENS_1:3;
consider A1 being non empty set, d1 being distance_function of A1,L,
Aq1 being non empty set, dq1 being distance_function of Aq1,L
such that
Aq1, dq1 is_extension2_of A1,d1 and
A30: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def12;
A31: (S.j)`2 = d1 by A30,MCART_1:def 2;
A32: (S.j)`1 = A1 by A30,MCART_1:def 1;
x = dom (F.j) by A28,A29,FUNCT_6:31
.= dom d1 by A22,A31
.= [:(S.j)`1,(S.j)`1:] by A32,FUNCT_2:def 1;
hence x in PP;
end;
let x be set; assume x in PP;
then consider j being Nat such that
A33: x = [:(S.j)`1,(S.j)`1:];
consider A1 being non empty set, d1 being distance_function of A1,L,
Aq1 being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A34: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def12;
A35: (S.j)`2 = d1 by A34,MCART_1:def 2;
A36: (S.j)`1 = A1 by A34,MCART_1:def 1;
j in NAT;
then A37: j in dom doms F by A21,EXTENS_1:3;
x = dom d1 by A33,A36,FUNCT_2:def 1
.= dom (F.j) by A22,A35
.= (doms F).j by A21,FUNCT_6:31;
hence x in rng doms F by A37,FUNCT_1:def 5;
end;
LL = PP
proof
thus LL c= PP
proof
let x be set; assume x in LL;
then consider J being Element of X such that
A38: x = [:J,J:] and
A39: J in X;
consider j being Nat such that
A40: J = (S.j)`1 by A39;
thus x in PP by A38,A40;
end;
let x be set;
assume x in PP;
then consider j being Nat such that
A41: x = [:(S.j)`1,(S.j)`1:];
(S.j)`1 in X;
hence x in LL by A41;
end;
then [:FS,FS:] = union rng doms F by A1,A14,A27,LATTICE5:3
.= dom FD by A23,LATTICE5:1;
then FD is Function of [:FS,FS:],A by A12,A13,FUNCT_2:def 1,RELSET_1:11;
then reconsider FD as BiFunction of FS,L;
A42: FD is zeroed
proof
let x be Element of FS;
consider y being set such that
A43: x in y & y in X by A1,TARSKI:def 4;
consider j being Nat such that
A44: y = (S.j)`1 by A43;
consider A1 being non empty set, d1 being distance_function of A1,L,
Aq1 being non empty set, dq1 being distance_function of Aq1,L
such that Aq1, dq1 is_extension2_of A1,d1 and
A45: S.j = [A1,d1] & S.(j+1) = [Aq1,dq1] by Def12;
A46: (S.j)`2 = d1 by A45,MCART_1:def 2;
reconsider x' = x as Element of A1 by A43,A44,A45,MCART_1:def 1;
d1 in { (S.i)`2 where i is Nat: not contradiction} by A46;
then A47: d1 c= FD by ZFMISC_1:92;
A48: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
thus FD.(x,x) = FD.[x',x'] by BINOP_1:def 1
.= d1.[x',x'] by A47,A48,GRFUNC_1:8
.= d1.(x',x') by BINOP_1:def 1
.= Bottom L by LATTICE5:def 7;
end;
A49: FD is symmetric
proof
let x,y be Element of FS;
consider x1 being set such that
A50: x in x1 & x1 in X by A1,TARSKI:def 4;
consider k being Nat such that
A51: x1 = (S.k)`1 by A50;
consider A1 being non empty set, d1 being distance_function of A1,L,
Aq1 being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A52: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def12;
A53: (S.k)`2 = d1 by A52,MCART_1:def 2;
A54: (S.k)`1 = A1 by A52,MCART_1:def 1;
d1 in { (S.i)`2 where i is Nat: not contradiction} by A53;
then A55: d1 c= FD by ZFMISC_1:92;
A56: x in A1 by A50,A51,A52,MCART_1:def 1;
consider y1 being set such that
A57: y in y1 & y1 in X by A1,TARSKI:def 4;
consider l being Nat such that
A58: y1 = (S.l)`1 by A57;
consider A2 being non empty set, d2 being distance_function of A2,L,
Aq2 being non empty set, dq2 being distance_function of Aq2,L such that
Aq2, dq2 is_extension2_of A2,d2 and
A59: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def12;
A60: (S.l)`2 = d2 by A59,MCART_1:def 2;
A61: (S.l)`1 = A2 by A59,MCART_1:def 1;
d2 in { (S.i)`2 where i is Nat: not contradiction} by A60;
then A62: d2 c= FD by ZFMISC_1:92;
A63: y in A2 by A57,A58,A59,MCART_1:def 1;
per cases;
suppose k <= l;
then A1 c= A2 by A54,A61,Th31;
then reconsider x'=x,y'=y as Element of A2 by A56,A57,A58,A59,MCART_1:def
1;
A64: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
thus FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d2.[x',y'] by A62,A64,GRFUNC_1:8
.= d2.(x',y') by BINOP_1:def 1
.= d2.(y',x') by LATTICE5:def 6
.= d2.[y',x'] by BINOP_1:def 1
.= FD.[y',x'] by A62,A64,GRFUNC_1:8
.= FD.(y,x) by BINOP_1:def 1;
suppose l <= k;
then A2 c= A1 by A54,A61,Th31;
then reconsider x'=x,y'=y as Element of A1 by A50,A51,A52,A63,MCART_1:def
1;
A65: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
thus FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d1.[x',y'] by A55,A65,GRFUNC_1:8
.= d1.(x',y') by BINOP_1:def 1
.= d1.(y',x') by LATTICE5:def 6
.= d1.[y',x'] by BINOP_1:def 1
.= FD.[y',x'] by A55,A65,GRFUNC_1:8
.= FD.(y,x) by BINOP_1:def 1;
end;
FD is u.t.i.
proof
let x,y,z be Element of FS;
consider x1 being set such that
A66: x in x1 & x1 in X by A1,TARSKI:def 4;
consider k being Nat such that
A67: x1 = (S.k)`1 by A66;
consider A1 being non empty set, d1 being distance_function of A1,L,
Aq1 being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension2_of A1,d1 and
A68: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def12;
A69: (S.k)`2 = d1 by A68,MCART_1:def 2;
A70: (S.k)`1 = A1 by A68,MCART_1:def 1;
d1 in { (S.i)`2 where i is Nat: not contradiction} by A69;
then A71: d1 c= FD by ZFMISC_1:92;
A72: x in A1 by A66,A67,A68,MCART_1:def 1;
A73: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
consider y1 being set such that
A74: y in y1 & y1 in X by A1,TARSKI:def 4;
consider l being Nat such that
A75: y1 = (S.l)`1 by A74;
consider A2 being non empty set, d2 being distance_function of A2,L,
Aq2 being non empty set, dq2 being distance_function of Aq2,L such that
Aq2, dq2 is_extension2_of A2,d2 and
A76: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def12;
A77: (S.l)`2 = d2 by A76,MCART_1:def 2;
A78: (S.l)`1 = A2 by A76,MCART_1:def 1;
d2 in { (S.i)`2 where i is Nat: not contradiction} by A77;
then A79: d2 c= FD by ZFMISC_1:92;
A80: y in A2 by A74,A75,A76,MCART_1:def 1;
A81: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
consider z1 being set such that
A82: z in z1 & z1 in X by A1,TARSKI:def 4;
consider n being Nat such that
A83: z1 = (S.n)`1 by A82;
consider A3 being non empty set, d3 being distance_function of A3,L,
Aq3 being non empty set, dq3 being distance_function of Aq3,L such that
Aq3, dq3 is_extension2_of A3,d3 and
A84: S.n = [A3,d3] & S.(n+1) = [Aq3,dq3] by Def12;
A85: (S.n)`2 = d3 by A84,MCART_1:def 2;
A86: (S.n)`1 = A3 by A84,MCART_1:def 1;
d3 in { (S.i)`2 where i is Nat: not contradiction} by A85;
then A87: d3 c= FD by ZFMISC_1:92;
A88: z in A3 by A82,A83,A84,MCART_1:def 1;
A89: dom d3 = [:A3,A3:] by FUNCT_2:def 1;
per cases;
suppose k <= l;
then A90: A1 c= A2 by A70,A78,Th31;
thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z)
proof
per cases;
suppose l <= n;
then A91: A2 c= A3 by A78,A86,Th31;
then A1 c= A3 by A90,XBOOLE_1:1;
then reconsider x' = x, y' = y, z' = z as Element of A3
by A72,A80,A82,A83,A84,A91,MCART_1:def 1;
A92: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d3.[x',y'] by A87,A89,GRFUNC_1:8
.= d3.(x',y') by BINOP_1:def 1;
A93: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1
.= d3.[y',z'] by A87,A89,GRFUNC_1:8
.= d3.(y',z') by BINOP_1:def 1;
FD.(x,z) = FD.[x',z'] by BINOP_1:def 1
.= d3.[x',z'] by A87,A89,GRFUNC_1:8
.= d3.(x',z') by BINOP_1:def 1;
hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A92,A93,LATTICE5:def 8;
suppose n <= l;
then A3 c= A2 by A78,A86,Th31;
then reconsider x' = x, y' = y, z' = z as Element of A2
by A72,A74,A75,A76,A88,A90,MCART_1:def 1;
A94: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d2.[x',y'] by A79,A81,GRFUNC_1:8
.= d2.(x',y') by BINOP_1:def 1;
A95: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1
.= d2.[y',z'] by A79,A81,GRFUNC_1:8
.= d2.(y',z') by BINOP_1:def 1;
FD.(x,z) = FD.[x',z'] by BINOP_1:def 1
.= d2.[x',z'] by A79,A81,GRFUNC_1:8
.= d2.(x',z') by BINOP_1:def 1;
hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A94,A95,LATTICE5:def 8;
end;
suppose l <= k;
then A96: A2 c= A1 by A70,A78,Th31;
thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z)
proof
per cases;
suppose k <= n;
then A97: A1 c= A3 by A70,A86,Th31;
then A2 c= A3 by A96,XBOOLE_1:1;
then reconsider x' = x, y' = y, z' = z as Element of A3
by A72,A80,A82,A83,A84,A97,MCART_1:def 1;
A98: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d3.[x',y'] by A87,A89,GRFUNC_1:8
.= d3.(x',y') by BINOP_1:def 1;
A99: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1
.= d3.[y',z'] by A87,A89,GRFUNC_1:8
.= d3.(y',z') by BINOP_1:def 1;
FD.(x,z) = FD.[x',z'] by BINOP_1:def 1
.= d3.[x',z'] by A87,A89,GRFUNC_1:8
.= d3.(x',z') by BINOP_1:def 1;
hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A98,A99,LATTICE5:def 8;
suppose n <= k;
then A3 c= A1 by A70,A86,Th31;
then reconsider x' = x, y' = y, z' = z as Element of A1
by A66,A67,A68,A80,A88,A96,MCART_1:def 1;
A100: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d1.[x',y'] by A71,A73,GRFUNC_1:8
.= d1.(x',y') by BINOP_1:def 1;
A101: FD.(y,z) = FD.[y',z'] by BINOP_1:def 1
.= d1.[y',z'] by A71,A73,GRFUNC_1:8
.= d1.(y',z') by BINOP_1:def 1;
FD.(x,z) = FD.[x',z'] by BINOP_1:def 1
.= d1.[x',z'] by A71,A73,GRFUNC_1:8
.= d1.(x',z') by BINOP_1:def 1;
hence FD.(x,y) "\/" FD.(y,z) >= FD.(x,z) by A100,A101,LATTICE5:def 8
;
end;
end;
hence thesis by A42,A49;
end;
theorem Th34:
for L be lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF(L)
for FS being non empty set
for FD being distance_function of FS,L
for x,y being Element of FS for a,b being Element of L
st FS = union { (S.i)`1 where i is Nat: not contradiction} &
FD = union { (S.i)`2 where i is Nat: not contradiction} &
FD.(x,y) <= a"\/"b
ex z1,z2 being Element of FS st FD.(x,z1) = a &
FD.(z1,z2) = (FD.(x,y)"\/"a)"/\"b & FD.(z2,y) = a
proof
let L be lower-bounded modular LATTICE;
let S be ExtensionSeq2 of the carrier of L, BasicDF(L);
let FS be non empty set, FD be distance_function of FS,L;
let x,y be Element of FS; let a,b be Element of L; assume that
A1: FS = union { (S.i)`1 where i is Nat: not contradiction} &
FD = union { (S.i)`2 where i is Nat: not contradiction} and
A2: FD.(x,y) <= a"\/"b;
(S.0)`1 in { (S.i)`1 where i is Nat: not contradiction};
then reconsider X = { (S.i)`1 where i is Nat: not contradiction}
as non empty set;
consider x1 being set such that
A3: x in x1 & x1 in X by A1,TARSKI:def 4;
consider k being Nat such that
A4: x1 = (S.k)`1 by A3;
consider A1 being non empty set, d1 being distance_function of A1,L,
Aq1 being non empty set, dq1 being distance_function of Aq1,L such that
A5: Aq1, dq1 is_extension2_of A1,d1 and
A6: S.k = [A1,d1] & S.(k+1) = [Aq1,dq1] by Def12;
A7: (S.k)`2 = d1 by A6,MCART_1:def 2;
A8: (S.k)`1 = A1 by A6,MCART_1:def 1;
A9: (S.(k+1))`1 = Aq1 by A6,MCART_1:def 1;
A10: (S.(k+1))`2 = dq1 by A6,MCART_1:def 2;
d1 in { (S.i)`2 where i is Nat: not contradiction} by A7;
then A11: d1 c= FD by A1,ZFMISC_1:92;
dq1 in { (S.i)`2 where i is Nat: not contradiction} by A10;
then A12: dq1 c= FD by A1,ZFMISC_1:92;
Aq1 in { (S.i)`1 where i is Nat: not contradiction} by A9;
then A13: Aq1 c= FS by A1,ZFMISC_1:92;
A14: x in A1 by A3,A4,A6,MCART_1:def 1;
consider y1 being set such that
A15: y in y1 & y1 in X by A1,TARSKI:def 4;
consider l being Nat such that
A16: y1 = (S.l)`1 by A15;
consider A2 being non empty set, d2 being distance_function of A2,L,
Aq2 being non empty set, dq2 being distance_function of Aq2,L such that
A17: Aq2, dq2 is_extension2_of A2,d2 and
A18: S.l = [A2,d2] & S.(l+1) = [Aq2,dq2] by Def12;
A19: (S.l)`2 = d2 by A18,MCART_1:def 2;
A20: (S.l)`1 = A2 by A18,MCART_1:def 1;
A21: (S.(l+1))`1 = Aq2 by A18,MCART_1:def 1;
A22: (S.(l+1))`2 = dq2 by A18,MCART_1:def 2;
d2 in { (S.i)`2 where i is Nat: not contradiction} by A19;
then A23: d2 c= FD by A1,ZFMISC_1:92;
dq2 in { (S.i)`2 where i is Nat: not contradiction} by A22;
then A24: dq2 c= FD by A1,ZFMISC_1:92;
Aq2 in { (S.i)`1 where i is Nat: not contradiction} by A21;
then A25: Aq2 c= FS by A1,ZFMISC_1:92;
A26: y in A2 by A15,A16,A18,MCART_1:def 1;
per cases;
suppose k <= l;
then A1 c= A2 by A8,A20,Th31;
then reconsider x'=x,y'=y as Element of A2 by A14,A15,A16,A18,MCART_1:def 1;
A27: x' in A2 & y' in A2;
A28: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
A29: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d2.[x',y'] by A23,A28,GRFUNC_1:8
.= d2.(x',y') by BINOP_1:def 1;
then consider z1,z2 being Element of Aq2 such that
A30: dq2.(x,z1) = a and
A31: dq2.(z1,z2) = (d2.(x',y')"\/"a)"/\"b and
A32: dq2.(z2,y) = a by A2,A17,Th30;
z1 in Aq2 & z2 in Aq2;
then reconsider z1' = z1, z2' = z2 as Element of FS by A25;
l <= l+1 by NAT_1:29;
then A2 c= Aq2 by A20,A21,Th31;
then reconsider x'' = x',y'' = y' as Element of Aq2 by A27;
A33: dom dq2 = [:Aq2,Aq2:] by FUNCT_2:def 1;
take z1',z2';
thus FD.(x,z1') = FD.[x'',z1] by BINOP_1:def 1
.= dq2.[x'',z1] by A24,A33,GRFUNC_1:8
.= a by A30,BINOP_1:def 1;
thus FD.(z1',z2') = FD.[z1,z2] by BINOP_1:def 1
.= dq2.[z1,z2] by A24,A33,GRFUNC_1:8
.= (FD.(x,y)"\/"a)"/\"b by A29,A31,BINOP_1:def 1;
thus FD.(z2',y) = FD.[z2,y''] by BINOP_1:def 1
.= dq2.[z2,y''] by A24,A33,GRFUNC_1:8
.= a by A32,BINOP_1:def 1;
suppose l <= k;
then A2 c= A1 by A8,A20,Th31;
then reconsider x'=x,y'=y as Element of A1 by A3,A4,A6,A26,MCART_1:def 1;
A34: x' in A1 & y' in A1;
A35: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
A36: FD.(x,y) = FD.[x',y'] by BINOP_1:def 1
.= d1.[x',y'] by A11,A35,GRFUNC_1:8
.= d1.(x',y') by BINOP_1:def 1;
then consider z1,z2 being Element of Aq1 such that
A37: dq1.(x,z1) = a and
A38: dq1.(z1,z2) = (d1.(x',y')"\/"a)"/\"b and
A39: dq1.(z2,y) = a by A2,A5,Th30;
z1 in Aq1 & z2 in Aq1;
then reconsider z1' = z1, z2' = z2 as Element of FS by A13;
k <= k+1 by NAT_1:29;
then A1 c= Aq1 by A8,A9,Th31;
then reconsider x'' = x',y'' = y' as Element of Aq1 by A34;
A40: dom dq1 = [:Aq1,Aq1:] by FUNCT_2:def 1;
take z1',z2';
thus FD.(x,z1') = FD.[x'',z1] by BINOP_1:def 1
.= dq1.[x'',z1] by A12,A40,GRFUNC_1:8
.= a by A37,BINOP_1:def 1;
thus FD.(z1',z2') = FD.[z1,z2] by BINOP_1:def 1
.= dq1.[z1,z2] by A12,A40,GRFUNC_1:8
.= (FD.(x,y)"\/"a)"/\"b by A36,A38,BINOP_1:def 1;
thus FD.(z2',y) = FD.[z2,y''] by BINOP_1:def 1
.= dq1.[z2,y''] by A12,A40,GRFUNC_1:8
.= a by A39,BINOP_1:def 1;
end;
Lm3:
for m being Nat st m in Seg 4 holds (m = 1 or m = 2 or m = 3 or m = 4)
proof
let m be Nat;
assume
A1: m in Seg 4;
then 1 <= m & m <= 4 by FINSEQ_1:3;
then m = 0 or m = 1 or m = 2 or m = 3 or m = 4 by CQC_THE1:5;
hence m = 1 or m = 2 or m = 3 or m = 4 by A1,FINSEQ_1:3;
end;
Lm4:
for j being Nat st 1 <= j & j < 4 holds j = 1 or j = 2 or j = 3
proof
let j be Nat; assume
A1: 1 <= j & j < 4;
then j < 3+1;
then j <= 3 by NAT_1:38;
then j = 0 or j = 1 or j = 2 or j = 3 by CQC_THE1:4;
hence j = 1 or j = 2 or j = 3 by A1;
end;
theorem Th35:
for L be lower-bounded modular LATTICE
for S being ExtensionSeq2 of the carrier of L, BasicDF(L)
for FS being non empty set
for FD being distance_function of FS,L
for f being Homomorphism of L,EqRelLATT FS
for e1,e2 being Equivalence_Relation of FS
for x,y being set st f = alpha FD &
FS = union { (S.i)`1 where i is Nat: not contradiction} &
FD = union { (S.i)`2 where i is Nat: not contradiction} &
e1 in the carrier of Image f & e2 in the carrier of Image f &
[x,y] in e1 "\/" e2
ex F being non empty FinSequence of FS
st len F = 2+2 & x,y are_joint_by F,e1,e2
proof
let L be lower-bounded modular LATTICE;
let S be ExtensionSeq2 of the carrier of L, BasicDF(L);
let FS be non empty set;
let FD be distance_function of FS,L;
let f be Homomorphism of L,EqRelLATT FS;
let e1,e2 be Equivalence_Relation of FS;
let x,y be set;
assume that
A1: f = alpha FD and
A2: FS = union { (S.i)`1 where i is Nat: not contradiction} &
FD = union { (S.i)`2 where i is Nat: not contradiction} and
A3: e1 in the carrier of Image f & e2 in the carrier of Image f and
A4: [x,y] in e1 "\/" e2;
Image f = subrelstr rng f by YELLOW_2:def 2;
then A5:the carrier of Image f = rng f by YELLOW_0:def 15;
then consider a being set such that
A6: a in dom f and
A7: e1 = f.a by A3,FUNCT_1:def 5;
consider b being set such that
A8: b in dom f and
A9: e2 = f.b by A3,A5,FUNCT_1:def 5;
reconsider a,b as Element of L by A6,A8;
field (e1 "\/" e2) = FS by EQREL_1:15;
then reconsider u = x, v = y as Element of FS by A4,RELAT_1:30;
reconsider a,b as Element of L;
consider e1' being Equivalence_Relation of FS such that
A10: e1' = f.a and
A11: for u,v being Element of FS holds [u,v] in e1' iff FD.(u,v) <= a
by A1,LATTICE5:def 9;
consider e2' being Equivalence_Relation of FS such that
A12: e2' = f.b and
A13: for u,v being Element of FS holds [u,v] in e2' iff FD.(u,v) <= b
by A1,LATTICE5:def 9;
consider e being Equivalence_Relation of FS such that
A14: e = f.(a"\/"b) and
A15: for u,v being Element of FS holds [u,v] in e iff
FD.(u,v) <= a"\/"b by A1,LATTICE5:def 9;
e = f.a"\/"f.b by A14,WAYBEL_6:2
.= e1 "\/" e2 by A7,A9,LATTICE5:10;
then A16: FD.(u,v) <= a"\/"b by A4,A15;
then consider z1,z2 being Element of FS such that
A17: FD.(u,z1) = a and
A18: FD.(z1,z2) = (FD.(u,v)"\/"a)"/\"b and
A19: FD.(z2,v) = a by A2,Th34;
defpred P[set,set] means
($1 = 1 implies $2 = u) & ($1 = 2 implies $2 = z1) &
($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = v);
A20: for m being Nat, w1,w2 being set st m in Seg 4 & P[m,w1] & P[m,w2]
holds w1 = w2 by Lm3;
A21: for m being Nat st m in Seg 4 ex w being set st P[m,w]
proof
let m be Nat;
assume
A22: m in Seg 4;
per cases by A22,Lm3;
suppose A23: m = 1; take w = x; thus P[m,w] by A23;
suppose A24: m = 2; take w = z1; thus P[m,w] by A24;
suppose A25: m = 3; take w = z2; thus P[m,w] by A25;
suppose A26: m = 4; take w = y; thus P[m,w] by A26;
end;
ex p being FinSequence st dom p = Seg 4
& for k being Nat st k in Seg 4 holds P[k,p.k] from SeqEx(A20,A21);
then consider h being FinSequence such that
A27: dom h = Seg 4 and
A28: for m being Nat st m in Seg 4 holds
(m = 1 implies h.m = u) & (m = 2 implies h.m = z1) &
(m = 3 implies h.m = z2) & (m = 4 implies h.m = v);
Seg 4 = { n where n is Nat: 1 <= n & n <= 4 } by FINSEQ_1:def 1;
then A29: 1 in Seg 4 & 2 in Seg 4 & 3 in Seg 4 & 4 in Seg 4;
A30: len h = 4 by A27,FINSEQ_1:def 3;
rng h c= FS
proof
let w be set;
assume w in rng h;
then consider j be set such that
A31: j in dom h & w = h.j by FUNCT_1:def 5;
per cases by A27,A31,Lm3;
suppose j = 1; then h.j = u by A28,A29; hence w in FS by A31;
suppose j = 2; then h.j = z1 by A28,A29; hence w in FS by A31;
suppose j = 3; then h.j = z2 by A28,A29; hence w in FS by A31;
suppose j = 4; then h.j = v by A28,A29; hence w in FS by A31;
end;
then reconsider h as FinSequence of FS by FINSEQ_1:def 4;
len h <> 0 by A27,FINSEQ_1:def 3;
then reconsider h as non empty FinSequence of FS by FINSEQ_1:25;
take h;
thus len h = 2+2 by A27,FINSEQ_1:def 3;
A32: h.1 = x by A28,A29;
A33: h.(len h) = h.4 by A27,FINSEQ_1:def 3
.= y by A28,A29;
for j being Nat st 1 <= j & j < len h holds
(j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
proof
let j be Nat;
assume
A34: 1 <= j & j < len h;
per cases by A30,A34,Lm4;
suppose
A35: j = 1;
[u,z1] in e1' by A11,A17;
then [h.1,z1] in e1' by A28,A29;
hence (j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
by A7,A10,A28,A29,A35,Lm1;
suppose
A36: j = 2;
consider i being Nat such that
A37: i = 1;
A38: 2*i = j by A36,A37;
FD.(u,v)"\/"a <= a"\/"b"\/"a by A16,WAYBEL_1:3;
then FD.(u,v)"\/"a <= b"\/"(a"\/"a) by LATTICE3:14;
then FD.(u,v)"\/"a <= b"\/"a by YELLOW_5:1;
then (FD.(u,v)"\/"a)"/\"b <= b"/\"(b"\/"a) by WAYBEL_1:2;
then (FD.(u,v)"\/"a)"/\"b <= b by LATTICE3:18;
then [z1,z2] in e2' by A13,A18;
then [h.2,z2] in e2' by A28,A29;
hence (j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
by A9,A12,A28,A29,A36,A38;
suppose
A39: j = 3;
consider i being Nat such that
A40: i = 1;
A41: 2*i+1 = j by A39,A40;
[z2,v] in e1' by A11,A19;
then [h.3,v] in e1' by A28,A29;
hence (j is odd implies [h.j,h.(j+1)] in e1) &
(j is even implies [h.j,h.(j+1)] in e2)
by A7,A10,A28,A29,A39,A41;
end;
hence thesis by A32,A33,LATTICE5:def 3;
end;
theorem Th36:
for L be lower-bounded modular LATTICE
holds L has_a_representation_of_type<= 2
proof
let L be lower-bounded modular LATTICE;
set A = the carrier of L,
D = BasicDF(L);
A1: D is onto by LATTICE5:43;
consider S being ExtensionSeq2 of A,D;
A2: S.0 = [A,D] by Def12;
then A3: (S.0)`1 = A by MCART_1:def 1;
set FS = union { (S.i)`1 where i is Nat: not contradiction};
(S.0)`1 in { (S.i)`1 where i is Nat: not contradiction};
then A4: A c= FS by A3,ZFMISC_1:92;
consider xx being set such that
A5: xx in A by XBOOLE_0:def 1;
reconsider FS as non empty set by A4,A5;
reconsider FD = union { (S.i)`2 where i is Nat: not contradiction}
as distance_function of FS,L by Th33;
A6: FD is onto
proof
A7: rng D = A by A1,FUNCT_2:def 3;
for w being set st w in A ex z being set st z in [:FS,FS:] & w = FD.z
proof
let w be set;
assume w in A;
then consider z being set such that
A8: z in [:A,A:] and
A9: D.z = w by A7,FUNCT_2:17;
take z;
A10: S.0 = [A,D] by Def12;
then A11: A = (S.0)`1 by MCART_1:def 1;
(S.0)`1 in { (S.i)`1 where i is Nat: not contradiction};
then A c= FS by A11,ZFMISC_1:92;
then [:A,A:] c= [:FS,FS:] by ZFMISC_1:119;
hence z in [:FS,FS:] by A8;
A12: z in dom D by A8,FUNCT_2:def 1;
A13: D = (S.0)`2 by A10,MCART_1:def 2;
(S.0)`2 in { (S.i)`2 where i is Nat: not contradiction};
then D c= FD by A13,ZFMISC_1:92;
hence w = FD.z by A9,A12,GRFUNC_1:8;
end;
then rng FD = A by FUNCT_2:16;
hence FD is onto by FUNCT_2:def 3;
end;
alpha FD is join-preserving
proof
let a,b be Element of L;
set f = alpha FD;
A14: ex_sup_of f.:{a,b},EqRelLATT FS by YELLOW_0:17;
A15: dom f = the carrier of L by FUNCT_2:def 1;
consider e1 being Equivalence_Relation of FS such that
A16: e1 = f.a and
A17: for x,y being Element of FS holds [x,y] in e1 iff FD.(x,y) <= a
by LATTICE5:def 9;
consider e2 being Equivalence_Relation of FS such that
A18: e2 = f.b and
A19: for x,y being Element of FS holds [x,y] in e2 iff FD.(x,y) <= b
by LATTICE5:def 9;
consider e3 being Equivalence_Relation of FS such that
A20: e3 = f.(a "\/" b) and
A21: for x,y being Element of FS holds [x,y] in e3 iff FD.(x,y) <= a"\/"b
by LATTICE5:def 9;
A22: field e1 = FS by EQREL_1:15;
A23: field e2 = FS by EQREL_1:15;
A24: field e3 = FS by EQREL_1:15;
A25: e1 "\/" e2 c= e3
proof
now
let x,y be set;
assume
A26: [x,y] in e1;
then reconsider x' = x, y' = y as Element of FS by A22,RELAT_1:30;
A27: FD.(x',y') <= a by A17,A26;
a <= a "\/" b by YELLOW_0:22;
then FD.(x',y') <= a "\/" b by A27,ORDERS_1:26;
hence [x,y] in e3 by A21;
end;
then A28: e1 c= e3 by RELAT_1:def 3;
now
let x,y be set;
assume
A29: [x,y] in e2;
then reconsider x' = x, y' = y as Element of FS by A23,RELAT_1:30;
A30: FD.(x',y') <= b by A19,A29;
b <= b "\/" a by YELLOW_0:22;
then FD.(x',y') <= b "\/" a by A30,ORDERS_1:26;
hence [x,y] in e3 by A21;
end;
then e2 c= e3 by RELAT_1:def 3;
then e1 \/ e2 c= e3 by A28,XBOOLE_1:8;
hence thesis by EQREL_1:def 3;
end;
A31: e3 c= e1 "\/" e2
proof
for u,v being set holds [u,v] in e3 implies [u,v] in e1 "\/" e2
proof
let u,v be set;
assume
A32: [u,v] in e3;
then reconsider x = u, y = v as Element of FS by A24,RELAT_1:30;
A33: u in FS by A24,A32,RELAT_1:30;
A34: FD.(x,y) <= a"\/"b by A21,A32;
then consider z1,z2 being Element of FS such that
A35: FD.(x,z1) = a and
A36: FD.(z1,z2) = (FD.(x,y)"\/"a)"/\"b and
A37: FD.(z2,y) = a by Th34;
defpred P[set,set] means
($1 = 1 implies $2 = x) & ($1 = 2 implies $2 = z1) &
($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = y);
A38: for m being Nat, w1,w2 being set st m in Seg 4 & P[m,w1] & P[m,w2]
holds w1 = w2 by Lm3;
A39: for m being Nat st m in Seg 4 ex w being set st P[m,w]
proof
let m be Nat;
assume
A40: m in Seg 4;
per cases by A40,Lm3;
suppose
A41: m = 1;
take w = x;
thus P[m,w] by A41;
suppose
A42: m = 2;
take w = z1;
thus P[m,w] by A42;
suppose
A43: m = 3;
take w = z2;
thus P[m,w] by A43;
suppose
A44: m = 4;
take w = y;
thus P[m,w] by A44;
end;
ex p being FinSequence st dom p = Seg 4 &
for k being Nat st k in Seg 4 holds P[k,p.k] from SeqEx(A38,A39);
then consider h being FinSequence such that
A45: dom h = Seg 4 and
A46: for m being Nat st m in Seg 4 holds
(m = 1 implies h.m = x) & (m = 2 implies h.m = z1) &
(m = 3 implies h.m = z2) & (m = 4 implies h.m = y);
Seg 4 = { n where n is Nat: 1 <= n & n <= 4 } by FINSEQ_1:def 1
;
then A47: 1 in Seg 4 & 2 in Seg 4 & 3 in Seg 4 & 4 in Seg 4;
A48: len h = 4 by A45,FINSEQ_1:def 3;
A49: u = h.1 by A46,A47;
A50: v = h.4 by A46,A47
.= h.(len h) by A45,FINSEQ_1:def 3;
for j being Nat st 1 <= j & j < len h
holds [h.j,h.(j+1)] in e1 \/ e2
proof
let j be Nat;
assume
A51: 1 <= j & j < len h;
per cases by A48,A51,Lm4;
suppose
A52: j = 1;
[x,z1] in e1 by A17,A35;
then [h.1,z1] in e1 by A46,A47;
then [h.1,h.2] in e1 by A46,A47;
hence [h.j,h.(j+1)] in e1 \/ e2 by A52,XBOOLE_0:def 2;
suppose
A53: j = 2;
FD.(x,y)"\/"a <= a"\/"b"\/"a by A34,WAYBEL_1:3;
then FD.(x,y)"\/"a <= b"\/"(a"\/"a) by LATTICE3:14;
then FD.(x,y)"\/"a <= b"\/"a by YELLOW_5:1;
then (FD.(x,y)"\/"a)"/\"b <= b"/\"(b"\/"a) by WAYBEL_1:2;
then (FD.(x,y)"\/"a)"/\"b <= b by LATTICE3:18;
then [z1,z2] in e2 by A19,A36;
then [h.2,z2] in e2 by A46,A47;
then [h.2,h.3] in e2 by A46,A47;
hence [h.j,h.(j+1)] in e1 \/ e2 by A53,XBOOLE_0:def 2;
suppose
A54: j = 3;
[z2,y] in e1 by A17,A37;
then [h.3,y] in e1 by A46,A47;
then [h.3,h.4] in e1 by A46,A47;
hence [h.j,h.(j+1)] in e1 \/ e2 by A54,XBOOLE_0:def 2;
end;
hence [u,v] in e1 "\/" e2 by A33,A48,A49,A50,EQREL_1:36;
end;
hence thesis by RELAT_1:def 3;
end;
sup (f.:{a,b}) = sup {f.a,f.b} by A15,FUNCT_1:118
.= f.a "\/" f.b by YELLOW_0:41
.= e1 "\/" e2 by A16,A18,LATTICE5:10
.= f.(a "\/" b) by A20,A25,A31,XBOOLE_0:def 10
.= f.sup {a,b} by YELLOW_0:41;
hence f preserves_sup_of {a,b} by A14,WAYBEL_0:def 31;
end;
then reconsider f = alpha FD as Homomorphism of L,EqRelLATT FS by
LATTICE5:16;
A55: Image f = subrelstr rng f by YELLOW_2:def 2;
A56: dom f = the carrier of L by FUNCT_2:def 1;
A57: ex e being Equivalence_Relation of FS st
e in the carrier of Image f & e <> id FS
proof
consider A' being non empty set, d' being distance_function of A',L,
Aq' being non empty set, dq' being distance_function of Aq',L
such that
A58: Aq', dq' is_extension2_of A',d' and
A59: S.0 = [A',d'] & S.(0+1) = [Aq',dq'] by Def12;
A' = A & d' = D by A2,A59,ZFMISC_1:33;
then consider q being QuadrSeq of D such that
A60: Aq' = NextSet2(D) and
A61: dq' = NextDelta2(q) by A58,Def11;
A62: (S.1)`2 = NextDelta2(q) by A59,A61,MCART_1:def 2;
(S.1)`2 in { (S.i)`2 where i is Nat: not contradiction};
then A63: NextDelta2(q) c= FD by A62,ZFMISC_1:92;
A64: (S.1)`1 = NextSet2(D) by A59,A60,MCART_1:def 1;
(S.1)`1 in { (S.i)`1 where i is Nat: not contradiction};
then A65: NextSet2(D) c= FS by A64,ZFMISC_1:92;
succ {} c= DistEsti(D) by Th1;
then {} in DistEsti(D) by ORDINAL1:33;
then A66: {} in dom q by LATTICE5:28;
then q.{} in rng q by FUNCT_1:def 5;
then q.{} in {[u,v,a',b'] where u is Element of A, v is Element of A,
a' is Element of L, b' is Element of L: D.(u,v) <= a'"\/"b'}
by LATTICE5:def 14;
then consider u,v be Element of A, a,b be Element of L such that
A67: q.{} = [u,v,a,b] & D.(u,v) <= a"\/"b;
ConsecutiveSet2(A,{}) = A by Th15;
then reconsider Q = Quadr2(q,{}) as
Element of [:A,A,the carrier of L,the carrier of L:];
A68: Quadr2(q,{}) = [u,v,a,b] by A66,A67,Def7;
consider e being Equivalence_Relation of FS such that
A69: e = f.b and
A70: for x,y being Element of FS holds [x,y] in e iff FD.(x,y) <= b
by LATTICE5:def 9;
take e;
e in rng f by A56,A69,FUNCT_1:def 5;
hence e in the carrier of Image f by A55,YELLOW_0:def 15;
A71: new_set2 A = new_set2 ConsecutiveSet2(A,{}) by Th15
.= ConsecutiveSet2(A,succ {}) by Th16;
A72: NextSet2(D) = ConsecutiveSet2(A,DistEsti(D)) by Def9;
A73: succ {} c= DistEsti(D) by Th1;
then A74: new_set2 A c= NextSet2(D) by A71,A72,Th22;
A75: ConsecutiveSet2(A,{}) = A & ConsecutiveDelta2(q,{}) = D by Th15,Th19;
A76: ConsecutiveDelta2(q,succ {}) =
new_bi_fun2(BiFun(ConsecutiveDelta2(q,{}),
ConsecutiveSet2(A,{}),L),Quadr2(q,{})) by Th20
.= new_bi_fun2(D,Q) by A75,LATTICE5:def 16;
ConsecutiveDelta2(q,DistEsti(D)) = NextDelta2(q) by Def10;
then new_bi_fun2(D,Q) c= NextDelta2(q) by A73,A76,Th25;
then A77: new_bi_fun2(D,Q) c= FD by A63,XBOOLE_1:1;
A78: new_set2 A c= FS by A65,A74,XBOOLE_1:1;
A79: dom new_bi_fun2(D,Q) = [:new_set2 A,new_set2 A:] by FUNCT_2:def 1;
{A} in {{A}, {{A}} } by TARSKI:def 2;
then {A} in A \/ {{A}, {{A}} } by XBOOLE_0:def 2;
then A80: {A} in new_set2 A by Def4;
{{A}} in {{A}, {{A}} } by TARSKI:def 2;
then {{A}} in A \/ {{A}, {{A}} } by XBOOLE_0:def 2;
then A81: {{A}} in new_set2 A by Def4;
then A82: [{A},{{A}}] in dom new_bi_fun2(D,Q) by A79,A80,ZFMISC_1:106;
A83: b = Q`4 by A68,MCART_1:def 11;
reconsider W = {A}, V = {{A}} as Element of FS by A78,A80,A81;
FD.(W,V) = FD.[{A},{{A}}] by BINOP_1:def 1
.= new_bi_fun2(D,Q).[{A},{{A}}] by A77,A82,GRFUNC_1:8
.= new_bi_fun2(D,Q).({A},{{A}}) by BINOP_1:def 1
.= (D.(Q`1,Q`2)"\/"Q`3)"/\"Q`4 by Def5;
then FD.(W,V) <= b by A83,YELLOW_0:23;
then A84: [{A},{{A}}] in e by A70;
{A} <> {{A}}
proof
assume {A} = {{A}};
then {A} in {A} by TARSKI:def 1;
hence contradiction;
end;
hence e <> id FS by A84,RELAT_1:def 10;
end;
FS is non trivial set
proof
now
assume that
A85: FS is trivial;
consider x being set such that
A86: FS = {x} by A85,REALSET1:def 12;
consider e being Equivalence_Relation of FS such that
A87: e in the carrier of Image f & e <> id FS by A57;
A88: field e = {x} by A86,EQREL_1:16;
A89: id FS c= e by A86,A88,RELAT_2:17;
A90: [:{x},{x}:] = {[x,x]} by ZFMISC_1:35;
id({x}) = {[x,x]} by SYSREL:30;
hence contradiction by A86,A87,A89,A90,XBOOLE_0:def 10;
end;
hence thesis;
end;
then reconsider FS as non trivial set;
take FS;
reconsider f as Homomorphism of L,EqRelLATT FS;
take f;
thus f is one-to-one by A6,LATTICE5:17;
reconsider FD as distance_function of FS,L;
thus Image f is finitely_typed
proof
take FS;
thus for e being set st e in the carrier of Image f
holds e is Equivalence_Relation of FS
proof
let e be set;
assume
e in the carrier of Image f;
then e in rng f by YELLOW_2:11;
then consider x being set such that
A91: x in dom f and
A92: e = f.x by FUNCT_1:def 5;
reconsider x as Element of L by A91;
consider E being Equivalence_Relation of FS such that
A93: E = f.x and
for u,v being Element of FS holds [u,v] in E iff FD.(u,v) <= x
by LATTICE5:def 9;
thus thesis by A92,A93;
end;
take 2+2;
thus thesis by Th35;
end;
thus ex e being Equivalence_Relation of FS st
e in the carrier of Image f & e <> id FS
proof
consider A' being non empty set, d' being distance_function of A',L,
Aq' being non empty set, dq' being distance_function of Aq',L
such that
A94: Aq', dq' is_extension2_of A',d' and
A95: S.0 = [A',d'] & S.(0+1) = [Aq',dq'] by Def12;
A' = A & d' = D by A2,A95,ZFMISC_1:33;
then consider q being QuadrSeq of D such that
A96: Aq' = NextSet2(D) and
A97: dq' = NextDelta2(q) by A94,Def11;
A98: (S.1)`2 = NextDelta2(q) by A95,A97,MCART_1:def 2;
(S.1)`2 in { (S.i)`2 where i is Nat: not contradiction};
then A99: NextDelta2(q) c= FD by A98,ZFMISC_1:92;
A100: (S.1)`1 = NextSet2(D) by A95,A96,MCART_1:def 1;
(S.1)`1 in { (S.i)`1 where i is Nat: not contradiction};
then A101: NextSet2(D) c= FS by A100,ZFMISC_1:92;
succ {} c= DistEsti(D) by Th1;
then {} in DistEsti(D) by ORDINAL1:33;
then A102: {} in dom q by LATTICE5:28;
then q.{} in rng q by FUNCT_1:def 5;
then q.{} in {[u,v,a',b'] where u is Element of A, v is Element of A,
a' is Element of L, b' is Element of L: D.(u,v) <= a'"\/"b'}
by LATTICE5:def 14;
then consider u,v be Element of A, a,b be Element of L such that
A103: q.{} = [u,v,a,b] & D.(u,v) <= a"\/"b;
ConsecutiveSet2(A,{}) = A by Th15;
then reconsider Q = Quadr2(q,{}) as
Element of [:A,A,the carrier of L,the carrier of L:];
A104: Quadr2(q,{}) = [u,v,a,b] by A102,A103,Def7;
consider e being Equivalence_Relation of FS such that
A105: e = f.b and
A106: for x,y being Element of FS holds [x,y] in e iff FD.(x,y) <= b
by LATTICE5:def 9;
take e;
e in rng f by A56,A105,FUNCT_1:def 5;
hence e in the carrier of Image f by A55,YELLOW_0:def 15;
A107: new_set2 A = new_set2 ConsecutiveSet2(A,{}) by Th15
.= ConsecutiveSet2(A,succ {}) by Th16;
A108: NextSet2(D) = ConsecutiveSet2(A,DistEsti(D)) by Def9;
A109: succ {} c= DistEsti(D) by Th1;
then A110: new_set2 A c= NextSet2(D) by A107,A108,Th22;
A111: ConsecutiveSet2(A,{}) = A & ConsecutiveDelta2(q,{}) = D by Th15,Th19;
A112: ConsecutiveDelta2(q,succ {}) =
new_bi_fun2(BiFun(ConsecutiveDelta2(q,{}),
ConsecutiveSet2(A,{}),L),Quadr2(q,{})) by Th20
.= new_bi_fun2(D,Q) by A111,LATTICE5:def 16;
ConsecutiveDelta2(q,DistEsti(D)) = NextDelta2(q) by Def10;
then new_bi_fun2(D,Q) c= NextDelta2(q) by A109,A112,Th25;
then A113: new_bi_fun2(D,Q) c= FD by A99,XBOOLE_1:1;
A114: new_set2 A c= FS by A101,A110,XBOOLE_1:1;
A115: dom new_bi_fun2(D,Q) = [:new_set2 A,new_set2 A:] by FUNCT_2:def 1;
{A} in {{A}, {{A}} } by TARSKI:def 2;
then {A} in A \/ {{A}, {{A}} } by XBOOLE_0:def 2;
then A116: {A} in new_set2 A by Def4;
{{A}} in {{A}, {{A}} } by TARSKI:def 2;
then {{A}} in A \/ {{A}, {{A}} } by XBOOLE_0:def 2;
then A117: {{A}} in new_set2 A by Def4;
then A118: [{A},{{A}}] in dom new_bi_fun2(D,Q) by A115,A116,ZFMISC_1:106;
A119: b = Q`4 by A104,MCART_1:def 11;
reconsider W = {A}, V = {{A}} as Element of FS by A114,A116,A117;
FD.(W,V) = FD.[{A},{{A}}] by BINOP_1:def 1
.= new_bi_fun2(D,Q).[{A},{{A}}] by A113,A118,GRFUNC_1:8
.= new_bi_fun2(D,Q).({A},{{A}}) by BINOP_1:def 1
.= (D.(Q`1,Q`2)"\/"Q`3)"/\"Q`4 by Def5;
then FD.(W,V) <= b by A119,YELLOW_0:23;
then A120: [{A},{{A}}] in e by A106;
{A} <> {{A}}
proof
assume {A} = {{A}};
then {A} in {A} by TARSKI:def 1;
hence contradiction;
end;
hence e <> id FS by A120,RELAT_1:def 10;
end;
for e1,e2 being Equivalence_Relation of FS
for x,y being set st
e1 in the carrier of Image f & e2 in the carrier of Image f &
[x,y] in e1 "\/" e2
ex F being non empty FinSequence of FS st
len F = 2+2 & x,y are_joint_by F,e1,e2 by Th35;
hence type_of Image f <= 2 by A57,LATTICE5:15;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: <=> :: L has_a_representation_of_type<= 2 iff L is modular ::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
theorem
for L be lower-bounded LATTICE
holds L has_a_representation_of_type<= 2 iff L is modular by Th9,Th36;