:: J\'onsson Theorem
:: by Jaros{\l}aw Gryko
::
:: Received November 13, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, FUNCOP_1, TARSKI, RELAT_1, FUNCT_6, XBOOLE_0,
ZFMISC_1, SUBSET_1, ORDINAL1, ORDERS_2, LATTICE3, MSUALG_5, STRUCT_0,
EQREL_1, PBOOLE, LATTICES, XXREAL_0, REWRITE1, SETFAM_1, RELAT_2,
WAYBEL_0, GROUP_6, YELLOW_0, ORDINAL2, FINSEQ_1, ARYTM_3, ABIAN,
FINSEQ_2, ARYTM_1, CARD_1, ORDINAL4, NAT_1, VALUED_0, FUNCT_2, MCART_1,
PARTFUN1, LATTICE5, RECDEF_2;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1,
RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, FUNCT_6, CARD_1, XCMPLX_0,
ORDINAL1, NUMBERS, NAT_1, NAT_D, SETFAM_1, ORDINAL2, MCART_1, DOMAIN_1,
PARTFUN1, FUNCOP_1, STRUCT_0, ORDERS_2, EQREL_1, MSUALG_5, FINSEQ_1,
FINSEQ_2, SEQ_4, LATTICES, LATTICE3, BINOP_1, YELLOW_0, WAYBEL_0,
YELLOW_2, ABIAN, XXREAL_0;
constructors SETFAM_1, BINOP_1, DOMAIN_1, ORDINAL2, NAT_1, CLASSES1, SEQ_4,
FINSOP_1, FUNCT_6, RFUNCT_3, BINARITH, ABIAN, LATTICE3, MSUALG_5,
YELLOW_2, NAT_D, RELSET_1, XTUPLE_0, NUMBERS, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, PARTFUN1, FUNCOP_1, XREAL_0,
CARD_1, MEMBERED, FINSEQ_1, ABIAN, STRUCT_0, LATTICES, LATTICE3,
YELLOW_0, YELLOW_1, RELAT_1, XXREAL_2, RELSET_1, FINSEQ_2, FUNCT_1,
XTUPLE_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, LATTICE3, FUNCOP_1, WAYBEL_0, XBOOLE_0;
equalities TARSKI, LATTICE3, BINOP_1, FINSEQ_1, FINSEQ_2, ORDINAL1;
expansions TARSKI, LATTICE3, WAYBEL_0, XBOOLE_0, BINOP_1, ORDINAL1;
theorems EQREL_1, RELAT_1, RELAT_2, FINSEQ_1, FINSEQ_2, MSUALG_5, ORDERS_2,
TARSKI, ENUMSET1, ORDINAL1, ORDINAL3, WELLORD2, TREES_2, PARTFUN1,
GRFUNC_1, FUNCT_6, FINSEQ_5, NAT_1, INT_1, ZFMISC_1, FUNCT_1, FUNCT_2,
FILTER_0, LATTICES, LATTICE3, YELLOW_0, YELLOW_2, YELLOW_3, YELLOW_5,
WAYBEL_0, WAYBEL_1, WAYBEL_6, RELSET_1, CARD_1, FINSEQ_3, SETFAM_1,
XBOOLE_0, XBOOLE_1, ORDERS_1, FUNCOP_1, XREAL_1, XXREAL_0, XXREAL_2,
XREAL_0, XTUPLE_0, XREGULAR;
schemes DOMAIN_1, FUNCT_2, RELSET_1, RECDEF_1, ORDINAL2, NAT_1, FINSEQ_1,
CLASSES1, BINOP_1;
begin :: Preliminaries
theorem Th1:
for f being Function, F being Function-yielding Function st f =
union rng F holds dom f = union rng doms F
proof
let f be Function;
let F be Function-yielding Function;
assume
A1: f = union rng F;
thus dom f c= union rng doms F
proof
let x be object;
assume x in dom f;
then [x,f.x] in union rng F by A1,FUNCT_1:def 2;
then consider g being set such that
A2: [x,f.x] in g and
A3: g in rng F by TARSKI:def 4;
consider u being object such that
A4: u in dom F and
A5: g = F.u by A3,FUNCT_1:def 3;
u in dom doms F by A4,A5,FUNCT_6:22;
then
A6: (doms F).u in rng doms F by FUNCT_1:def 3;
x in dom (F.u) by A2,A5,FUNCT_1:1;
then x in (doms F).u by A4,FUNCT_6:22;
hence thesis by A6,TARSKI:def 4;
end;
let x be object;
assume x in union rng doms F;
then consider A be set such that
A7: x in A and
A8: A in rng doms F by TARSKI:def 4;
consider u being object such that
A9: u in dom doms F and
A10: A = (doms F).u by A8,FUNCT_1:def 3;
A11: u in dom F by A9,FUNCT_6:59;
then
A12: F.u in rng F by FUNCT_1:def 3;
consider g being Function such that
A13: g = F.u;
A = dom (F.u) by A10,A11,FUNCT_6:22;
then [x,g.x] in F.u by A7,A13,FUNCT_1:def 2;
then [x,g.x] in f by A1,A12,TARSKI:def 4;
hence thesis by FUNCT_1:1;
end;
theorem Th2:
for A,B being non empty set holds [:union A, union B:] = union {
[:a,b:] where a is Element of A, b is Element of B : a in A & b in B }
proof
let A,B be non empty set;
set Y = { [:a,b:] where a is Element of A, b is Element of B : a in A & b in
B };
thus [:union A, union B:] c= union Y
proof
let z be object;
assume
A1: z in [:union A, union B:];
then consider x,y being object such that
A2: z = [x,y] by RELAT_1:def 1;
y in union B by A1,A2,ZFMISC_1:87;
then consider b9 being set such that
A3: y in b9 and
A4: b9 in B by TARSKI:def 4;
x in union A by A1,A2,ZFMISC_1:87;
then consider a9 being set such that
A5: x in a9 and
A6: a9 in A by TARSKI:def 4;
reconsider b9 as Element of B by A4;
reconsider a9 as Element of A by A6;
A7: [:a9,b9:] in Y;
z in [:a9,b9:] by A2,A5,A3,ZFMISC_1:def 2;
hence thesis by A7,TARSKI:def 4;
end;
let z be object;
assume z in union Y;
then consider e being set such that
A8: z in e and
A9: e in Y by TARSKI:def 4;
consider a9 being Element of A, b9 being Element of B such that
A10: [:a9,b9:] = e and
a9 in A and
b9 in B by A9;
consider x,y being object such that
A11: x in a9 & y in b9 and
A12: z = [x,y] by A8,A10,ZFMISC_1:def 2;
x in union A & y in union B by A11,TARSKI:def 4;
hence thesis by A12,ZFMISC_1:def 2;
end;
theorem Th3:
for A being non empty set st A is c=-linear holds [:union A,
union A:] = union { [:a,a:] where a is Element of A : a in A }
proof
let A be non empty set;
set X = { [:a,a:] where a is Element of A : a in A }, Y = { [:a,b:] where a
is Element of A, b is Element of A : a in A & b in A };
assume
A1: A is c=-linear;
A2: union Y c= union X
proof
let Z be object;
assume Z in union Y;
then consider z being set such that
A3: Z in z and
A4: z in Y by TARSKI:def 4;
consider a,b being Element of A such that
A5: z = [:a,b:] and
a in A and
b in A by A4;
A6: a,b are_c=-comparable by A1;
per cases by A6;
suppose
A7: a c= b;
A8: [:b,b:] in X;
[:a,b:] c= [:b,b:] by A7,ZFMISC_1:95;
hence thesis by A3,A5,A8,TARSKI:def 4;
end;
suppose
A9: b c= a;
A10: [:a,a:] in X;
[:a,b:] c= [:a,a:] by A9,ZFMISC_1:95;
hence thesis by A3,A5,A10,TARSKI:def 4;
end;
end;
X c= Y
proof
let Z be object;
assume Z in X;
then ex a being Element of A st Z = [:a,a:] & a in A;
hence thesis;
end;
then union X c= union Y by ZFMISC_1:77;
then union X = union Y by A2;
hence thesis by Th2;
end;
begin :: An equivalence lattice of a set
reserve X for non empty set;
definition
let A be set;
func EqRelLATT A -> Poset equals
LattPOSet EqRelLatt A;
correctness;
end;
registration
let A be set;
cluster EqRelLATT A -> with_infima with_suprema;
coherence;
end;
theorem Th4:
for A, x being set holds x in the carrier of EqRelLATT A iff x is
Equivalence_Relation of A
proof
let A, x be set;
hereby
assume x in the carrier of EqRelLATT A;
then reconsider e = x as Element of LattPOSet EqRelLatt A;
%e = e;
then
A1: x in the carrier of EqRelLatt A;
the carrier of EqRelLatt A = {r where r is Relation of A,A : r is
Equivalence_Relation of A} by MSUALG_5:def 2;
then
ex x9 being Relation of A,A st x9 = x & x9 is Equivalence_Relation of
A by A1;
hence x is Equivalence_Relation of A;
end;
A2: the carrier of EqRelLatt A = {r where r is Relation of A,A : r is
Equivalence_Relation of A} by MSUALG_5:def 2;
assume x is Equivalence_Relation of A;
then x in the carrier of EqRelLatt A by A2;
then reconsider e = x as Element of EqRelLatt A;
reconsider e as Element of EqRelLATT A;
e in the carrier of EqRelLATT A;
hence thesis;
end;
theorem Th5:
for A being set, x,y being Element of EqRelLatt A holds x [= y iff x c= y
proof
let A be set, x,y be Element of EqRelLatt A;
reconsider x9 = x,y9 = y as Equivalence_Relation of A by MSUALG_5:21;
A1: x9 /\ y9 = x9 iff x9 c= y9 by XBOOLE_1:17,28;
x "/\" y = (the L_meet of EqRelLatt A).(x9,y9) by LATTICES:def 2
.= x9 /\ y9 by MSUALG_5:def 2;
hence thesis by A1,LATTICES:4;
end;
theorem Th6:
for A being set, a,b being Element of EqRelLATT A holds a <= b iff a c= b
proof
let A be set, a,b be Element of EqRelLATT A;
set El = EqRelLatt A;
reconsider a9 = a as Element of El;
reconsider b9 = b as Element of El;
thus a <= b implies a c= b
proof
assume a <= b;
then a9% <= b9%;
then a9 [= b9 by LATTICE3:7;
hence thesis by Th5;
end;
thus a c= b implies a <= b
proof
assume a c= b;
then a9 [= b9 by Th5;
then a9% <= b9% by LATTICE3:7;
hence thesis;
end;
end;
theorem Th7:
for L being Lattice, a,b being Element of LattPOSet L holds a
"/\" b = %a "/\" %b
proof
let L be Lattice, a,b be Element of LattPOSet L;
reconsider x = a, y = b as Element of L;
set c = x "/\" y;
A1: c [= x by LATTICES:6;
A2: c [= y by LATTICES:6;
A3: c% = c;
reconsider c as Element of LattPOSet L;
A4: y% = y;
then
A5: c <= b by A2,A3,LATTICE3:7;
A6: x% = x;
A7: for d being Element of LattPOSet L st d <= a & d <= b holds d <= c
proof
let d be Element of LattPOSet L;
reconsider z = d as Element of L;
A8: z% = z;
assume d <= a & d <= b;
then z [= x & z [= y by A6,A4,A8,LATTICE3:7;
then z [= x "/\" y by FILTER_0:7;
hence thesis by A3,A8,LATTICE3:7;
end;
c <= a by A1,A3,A6,LATTICE3:7;
hence thesis by A5,A7,YELLOW_0:23;
end;
theorem Th8:
for A being set, a,b being Element of EqRelLATT A holds a "/\" b = a /\ b
proof
let A be set, a,b be Element of EqRelLATT A;
A1: now
let x,y be Element of EqRelLatt A;
reconsider e1 = x as Equivalence_Relation of A by MSUALG_5:21;
reconsider e2 = y as Equivalence_Relation of A by MSUALG_5:21;
thus x "/\" y = (the L_meet of EqRelLatt A).(e1,e2) by LATTICES:def 2
.= x /\ y by MSUALG_5:def 2;
end;
reconsider y = b as Element of LattPOSet EqRelLatt A;
reconsider x = a as Element of LattPOSet EqRelLatt A;
reconsider x as Element of EqRelLatt A;
reconsider y as Element of EqRelLatt A;
%(x%) = x% & %(y%) = y%;
hence a "/\" b = x "/\" y by Th7
.= a /\ b by A1;
end;
theorem Th9:
for L being Lattice, a,b being Element of LattPOSet L holds a
"\/" b = %a "\/" %b
proof
let L be Lattice, a,b be Element of LattPOSet L;
reconsider x = a, y = b as Element of L;
set c = x "\/" y;
A1: c% = c;
A2: y [= c & y% = y by LATTICES:5;
A3: x [= c & x% = x by LATTICES:5;
reconsider c as Element of LattPOSet L;
A4: b <= c by A1,A2,LATTICE3:7;
A5: for d being Element of LattPOSet L st a <= d & b <= d holds c <= d
proof
let d be Element of LattPOSet L;
assume that
A6: a <= d and
A7: b <= d;
reconsider z = d as Element of L;
y% <= z% by A7;
then
A8: y [= z by LATTICE3:7;
x% <= z% by A6;
then x [= z by LATTICE3:7;
then x "\/" y [= z by A8,FILTER_0:6;
then (x "\/" y)% <= z% by LATTICE3:7;
hence thesis;
end;
a <= c by A1,A3,LATTICE3:7;
hence thesis by A4,A5,YELLOW_0:22;
end;
theorem Th10:
for A being set, a,b being Element of EqRelLATT A for E1,E2
being Equivalence_Relation of A st a = E1 & b = E2 holds a "\/" b = E1 "\/" E2
proof
let A be set, a,b be Element of EqRelLATT A, E1,E2 be Equivalence_Relation
of A;
assume
A1: a = E1 & b = E2;
reconsider y = b as Element of LattPOSet EqRelLatt A;
reconsider x = a as Element of LattPOSet EqRelLatt A;
reconsider x as Element of EqRelLatt A;
reconsider y as Element of EqRelLatt A;
%(x%) = x% & %(y%) = y%;
hence a "\/" b = x "\/" y by Th9
.= (the L_join of EqRelLatt A).(x,y) by LATTICES:def 1
.= E1 "\/" E2 by A1,MSUALG_5:def 2;
end;
definition
let L be non empty RelStr;
redefine attr L is complete means :: redefines complete (LATTICE3, definition)
for X being Subset of L ex a being Element
of L st a is_<=_than X & for b being Element of L st b is_<=_than X holds b <=
a;
compatibility
proof
hereby
assume
A1: L is complete;
let X be Subset of L;
set Y = { c where c is Element of L: c is_<=_than X };
consider p being Element of L such that
A2: Y is_<=_than p and
A3: for r being Element of L st Y is_<=_than r holds p <= r by A1;
take p;
thus p is_<=_than X
proof
let q be Element of L;
assume
A4: q in X;
Y is_<=_than q
proof
let s be Element of L;
assume s in Y;
then ex t being Element of L st s = t & t is_<=_than X;
hence thesis by A4;
end;
hence thesis by A3;
end;
let b be Element of L;
assume b is_<=_than X;
then b in Y;
hence b <= p by A2;
end;
assume
A5: for X being Subset of L ex a being Element of L st a is_<=_than X
& for b being Element of L st b is_<=_than X holds b <= a;
let X be set;
set Y = { c where c is Element of L: X is_<=_than c };
Y c= the carrier of L
proof
let x be object;
assume x in Y;
then ex c being Element of L st x = c & X is_<=_than c;
hence thesis;
end;
then consider p being Element of L such that
A6: p is_<=_than Y and
A7: for r being Element of L st r is_<=_than Y holds r <= p by A5;
take p;
thus X is_<=_than p
proof
let q be Element of L;
assume
A8: q in X;
q is_<=_than Y
proof
let s be Element of L;
assume s in Y;
then ex t being Element of L st s = t & X is_<=_than t;
hence thesis by A8;
end;
hence thesis by A7;
end;
let r be Element of L;
assume X is_<=_than r;
then r in Y;
hence thesis by A6;
end;
end;
registration
let A be set;
cluster EqRelLATT A -> complete;
coherence
proof
let X be Subset of EqRelLATT A;
set B = X /\ the carrier of EqRelLATT A;
B c= bool [:A,A:]
proof
let x be object;
assume x in B;
then x is Equivalence_Relation of A by Th4;
hence thesis;
end;
then reconsider B as Subset-Family of [:A,A:];
consider b being Subset of [:A,A:] such that
A1: b = Intersect(B);
for x being object holds x in A implies [x,x] in b
proof
let x be object;
assume
A2: x in A;
A3: for Y being set st Y in B holds [x,x] in Y
proof
let Y be set;
assume Y in B;
then Y is Equivalence_Relation of A by Th4;
hence thesis by A2,EQREL_1:5;
end;
[x,x] in [:A,A:] by A2,ZFMISC_1:def 2;
hence thesis by A1,A3,SETFAM_1:43;
end;
then
A4: b is_reflexive_in A by RELAT_2:def 1;
reconsider b as Relation of A;
A5: dom b = A & field b = A by A4,ORDERS_1:13;
for x,y,z being object holds x in A & y in A & z in A & [x,y] in b & [y,
z] in b implies [x,z] in b
proof
let x,y,z be object;
assume that
A6: x in A and
y in A and
A7: z in A and
A8: [x,y] in b & [y,z] in b;
A9: for Y being set st Y in B holds [x,z] in Y
proof
let Y be set;
assume
A10: Y in B;
then
A11: Y is Equivalence_Relation of A by Th4;
[x,y] in Y & [y,z] in Y by A1,A8,A10,SETFAM_1:43;
hence thesis by A11,EQREL_1:7;
end;
[x,z] in [:A,A:] by A6,A7,ZFMISC_1:def 2;
hence thesis by A1,A9,SETFAM_1:43;
end;
then
A12: b is_transitive_in A by RELAT_2:def 8;
for x,y being object st x in A & y in A & [x,y] in b holds [y,x] in b
proof
let x,y be object;
assume that
A13: x in A & y in A and
A14: [x,y] in b;
A15: for Y being set st Y in B holds [y,x] in Y
proof
let Y be set;
assume Y in B;
then [x,y] in Y & Y is Equivalence_Relation of A by A1,A14,Th4,
SETFAM_1:43;
hence thesis by EQREL_1:6;
end;
[y,x] in [:A,A:] by A13,ZFMISC_1:def 2;
hence thesis by A1,A15,SETFAM_1:43;
end;
then b is_symmetric_in A by RELAT_2:def 3;
then reconsider b as Equivalence_Relation of A by A5,A12,PARTFUN1:def 2
,RELAT_2:def 11,def 16;
reconsider b as Element of EqRelLATT A by Th4;
take b;
now
let a be Element of EqRelLATT A;
reconsider a9 = a as Equivalence_Relation of A by Th4;
reconsider b9 = b as Equivalence_Relation of A;
assume a in X /\ the carrier of EqRelLATT A;
then for x,y being object holds [x,y] in b9 implies [x,y] in a9 by A1,
SETFAM_1:43;
then b9 c= a9 by RELAT_1:def 3;
hence b <= a by Th6;
end;
then b is_<=_than X /\ the carrier of EqRelLATT A;
hence b is_<=_than X by YELLOW_0:5;
let a be Element of EqRelLATT A;
reconsider a9 = a as Equivalence_Relation of A by Th4;
assume a is_<=_than X;
then
A16: a is_<=_than X /\ the carrier of EqRelLATT A by YELLOW_0:5;
A17: for d being Element of EqRelLATT A st d in B holds a9 c= d
by A16,Th6;
a9 c= Intersect(B)
proof
let x be object;
assume
A18: x in a9;
for Y being set st Y in B holds x in Y
proof
let Y be set;
assume Y in B;
then a9 c= Y by A17;
hence thesis by A18;
end;
hence thesis by A18,SETFAM_1:43;
end;
hence a <= b by A1,Th6;
end;
end;
begin :: A type of a sublattice of equivalence lattice of a set
registration
let L1,L2 be LATTICE;
cluster meet-preserving join-preserving for Function of L1,L2;
existence
proof
set z = the Element of L2;
reconsider f = (the carrier of L1) --> z as Function of L1,L2;
take f;
for x,y being Element of L1 holds f.(x "/\" y) = f.x "/\" f.y
by YELLOW_5:2;
hence f is meet-preserving by WAYBEL_6:1;
for x,y being Element of L1 holds f.(x "\/" y) = f.x "\/" f.y
by YELLOW_5:1;
hence thesis by WAYBEL_6:2;
end;
end;
definition
let L1,L2 be LATTICE;
mode Homomorphism of L1,L2
is meet-preserving join-preserving Function of L1,L2;
end;
registration
let L be LATTICE;
cluster meet-inheriting join-inheriting strict for SubRelStr of L;
existence
proof
set a = the Element of L;
set r = the Relation of {a};
A1: for x,y being Element of L st x in {a} & y in {a} & ex_sup_of {x,y},L
holds sup {x,y} in {a}
proof
let x,y be Element of L;
assume that
A2: x in {a} & y in {a} and
ex_sup_of {x,y},L;
x = a & y = a by A2,TARSKI:def 1;
then sup {x,y} = a"\/"a by YELLOW_0:41
.= a by YELLOW_5:1;
hence thesis by TARSKI:def 1;
end;
r c= the InternalRel of L
proof
let z be object;
assume z in r;
then consider x,y be object such that
A3: z = [x,y] and
A4: x in {a} and
A5: y in {a} by RELSET_1:2;
x = a by A4,TARSKI:def 1;
then
A6: z = [a,a] by A3,A5,TARSKI:def 1;
a <= a;
hence thesis by A6,ORDERS_2:def 5;
end;
then reconsider S=RelStr(# {a}, r#) as strict SubRelStr of L by
YELLOW_0:def 13;
take S;
for x,y being Element of L st x in {a} & y in {a} & ex_inf_of {x,y},L
holds inf {x,y} in {a}
proof
let x,y be Element of L;
assume that
A7: x in {a} & y in {a} and
ex_inf_of {x,y},L;
x = a & y = a by A7,TARSKI:def 1;
then inf {x,y} = a"/\"a by YELLOW_0:40
.= a by YELLOW_5:2;
hence thesis by TARSKI:def 1;
end;
hence thesis by A1,YELLOW_0:def 16,def 17;
end;
end;
definition
let L be non empty RelStr;
mode Sublattice of L is meet-inheriting join-inheriting SubRelStr of L;
end;
registration
let L1, L2 be LATTICE;
let f be Homomorphism of L1,L2;
cluster Image f -> meet-inheriting join-inheriting;
coherence
proof
set S = subrelstr rng f;
A1: the carrier of S = rng f by YELLOW_0:def 15;
A2: dom f = the carrier of L1 by FUNCT_2:def 1;
for x,y being Element of L2 st x in the carrier of S & y in the
carrier of S & ex_sup_of {x,y},L2 holds sup {x,y} in the carrier of S
proof
let x,y be Element of L2;
assume that
A3: x in the carrier of S and
A4: y in the carrier of S and
ex_sup_of {x,y},L2;
consider a being object such that
A5: a in dom f and
A6: x = f.a by A1,A3,FUNCT_1:def 3;
consider b being object such that
A7: b in dom f and
A8: y = f.b by A1,A4,FUNCT_1:def 3;
reconsider a9 = a, b9 = b as Element of L1 by A5,A7;
A9: f preserves_sup_of {a9,b9} & ex_sup_of {a9,b9},L1 by WAYBEL_0:def 35
,YELLOW_0:20;
sup {x,y} = sup (f.:{a9,b9}) by A5,A6,A7,A8,FUNCT_1:60
.= f.sup {a9,b9} by A9;
hence thesis by A1,A2,FUNCT_1:def 3;
end;
then
A10: S is join-inheriting by YELLOW_0:def 17;
for x,y being Element of L2 st x in the carrier of S & y in the
carrier of S & ex_inf_of {x,y},L2 holds inf {x,y} in the carrier of S
proof
let x,y be Element of L2;
assume that
A11: x in the carrier of S and
A12: y in the carrier of S and
ex_inf_of {x,y},L2;
consider a being object such that
A13: a in dom f and
A14: x = f.a by A1,A11,FUNCT_1:def 3;
consider b being object such that
A15: b in dom f and
A16: y = f.b by A1,A12,FUNCT_1:def 3;
reconsider a9 = a, b9 = b as Element of L1 by A13,A15;
A17: f preserves_inf_of {a9,b9} & ex_inf_of {a9,b9},L1 by WAYBEL_0:def 34
,YELLOW_0:21;
inf {x,y} = inf (f.:{a9,b9}) by A13,A14,A15,A16,FUNCT_1:60
.= f.inf {a9,b9} by A17;
hence thesis by A1,A2,FUNCT_1:def 3;
end;
then S is meet-inheriting by YELLOW_0:def 16;
hence thesis by A10,YELLOW_2:def 2;
end;
end;
reserve e,e1,e2,e19,e29 for Equivalence_Relation of X,
x,y,x9,y9 for set;
definition
let X;
let f be non empty FinSequence of X;
let x,y be object;
let R1, R2 be Relation;
pred x,y are_joint_by f,R1,R2 means
f.1 = x & f.(len f) = y & for i
being Element of NAT st 1 <= i & i < len f holds (i is odd implies [f.i,f.(i+1)
] in R1) & (i is even implies [f.i,f.(i+1)] in R2);
end;
theorem Th11:
for x being set, o being Element of NAT, R1,R2 being Relation, f
being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X
& f = o |-> x holds x,x are_joint_by f,R1,R2
proof
let x be set, o be Element of NAT, R1,R2 be Relation, f be non empty
FinSequence of X;
assume that
A1: R1 is_reflexive_in X and
A2: R2 is_reflexive_in X and
A3: f = o |-> x;
A4: dom f = Seg(o) by A3;
then
A5: f.1 = x by A3,FINSEQ_5:6,FUNCOP_1:7;
A6: for i being Element of NAT st 1 <= i & i < len f holds (i is odd implies
[f.i,f.(i+1)] in R1) & (i is even implies [f.i,f.(i+1)] in R2)
proof
let i be Element of NAT;
assume that
A7: 1 <= i and
A8: i < len f;
A9: i is even implies [f.i,f.(i+1)] in R2
proof
1 <= i+1 & i+1 <= len f by A7,A8,NAT_1:13;
then i+1 in Seg(len f);
then i+1 in Seg(o) by A3,CARD_1:def 7;
then
A10: f.(i+1) = x by A3,FUNCOP_1:7;
assume i is even;
i <= o by A3,A8,CARD_1:def 7;
then i in Seg(o) by A7;
then
A11: f.i = x by A3,FUNCOP_1:7;
x in X by A4,A5,FINSEQ_2:11,FINSEQ_5:6;
hence thesis by A2,A10,A11,RELAT_2:def 1;
end;
i is odd implies [f.i,f.(i+1)] in R1
proof
1 <= i+1 & i+1 <= len f by A7,A8,NAT_1:13;
then i+1 in Seg(len f);
then i+1 in Seg(o) by A3,CARD_1:def 7;
then
A12: f.(i+1) = x by A3,FUNCOP_1:7;
assume i is odd;
i <= o by A3,A8,CARD_1:def 7;
then i in Seg(o) by A7;
then
A13: f.i = x by A3,FUNCOP_1:7;
x in X by A4,A5,FINSEQ_2:11,FINSEQ_5:6;
hence thesis by A1,A12,A13,RELAT_2:def 1;
end;
hence thesis by A9;
end;
len f in Seg(o) by A4,FINSEQ_5:6;
then f.(len f) = x by A3,FUNCOP_1:7;
hence thesis by A5,A6;
end;
Lm1: now
let i,n,m be Element of NAT;
assume 1 <= i & i < n+m;
then 1 <= i & i < n or n = i & i < n+m or n < i & i < n+m by XXREAL_0:1;
hence 1 <= i & i < n or n = i & i < n+m or n+1 <= i & i < n+m by NAT_1:13;
end;
theorem Th12:
for x,y being object, R1,R2 being Relation, n,m being Element of
NAT st (n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non
empty FinSequence of X st len f = n & x,y are_joint_by f,R1,R2) ex h being non
empty FinSequence of X st len h = m & x,y are_joint_by h,R1,R2
proof
let x,y be object, R1,R2 be Relation, n,m be Element of NAT;
assume that
A1: n <= m and
A2: R1 is_reflexive_in X and
A3: R2 is_reflexive_in X;
given f being non empty FinSequence of X such that
A4: len f = n and
A5: x,y are_joint_by f,R1,R2;
A6: f.(len f) = y by A5;
per cases by A1,XXREAL_0:1;
suppose
A7: n < m;
len f in dom f by FINSEQ_5:6;
then y in rng f by A6,FUNCT_1:def 3;
then reconsider y9 = y as Element of X;
reconsider i = m - n as Element of NAT by A1,INT_1:5;
reconsider g = i |-> y9 as FinSequence of X;
i > 0 by A7,XREAL_1:50;
then reconsider g as non empty FinSequence of X;
A8: 1 in dom g by FINSEQ_5:6;
reconsider h = f^g as non empty FinSequence of X;
take h;
A9: len g = m-n by CARD_1:def 7;
A10: y,y are_joint_by g,R1,R2 by A2,A3,Th11;
thus len h = len f + len g by FINSEQ_1:22
.= n+(m-n) by A4,CARD_1:def 7
.= m;
A11: len g in dom g by FINSEQ_5:6;
thus x,y are_joint_by h,R1,R2
proof
rng f <> {};
then 1 in dom f by FINSEQ_3:32;
hence h.1 = f.1 by FINSEQ_1:def 7
.= x by A5;
thus h.(len h) = h.(len f + len g) by FINSEQ_1:22
.= g.(len g) by A11,FINSEQ_1:def 7
.= y by A10;
let j be Element of NAT;
A12: dom f = Seg(len f) by FINSEQ_1:def 3;
assume
A13: 1 <= j & j < len h;
thus j is odd implies [h.j,h.(j+1)] in R1
proof
assume
A14: j is odd;
per cases by A13,Lm1,FINSEQ_1:22;
suppose
A15: 1 <= j & j < len f;
then 1 <= j+1 & j+1 <= len f by NAT_1:13;
then j+1 in dom f by A12;
then
A16: f.(j+1) = h.(j+1) by FINSEQ_1:def 7;
j in dom f by A12,A15;
then f.j = h.j by FINSEQ_1:def 7;
hence thesis by A5,A14,A15,A16;
end;
suppose
A17: j = len f;
then j in dom f by FINSEQ_5:6;
then
A18: h.j = y by A6,A17,FINSEQ_1:def 7;
h.(j+1) = g.1 by A8,A17,FINSEQ_1:def 7
.= y by A10;
hence thesis by A2,A18,RELAT_2:def 1;
end;
suppose
A19: len f + 1 <= j & j < len f + len g;
then j+1 <= len f + len g by NAT_1:13;
then
A20: j+1 <= len h by FINSEQ_1:22;
A21: 1 <= j - len f by A19,XREAL_1:19;
then 0 < j - len f by XXREAL_0:2;
then
A22: 0 + len f < j -len f + len f by XREAL_1:6;
then reconsider k = j - len f as Element of NAT by INT_1:5;
A23: j - len f < len f + len g - len f by A19,XREAL_1:9;
then
A24: k+1 <= len g by NAT_1:13;
j < j+1 by XREAL_1:29;
then len f < j+1 by A22,XXREAL_0:2;
then
A25: h.(j+1) = g.(j+1-len f) by A20,FINSEQ_1:24
.= g.(k+1);
1 <= k+1 by A21,NAT_1:13;
then k+1 in Seg (len g) by A24;
then
A26: g.(k+1) = y by A9,FUNCOP_1:7;
k in Seg (len g) by A21,A23;
then g.k = y by A9,FUNCOP_1:7;
then h.j = y by A19,FINSEQ_1:23;
hence thesis by A2,A26,A25,RELAT_2:def 1;
end;
end;
assume
A27: j is even;
per cases by A13,Lm1,FINSEQ_1:22;
suppose
A28: 1 <= j & j < len f;
then 1 <= j+1 & j+1 <= len f by NAT_1:13;
then j+1 in dom f by A12;
then
A29: f.(j+1) = h.(j+1) by FINSEQ_1:def 7;
j in dom f by A12,A28;
then f.j = h.j by FINSEQ_1:def 7;
hence thesis by A5,A27,A28,A29;
end;
suppose
A30: j = len f;
then j in dom f by FINSEQ_5:6;
then
A31: h.j = y by A6,A30,FINSEQ_1:def 7;
h.(j+1) = g.1 by A8,A30,FINSEQ_1:def 7
.= y by A10;
hence thesis by A3,A31,RELAT_2:def 1;
end;
suppose
A32: len f + 1 <= j & j < len f + len g;
then j+1 <= len f + len g by NAT_1:13;
then
A33: j+1 <= len h by FINSEQ_1:22;
A34: 1 <= j - len f by A32,XREAL_1:19;
then 0 < j - len f by XXREAL_0:2;
then
A35: 0 + len f < j -len f + len f by XREAL_1:6;
then reconsider k = j - len f as Element of NAT by INT_1:5;
A36: j - len f < len f + len g - len f by A32,XREAL_1:9;
then
A37: k+1 <= len g by NAT_1:13;
j < j+1 by XREAL_1:29;
then len f < j+1 by A35,XXREAL_0:2;
then
A38: h.(j+1) = g.(j+1-len f) by A33,FINSEQ_1:24
.= g.(k+1);
1 <= k+1 by A34,NAT_1:13;
then k+1 in Seg (len g) by A37;
then
A39: g.(k+1) = y by A9,FUNCOP_1:7;
k in Seg (len g) by A34,A36;
then g.k = y by A9,FUNCOP_1:7;
then h.j = y by A32,FINSEQ_1:23;
hence thesis by A3,A39,A38,RELAT_2:def 1;
end;
end;
end;
suppose
n = m;
hence thesis by A4,A5;
end;
end;
definition
let X;
let Y be Sublattice of EqRelLATT X;
given e such that
A1: e in the carrier of Y and
A2: e <> id X;
given o being Element of NAT such that
A3: for e1,e2 for x,y being object
st e1 in the carrier of Y & e2 in the carrier of Y & [
x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = o & x
,y are_joint_by F,e1,e2;
func type_of Y -> Element of NAT means
:Def4:
(for e1,e2 for x,y being object st e1 in the
carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being
non empty FinSequence of X st len F = it+2 & x,y are_joint_by F,e1,e2)) &
ex e1,e2 st ex x,y being object
st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/"
e2 & not (ex F being non empty FinSequence of X st len F = it+1 & x,y
are_joint_by F,e1,e2);
existence
proof
defpred X[Element of NAT] means
for e1,e2 for x,y being object st e1 in the carrier of Y &
e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty
FinSequence of X st len F = $1+2 & x,y are_joint_by F,e1,e2;
set A = { n where n is Element of NAT : X[n] };
consider e1,e2 such that
A4: e1 = e & e2 = e;
A5: field e = X by EQREL_1:9;
then id X c= e by RELAT_2:1;
then not e c= id X by A2;
then consider x,y being object such that
A6: [x,y] in e and
A7: not [x,y] in id X by RELAT_1:def 3;
A8: not x in X or x <> y by A7,RELAT_1:def 10;
A9: [x,y] in e1 "\/" e2 by A6,A4;
then consider F being non empty FinSequence of X such that
A10: len F = o and
A11: x,y are_joint_by F,e1,e2 by A1,A3,A4;
A12: F.1 = x & F.(len F) = y by A11;
o >= 2
proof
assume not thesis;
then len F < 1 + 1 by A10;
then 0 <= len F & len F <= 0 + 1 by NAT_1:2,13;
hence contradiction by A5,A6,A8,A12,NAT_1:9,RELAT_1:15;
end;
then consider o9 being Nat such that
A13: o = 2 + o9 by NAT_1:10;
A14: A is Subset of NAT from DOMAIN_1:sch 7;
o9 in NAT by ORDINAL1:def 12;
then consider k being Element of NAT such that
k = o9 and
A15: for e1,e2 for x,y being object
st e1 in the carrier of Y & e2 in the carrier of Y
& [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = k+
2 & x,y are_joint_by F,e1,e2 by A3,A13;
k in A by A15;
then reconsider A as non empty Subset of NAT by A14;
set m = min A;
A16: ex e1,e2 st ex x,y being object
st e1 in the carrier of Y & e2 in the carrier of Y & [x,
y] in e1 "\/" e2 & not (ex F being non empty FinSequence of X st len F = m+1 &
x,y are_joint_by F,e1,e2)
proof
assume
A17: not thesis;
then consider F being non empty FinSequence of X such that
A18: len F = m+1 and
A19: x,y are_joint_by F,e1,e2 by A1,A4,A9;
A20: F.1 = x & F.(len F) = y by A19;
len F >= 2
proof
assume not thesis;
then len F < 1 + 1;
then 0 <= len F & len F <= 0 + 1 by NAT_1:2,13;
hence contradiction by A5,A6,A8,A20,NAT_1:9,RELAT_1:15;
end;
then m + 1 >= 1 + 1 by A18;
then
A21: m >= 1 by XREAL_1:6;
then m + 1 = m - 1 + 2 & m - 1 = m -' 1 by XREAL_1:233;
then
A22: m -' 1 in A by A17;
m < m + 1 by XREAL_1:29;
then
A23: m - 1 < m + 1 - 1 by XREAL_1:9;
m - 1 >= 0 by A21,XREAL_1:48;
then m -' 1 < m by A23,XREAL_0:def 2;
hence contradiction by A22,XXREAL_2:def 7;
end;
m in A by XXREAL_2:def 7;
then ex m9 being Element of NAT st m9 = m &
for e1,e2 for x,y being object st e1 in the
carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being
non empty FinSequence of X st len F = m9+ 2 & x,y are_joint_by F,e1,e2;
hence thesis by A16;
end;
uniqueness
proof
let n1,n2 be Element of NAT;
assume
A24: for e1,e2 for x,y being object
st e1 in the carrier of Y & e2 in the carrier of Y
& [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = n1
+2 & x,y are_joint_by F,e1,e2;
given e19,e29 being Equivalence_Relation of X,x9,y9 being object such that
A25: e19 in the carrier of Y & e29 in the carrier of Y & [x9,y9] in
e19 "\/" e29 and
A26: not (ex F being non empty FinSequence of X st len F = n1+1 & x9,
y9 are_joint_by F,e19,e29);
assume for e1,e2 for x,y being object
st e1 in the carrier of Y & e2 in the carrier of Y
& [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = n2
+2 & x,y are_joint_by F,e1,e2;
then
A27: ex F2 being non empty FinSequence of X st len F2 = n2+2 & x9,y9
are_joint_by F2,e19,e29 by A25;
field e29 = X by EQREL_1:9;
then
A28: e29 is_reflexive_in X by RELAT_2:def 9;
field e19 = X by EQREL_1:9;
then
A29: e19 is_reflexive_in X by RELAT_2:def 9;
given e1,e2 being Equivalence_Relation of X,x,y being object such that
A30: e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 and
A31: not (ex F being non empty FinSequence of X st len F = n2+1 & x,y
are_joint_by F,e1,e2);
A32: ex F1 being non empty FinSequence of X st len F1 = n1+2 & x,y
are_joint_by F1,e1,e2 by A24,A30;
field e2 = X by EQREL_1:9;
then
A33: e2 is_reflexive_in X by RELAT_2:def 9;
field e1 = X by EQREL_1:9;
then
A34: e1 is_reflexive_in X by RELAT_2:def 9;
assume
A35: not thesis;
per cases by A35,XXREAL_0:1;
suppose
n1 < n2;
then n1+2 < n2+(1+1) by XREAL_1:6;
then n1+2 < (n2+1)+1;
then n1+2 <= n2+1 by NAT_1:13;
hence contradiction by A31,A32,A34,A33,Th12;
end;
suppose
n2 < n1;
then n2+2 < n1+(1+1) by XREAL_1:6;
then n2+2 < (n1+1)+1;
then n2+2 <= n1+1 by NAT_1:13;
hence contradiction by A26,A27,A29,A28,Th12;
end;
end;
end;
theorem Th13:
for Y being Sublattice of EqRelLATT X, n being Element of NAT st
(ex e st e in the carrier of Y & e <> id X) &
(for e1,e2 for x,y being object st e1 in the
carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds (ex F being
non empty FinSequence of X st len F = n+2 & x,y are_joint_by F,e1,e2)) holds
type_of Y <= n
proof
let Y be Sublattice of EqRelLATT X, n be Element of NAT;
assume that
A1: ex e st e in the carrier of Y & e <> id X and
A2: for e1,e2 for x,y being object
st e1 in the carrier of Y & e2 in the carrier of Y & [
x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st len F = n+2 &
x,y are_joint_by F,e1,e2 and
A3: n < type_of Y;
n+1 <= type_of Y by A3,NAT_1:13;
then consider m being Nat such that
A4: type_of Y = (n+1)+m by NAT_1:10;
reconsider m as Element of NAT by ORDINAL1:def 12;
n+1+m+1 = n+m+2;
then consider e1,e2 being Equivalence_Relation of X,x,y being object
such that
A5: e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 and
A6: not (ex F being non empty FinSequence of X st len F = (n+m)+2 & x,y
are_joint_by F,e1,e2) by A1,A4,Def4;
A7: n+2+m = (n+m)+2;
field e2 = X by EQREL_1:9;
then
A8: e2 is_reflexive_in X by RELAT_2:def 9;
field e1 = X by EQREL_1:9;
then
A9: e1 is_reflexive_in X by RELAT_2:def 9;
ex F1 being non empty FinSequence of X st len F1 = n+2 & x,y are_joint_by
F1,e1,e2 by A2,A5;
hence contradiction by A6,A9,A8,A7,Th12,NAT_1:11;
end;
begin :: A meet-representation of a lattice
reserve A for non empty set,
L for lower-bounded LATTICE;
definition
let A be set, L be 1-sorted;
mode BiFunction of A,L is Function of [:A,A:],the carrier of L;
end;
definition
let A be non empty set, L be 1-sorted;
let f be BiFunction of A,L;
let x,y be Element of A;
redefine func f.(x,y) -> Element of L; :: redefines . (BINOP_1, definition)
coherence
proof
reconsider xy = [x,y] as Element of [:A,A:];
f.xy is Element of L;
hence thesis;
end;
end;
definition
let A;
let L be 1-sorted;
let f be BiFunction of A,L;
attr f is symmetric means
:Def5:
for x,y being Element of A holds f.(x,y) = f.(y,x);
end;
definition
let A,L;
let f be BiFunction of A,L;
attr f is zeroed means
:Def6:
for x being Element of A holds f.(x,x) = Bottom L;
attr f is u.t.i. means
:Def7:
for x,y,z being Element of A holds f.(x,y) "\/" f.(y,z) >= f.(x,z);
end;
:: f is u.t.i. means that f satisfies the triangle inequality
registration
let A, L;
cluster symmetric zeroed u.t.i. for BiFunction of A,L;
existence
proof
reconsider f = [:A,A:] --> Bottom L as Function of [:A,A:],the carrier of
L;
A1: for x,y being Element of A holds f.[x,y] = Bottom L;
reconsider f as BiFunction of A,L;
for x,y being Element of A holds f.(x,y) = f.(y,x)
proof
let x,y be Element of A;
thus f.(x,y) = Bottom L by A1
.= f.(y,x) by A1;
end;
then
A2: f is symmetric;
for x,y,z being Element of A holds f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
let x,y,z be Element of A;
A3: f.(x,z) <= Bottom L by A1;
f.(x,y) = Bottom L & f.(y,z) = Bottom L by A1;
hence thesis by A3,YELLOW_5:1;
end;
then
A4: f is u.t.i.;
for x being Element of A holds f.(x,x) = Bottom L by A1;
then f is zeroed;
hence thesis by A2,A4;
end;
end;
definition
let A, L;
mode distance_function of A,L is symmetric zeroed u.t.i. BiFunction of A,L;
end;
definition
let A, L;
let d be distance_function of A,L;
func alpha d -> Function of L,EqRelLATT A means
:Def8:
for e being Element
of L ex E being Equivalence_Relation of A st E = it.e & for x,y be Element of A
holds [x,y] in E iff d.(x,y) <= e;
existence
proof
defpred X[Element of L,Element of EqRelLATT A] means ex E being
Equivalence_Relation of A st E = $2 & for x,y be Element of A holds [x,y] in E
iff d.(x,y) <= $1;
A1: for e being Element of L ex r being Element of EqRelLATT A st X[e,r]
proof
let e be Element of L;
defpred X[Element of A,Element of A] means d.($1,$2) <= e;
consider E being Relation of A,A such that
A2: for x,y being Element of A holds [x,y] in E iff X[x,y] from
RELSET_1:sch 2;
for x,y being object
holds x in A & y in A & [x,y] in E implies [y,x] in E
proof
let x,y be object;
assume that
A3: x in A and
A4: y in A and
A5: [x,y] in E;
reconsider y9 = y as Element of A by A4;
reconsider x9 = x as Element of A by A3;
d.(x9,y9) <= e by A2,A5;
then d.(y9,x9) <= e by Def5;
hence thesis by A2;
end;
then
A6: E is_symmetric_in A by RELAT_2:def 3;
for x be object holds x in A implies [x,x] in E
proof
let x be object;
assume x in A;
then reconsider x9 = x as Element of A;
Bottom L <= e by YELLOW_0:44;
then d.(x9,x9) <= e by Def6;
hence thesis by A2;
end;
then E is_reflexive_in A by RELAT_2:def 1;
then
A7: dom E = A & field E = A by ORDERS_1:13;
for x,y,z being object
holds x in A & y in A & z in A & [x,y] in E & [
y,z] in E implies [x,z] in E
proof
let x,y,z be object;
assume that
A8: x in A & y in A & z in A and
A9: [x,y] in E & [y,z] in E;
reconsider x9 = x, y9 = y, z9 = z as Element of A by A8;
d.(x9,y9) <= e & d.(y9,z9) <= e by A2,A9;
then
A10: d.(x9,y9) "\/" d.(y9,z9) <= e by YELLOW_0:22;
d.(x9,z9) <= d.(x9,y9) "\/" d.(y9,z9) by Def7;
then d.(x9,z9) <= e by A10,ORDERS_2:3;
hence thesis by A2;
end;
then E is_transitive_in A by RELAT_2:def 8;
then reconsider E as Equivalence_Relation of A by A7,A6,PARTFUN1:def 2
,RELAT_2:def 11,def 16;
reconsider E as Element of EqRelLATT A by Th4;
ex r being Element of EqRelLATT A st r = E;
hence thesis by A2;
end;
ex f being Function of L,EqRelLATT A st for e being Element of L holds
X[e,f.e] from FUNCT_2:sch 3(A1 );
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of L,EqRelLATT A such that
A11: for e being Element of L ex E being Equivalence_Relation of A st
E = f1.e & for x,y be Element of A holds [x,y] in E iff d.(x,y) <= e and
A12: for e being Element of L ex E being Equivalence_Relation of A st
E = f2.e & for x,y be Element of A holds [x,y] in E iff d.(x,y) <= e;
reconsider f19=f1, f29=f2 as Function of the carrier of L, the carrier of
EqRelLATT A;
for e being Element of L holds f1.e = f2.e
proof
let e be Element of L;
consider E1 being Equivalence_Relation of A such that
A13: E1 = f1.e and
A14: for x,y being Element of A holds [x,y] in E1 iff d.(x,y) <= e by A11;
consider E2 being Equivalence_Relation of A such that
A15: E2 = f2.e and
A16: for x,y being Element of A holds [x,y] in E2 iff d.(x,y) <= e by A12;
A17: for x,y being Element of A holds [x,y] in E1 iff [x,y] in E2
proof
let x,y be Element of A;
[x,y] in E1 iff d.(x,y) <= e by A14;
hence thesis by A16;
end;
for x,y being object holds [x,y] in E1 iff [x,y] in E2
proof
let x,y be object;
A18: field E1 = A by EQREL_1:9;
hereby
assume
A19: [x,y] in E1;
then reconsider x9 = x, y9 = y as Element of A by A18,RELAT_1:15;
[x9,y9] in E2 by A17,A19;
hence [x,y] in E2;
end;
assume
A20: [x,y] in E2;
field E2 = A by EQREL_1:9;
then reconsider x9 = x, y9 = y as Element of A by A20,RELAT_1:15;
[x9,y9] in E1 by A17,A20;
hence thesis;
end;
hence thesis by A13,A15,RELAT_1:def 2;
end;
then for e be object st e in the carrier of L holds f19.e = f29.e;
hence f1 = f2 by FUNCT_2:12;
end;
end;
theorem Th14:
for d being distance_function of A,L holds alpha d is meet-preserving
proof
let d be distance_function of A,L;
let a,b be Element of L;
set f = alpha d;
A1: ex_inf_of f.:{a,b},EqRelLATT A by YELLOW_0:17;
consider E3 being Equivalence_Relation of A such that
A2: E3 = f.(a "/\" b) and
A3: for x,y being Element of A holds [x,y] in E3 iff d.(x,y) <= a "/\" b
by Def8;
consider E2 being Equivalence_Relation of A such that
A4: E2 = f.b and
A5: for x,y being Element of A holds [x,y] in E2 iff d.(x,y) <= b by Def8;
consider E1 being Equivalence_Relation of A such that
A6: E1 = f.a and
A7: for x,y being Element of A holds [x,y] in E1 iff d.(x,y) <= a by Def8;
A8: for x,y being Element of A holds [x,y] in E1 /\ E2 iff [x,y] in E3
proof
let x,y be Element of A;
hereby
assume
A9: [x,y] in E1 /\ E2;
then [x,y] in E2 by XBOOLE_0:def 4;
then
A10: d.(x,y) <= b by A5;
[x,y] in E1 by A9,XBOOLE_0:def 4;
then d.(x,y) <= a by A7;
then d.(x,y) <= a "/\" b by A10,YELLOW_0:23;
hence [x,y] in E3 by A3;
end;
assume [x,y] in E3;
then
A11: d.(x,y) <= a "/\" b by A3;
a "/\" b <= b by YELLOW_0:23;
then d.(x,y) <= b by A11,ORDERS_2:3;
then
A12: [x,y] in E2 by A5;
a "/\" b <= a by YELLOW_0:23;
then d.(x,y) <= a by A11,ORDERS_2:3;
then [x,y] in E1 by A7;
hence thesis by A12,XBOOLE_0:def 4;
end;
A13: for x,y being object holds [x,y] in E1 /\ E2 iff [x,y] in E3
proof
let x,y be object;
field E1 /\ field E2 = A /\ field E2 by EQREL_1:9
.= A /\ A by EQREL_1:9
.= A;
then
A14: field (E1 /\ E2) c= A by RELAT_1:19;
hereby
assume
A15: [x,y] in E1 /\ E2;
then x in field (E1 /\ E2) & y in field (E1 /\ E2) by RELAT_1:15;
then reconsider x9 = x, y9 = y as Element of A by A14;
[x9,y9] in E3 by A8,A15;
hence [x,y] in E3;
end;
assume
A16: [x,y] in E3;
field E3 = A by EQREL_1:9;
then reconsider x9 = x, y9 = y as Element of A by A16,RELAT_1:15;
[x9,y9] in E1 /\ E2 by A8,A16;
hence thesis;
end;
dom f = the carrier of L by FUNCT_2:def 1;
then inf (f.:{a,b}) = inf {f.a,f.b} by FUNCT_1:60
.= f.a "/\" f.b by YELLOW_0:40
.= E1 /\ E2 by A6,A4,Th8
.= f.(a "/\" b) by A2,A13,RELAT_1:def 2
.= f.inf {a,b} by YELLOW_0:40;
hence thesis by A1;
end;
theorem Th15:
for d being distance_function of A,L st d is onto holds alpha d is one-to-one
proof
let d be distance_function of A,L;
set f = alpha d;
assume d is onto;
then
A1: rng d = the carrier of L by FUNCT_2:def 3;
for a,b being Element of L st f.a = f.b holds a = b
proof
let a,b be Element of L;
assume
A2: f.a = f.b;
consider z1 be object such that
A3: z1 in [:A,A:] and
A4: d.z1 = a by A1,FUNCT_2:11;
consider x1,y1 being object such that
A5: x1 in A & y1 in A and
A6: z1 = [x1,y1] by A3,ZFMISC_1:def 2;
reconsider x1,y1 as Element of A by A5;
consider z2 be object such that
A7: z2 in [:A,A:] and
A8: d.z2 = b by A1,FUNCT_2:11;
consider x2,y2 being object such that
A9: x2 in A & y2 in A and
A10: z2 = [x2,y2] by A7,ZFMISC_1:def 2;
reconsider x2,y2 as Element of A by A9;
consider E1 being Equivalence_Relation of A such that
A11: E1 = f.a and
A12: for x,y be Element of A holds [x,y] in E1 iff d.(x,y) <= a by Def8;
consider E2 being Equivalence_Relation of A such that
A13: E2 = f.b and
A14: for x,y be Element of A holds [x,y] in E2 iff d.(x,y) <= b by Def8;
A15: d.(x2,y2) = b by A8,A10;
then [x2,y2] in E2 by A14;
then
A16: b <= a by A2,A15,A11,A12,A13;
A17: d.(x1,y1) = a by A4,A6;
then [x1,y1] in E1 by A12;
then a <= b by A2,A17,A11,A13,A14;
hence thesis by A16,ORDERS_2:2;
end;
hence thesis by WAYBEL_1:def 1;
end;
begin :: J\'onsson theorem
definition
let A be set;
func new_set A -> set equals
A \/ {{A}, {{A}}, {{{A}}} };
correctness;
end;
registration
let A be set;
cluster new_set A -> non empty;
coherence;
end;
definition
let A,L;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
func new_bi_fun(d,q) -> BiFunction of new_set A,L means
:Def10:
(for u,v
being Element of A holds it.(u,v) = d.(u,v) ) & it.({A},{A}) = Bottom L & it.({
{A}},{{A}}) = Bottom L & it.({{{A}}},{{{A}}}) = Bottom L & it.({{A}},{{{A}}}) =
q`3_4 & it.({{{A}}},{{A}}) = q`3_4 & it.({A},{{A}}) = q`4_4 &
it.({{A}},{A}) = q`4_4 &
it.({A},{{{A}}}) = (q`3_4)"\/"(q`4_4) &
it.({{{A}}},{A}) = (q`3_4)"\/"(q`4_4) &
for u being
Element of A holds it.(u,{A}) = d.(u,q`1_4)"\/"(q`3_4) &
it.({A},u) = d.(u,q`1_4)"\/"(q`3_4) &
it.(u,{{A}}) = d.(u,q`1_4)"\/"(q`3_4)"\/"(q`4_4) &
it.({{A}},u) = d.(u,q`1_4)"\/"(q`3_4)
"\/" (q`4_4) & it.(u,{{{A}}}) = d.(u,q`2_4)"\/"(q`4_4) &
it.({{{A}}},u) = d.(u,q`2_4)"\/"(q`4_4);
existence
proof
reconsider a = q`3_4, b = q`4_4 as Element of L;
set x = q`1_4, y = q`2_4;
defpred X[Element of new_set A,Element of new_set A,Element of L] means (
$1 in A & $2 in A implies $3 = d.($1,$2)) & ($1 = {{A}} & $2 = {{{A}}} or $2 =
{{A}} & $1 = {{{A}}} implies $3 = a) & ($1 = {A} & $2 = {{A}} or $2 = {A} & $1
= {{A}} implies $3 = b) & ($1 = {A} & $2 = {{{A}}} or $2 = {A} & $1 = {{{A}}}
implies $3 = a"\/"b) & (($1 = {A} or $1 = {{A}} or $1 = {{{A}}}) & $2 = $1
implies $3 = Bottom L) & ($1 in A & $2 = {A} implies ex p9 being Element of A
st p9 = $1 & $3 = d.(p9,x)"\/"a) & ($1 in A & $2 = {{A}} implies ex p9 being
Element of A st p9 = $1 & $3 = d.(p9,x)"\/"a"\/"b) & ($1 in A & $2 = {{{A}}}
implies ex p9 being Element of A st p9 = $1 & $3 = d.(p9,y)"\/"b) & ($2 in A &
$1 = {A} implies ex q9 being Element of A st q9 = $2 & $3 = d.(q9,x)"\/"a) & (
$2 in A & $1 = {{A}} implies ex q9 being Element of A st q9 = $2 & $3 = d.(q9,x
)"\/"a"\/"b) & ($2 in A & $1 = {{{A}}} implies ex q9 being Element of A st q9 =
$2 & $3 = d.(q9,y)"\/"b);
{{A}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:def 1;
then
A1: {{A}} in new_set A by XBOOLE_0:def 3;
A2: for p,q being Element of new_set A ex r being Element of L st X[p,q,r]
proof
let p,q be Element of new_set A;
A3: p in A or p in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 3;
A4: q in A or q in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 3;
A5: (p = {A} or p = {{A}} or p = {{{A}}}) & p = q iff p = {A} & q = {A}
or p = {{A}} & q = {{A}} or p = {{{A}}} & q = {{{A}}};
A6: not {A} in A by TARSKI:def 1;
A7: {{A}} <> {{{A}}}
proof
assume {{A}} = {{{A}}};
then {{A}} in {{A}} by TARSKI:def 1;
hence contradiction;
end;
A8: not {{{A}}} in A
proof
A9: {{A}} in {{{A}}} by TARSKI:def 1;
A10: A in {A} & {A} in {{A}} by TARSKI:def 1;
assume {{{A}}} in A;
hence contradiction by A10,A9,XREGULAR:8;
end;
A11: {A} <> {{{A}}}
proof
assume {A} = {{{A}}};
then {{A}} in {A} by TARSKI:def 1;
hence contradiction by TARSKI:def 1;
end;
A12: not {{A}} in A
proof
A13: A in {A} & {A} in {{A}} by TARSKI:def 1;
assume {{A}} in A;
hence contradiction by A13,XREGULAR:7;
end;
per cases by A3,A4,A5,ENUMSET1:def 1;
suppose
p in A & q in A;
then reconsider p9=p,q9=q as Element of A;
take d.(p9,q9);
thus thesis by A6,A12,A8;
end;
suppose
A14: p = {{A}} & q = {{{A}}} or q = {{A}} & p = {{{A}}};
take a;
thus thesis by A7,A11,A12,A8,A14;
end;
suppose
A15: p = {A} & q = {{A}} or q = {A} & p = {{A}};
take b;
thus thesis by A7,A11,A12,A15,TARSKI:def 1;
end;
suppose
A16: p = {A} & q = {{{A}}} or q = {A} & p = {{{A}}};
take a"\/"b;
thus thesis by A7,A11,A8,A16,TARSKI:def 1;
end;
suppose
A17: (p = {A} or p = {{A}} or p = {{{A}}}) & q = p;
take Bottom L;
thus thesis by A7,A11,A12,A8,A17,TARSKI:def 1;
end;
suppose
A18: p in A & q = {A};
then reconsider p9 = p as Element of A;
take d.(p9,x)"\/"a;
thus thesis by A11,A12,A8,A18,TARSKI:def 1;
end;
suppose
A19: p in A & q = {{A}};
then reconsider p9 = p as Element of A;
take d.(p9,x)"\/"a"\/"b;
thus thesis by A7,A12,A8,A19,TARSKI:def 1;
end;
suppose
A20: p in A & q = {{{A}}};
then reconsider p9 = p as Element of A;
take d.(p9,y)"\/"b;
thus thesis by A7,A11,A12,A8,A20,TARSKI:def 1;
end;
suppose
A21: q in A & p = {A};
then reconsider q9 = q as Element of A;
take d.(q9,x)"\/"a;
thus thesis by A11,A12,A8,A21,TARSKI:def 1;
end;
suppose
A22: q in A & p = {{A}};
then reconsider q9 = q as Element of A;
take d.(q9,x)"\/"a"\/"b;
thus thesis by A7,A12,A8,A22,TARSKI:def 1;
end;
suppose
A23: q in A & p = {{{A}}};
then reconsider q9 = q as Element of A;
take d.(q9,y)"\/"b;
thus thesis by A7,A11,A12,A8,A23,TARSKI:def 1;
end;
end;
consider f being Function of [:new_set A,new_set A:],the carrier of L such
that
A24: for p,q being Element of new_set A holds X[p,q,f.(p,q)] from
BINOP_1:sch 3(A2);
{{{A}}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:def 1;
then
A25: {{{A}}} in new_set A by XBOOLE_0:def 3;
reconsider f as BiFunction of new_set A,L;
{A} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:def 1;
then
A26: {A} in new_set A by XBOOLE_0:def 3;
A27: for u being Element of A holds f.({A},u) = d.(u,x)"\/"a & f.({{A}},u)
= d.(u,x)"\/"a"\/"b & f.({{{A}}},u) = d.(u,y)"\/"b
proof
let u be Element of A;
reconsider u9 = u as Element of new_set A by XBOOLE_0:def 3;
ex u1 being Element of A st u1 = u9 & f.({A},u9) = d.(u1,x)"\/"a by A26
,A24;
hence f.({A},u) = d.(u,x)"\/"a;
ex u2 being Element of A st u2 = u9 & f.({{A}},u9) = d.( u2,x)"\/"a
"\/"b by A1,A24;
hence f.({{A}},u) = d.(u,x)"\/"a"\/"b;
ex u3 being Element of A st u3 = u9 & f.({{{A}}},u9) = d .(u3,y)"\/"
b by A25,A24;
hence thesis;
end;
take f;
A28: for u,v being Element of A holds f.(u,v) = d.(u,v)
proof
let u,v be Element of A;
reconsider u9 = u, v9 = v as Element of new_set A by XBOOLE_0:def 3;
thus f.(u,v) = f.(u9,v9) .= d.(u,v) by A24;
end;
for u being Element of A holds f.(u,{A}) = d.(u,x)"\/"a & f.(u,{{A}})
= d.(u,x)"\/"a"\/"b & f.(u,{{{A}}}) = d.(u,y)"\/"b
proof
let u be Element of A;
reconsider u9 = u as Element of new_set A by XBOOLE_0:def 3;
ex u1 being Element of A st u1 = u9 & f.(u9,{A}) = d.(u1,x)"\/"a by A26
,A24;
hence f.(u,{A}) = d.(u,x)"\/"a;
ex u2 being Element of A st u2 = u9 & f.(u9,{{A}}) = d.( u2,x)"\/"a
"\/"b by A1,A24;
hence f.(u,{{A}}) = d.(u,x)"\/"a"\/"b;
ex u3 being Element of A st u3 = u9 & f.(u9,{{{A}}}) = d .(u3,y)"\/"
b by A25,A24;
hence thesis;
end;
hence thesis by A26,A1,A25,A24,A28,A27;
end;
uniqueness
proof
set x = q`1_4, y = q`2_4, a = q`3_4, b = q`4_4;
let f1,f2 be BiFunction of new_set A,L such that
A29: for u,v being Element of A holds f1.(u,v) = d.(u,v) and
A30: f1.({A},{A}) = Bottom L and
A31: f1.({{A}},{{A}}) = Bottom L and
A32: f1.({{{A}}},{{{A}}}) = Bottom L and
A33: f1.({{A}},{{{A}}}) = a and
A34: f1.({{{A}}},{{A}}) = a and
A35: f1.({A},{{A}}) = b and
A36: f1.({{A}},{A}) = b and
A37: f1.({A},{{{A}}}) = a"\/"b and
A38: f1.({{{A}}},{A}) = a"\/"b and
A39: for u being Element of A holds f1.(u,{A}) = d.(u,x)"\/"a & f1.({A
},u) = d.(u,x)"\/"a & f1.(u,{{A}}) = d.(u,x)"\/"a"\/"b & f1.({{A}},u) = d.(u,x)
"\/"a"\/"b & f1.(u,{{{A}}}) = d.(u,y)"\/"b & f1.({{{A}}},u) = d.(u,y)"\/"b
and
A40: for u,v being Element of A holds f2.(u,v) = d.(u,v) and
A41: f2.({A},{A}) = Bottom L and
A42: f2.({{A}},{{A}}) = Bottom L and
A43: f2.({{{A}}},{{{A}}}) = Bottom L and
A44: f2.({{A}},{{{A}}}) = a and
A45: f2.({{{A}}},{{A}}) = a and
A46: f2.({A},{{A}}) = b and
A47: f2.({{A}},{A}) = b and
A48: f2.({A},{{{A}}}) = a"\/"b and
A49: f2.({{{A}}},{A}) = a"\/"b and
A50: for u being Element of A holds f2.(u,{A}) = d.(u,x)"\/"a & f2.({A
},u) = d.(u,x)"\/"a & f2.(u,{{A}}) = d.(u,x)"\/"a"\/"b & f2.({{A}},u) = d.(u,x)
"\/"a"\/"b & f2.(u,{{{A}}}) = d.(u,y)"\/"b & f2.({{{A}}},u) = d.(u,y)"\/"b;
now
let p,q be Element of new_set A;
A51: p in A or p in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 3;
A52: q in A or q in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 3;
per cases by A51,A52,ENUMSET1:def 1;
suppose
A53: p in A & q in A;
hence f1.(p,q) = d.(p,q) by A29
.= f2.(p,q) by A40,A53;
end;
suppose
A54: p in A & q = {A};
then reconsider p9 = p as Element of A;
thus f1.(p,q) = d.(p9,x)"\/"a by A39,A54
.= f2.(p,q) by A50,A54;
end;
suppose
A55: p in A & q = {{A}};
then reconsider p9 = p as Element of A;
thus f1.(p,q) = d.(p9,x)"\/"a"\/"b by A39,A55
.= f2.(p,q) by A50,A55;
end;
suppose
A56: p in A & q = {{{A}}};
then reconsider p9 = p as Element of A;
thus f1.(p,q) = d.(p9,y)"\/"b by A39,A56
.= f2.(p,q) by A50,A56;
end;
suppose
A57: p = {A} & q in A;
then reconsider q9 = q as Element of A;
thus f1.(p,q) = d.(q9,x)"\/"a by A39,A57
.= f2.(p,q) by A50,A57;
end;
suppose
p = {A} & q = {A};
hence f1.(p,q) = f2.(p,q) by A30,A41;
end;
suppose
p = {A} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A35,A46;
end;
suppose
p = {A} & q = {{{A}}};
hence f1.(p,q) = f2.(p,q) by A37,A48;
end;
suppose
A58: p = {{A}} & q in A;
then reconsider q9 = q as Element of A;
thus f1.(p,q) = d.(q9,x)"\/"a"\/"b by A39,A58
.= f2.(p,q) by A50,A58;
end;
suppose
p = {{A}} & q = {A};
hence f1.(p,q) = f2.(p,q) by A36,A47;
end;
suppose
p = {{A}} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A31,A42;
end;
suppose
p = {{A}} & q = {{{A}}};
hence f1.(p,q) = f2.(p,q) by A33,A44;
end;
suppose
A59: p = {{{A}}} & q in A;
then reconsider q9 = q as Element of A;
thus f1.(p,q) = d.(q9,y)"\/"b by A39,A59
.= f2.(p,q) by A50,A59;
end;
suppose
p = {{{A}}} & q = {A};
hence f1.(p,q) = f2.(p,q) by A38,A49;
end;
suppose
p = {{{A}}} & q = {{A}};
hence f1.(p,q) = f2.(p,q) by A34,A45;
end;
suppose
p = {{{A}}} & q = {{{A}}};
hence f1.(p,q) = f2.(p,q) by A32,A43;
end;
end;
hence f1 = f2;
end;
end;
theorem Th16:
for d being BiFunction of A,L st d is zeroed for q being Element
of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun(d,q) is zeroed
proof
let d be BiFunction of A,L;
assume
A1: d is zeroed;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set f = new_bi_fun(d,q);
for u being Element of new_set A holds f.(u,u) = Bottom L
proof
let u be Element of new_set A;
A2: u in A or u in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 3;
per cases by A2,ENUMSET1:def 1;
suppose
u in A;
then reconsider u9 = u as Element of A;
thus f.(u,u) = d.(u9,u9) by Def10
.= Bottom L by A1;
end;
suppose
u = {A} or u = {{A}} or u = {{{A}}};
hence thesis by Def10;
end;
end;
hence thesis;
end;
theorem Th17:
for d being BiFunction of A,L st d is symmetric for q being
Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun(d,q) is
symmetric
proof
let d be BiFunction of A,L;
assume
A1: d is symmetric;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set f = new_bi_fun(d,q), x = q`1_4, y = q`2_4, a = q`3_4, b = q`4_4;
let p,q be Element of new_set A;
A2: p in A or p in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 3;
A3: q in A or q in {{A},{{A}},{{{A}}}} by XBOOLE_0:def 3;
per cases by A2,A3,ENUMSET1:def 1;
suppose
p in A & q in A;
then reconsider p9 = p, q9 = q as Element of A;
thus f.(p,q) = d.(p9,q9) by Def10
.= d.(q9,p9) by A1
.= f.(q,p) by Def10;
end;
suppose
A4: p in A & q = {A};
then reconsider p9 = p as Element of A;
thus f.(p,q) = d.(p9,x)"\/"a by A4,Def10
.= f.(q,p) by A4,Def10;
end;
suppose
A5: p in A & q = {{A}};
then reconsider p9 = p as Element of A;
thus f.(p,q) = d.(p9,x)"\/"a"\/"b by A5,Def10
.= f.(q,p) by A5,Def10;
end;
suppose
A6: p in A & q = {{{A}}};
then reconsider p9 = p as Element of A;
thus f.(p,q) = d.(p9,y)"\/"b by A6,Def10
.= f.(q,p) by A6,Def10;
end;
suppose
A7: p = {A} & q in A;
then reconsider q9 = q as Element of A;
thus f.(p,q) = d.(q9,x)"\/"a by A7,Def10
.= f.(q,p) by A7,Def10;
end;
suppose
p = {A} & q = {A};
hence thesis;
end;
suppose
A8: p = {A} & q = {{A}};
hence f.(p,q) = b by Def10
.= f.(q,p) by A8,Def10;
end;
suppose
A9: p = {A} & q = {{{A}}};
hence f.(p,q) = a"\/"b by Def10
.= f.(q,p) by A9,Def10;
end;
suppose
A10: p = {{A}} & q in A;
then reconsider q9 = q as Element of A;
thus f.(p,q) = d.(q9,x)"\/"a"\/"b by A10,Def10
.= f.(q,p) by A10,Def10;
end;
suppose
A11: p = {{A}} & q = {A};
hence f.(p,q) = b by Def10
.= f.(q,p) by A11,Def10;
end;
suppose
p = {{A}} & q = {{A}};
hence thesis;
end;
suppose
A12: p = {{A}} & q = {{{A}}};
hence f.(p,q) = a by Def10
.= f.(q,p) by A12,Def10;
end;
suppose
A13: p = {{{A}}} & q in A;
then reconsider q9 = q as Element of A;
thus f.(p,q) = d.(q9,y)"\/"b by A13,Def10
.= f.(q,p) by A13,Def10;
end;
suppose
A14: p = {{{A}}} & q = {A};
hence f.(p,q) = a"\/"b by Def10
.= f.(q,p) by A14,Def10;
end;
suppose
A15: p = {{{A}}} & q = {{A}};
hence f.(p,q) = a by Def10
.= f.(q,p) by A15,Def10;
end;
suppose
p = {{{A}}} & q = {{{A}}};
hence thesis;
end;
end;
theorem Th18:
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_4,q`2_4)
<= (q`3_4)"\/"(q`4_4) holds new_bi_fun(d,q) is u.t.i.
proof
let d be BiFunction of A,L;
assume that
A1: d is symmetric and
A2: d is u.t.i.;
reconsider B = {{A}, {{A}}, {{{A}}}} as non empty set;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set x = q`1_4, y = q`2_4, f = new_bi_fun(d,q);
reconsider a = q`3_4,b = q`4_4 as Element of L;
A3: for p,q,u being Element of new_set A st p in A & q in B & u in A holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
assume
A4: p in A & q in B & u in A;
per cases by A4,ENUMSET1:def 1;
suppose
A5: p in A & u in A & q = {A};
then reconsider p9 = p, u9 = u as Element of A;
d.(p9,u9) <= d.(p9,x) "\/" d.(x,u9) by A2;
then
A6: d.(p9,x) "\/" d.(u9,x) <= (d.(p9,x) "\/" d.(u9,x))"\/"a & d.(p9,u9)
<= d.(p9,x) "\/" d.(u9,x) by A1,YELLOW_0:22;
(d.(p9,x)"\/"d.(u9,x))"\/"a = d.(p9,x)"\/"(d.(u9,x)"\/"a) by LATTICE3:14
.= d.(p9,x)"\/"(d.(u9,x)"\/"(a"\/"a)) by YELLOW_5:1
.= d.(p9,x)"\/"((d.(u9,x)"\/"a)"\/"a) by LATTICE3:14
.= (d.(p9,x)"\/"a) "\/" (d.(u9,x)"\/"a) by LATTICE3:14;
then
A7: d.(p9,u9) <= (d.(p9,x)"\/"a) "\/" (d.(u9,x)"\/"a) by A6,ORDERS_2:3;
f.(p,q) = d.(p9,x)"\/"a & f.(q,u) = d.(u9,x)"\/"a by A5,Def10;
hence thesis by A7,Def10;
end;
suppose
A8: p in A & u in A & q = {{A}};
then reconsider p9 = p, u9 = u as Element of A;
d.(p9,u9) <= d.(p9,x) "\/" d.(x,u9) by A2;
then
A9: d.(p9,x) "\/" d.(u9,x) <= (d.(p9,x) "\/" d.(u9,x))"\/"(a"\/" b) & d
.(p9,u9) <= d.(p9,x) "\/" d.(u9,x) by A1,YELLOW_0:22;
(d.(p9,x)"\/"d.(u9,x))"\/"(a"\/"b) = d.(p9,x)"\/"(d.(u9,x)"\/"(a
"\/" b)) by LATTICE3:14
.= d.(p9,x)"\/"(d.(u9,x)"\/"((a"\/"b)"\/"(a"\/"b))) by YELLOW_5:1
.= d.(p9,x)"\/"((d.(u9,x)"\/"(a"\/"b))"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p9,x)"\/"(a"\/"b))"\/"(d.(u9,x)"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p9,x)"\/"a"\/"b) "\/" (d.(u9,x)"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p9,x)"\/"a"\/"b) "\/" (d.(u9,x)"\/"a"\/"b) by LATTICE3:14;
then
A10: d.(p9,u9) <= (d.(p9,x)"\/"a"\/"b) "\/" (d.(u9,x)"\/"a"\/" b) by A9,
ORDERS_2:3;
f.(p,q) = d.(p9,x)"\/"a"\/"b & f.(q,u) = d.(u9,x)"\/"a"\/"b by A8,Def10;
hence thesis by A10,Def10;
end;
suppose
A11: p in A & u in A & q = {{{A}}};
then reconsider p9 = p, u9 = u as Element of A;
d.(p9,u9) <= d.(p9,y) "\/" d.(y,u9) by A2;
then
A12: d.(p9,y) "\/" d.(u9,y) <= (d.(p9,y) "\/" d.(u9,y))"\/"b & d.(p9,u9)
<= d.(p9,y) "\/" d.(u9,y) by A1,YELLOW_0:22;
(d.(p9,y)"\/"d.(u9,y))"\/"b = d.(p9,y)"\/"(d.(u9,y)"\/"b) by LATTICE3:14
.= d.(p9,y)"\/"(d.(u9,y)"\/"(b"\/"b)) by YELLOW_5:1
.= d.(p9,y)"\/"((d.(u9,y)"\/"b)"\/"b) by LATTICE3:14
.= (d.(p9,y)"\/"b) "\/" (d.(u9,y)"\/"b) by LATTICE3:14;
then
A13: d.(p9,u9) <= (d.(p9,y)"\/"b) "\/" (d.(u9,y)"\/"b) by A12,ORDERS_2:3;
f.(p,q) = d.(p9,y)"\/"b & f.(q,u) = d.(u9,y)"\/"b by A11,Def10;
hence thesis by A13,Def10;
end;
end;
assume
A14: d.(q`1_4,q`2_4) <= (q`3_4)"\/"(q`4_4);
A15: for p,q,u being Element of new_set A st p in B & q in B & u in A holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
assume that
A16: p in B & q in B and
A17: u in A;
reconsider u9 = u as Element of A by A17;
per cases by A16,A17,ENUMSET1:def 1;
suppose
A18: u in A & q = {A} & p = {A};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/" f.(q,u) by Def10
.= f.(p,u) by A18,WAYBEL_1:3;
hence thesis;
end;
suppose
A19: u in A & q = {A} & p = {{A}};
then f.(p,q)"\/"f.(q,u) = b"\/"f.(q,u) by Def10
.= d.(u9,x)"\/"a"\/" b by A19,Def10;
hence thesis by A19,Def10;
end;
suppose
A20: u in A & q = {A} & p = {{{A}}};
b"\/"(a"\/"b) = (b"\/"b)"\/"a by LATTICE3:14
.= b"\/"a by YELLOW_5:1
.= b"\/"(a"\/"a) by YELLOW_5:1
.= a"\/"(a"\/"b) by LATTICE3:14;
then
A21: (d.(u9,x)"\/"b)"\/"(a"\/"b) = d.(u9,x)"\/"(a"\/"(a"\/" b)) by LATTICE3:14
.= (a"\/"b)"\/"(d.(u9,x)"\/"a) by LATTICE3:14
.= f.(p,q)"\/"(d.(u9,x)"\/" a) by A20,Def10;
d.(u9,y) <= d.(u9,x)"\/"d.(x,y) by A2;
then
A22: d.(u9,y)"\/"b <= (d.(u9,x)"\/"d.(x,y))"\/"b by WAYBEL_1:2;
d.(u9,x)"\/"b <= d.(u9,x)"\/"b;
then
A23: (d.(u9,x)"\/"d.(x,y))"\/"b = (d.(u9,x)"\/"b)"\/"d.(x,y) & (d.(u9,x
)"\/"b) "\/"d.(x,y) <= (d.(u9,x)"\/"b)"\/"(a"\/" b) by A14,LATTICE3:14
,YELLOW_3:3;
f.(p,u) = d.(u9,y)"\/"b by A20,Def10;
then f.(p,u) <= (d.(u9,x)"\/"b)"\/"(a"\/"b) by A22,A23,ORDERS_2:3;
hence thesis by A20,A21,Def10;
end;
suppose
A24: u in A & q = {{A}} & p = {A};
then f.(p,q)"\/"f.(q,u) = b"\/"f.(q,u) by Def10
.= b"\/"(d.(u9,x)"\/"a"\/" b) by A24,Def10
.= b"\/"(b"\/"f.(p,u)) by A24,Def10
.= (b"\/"b)"\/"f.(p,u) by LATTICE3:14
.= b"\/"f.(p,u) by YELLOW_5:1;
hence thesis by YELLOW_0:22;
end;
suppose
A25: u in A & q = {{A}} & p = {{A}};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/" f.(q,u) by Def10
.= f.(p,u) by A25,WAYBEL_1:3;
hence thesis;
end;
suppose
A26: u in A & q = {{A}} & p = {{{A}}};
b"\/"(a"\/"b) = (b"\/"b)"\/"a by LATTICE3:14
.= b"\/"a by YELLOW_5:1
.= b"\/"(a"\/"a) by YELLOW_5:1
.= (a"\/"b)"\/"a by LATTICE3:14;
then
A27: (d.(u9,x)"\/"b)"\/"(a"\/"b) = d.(u9,x)"\/"((a"\/"b)"\/"a) by LATTICE3:14
.= (d.(u9,x)"\/"(a"\/"b))"\/"a by LATTICE3:14
.= (d.(u9,x)"\/"a"\/"b)"\/"a by LATTICE3:14
.= f.(p,q)"\/"(d.(u9,x)"\/"a"\/"b) by A26,Def10;
d.(u9,x)"\/"b <= d.(u9,x)"\/"b;
then
A28: (d.(u9,x)"\/"d.(x,y))"\/"b = (d.(u9,x)"\/"b)"\/"d.(x,y) & (d.(u9,x
)"\/"b) "\/"d.(x,y) <= (d.(u9,x)"\/"b)"\/"(a"\/" b) by A14,LATTICE3:14
,YELLOW_3:3;
d.(u9,y) <= d.(u9,x)"\/"d.(x,y) by A2;
then
A29: d.(u9,y)"\/"b <= (d.(u9,x)"\/"d.(x,y))"\/"b by WAYBEL_1:2;
f.(p,u) = d.(u9,y)"\/"b by A26,Def10;
then f.(p,u) <= (d.(u9,x)"\/"b)"\/"(a"\/"b) by A29,A28,ORDERS_2:3;
hence thesis by A26,A27,Def10;
end;
suppose
A30: u in A & q = {{{A}}} & p = {A};
A31: a"\/"(a"\/"b) = (a"\/"a)"\/"b by LATTICE3:14
.= a"\/"b by YELLOW_5:1
.= a"\/"(b"\/"b) by YELLOW_5:1
.= b"\/"(a"\/"b) by LATTICE3:14;
A32: (a"\/"d.(u9,y))"\/"(a"\/"b) = d.(u9,y)"\/"(a"\/"(a"\/"b)) by LATTICE3:14
.= (d.(u9,y)"\/"b)"\/"(a"\/"b) by A31,LATTICE3:14
.= f.(p,q)"\/"(d.(u9,y)"\/"b) by A30,Def10;
a"\/"d.(u9,y) <= a"\/"d.(u9,y);
then
A33: (a"\/"d.(u9,y))"\/"d.(x,y) <= (a"\/"d.(u9,y))"\/"(a"\/" b) by A14,
YELLOW_3:3;
d.(u9,x) <= d.(u9,y)"\/"d.(y,x) by A2;
then
A34: d.(u9,x)"\/"a <= (d.(u9,y)"\/"d.(y,x))"\/"a by WAYBEL_1:2;
A35: (d.(u9,y)"\/"d.(y,x))"\/"a = d.(y,x)"\/"(d.(u9,y)"\/"a) by LATTICE3:14
.= (a"\/"d.(u9,y))"\/"d.(x,y) by A1;
f.(p,u) = d.(u9,x)"\/"a by A30,Def10;
then f.(p,u) <= (a"\/"d.(u9,y))"\/"(a"\/"b) by A34,A35,A33,ORDERS_2:3;
hence thesis by A30,A32,Def10;
end;
suppose
A36: u in A & q = {{{A}}} & p = {{A}};
then
A37: f.(p,u) = d.(u9,x)"\/"a"\/"b by Def10
.= d.(u9,x)"\/"(a"\/" b) by LATTICE3:14;
(a"\/"b)"\/"d.(u9,y) <= (a"\/"b)"\/"d.(u9,y);
then
A38: ((a"\/"b)"\/"d.(u9,y))"\/"d.(x,y) <= ((a"\/"b)"\/"d.(u9,y))"\/"(a
"\/"b) by A14,YELLOW_3:3;
d.(u9,x) <= d.(u9,y)"\/"d.(y,x) by A2;
then
A39: d.(u9,x)"\/"(a"\/"b) <= (d.(u9,y)"\/"d.(y,x))"\/"(a"\/"b) by WAYBEL_1:2;
A40: (d.(u9,y)"\/"d.(y,x))"\/"(a"\/"b) = ((a"\/"b)"\/"d.(u9,y))"\/" d.(
y,x) by LATTICE3:14
.= ((a"\/"b)"\/"d.(u9,y))"\/"d.(x,y) by A1;
f.(p,q)"\/"f.(q,u) = a"\/"f.(q,u) by A36,Def10
.= a"\/"(b"\/" d.(u9,y)) by A36,Def10
.= (a"\/"b)"\/"d.(u9,y) by LATTICE3:14
.= ((a"\/"b)"\/"(a"\/"b))"\/"d.(u9,y) by YELLOW_5:1
.= (a"\/"b)"\/"(d.(u9,y)"\/"(a"\/"b)) by LATTICE3:14;
hence thesis by A37,A39,A40,A38,ORDERS_2:3;
end;
suppose
A41: u in A & q = {{{A}}} & p = {{{A}}};
then f.(p,q)"\/"f.(q,u) = Bottom L"\/" f.(q,u) by Def10
.= f.(p,u) by A41,WAYBEL_1:3;
hence thesis;
end;
end;
A42: for p,q,u being Element of new_set A st p in B & q in A & u in A holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
assume that
A43: p in B and
A44: q in A & u in A;
reconsider q9 = q, u9 = u as Element of A by A44;
per cases by A43,A44,ENUMSET1:def 1;
suppose
A45: p = {A} & q in A & u in A;
d.(u9,x) <= d.(u9,q9) "\/" d.(q9,x) by A2;
then d.(u9,x) <= d.(q9,u9) "\/" d.(q9,x) by A1;
then d.(u9,x)"\/"a <= (d.(q9,x)"\/"d.(q9,u9))"\/"a by WAYBEL_1:2;
then
A46: d.(u9,x)"\/"a <= (d.(q9,x)"\/"a)"\/"d.(q9,u9) by LATTICE3:14;
A47: f.(q,u) = d.(q9,u9) by Def10;
f.(p,q) = d.(q9,x)"\/"a by A45,Def10;
hence thesis by A45,A47,A46,Def10;
end;
suppose
A48: p = {{A}} & q in A & u in A;
d.(u9,x) <= d.(u9,q9) "\/" d.(q9,x) by A2;
then d.(u9,x) <= d.(q9,u9) "\/" d.(q9,x) by A1;
then d.(u9,x)"\/"(a"\/"b) <= (d.(q9,x)"\/"d.(q9,u9))"\/"(a"\/" b) by
WAYBEL_1:2;
then
d.(u9,x)"\/"a"\/"b <= (d.(q9,x)"\/"d.(q9,u9))"\/"(a"\/" b) by LATTICE3:14;
then
d.(u9,x)"\/"a"\/"b <= (d.(q9,x)"\/"(a"\/"b))"\/" d.(q9,u9) by LATTICE3:14;
then
A49: d.(u9,x)"\/"a"\/"b <= (d.(q9,x)"\/"a"\/"b)"\/"d.(q9,u9) by LATTICE3:14;
A50: f.(q,u) = d.(q9,u9) by Def10;
f.(p,q) = d.(q9,x)"\/"a"\/"b by A48,Def10;
hence thesis by A48,A50,A49,Def10;
end;
suppose
A51: p = {{{A}}} & q in A & u in A;
d.(u9,y) <= d.(u9,q9) "\/" d.(q9,y) by A2;
then d.(u9,y) <= d.(q9,u9) "\/" d.(q9,y) by A1;
then d.(u9,y)"\/"b <= (d.(q9,y)"\/"d.(q9,u9))"\/"b by WAYBEL_1:2;
then
A52: d.(u9,y)"\/"b <= (d.(q9,y)"\/"b)"\/"d.(q9,u9) by LATTICE3:14;
A53: f.(q,u) = d.(q9,u9) by Def10;
f.(p,q) = d.(q9,y)"\/"b by A51,Def10;
hence thesis by A51,A53,A52,Def10;
end;
end;
A54: for p,q,u being Element of new_set A st p in A & q in A & u in B holds f
.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
assume
A55: p in A & q in A & u in B;
per cases by A55,ENUMSET1:def 1;
suppose
A56: p in A & q in A & u = {A};
then reconsider p9 = p, q9 = q as Element of A;
A57: f.(p,q) = d.(p9,q9) by Def10;
d.(p9,x) <= d.(p9,q9) "\/" d.(q9,x) by A2;
then
A58: d.(p9,x)"\/"a <= (d.(p9,q9) "\/" d.(q9,x))"\/"a by WAYBEL_1:2;
f.(p,u) = d.(p9,x)"\/"a & f.(q,u) = d.(q9,x)"\/"a by A56,Def10;
hence thesis by A57,A58,LATTICE3:14;
end;
suppose
A59: p in A & q in A & u = {{A}};
then reconsider p9 = p, q9 = q as Element of A;
A60: f.(p,q) = d.(p9,q9) by Def10;
d.(p9,x) <= d.(p9,q9) "\/" d.(q9,x) by A2;
then d.(p9,x)"\/"a <= (d.(p9,q9) "\/" d.(q9,x))"\/"a by WAYBEL_1:2;
then (d.(p9,x)"\/"a)"\/"b <= ((d.(p9,q9) "\/" d.(q9,x))"\/"a)"\/" b by
WAYBEL_1:2;
then
A61: d.(p9,x)"\/"a"\/"b <= (d.(p9,q9) "\/" (d.(q9,x)"\/"a))"\/"b by
LATTICE3:14;
f.(p,u) = d.(p9,x)"\/"a"\/"b & f.(q,u) = d.(q9,x)"\/"a"\/"b by A59,Def10;
hence thesis by A60,A61,LATTICE3:14;
end;
suppose
A62: p in A & q in A & u = {{{A}}};
then reconsider p9 = p, q9 = q as Element of A;
A63: f.(p,q) = d.(p9,q9) by Def10;
d.(p9,y) <= d.(p9,q9) "\/" d.(q9,y) by A2;
then
A64: d.(p9,y)"\/"b <= (d.(p9,q9) "\/" d.(q9,y))"\/"b by WAYBEL_1:2;
f.(p,u) = d.(p9,y)"\/"b & f.(q,u) = d.(q9,y)"\/"b by A62,Def10;
hence thesis by A63,A64,LATTICE3:14;
end;
end;
A65: for p,q,u being Element of new_set A st p in B & q in B & u in B holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
assume
A66: p in B & q in B & u in B;
per cases by A66,ENUMSET1:def 1;
suppose
A67: p = {A} & q = {A} & u = {A};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A67,Def10;
end;
suppose
A68: p = {A} & q = {A} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,u) by Def10
.= Bottom L"\/"b by A68,Def10
.= b by WAYBEL_1:3;
hence thesis by A68,Def10;
end;
suppose
A69: p = {A} & q = {A} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,u) by Def10
.= Bottom L"\/"(a"\/"b) by A69,Def10
.= a"\/"b by WAYBEL_1:3;
hence thesis by A69,Def10;
end;
suppose
A70: p = {A} & q = {{A}} & u = {A};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A70,Def10;
end;
suppose
A71: p = {A} & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = b"\/"f.(q,u) by Def10
.= Bottom L"\/"b by A71,Def10
.= b by WAYBEL_1:3;
hence thesis by A71,Def10;
end;
suppose
A72: p = {A} & q = {{A}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = b"\/"f.(q,u) by Def10
.= a"\/"b by A72,Def10;
hence thesis by A72,Def10;
end;
suppose
A73: p = {A} & q = {{{A}}} & u = {A};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A73,Def10;
end;
suppose
A74: p = {A} & q = {{{A}}} & u = {{A}};
then
A75: f.(p,u) = b by Def10;
f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by A74,Def10
.= (b"\/"a) "\/" a by A74,Def10
.= b"\/"(a"\/"a) by LATTICE3:14
.= b"\/"a by YELLOW_5:1;
hence thesis by A75,YELLOW_0:22;
end;
suppose
A76: p = {A} & q = {{{A}}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by Def10
.= Bottom L"\/"(a "\/" b) by A76,Def10
.= a"\/"b by WAYBEL_1:3
.= f.(p,q) by A76,Def10;
hence thesis by A76;
end;
suppose
A77: p = {{A}} & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = b"\/" f.(q,u) by Def10
.= Bottom L"\/"b by A77,Def10
.= b by WAYBEL_1:3
.= f.(p,q) by A77,Def10;
hence thesis by A77;
end;
suppose
A78: p = {{A}} & q = {A} & u = {{A}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A78,Def10;
end;
suppose
A79: p = {{A}} & q = {A} & u = {{{A}}};
then
A80: f.(p,u) = a by Def10;
f.(p,q) "\/" f.(q,u) = b"\/" f.(q,u) by A79,Def10
.= b"\/"(b"\/" a) by A79,Def10
.= (b"\/"b)"\/"a by LATTICE3:14
.= b"\/"a by YELLOW_5:1;
hence thesis by A80,YELLOW_0:22;
end;
suppose
A81: p = {{A}} & q = {{A}} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def10
.= Bottom L"\/"b by A81,Def10
.= b by WAYBEL_1:3;
hence thesis by A81,Def10;
end;
suppose
A82: p = {{A}} & q = {{A}} & u = {{A}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A82,Def10;
end;
suppose
A83: p = {{A}} & q = {{A}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def10
.= Bottom L"\/"a by A83,Def10
.= a by WAYBEL_1:3;
hence thesis by A83,Def10;
end;
suppose
A84: p = {{A}} & q = {{{A}}} & u = {A};
then
A85: f.(p,u) = b by Def10;
f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by A84,Def10
.= a"\/"(a"\/" b) by A84,Def10
.= (a"\/"a)"\/"b by LATTICE3:14
.= a"\/"b by YELLOW_5:1;
hence thesis by A85,YELLOW_0:22;
end;
suppose
A86: p = {{A}} & q = {{{A}}} & u = {{A}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A86,Def10;
end;
suppose
A87: p = {{A}} & q = {{{A}}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def10
.= Bottom L"\/"a by A87,Def10
.= a by WAYBEL_1:3
.= f.(p,q) by A87,Def10;
hence thesis by A87;
end;
suppose
A88: p = {{{A}}} & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by Def10
.= Bottom L"\/"(a "\/" b) by A88,Def10
.= a"\/"b by WAYBEL_1:3
.= f.(p,q) by A88,Def10;
hence thesis by A88;
end;
suppose
A89: p = {{{A}}} & q = {A} & u = {{A}};
then
A90: f.(p,u) = a by Def10;
f.(p,q) "\/" f.(q,u) = (a"\/"b)"\/" f.(q,u) by A89,Def10
.= (a"\/"b) "\/" b by A89,Def10
.= a"\/"(b"\/"b) by LATTICE3:14
.= a"\/"b by YELLOW_5:1;
hence thesis by A90,YELLOW_0:22;
end;
suppose
A91: p = {{{A}}} & q = {A} & u = {{{A}}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A91,Def10;
end;
suppose
A92: p = {{{A}}} & q = {{A}} & u = {A};
then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def10
.= a"\/"b by A92,Def10;
hence thesis by A92,Def10;
end;
suppose
A93: p = {{{A}}} & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = a"\/" f.(q,u) by Def10
.= Bottom L"\/"a by A93,Def10
.= a by WAYBEL_1:3
.= f.(p,q) by A93,Def10;
hence thesis by A93;
end;
suppose
A94: p = {{{A}}} & q = {{A}} & u = {{{A}}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A94,Def10;
end;
suppose
A95: p = {{{A}}} & q = {{{A}}} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def10
.= Bottom L"\/"(a"\/"b) by A95,Def10
.= a"\/"b by WAYBEL_1:3;
hence thesis by A95,Def10;
end;
suppose
A96: p = {{{A}}} & q = {{{A}}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/" f.(p,u) by Def10
.= Bottom L"\/"a by A96,Def10
.= a by WAYBEL_1:3;
hence thesis by A96,Def10;
end;
suppose
A97: p = {{{A}}} & q = {{{A}}} & u = {{{A}}};
Bottom L <= f.(p,q) "\/" f.(q,u) by YELLOW_0:44;
hence thesis by A97,Def10;
end;
end;
A98: for p,q,u being Element of new_set A st p in B & q in A & u in B holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
assume that
A99: p in B and
A100: q in A and
A101: u in B;
reconsider q9 = q as Element of A by A100;
per cases by A99,A100,A101,ENUMSET1:def 1;
suppose
q in A & p = {A} & u = {A};
then f.(p,u) = Bottom L by Def10;
hence thesis by YELLOW_0:44;
end;
suppose
A102: q in A & p = {A} & u = {{A}};
then
A103: f.(p,q) "\/" f.(q,u) = f.(p,q)"\/"(d.(q9,x)"\/"a"\/"b) by Def10
.= f.(p,q)"\/"(d.(q9,x)"\/"(a"\/"b)) by LATTICE3:14
.= (f.(p,q)"\/"d.(q9,x))"\/"(a"\/"b) by LATTICE3:14
.= ((f.(p,q)"\/"d.(q9,x))"\/"a)"\/"b by LATTICE3:14;
f.(p,u) = b by A102,Def10;
hence thesis by A103,YELLOW_0:22;
end;
suppose
A104: q in A & p = {A} & u = {{{A}}};
then
A105: f.(p,u) = a"\/"b by Def10;
f.(p,q) "\/" f.(q,u) = (d.(q9,x)"\/"a)"\/"f.(q,u) by A104,Def10
.= (d.(q9,x)"\/"a)"\/"(d.(q9,y)"\/"b) by A104,Def10
.= d.(q9,x)"\/"(a"\/"(d.(q9,y)"\/"b)) by LATTICE3:14
.= d.(q9,x)"\/"(d.(q9,y)"\/"(a"\/"b)) by LATTICE3:14
.= (d.(q9,x)"\/"d.(q9,y))"\/"(a"\/"b) by LATTICE3:14;
hence thesis by A105,YELLOW_0:22;
end;
suppose
A106: q in A & p = {{A}} & u = {A};
then
A107: f.(p,q) "\/" f.(q,u) = (d.(q9,x)"\/"a"\/"b)"\/"f.(q,u) by Def10
.= f.(q,u)"\/"(d.(q9,x)"\/"(a"\/"b)) by LATTICE3:14
.= (f.(q,u)"\/"d.(q9,x))"\/"(a"\/"b) by LATTICE3:14
.= ((f.(q,u)"\/"d.(q9,x))"\/"a)"\/"b by LATTICE3:14;
f.(p,u) = b by A106,Def10;
hence thesis by A107,YELLOW_0:22;
end;
suppose
q in A & p = {{A}} & u = {{A}};
then f.(p,u) = Bottom L by Def10;
hence thesis by YELLOW_0:44;
end;
suppose
A108: q in A & p = {{A}} & u = {{{A}}};
then
A109: f.(p,q) "\/" f.(q,u) = (d.(q9,x)"\/"a"\/"b)"\/"f.(q,u) by Def10
.= (a"\/"(d.(q9,x)"\/"b))"\/"f.(q,u) by LATTICE3:14
.= a"\/"((d.(q9,x)"\/"b)"\/"f.(q,u)) by LATTICE3:14;
f.(p,u) = a by A108,Def10;
hence thesis by A109,YELLOW_0:22;
end;
suppose
A110: q in A & p = {{{A}}} & u = {A};
then
A111: f.(p,u) = a"\/"b by Def10;
f.(p,q) "\/" f.(q,u) = (d.(q9,y)"\/"b)"\/"f.(q,u) by A110,Def10
.= (d.(q9,y)"\/"b)"\/"(d.(q9,x)"\/"a) by A110,Def10
.= d.(q9,y)"\/"(b"\/"(d.(q9,x)"\/"a)) by LATTICE3:14
.= d.(q9,y)"\/"(d.(q9,x)"\/"(b"\/"a)) by LATTICE3:14
.= (d.(q9,y)"\/"d.(q9,x))"\/"(a"\/"b) by LATTICE3:14;
hence thesis by A111,YELLOW_0:22;
end;
suppose
A112: q in A & p = {{{A}}} & u = {{A}};
then
A113: f.(p,q) "\/" f.(q,u) = f.(p,q)"\/"(d.(q9,x)"\/"a"\/"b) by Def10
.= f.(p,q)"\/"(d.(q9,x)"\/"(a"\/"b)) by LATTICE3:14
.= (f.(p,q)"\/"d.(q9,x))"\/"(a"\/"b) by LATTICE3:14
.= ((f.(p,q)"\/"d.(q9,x))"\/"b)"\/"a by LATTICE3:14;
f.(p,u) = a by A112,Def10;
hence thesis by A113,YELLOW_0:22;
end;
suppose
q in A & p = {{{A}}} & u = {{{A}}};
then f.(p,u) = Bottom L by Def10;
hence thesis by YELLOW_0:44;
end;
end;
A114: for p,q,u being Element of new_set A st p in A & q in B & u in B holds
f.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
assume that
A115: p in A and
A116: q in B & u in B;
reconsider p9 = p as Element of A by A115;
per cases by A115,A116,ENUMSET1:def 1;
suppose
A117: p in A & q = {A} & u = {A};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def10
.= f.(p,q) by WAYBEL_1:3;
hence thesis by A117;
end;
suppose
A118: p in A & q = {A} & u = {{A}};
then f.(p,u) = d.(p9,x)"\/"a"\/"b by Def10
.= f.(p,q)"\/"b by A118,Def10;
hence thesis by A118,Def10;
end;
suppose
A119: p in A & q = {A} & u = {{{A}}};
d.(p9,y) <= d.(p9,x)"\/"d.(x,y) by A2;
then d.(p9,y)"\/"b <= (d.(p9,x)"\/"d.(x,y))"\/"b by WAYBEL_1:2;
then
A120: f.(p,u) <= (d.(p9,x)"\/"d.(x,y))"\/"b by A119,Def10;
d.(p9,x)"\/"b <= d.(p9,x)"\/"b;
then
(d.(p9,x)"\/"d.(x,y))"\/"b = (d.(p9,x)"\/"b)"\/"d.(x,y) & (d.(p9,x)
"\/"b) "\/"d.(x,y) <= (d.(p9,x)"\/"b)"\/"(a"\/" b) by A14,LATTICE3:14
,YELLOW_3:3;
then
A121: f.(p,u) <= (d.(p9,x)"\/"b)"\/"(a"\/"b) by A120,ORDERS_2:3;
A122: (d.(p9,x)"\/"b)"\/"(a"\/"b) = d.(p9,x)"\/"((b"\/"a)"\/"b) by LATTICE3:14
.= d.(p9,x)"\/"(a"\/"(b"\/"b)) by LATTICE3:14
.= d.(p9,x)"\/"(a"\/"b) by YELLOW_5:1
.= d.(p9,x)"\/"((a"\/"a)"\/"b) by YELLOW_5:1
.= d.(p9,x)"\/"(a"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p9,x)"\/"a)"\/"(a"\/"b) by LATTICE3:14;
f.(p,q) = d.(p9,x)"\/"a by A119,Def10;
hence thesis by A119,A121,A122,Def10;
end;
suppose
A123: p in A & q = {{A}} & u = {A};
then f.(p,q) = d.(p9,x)"\/"a"\/"b by Def10
.= f.(p,u)"\/"b by A123,Def10;
then f.(p,q) "\/" f.(q,u) = (f.(p,u)"\/"b)"\/"b by A123,Def10
.= f.(p,u)"\/"(b"\/"b) by LATTICE3:14
.= f.(p,u)"\/"b by YELLOW_5:1;
hence thesis by YELLOW_0:22;
end;
suppose
A124: p in A & q = {{A}} & u = {{A}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def10
.= f.(p,q) by WAYBEL_1:3;
hence thesis by A124;
end;
suppose
A125: p in A & q = {{A}} & u = {{{A}}};
d.(p9,y) <= d.(p9,x)"\/"d.(x,y) by A2;
then d.(p9,y)"\/"b <= (d.(p9,x)"\/"d.(x,y))"\/"b by WAYBEL_1:2;
then
A126: f.(p,u) <= (d.(p9,x)"\/"d.(x,y))"\/"b by A125,Def10;
d.(p9,x)"\/"b <= d.(p9,x)"\/"b;
then
(d.(p9,x)"\/"d.(x,y))"\/"b = (d.(p9,x)"\/"b)"\/"d.(x,y) & (d.(p9,x)
"\/"b) "\/"d.(x,y) <= (d.(p9,x)"\/"b)"\/"(a"\/" b) by A14,LATTICE3:14
,YELLOW_3:3;
then
A127: f.(p,u) <= (d.(p9,x)"\/"b)"\/"(a"\/"b) by A126,ORDERS_2:3;
A128: (d.(p9,x)"\/"b)"\/"(a"\/"b) = d.(p9,x)"\/"((b"\/"a)"\/"b) by LATTICE3:14
.= d.(p9,x)"\/"(a"\/"(b"\/"b)) by LATTICE3:14
.= d.(p9,x)"\/"(a"\/"b) by YELLOW_5:1
.= d.(p9,x)"\/"((a"\/"a)"\/"b) by YELLOW_5:1
.= d.(p9,x)"\/"(a"\/"(a"\/"b)) by LATTICE3:14
.= (d.(p9,x)"\/"(a"\/"b))"\/"a by LATTICE3:14
.= (d.(p9,x)"\/"a"\/"b)"\/"a by LATTICE3:14;
f.(p,q) = d.(p9,x)"\/"a"\/"b by A125,Def10;
hence thesis by A125,A127,A128,Def10;
end;
suppose
A129: p in A & q = {{{A}}} & u = {A};
d.(p9,x) <= d.(p9,y)"\/"d.(y,x) by A2;
then d.(p9,x)"\/"a <= (d.(p9,y)"\/"d.(y,x))"\/"a by WAYBEL_1:2;
then
A130: f.(p,u) <= (d.(p9,y)"\/"d.(y,x))"\/"a by A129,Def10;
d.(y,x) <= a"\/"b & d.(p9,y)"\/"a <= d.(p9,y)"\/"a by A1,A14;
then
(d.(p9,y)"\/"d.(y,x))"\/"a = (d.(p9,y)"\/"a)"\/"d.(y,x) & (d.(p9,y)
"\/"a) "\/"d.(y,x) <= (d.(p9,y)"\/"a)"\/"(a"\/" b) by LATTICE3:14,YELLOW_3:3;
then
A131: f.(p,u) <= (d.(p9,y)"\/"a)"\/"(a"\/"b) by A130,ORDERS_2:3;
A132: (d.(p9,y)"\/"a)"\/"(a"\/"b) = (d.(p9,y)"\/"a"\/"a)"\/"b by LATTICE3:14
.=(d.(p9,y)"\/"(a"\/"a))"\/" b by LATTICE3:14
.= (d.(p9,y)"\/"a)"\/"b by YELLOW_5:1
.= d.(p9,y)"\/"(a"\/"b) by LATTICE3:14
.= d.(p9,y)"\/"(a"\/"(b"\/"b)) by YELLOW_5:1
.= d.(p9,y)"\/"((a"\/"b)"\/"b) by LATTICE3:14
.= (d.(p9,y)"\/"b)"\/"(a"\/"b) by LATTICE3:14;
f.(p,q) = d.(p9,y)"\/"b by A129,Def10;
hence thesis by A129,A131,A132,Def10;
end;
suppose
A133: p in A & q = {{{A}}} & u = {{A}};
d.(p9,x) <= d.(p9,y)"\/"d.(y,x) by A2;
then
A134: d.(p9,x)"\/"(a"\/"b) <= (d.(p9,y)"\/"d.(y,x))"\/"(a"\/"b) by WAYBEL_1:2;
f.(p,u) = d.(p9,x)"\/"a"\/"b by A133,Def10;
then
A135: f.(p,u) <= (d.(p9,y)"\/"d.(y,x))"\/"(a"\/"b) by A134,LATTICE3:14;
A136: (d.(p9,y)"\/"a)"\/"(a"\/"b) = (d.(p9,y)"\/"a"\/"a)"\/"b by LATTICE3:14
.=(d.(p9,y)"\/"(a"\/"a))"\/" b by LATTICE3:14
.= (d.(p9,y)"\/"a)"\/"b by YELLOW_5:1
.= (d.(p9,y)"\/"b)"\/" a by LATTICE3:14;
A137: f.(p,q) = d.(p9,y)"\/"b by A133,Def10;
A138: d.(p9,y)"\/"(a"\/"b) <= d.(p9,y)"\/"(a"\/"b);
d.(y,x) <= a"\/"b & (d.(p9,y)"\/"d.(y,x))"\/"(a"\/"b) = (d.(p9,y)
"\/"(a"\/"b ))"\/" d.(y,x) by A1,A14,LATTICE3:14;
then
A139: (d.(p9,y)"\/"d.(y,x))"\/"(a"\/"b)<=(d.(p9,y)"\/"(a"\/"b))"\/"( a
"\/" b) by A138,YELLOW_3:3;
(d.(p9,y)"\/"a)"\/"(a"\/"b) = (d.(p9,y)"\/"a)"\/"((a"\/"b)"\/"(a
"\/" b)) by YELLOW_5:1
.= d.(p9,y)"\/"(a"\/"((a"\/"b)"\/"(a"\/"b))) by LATTICE3:14
.= d.(p9,y)"\/"((a"\/"(a"\/"b))"\/"(a"\/"b)) by LATTICE3:14
.= d.(p9,y)"\/"(((a"\/"a)"\/"b)"\/"(a"\/"b)) by LATTICE3:14
.= d.(p9,y)"\/"((a"\/"b)"\/"(a"\/"b)) by YELLOW_5:1
.= (d.(p9,y)"\/"(a"\/"b))"\/"(a"\/"b) by LATTICE3:14;
then f.(p,u) <= (d.(p9,y)"\/"a)"\/"(a"\/"b) by A139,A135,ORDERS_2:3;
hence thesis by A133,A137,A136,Def10;
end;
suppose
A140: p in A & q = {{{A}}} & u = {{{A}}};
then f.(p,q) "\/" f.(q,u) = Bottom L"\/"f.(p,q) by Def10
.= f.(p,q) by WAYBEL_1:3;
hence thesis by A140;
end;
end;
A141: for p,q,u being Element of new_set A st p in A & q in A & u in A holds f
.(p,u) <= f.(p,q) "\/" f.(q,u)
proof
let p,q,u be Element of new_set A;
assume p in A & q in A & u in A;
then reconsider p9 = p, q9 = q, u9 = u as Element of A;
A142: f.(q,u) = d.(q9,u9) by Def10;
f.(p,u) = d.(p9,u9) & f.(p,q) = d.(p9,q9) by Def10;
hence thesis by A2,A142;
end;
for p,q,u being Element of new_set A holds f.(p,u) <= f.(p,q) "\/" f.( q,u)
proof
let p,q,u be Element of new_set A;
per cases by XBOOLE_0:def 3;
suppose
p in A & q in A & u in A;
hence thesis by A141;
end;
suppose
p in A & q in A & u in B;
hence thesis by A54;
end;
suppose
p in A & q in B & u in A;
hence thesis by A3;
end;
suppose
p in A & q in B & u in B;
hence thesis by A114;
end;
suppose
p in B & q in A & u in A;
hence thesis by A42;
end;
suppose
p in B & q in A & u in B;
hence thesis by A98;
end;
suppose
p in B & q in B & u in A;
hence thesis by A15;
end;
suppose
p in B & q in B & u in B;
hence thesis by A65;
end;
end;
hence thesis;
end;
theorem Th19:
for d be BiFunction of A,L for q be Element of [:A,A,the carrier
of L,the carrier of L:] holds d c= new_bi_fun(d,q)
proof
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
set g = new_bi_fun(d,q);
A1: A c= new_set A by XBOOLE_1:7;
A2: for z being object st z in dom d holds d.z = g.z
proof
let z be object;
assume
A3: z in dom d;
then consider x,y being object such that
A4: [x,y] = z by RELAT_1:def 1;
reconsider x9 = x, y9 = y as Element of A by A3,A4,ZFMISC_1:87;
d.[x,y] = d.(x9,y9) .= g.(x9,y9) by Def10
.= g.[x,y];
hence thesis by A4;
end;
dom d = [:A,A:] & dom g = [:new_set A,new_set A:] by FUNCT_2:def 1;
then dom d c= dom g by A1,ZFMISC_1:96;
hence thesis by A2,GRFUNC_1:2;
end;
definition
let A,L;
let d be BiFunction of A,L;
func DistEsti(d) -> Cardinal means
:Def11:
it,{ [x,y,a,b] where x is Element
of A, y is Element of A, a is Element of L, b is Element of L: d.(x,y) <= a"\/"
b} are_equipotent;
existence
proof
set D = { [x,y,a,b] where x is Element of A, y is Element of A, a is
Element of L, b is Element of L: d.(x,y) <= a"\/"b};
take card D;
thus thesis by CARD_1:def 2;
end;
uniqueness
by WELLORD2:15,CARD_1:2;
end;
theorem Th20:
for d be distance_function of A,L holds DistEsti(d) <> {}
proof
let d be distance_function of A,L;
set X = { [x,y,a,b] where x is Element of A, y is Element of A, a is Element
of L, b is Element of L: d.(x,y) <= a"\/"b};
set x9 = the Element of A;
consider z being set such that
A1: z = [x9,x9,Bottom L,Bottom L];
A2: DistEsti(d),X are_equipotent by Def11;
d.(x9,x9) = Bottom L by Def6
.= Bottom L "\/" Bottom L by YELLOW_5:1;
then z in X by A1;
hence thesis by A2,CARD_1:26;
end;
reserve T,L1 for Sequence,
O,O1,O2,O3,C for Ordinal;
definition
let A;
let O;
func ConsecutiveSet(A,O) -> set means
:Def12:
ex L0 being Sequence st it = last
L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal st succ C in succ O
holds L0.succ C = new_set L0.C) & for C being Ordinal st C in succ O & C <> 0
& C is limit_ordinal holds L0.C = union rng (L0|C);
correctness
proof
deffunc D(Ordinal,Sequence) = union rng $2;
deffunc C(Ordinal,set) = new_set $2;
(ex x being object,L1
st x = last L1 & dom L1 = succ O & L1.0 = A & (for C being
Ordinal st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C being Ordinal
st C in succ O & C <> 0 & C is limit_ordinal holds L1.C = D(C,L1|C) ) & for x1
,x2 being set st (ex L1 st x1 = last L1 & dom L1 = succ O & L1.0 = A & (for C
st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C st C in succ O & C <>
0 & C is limit_ordinal holds L1.C = D(C,L1|C) ) & (ex L1 st x2 = last L1 & dom
L1 = succ O & L1.0 = A & (for C st succ C in succ O holds L1.succ C = C(C,L1.C
)) & for C st C in succ O & C <> 0 & C is limit_ordinal holds L1.C = D(C,L1|C)
) holds x1 = x2 from ORDINAL2:sch 7;
hence thesis;
end;
end;
theorem Th21:
ConsecutiveSet(A,0) = A
proof
deffunc V(Ordinal,Sequence) = union rng $2;
deffunc U(Ordinal,set) = new_set $2;
deffunc F(Ordinal) = ConsecutiveSet(A,$1);
A1: for O being Ordinal, x being object holds x = F(O) iff ex L0 being
Sequence st x = last L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal
st succ C in succ O holds L0.succ C = U(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = V(C,L0|C) by Def12;
thus F(0) = A from ORDINAL2:sch 8(A1);
end;
theorem Th22:
ConsecutiveSet(A,succ O) = new_set ConsecutiveSet(A,O)
proof
deffunc V(Ordinal,Sequence) = union rng $2;
deffunc U(Ordinal,set) = new_set $2;
deffunc F(Ordinal) = ConsecutiveSet(A,$1);
A1: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal
st succ C in succ O holds L0.succ C = U(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = V(C,L0|C) by Def12;
for O holds F(succ O) = U(O,F(O)) from ORDINAL2:sch 9(A1);
hence thesis;
end;
theorem Th23:
O <> 0 & O is limit_ordinal & dom T = O & (for O1 being Ordinal
st O1 in O holds T.O1 = ConsecutiveSet(A,O1)) implies ConsecutiveSet(A,O) =
union rng T
proof
deffunc V(Ordinal,Sequence) = union rng $2;
deffunc U(Ordinal,set) = new_set $2;
deffunc F(Ordinal) = ConsecutiveSet(A,$1);
assume that
A1: O <> 0 & O is limit_ordinal and
A2: dom T = O and
A3: for O1 being Ordinal st O1 in O holds T.O1 = F(O1);
A4: for O being Ordinal, x being object holds x = F(O) iff ex L0 being
Sequence st x = last L0 & dom L0 = succ O & L0.0 = A & (for C being Ordinal
st succ C in succ O holds L0.succ C = U(C,L0.C)) & for C being Ordinal st C in
succ O & C <> 0 & C is limit_ordinal holds L0.C = V(C,L0|C) by Def12;
thus F(O) = V(O,T) from ORDINAL2:sch 10(A4,A1,A2,A3);
end;
registration
let A;
let O;
cluster ConsecutiveSet(A,O) -> non empty;
coherence
proof
defpred X[Ordinal] means ConsecutiveSet(A,$1) is non empty;
A1: for O st X[O] holds X[succ O]
proof
let O1;
assume ConsecutiveSet(A,O1) is non empty;
ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th22;
hence thesis;
end;
A2: for O st O <> 0 & O is limit_ordinal & for B being Ordinal st B in O
holds X[B] holds X[O]
proof
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
let O1;
assume that
A3: O1 <> 0 and
A4: O1 is limit_ordinal and
for O2 st O2 in O1 holds ConsecutiveSet(A,O2) is non empty;
A5: {} in O1 by A3,ORDINAL3:8;
consider Ls being Sequence such that
A6: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = U(
O2) from ORDINAL2:sch 2;
Ls.{} = ConsecutiveSet(A,{}) by A3,A6,ORDINAL3:8
.= A by Th21;
then
A7: A in rng Ls by A6,A5,FUNCT_1:def 3;
ConsecutiveSet(A,O1) = union rng Ls by A3,A4,A6,Th23;
then A c= ConsecutiveSet(A,O1) by A7,ZFMISC_1:74;
hence thesis;
end;
A8: X[0] by Th21;
for O holds X[O] from ORDINAL2:sch 1(A8,A1,A2);
hence thesis;
end;
end;
theorem Th24:
A c= ConsecutiveSet(A,O)
proof
defpred X[Ordinal] means A c= ConsecutiveSet(A,$1);
A1: for O1 st X[O1] holds X[succ O1]
proof
let O1;
ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th22;
then
A2: ConsecutiveSet(A,O1) c= ConsecutiveSet(A,succ O1) by XBOOLE_1:7;
assume A c= ConsecutiveSet(A,O1);
hence thesis by A2,XBOOLE_1:1;
end;
A3: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1
] holds X[O2]
proof
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
let O2;
assume that
A4: O2 <> 0 and
A5: O2 is limit_ordinal and
for O1 st O1 in O2 holds A c= ConsecutiveSet(A,O1);
A6: {} in O2 by A4,ORDINAL3:8;
consider Ls being Sequence such that
A7: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1)
from ORDINAL2:sch 2;
Ls.{} = ConsecutiveSet(A,{}) by A4,A7,ORDINAL3:8
.= A by Th21;
then
A8: A in rng Ls by A7,A6,FUNCT_1:def 3;
ConsecutiveSet(A,O2) = union rng Ls by A4,A5,A7,Th23;
hence thesis by A8,ZFMISC_1:74;
end;
A9: X[0] by Th21;
for O holds X[O] from ORDINAL2:sch 1(A9,A1,A3);
hence thesis;
end;
definition
let A,L;
let d be BiFunction of A,L;
mode QuadrSeq of d -> Sequence of [:A,A,the carrier of L,the carrier of L
:] means
:Def13:
dom it is Cardinal & it is one-to-one & rng it ={[x,y,a,b]
where x is Element of A, y is Element of A, a is Element of L, b is Element of
L: d.(x,y) <= a"\/"b};
existence
proof
set X = {[x,y,a,b] where x is Element of A, y is Element of A, a is
Element of L, b is Element of L: d.(x,y) <= a"\/"b};
card X,X are_equipotent by CARD_1:def 2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = card X and
A3: rng f = X by WELLORD2:def 4;
reconsider f as Sequence by A2,ORDINAL1:def 7;
rng f c= [:A,A,the carrier of L,the carrier of L:]
proof
let z be object;
assume z in rng f;
then
ex x,y being Element of A, a,b being Element of L st z = [x,y,a,b] &
d.(x,y) <= a"\/"b by A3;
hence thesis;
end;
then reconsider
f as Sequence of [:A,A,the carrier of L,the carrier of L:] by
RELAT_1:def 19;
take f;
thus dom f is Cardinal by A2;
thus f is one-to-one by A1;
thus thesis by A3;
end;
end;
definition
let A,L;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O;
assume
A1: O in dom q;
func Quadr(q,O) -> Element of [:ConsecutiveSet(A,O),ConsecutiveSet(A,O), the
carrier of L,the carrier of L:] equals
:Def14:
q.O;
correctness
proof
q.O in rng q by A1,FUNCT_1:def 3;
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 Def13;
then consider x,y be Element of A, a,b be Element of L such that
A2: q.O = [x,y,a,b] and
d.(x,y) <= a"\/"b;
reconsider a,b as Element of L;
A c= ConsecutiveSet(A,O) by Th24;
then reconsider x,y as Element of ConsecutiveSet(A,O);
reconsider z = [x,y,a,b] as Element of [:ConsecutiveSet(A,O),
ConsecutiveSet(A,O), the carrier of L,the carrier of L:];
z = q.O by A2;
hence thesis;
end;
end;
theorem Th25:
for d being BiFunction of A,L, q being QuadrSeq of d holds O in
DistEsti(d) iff O in dom q
proof
let d be BiFunction of A,L;
let q be QuadrSeq of d;
reconsider N = dom q as Cardinal by Def13;
reconsider M = DistEsti(d) as Cardinal;
q is one-to-one by Def13;
then
A1: dom q,rng q are_equipotent by WELLORD2:def 4;
DistEsti(d),{[x,y,a,b] where x is Element of A, y is Element of A, a is
Element of L, b is Element of L: d.(x,y) <= a"\/"b} are_equipotent by Def11;
then DistEsti(d),rng q are_equipotent by Def13;
then DistEsti(d),dom q are_equipotent by A1,WELLORD2:15;
then
A2: M = N by CARD_1:2;
hence O in DistEsti(d) implies O in dom q;
assume O in dom q;
hence thesis by A2;
end;
definition
let A,L;
let z be set;
assume
A1: z is BiFunction of A,L;
func BiFun(z,A,L) -> BiFunction of A,L equals
:Def15:
z;
coherence by A1;
end;
definition
let A,L;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O;
func ConsecutiveDelta(q,O) -> set means
:Def16:
ex L0 being Sequence st it = last
L0 & dom L0 = succ O & L0.0 = d & (for C being Ordinal st succ C in succ O
holds L0.succ C = new_bi_fun(BiFun(L0.C,ConsecutiveSet(A,C),L),Quadr(q,C))) &
for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds L0.C =
union rng(L0|C);
correctness
proof
deffunc D(Ordinal,Sequence) = union rng $2;
deffunc C(Ordinal,set) = new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr
(q,$1));
(ex x being object,L1
st x = last L1 & dom L1 = succ O & L1.0 = d & (for C being
Ordinal st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C being Ordinal
st C in succ O & C <> 0 & C is limit_ordinal holds L1.C = D(C,L1|C) ) & for x1
,x2 being set st (ex L1 st x1 = last L1 & dom L1 = succ O & L1.0 = d & (for C
st succ C in succ O holds L1.succ C = C(C,L1.C)) & for C st C in succ O & C <>
0 & C is limit_ordinal holds L1.C = D(C,L1|C) ) & (ex L1 st x2 = last L1 & dom
L1 = succ O & L1.0 = d & (for C st succ C in succ O holds L1.succ C = C(C,L1.C
)) & for C st C in succ O & C <> 0 & C is limit_ordinal holds L1.C = D(C,L1|C)
) holds x1 = x2 from ORDINAL2:sch 7;
hence thesis;
end;
end;
theorem Th26:
for d being BiFunction of A,L for q being QuadrSeq of d holds
ConsecutiveDelta(q,0) = d
proof
deffunc D(Ordinal,Sequence) = union rng $2;
let d be BiFunction of A,L, q be QuadrSeq of d;
deffunc C(Ordinal,set) = new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q
,$1));
deffunc F(Ordinal) = ConsecutiveDelta(q,$1);
A1: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = 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 <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def16;
thus F(0) = d from ORDINAL2:sch 8(A1);
end;
theorem Th27:
for d be BiFunction of A,L for q being QuadrSeq of d holds
ConsecutiveDelta(q,succ O) = new_bi_fun(BiFun(ConsecutiveDelta(q,O),
ConsecutiveSet(A,O),L),Quadr(q,O))
proof
deffunc D(Ordinal,Sequence) = union rng $2;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
deffunc C(Ordinal,set) = new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q
,$1));
deffunc F(Ordinal) = ConsecutiveDelta(q,$1);
A1: for O being Ordinal, It being object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = 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 <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def16;
for O holds F(succ O) = C(O,F(O)) from ORDINAL2:sch 9(A1);
hence thesis;
end;
theorem Th28:
for d be BiFunction of A,L for q being QuadrSeq of d holds O <>
0 & O is limit_ordinal & dom T = O & (for O1 being Ordinal st O1 in O holds T.
O1 = ConsecutiveDelta(q,O1)) implies ConsecutiveDelta(q,O) = union rng T
proof
deffunc D(Ordinal,Sequence) = union rng $2;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
deffunc C(Ordinal,set) = new_bi_fun(BiFun($2,ConsecutiveSet(A,$1),L),Quadr(q
,$1));
deffunc F(Ordinal) = ConsecutiveDelta(q,$1);
assume that
A1: O <> 0 & 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 object holds It = F(O) iff ex L0 being
Sequence st It = last L0 & dom L0 = succ O & L0.0 = 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 <> 0 & C is limit_ordinal holds L0.C = D(C,L0|C) by Def16;
thus F(O) = D(O,T) from ORDINAL2:sch 10(A4,A1,A2,A3);
end;
theorem Th29:
O1 c= O2 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2)
proof
defpred X[Ordinal] means O1 c= $1 implies ConsecutiveSet(A,O1) c=
ConsecutiveSet(A,$1);
A1: for O2 st X[O2] holds X[succ O2]
proof
let O2;
assume
A2: O1 c= O2 implies ConsecutiveSet(A,O1) c= ConsecutiveSet(A,O2);
assume
A3: O1 c= succ O2;
per cases;
suppose
O1 = succ O2;
hence thesis;
end;
suppose
O1 <> succ O2;
then O1 c< succ O2 by A3;
then
A4: O1 in succ O2 by ORDINAL1:11;
ConsecutiveSet(A,O2) c= new_set ConsecutiveSet(A,O2) by XBOOLE_1:7;
then ConsecutiveSet(A,O1) c= new_set ConsecutiveSet(A,O2) by A2,A4,
ORDINAL1:22;
hence thesis by Th22;
end;
end;
A5: for O2 st O2 <> 0 & O2 is limit_ordinal & for O3 st O3 in O2 holds X[
O3] holds X[O2]
proof
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
let O2;
assume that
A6: O2 <> 0 & O2 is limit_ordinal and
for O3 st O3 in O2 holds O1 c= O3 implies ConsecutiveSet(A,O1) c=
ConsecutiveSet(A,O3);
consider L being Sequence such that
A7: dom L = O2 & for O3 being Ordinal st O3 in O2 holds L.O3 = U(O3)
from ORDINAL2:sch 2;
A8: ConsecutiveSet(A,O2) = union rng L by A6,A7,Th23;
assume
A9: O1 c= O2;
per cases;
suppose
O1 = O2;
hence thesis;
end;
suppose
O1 <> O2;
then
A10: O1 c< O2 by A9;
then O1 in O2 by ORDINAL1:11;
then
A11: L.O1 in rng L by A7,FUNCT_1:def 3;
L.O1 = ConsecutiveSet(A,O1) by A7,A10,ORDINAL1:11;
hence thesis by A8,A11,ZFMISC_1:74;
end;
end;
A12: X[0];
for O2 holds X[O2] from ORDINAL2:sch 1(A12,A1,A5);
hence thesis;
end;
theorem Th30:
for d be BiFunction of A,L for q being QuadrSeq of d holds
ConsecutiveDelta(q,O) is BiFunction of ConsecutiveSet(A,O),L
proof
let d be BiFunction of A,L;
let q be QuadrSeq of d;
defpred Y[Ordinal] means ConsecutiveDelta(q,$1) is BiFunction of
ConsecutiveSet(A,$1),L;
A1: for O1 st Y[O1] holds Y[succ O1]
proof
let O1;
assume ConsecutiveDelta(q,O1) is BiFunction of ConsecutiveSet(A,O1),L;
then reconsider
CD = ConsecutiveDelta(q,O1) as BiFunction of ConsecutiveSet(A,
O1),L;
A2: ConsecutiveSet(A,succ O1) = new_set ConsecutiveSet(A,O1) by Th22;
ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th27
.= new_bi_fun(CD,Quadr(q,O1)) by Def15;
hence thesis by A2;
end;
A3: for O1 st O1 <> 0 & O1 is limit_ordinal & for O2 st O2 in O1 holds Y[O2]
holds Y[O1]
proof
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
let O1;
assume that
A4: O1 <> 0 and
A5: O1 is limit_ordinal and
A6: for O2 st O2 in O1 holds ConsecutiveDelta(q,O2) is BiFunction of
ConsecutiveSet(A,O2),L;
consider Ls being Sequence such that
A7: dom Ls = O1 & for O2 being Ordinal st O2 in O1 holds Ls.O2 = U(O2
) from ORDINAL2:sch 2;
A8: for O,O2 st O c= O2 & O2 in dom Ls holds Ls.O c= Ls.O2
proof
let O;
defpred X[Ordinal] means O c= $1 & $1 in dom Ls implies Ls.O c= Ls.$1;
A9: for O2 st O2 <> 0 & O2 is limit_ordinal & for O3 st O3 in O2 holds
X[O3] holds X[O2]
proof
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
let O2;
assume that
A10: O2 <> 0 & O2 is limit_ordinal and
for O3 st O3 in O2 holds O c= O3 & O3 in dom Ls implies Ls.O c= Ls
. O3;
assume that
A11: O c= O2 and
A12: O2 in dom Ls;
consider Lt being Sequence such that
A13: dom Lt = O2 & for O3 being Ordinal st O3 in O2 holds Lt.O3 =
U(O3) from ORDINAL2:sch 2;
A14: Ls.O2 = ConsecutiveDelta(q,O2) by A7,A12
.= union rng Lt by A10,A13,Th28;
per cases;
suppose
O = O2;
hence thesis;
end;
suppose
O <> O2;
then
A15: O c< O2 by A11;
then
A16: O in O2 by ORDINAL1:11;
then Ls.O = ConsecutiveDelta(q,O) by A7,A12,ORDINAL1:10
.= Lt.O by A13,A15,ORDINAL1:11;
then Ls.O in rng Lt by A13,A16,FUNCT_1:def 3;
hence thesis by A14,ZFMISC_1:74;
end;
end;
A17: for O2 st X[O2] holds X[succ O2]
proof
let O2;
assume
A18: O c= O2 & O2 in dom Ls implies Ls.O c= Ls.O2;
assume that
A19: O c= succ O2 and
A20: succ O2 in dom Ls;
per cases;
suppose
O = succ O2;
hence thesis;
end;
suppose
O <> succ O2;
then O c< succ O2 by A19;
then
A21: O in succ O2 by ORDINAL1:11;
A22: O2 in succ O2 by ORDINAL1:6;
then O2 in dom Ls by A20,ORDINAL1:10;
then reconsider cd2 = ConsecutiveDelta(q,O2) as BiFunction of
ConsecutiveSet(A,O2),L by A6,A7;
Ls.succ O2 = ConsecutiveDelta(q,succ O2) by A7,A20
.= new_bi_fun(BiFun(ConsecutiveDelta(q,O2), ConsecutiveSet(A,O2)
,L),Quadr(q,O2)) by Th27
.= new_bi_fun(cd2,Quadr(q,O2)) by Def15;
then ConsecutiveDelta(q,O2) c= Ls.succ O2 by Th19;
then Ls.O2 c= Ls.succ O2 by A7,A20,A22,ORDINAL1:10;
hence thesis by A18,A20,A21,A22,ORDINAL1:10,22;
end;
end;
A23: X[0];
thus for O2 holds X[O2] from ORDINAL2:sch 1(A23,A17,A9);
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 that
A24: x in rng Ls and
A25: y in rng Ls;
consider o1 being object such that
A26: o1 in dom Ls and
A27: Ls.o1 = x by A24,FUNCT_1:def 3;
consider o2 being object such that
A28: o2 in dom Ls and
A29: Ls.o2 = y by A25,FUNCT_1:def 3;
reconsider o19 = o1, o29 = o2 as Ordinal by A26,A28;
o19 c= o29 or o29 c= o19;
then x c= y or y c= x by A8,A26,A27,A28,A29;
hence thesis;
end;
then
A30: rng Ls is c=-linear;
set Y = the carrier of L, X = [:ConsecutiveSet(
A,O1),ConsecutiveSet(A,O1):], f = union rng Ls;
rng Ls c= PFuncs(X,Y)
proof
let z be object;
assume z in rng Ls;
then consider o being object such that
A31: o in dom Ls and
A32: z = Ls.o by FUNCT_1:def 3;
reconsider o as Ordinal by A31;
Ls.o = ConsecutiveDelta(q,o) by A7,A31;
then reconsider
h = Ls.o as BiFunction of ConsecutiveSet(A,o),L by A6,A7,A31;
o c= O1 by A7,A31,ORDINAL1:def 2;
then dom h = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):] &
ConsecutiveSet(A,o) c= ConsecutiveSet(A,O1) by Th29,FUNCT_2:def 1;
then rng h c= Y & dom h c= X by ZFMISC_1:96;
hence thesis by A32,PARTFUN1:def 3;
end;
then f in PFuncs(X,Y) by A30,TREES_2:40;
then
A33: ex g being Function st f = g & dom g c= X & rng g c= Y by PARTFUN1:def 3;
reconsider o1 = O1 as non empty Ordinal by A4;
set YY = the set of all
[:ConsecutiveSet(A,O2),ConsecutiveSet(A,O2):] where O2 is
Element of o1 ;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ts being Sequence such that
A34: dom Ts = O1 & for O2 being Ordinal st O2 in O1 holds Ts.O2 = U(O2
) from ORDINAL2:sch 2;
Ls is Function-yielding
proof
let x be object;
assume
A35: x in dom Ls;
then reconsider o = x as Ordinal;
Ls.o = ConsecutiveDelta(q,o) by A7,A35;
hence thesis by A6,A7,A35;
end;
then reconsider LsF = Ls as Function-yielding Function;
A36: rng doms LsF = YY
proof
thus rng doms LsF c= YY
proof
let Z be object;
assume Z in rng doms LsF;
then consider o being object such that
A37: o in dom doms LsF and
A38: Z = (doms LsF).o by FUNCT_1:def 3;
A39: o in dom LsF by A37,FUNCT_6:59;
then reconsider o9 = o as Element of o1 by A7;
Ls.o9 = ConsecutiveDelta(q,o9) by A7;
then reconsider
ls = Ls.o9 as BiFunction of ConsecutiveSet(A,o9),L by A6;
Z = dom ls by A38,A39,FUNCT_6:22
.= [:ConsecutiveSet(A,o9),ConsecutiveSet(A,o9):] by FUNCT_2:def 1;
hence thesis;
end;
let Z be object;
assume Z in YY;
then consider o being Element of o1 such that
A40: Z = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):];
Ls.o = ConsecutiveDelta(q,o) by A7;
then reconsider ls = Ls.o as BiFunction of ConsecutiveSet(A,o),L by A6;
o in dom LsF by A7;
then
A41: o in dom doms LsF by FUNCT_6:59;
Z = dom ls by A40,FUNCT_2:def 1
.= (doms LsF).o by A7,FUNCT_6:22;
hence thesis by A41,FUNCT_1:def 3;
end;
{} in O1 by A4,ORDINAL3:8;
then reconsider RTs = rng Ts as non empty set by A34,FUNCT_1:3;
reconsider f as Function by A33;
A42: dom f = union rng doms LsF by Th1;
A43: 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 object;
assume Z in YY;
then consider o being Element of o1 such that
A44: Z = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):];
Ts.o = ConsecutiveSet(A,o) by A34;
then reconsider CoS = ConsecutiveSet(A,o) as Element of RTs by A34,
FUNCT_1:def 3;
Z = [:CoS,CoS:] by A44;
hence thesis;
end;
let Z be object;
assume Z in XX;
then consider a being Element of RTs such that
A45: Z = [:a,a:] and
a in RTs;
consider o being object such that
A46: o in dom Ts and
A47: a = Ts.o by FUNCT_1:def 3;
reconsider o9 = o as Ordinal by A46;
a = ConsecutiveSet(A,o9) by A34,A46,A47;
hence thesis by A34,A45,A46;
end;
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 that
A48: x in RTs and
A49: y in RTs;
consider o1 being object such that
A50: o1 in dom Ts and
A51: Ts.o1 = x by A48,FUNCT_1:def 3;
consider o2 being object such that
A52: o2 in dom Ts and
A53: Ts.o2 = y by A49,FUNCT_1:def 3;
reconsider o19 = o1, o29 = o2 as Ordinal by A50,A52;
A54: Ts.o29 = ConsecutiveSet(A,o29) by A34,A52;
A55: o19 c= o29 or o29 c= o19;
Ts.o19 = ConsecutiveSet(A,o19) by A34,A50;
then x c= y or y c= x by A51,A53,A54,A55,Th29;
hence thesis;
end;
then
A56: RTs is c=-linear;
A57: ConsecutiveDelta(q,O1) = union rng Ls by A4,A5,A7,Th28;
X = [:union rng Ts, ConsecutiveSet(A,O1):] by A4,A5,A34,Th23
.= [:union RTs, union RTs :] by A4,A5,A34,Th23
.= dom f by A42,A36,A56,A43,Th3;
hence thesis by A57,A33,FUNCT_2:def 1,RELSET_1:4;
end;
ConsecutiveSet(A,{}) = A by Th21;
then
A58: Y[0] by Th26;
for O holds Y[O] from ORDINAL2:sch 1(A58,A1,A3);
hence thesis;
end;
definition
let A,L;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O;
redefine func ConsecutiveDelta(q,O) -> BiFunction of ConsecutiveSet(A,O),L; :: redefines ConsecutiveDelta (LATTICE5, definition)
coherence by Th30;
end;
theorem Th31:
for d be BiFunction of A,L for q being QuadrSeq of d holds d c=
ConsecutiveDelta(q,O)
proof
let d be BiFunction of A,L;
let q be QuadrSeq of d;
defpred X[Ordinal] means d c= ConsecutiveDelta(q,$1);
A1: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1
] holds X[O2]
proof
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
let O2;
assume that
A2: O2 <> 0 and
A3: O2 is limit_ordinal and
for O1 st O1 in O2 holds d c= ConsecutiveDelta(q,O1);
A4: {} in O2 by A2,ORDINAL3:8;
consider Ls being Sequence such that
A5: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1)
from ORDINAL2:sch 2;
Ls.{} = ConsecutiveDelta(q,{}) by A2,A5,ORDINAL3:8
.= d by Th26;
then
A6: d in rng Ls by A5,A4,FUNCT_1:def 3;
ConsecutiveDelta(q,O2) = union rng Ls by A2,A3,A5,Th28;
hence thesis by A6,ZFMISC_1:74;
end;
A7: for O1 st X[O1] holds X[succ O1]
proof
let O1;
ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th27
.= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def15;
then
A8: ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,succ O1) by Th19;
assume d c= ConsecutiveDelta(q,O1);
hence thesis by A8,XBOOLE_1:1;
end;
A9: X[0] by Th26;
for O holds X[O] from ORDINAL2:sch 1(A9,A7,A1);
hence thesis;
end;
theorem Th32:
for d being BiFunction of A,L for q being QuadrSeq of d st O1 c=
O2 holds ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2)
proof
let d be BiFunction of A,L;
let q be QuadrSeq of d;
defpred X[Ordinal] means O1 c= $1 implies ConsecutiveDelta(q,O1) c=
ConsecutiveDelta(q,$1);
A1: for O2 st O2 <> 0 & O2 is limit_ordinal & for O3 st O3 in O2 holds X[
O3] holds X[O2]
proof
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
let O2;
assume that
A2: O2 <> 0 & O2 is limit_ordinal and
for O3 st O3 in O2 holds O1 c= O3 implies ConsecutiveDelta(q,O1) c=
ConsecutiveDelta(q,O3);
consider L being Sequence such that
A3: dom L = O2 & for O3 being Ordinal st O3 in O2 holds L.O3 = U(O3)
from ORDINAL2:sch 2;
A4: ConsecutiveDelta(q,O2) = union rng L by A2,A3,Th28;
assume
A5: O1 c= O2;
per cases;
suppose
O1 = O2;
hence thesis;
end;
suppose
O1 <> O2;
then
A6: O1 c< O2 by A5;
then O1 in O2 by ORDINAL1:11;
then
A7: L.O1 in rng L by A3,FUNCT_1:def 3;
L.O1 = ConsecutiveDelta(q,O1) by A3,A6,ORDINAL1:11;
hence thesis by A4,A7,ZFMISC_1:74;
end;
end;
A8: for O2 st X[O2] holds X[succ O2]
proof
let O2;
assume
A9: O1 c= O2 implies ConsecutiveDelta(q,O1) c= ConsecutiveDelta(q,O2);
assume
A10: O1 c= succ O2;
per cases;
suppose
O1 = succ O2;
hence thesis;
end;
suppose
O1 <> succ O2;
then O1 c< succ O2 by A10;
then
A11: O1 in succ O2 by ORDINAL1:11;
ConsecutiveDelta(q,succ O2) = new_bi_fun(BiFun(ConsecutiveDelta(q,O2
), ConsecutiveSet(A,O2),L),Quadr(q,O2)) by Th27
.= new_bi_fun(ConsecutiveDelta(q,O2),Quadr(q,O2)) by Def15;
then ConsecutiveDelta(q,O2) c= ConsecutiveDelta(q,succ O2) by Th19;
hence thesis by A9,A11,ORDINAL1:22;
end;
end;
A12: X[0];
for O2 holds X[O2] from ORDINAL2:sch 1(A12,A8,A1);
hence thesis;
end;
theorem Th33:
for d be BiFunction of A,L st d is zeroed for q being QuadrSeq
of d holds ConsecutiveDelta(q,O) is zeroed
proof
let d be BiFunction of A,L;
assume
A1: d is zeroed;
let q be QuadrSeq of d;
defpred X[Ordinal] means ConsecutiveDelta(q,$1) is zeroed;
A2: for O1 st X[O1] holds X[succ O1]
proof
let O1;
assume ConsecutiveDelta(q,O1) is zeroed;
then
A3: new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is zeroed by Th16;
let z be Element of ConsecutiveSet(A,succ O1);
reconsider z9 = z as Element of new_set ConsecutiveSet(A,O1) by Th22;
ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th27
.= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def15;
hence
ConsecutiveDelta(q,succ O1).(z,z) = new_bi_fun(ConsecutiveDelta(q,O1)
,Quadr(q,O1)).(z9,z9)
.= Bottom L by A3;
end;
A4: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1
] holds X[O2]
proof
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
let O2;
assume that
A5: O2 <> 0 & O2 is limit_ordinal and
A6: for O1 st O1 in O2 holds ConsecutiveDelta(q,O1) is zeroed;
set CS = ConsecutiveSet(A,O2);
consider Ls being Sequence such that
A7: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1
) from ORDINAL2:sch 2;
ConsecutiveDelta(q,O2) = union rng Ls by A5,A7,Th28;
then reconsider f = union rng Ls as BiFunction of CS,L;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ts being Sequence such that
A8: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1
) from ORDINAL2:sch 2;
A9: ConsecutiveSet(A,O2) = union rng Ts by A5,A8,Th23;
f is zeroed
proof
let x be Element of CS;
consider y being set such that
A10: x in y and
A11: y in rng Ts by A9,TARSKI:def 4;
consider o being object such that
A12: o in dom Ts and
A13: y = Ts.o by A11,FUNCT_1:def 3;
reconsider o as Ordinal by A12;
A14: Ls.o = ConsecutiveDelta(q,o) by A7,A8,A12;
then reconsider h = Ls.o as BiFunction of ConsecutiveSet(A,o),L;
reconsider x9 = x as Element of ConsecutiveSet(A,o) by A8,A10,A12,A13;
A15: dom h = [:ConsecutiveSet(A,o),ConsecutiveSet(A,o):] by FUNCT_2:def 1;
A16: h is zeroed
proof
let z be Element of ConsecutiveSet(A,o);
A17: ConsecutiveDelta(q,o) is zeroed by A6,A8,A12;
thus h.(z,z) = ConsecutiveDelta(q,o).(z,z) by A7,A8,A12
.= Bottom L by A17;
end;
ConsecutiveDelta(q,o) in rng Ls by A7,A8,A12,A14,FUNCT_1:def 3;
then
A18: h c= f by A14,ZFMISC_1:74;
x in ConsecutiveSet(A,o) by A8,A10,A12,A13;
then [x,x] in dom h by A15,ZFMISC_1:87;
hence f.(x,x) = h.(x9,x9) by A18,GRFUNC_1:2
.= Bottom L by A16;
end;
hence thesis by A5,A7,Th28;
end;
A19: X[0]
proof
let z be Element of ConsecutiveSet(A,0);
reconsider z9 = z as Element of A by Th21;
thus ConsecutiveDelta(q,0).(z,z) = d.(z9,z9) by Th26
.= Bottom L by A1;
end;
for O holds X[O] from ORDINAL2:sch 1(A19,A2,A4);
hence thesis;
end;
theorem Th34:
for d be BiFunction of A,L st d is symmetric for q being
QuadrSeq of d holds ConsecutiveDelta(q,O) is symmetric
proof
let d be BiFunction of A,L;
assume
A1: d is symmetric;
let q be QuadrSeq of d;
defpred X[Ordinal] means ConsecutiveDelta(q,$1) is symmetric;
A2: for O1 st X[O1] holds X[succ O1]
proof
let O1;
assume ConsecutiveDelta(q,O1) is symmetric;
then
A3: new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is symmetric by Th17;
let x,y be Element of ConsecutiveSet(A,succ O1);
reconsider x9=x, y9=y as Element of new_set ConsecutiveSet(A,O1) by Th22;
A4: ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1),
ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th27
.= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def15;
hence
ConsecutiveDelta(q,succ O1).(x,y) = new_bi_fun(ConsecutiveDelta(q,O1)
,Quadr(q,O1)).(y9,x9) by A3
.= ConsecutiveDelta(q,succ O1).(y,x) by A4;
end;
A5: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[O1
] holds X[O2]
proof
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
let O2;
assume that
A6: O2 <> 0 & O2 is limit_ordinal and
A7: for O1 st O1 in O2 holds ConsecutiveDelta(q,O1) is symmetric;
set CS = ConsecutiveSet(A,O2);
consider Ls being Sequence such that
A8: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1
) from ORDINAL2:sch 2;
ConsecutiveDelta(q,O2) = union rng Ls by A6,A8,Th28;
then reconsider f = union rng Ls as BiFunction of CS,L;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ts being Sequence such that
A9: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1
) from ORDINAL2:sch 2;
A10: ConsecutiveSet(A,O2) = union rng Ts by A6,A9,Th23;
f is symmetric
proof
let x,y be Element of CS;
consider x1 being set such that
A11: x in x1 and
A12: x1 in rng Ts by A10,TARSKI:def 4;
consider o1 being object such that
A13: o1 in dom Ts and
A14: x1 = Ts.o1 by A12,FUNCT_1:def 3;
consider y1 being set such that
A15: y in y1 and
A16: y1 in rng Ts by A10,TARSKI:def 4;
consider o2 being object such that
A17: o2 in dom Ts and
A18: y1 = Ts.o2 by A16,FUNCT_1:def 3;
reconsider o1,o2 as Ordinal by A13,A17;
A19: x in ConsecutiveSet(A,o1) by A9,A11,A13,A14;
A20: Ls.o1 = ConsecutiveDelta(q,o1) by A8,A9,A13;
then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet(A,o1),L;
A21: h1 is symmetric
proof
let x,y be Element of ConsecutiveSet(A,o1);
A22: ConsecutiveDelta(q,o1) is symmetric by A7,A9,A13;
thus h1.(x,y) = ConsecutiveDelta(q,o1).(x,y) by A8,A9,A13
.= ConsecutiveDelta(q,o1).(y,x) by A22
.= h1.(y,x) by A8,A9,A13;
end;
A23: dom h1 = [:ConsecutiveSet(A,o1),ConsecutiveSet(A,o1):] by FUNCT_2:def 1;
A24: y in ConsecutiveSet(A,o2) by A9,A15,A17,A18;
A25: Ls.o2 = ConsecutiveDelta(q,o2) by A8,A9,A17;
then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet(A,o2),L;
A26: h2 is symmetric
proof
let x,y be Element of ConsecutiveSet(A,o2);
A27: ConsecutiveDelta(q,o2) is symmetric by A7,A9,A17;
thus h2.(x,y) = ConsecutiveDelta(q,o2).(x,y) by A8,A9,A17
.= ConsecutiveDelta(q,o2).(y,x) by A27
.= h2.(y,x) by A8,A9,A17;
end;
A28: dom h2 = [:ConsecutiveSet(A,o2),ConsecutiveSet(A,o2):] by FUNCT_2:def 1;
per cases;
suppose
o1 c= o2;
then
A29: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by Th29;
then
A30: [y,x] in dom h2 by A19,A24,A28,ZFMISC_1:87;
ConsecutiveDelta(q,o2) in rng Ls by A8,A9,A17,A25,FUNCT_1:def 3;
then
A31: h2 c= f by A25,ZFMISC_1:74;
reconsider x9=x, y9=y as Element of ConsecutiveSet(A,o2) by A9,A15,A17
,A18,A19,A29;
[x,y] in dom h2 by A19,A24,A28,A29,ZFMISC_1:87;
hence f.(x,y) = h2.(x9,y9) by A31,GRFUNC_1:2
.= h2.(y9,x9) by A26
.= f.(y,x) by A31,A30,GRFUNC_1:2;
end;
suppose
o2 c= o1;
then
A32: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o1) by Th29;
then
A33: [y,x] in dom h1 by A19,A24,A23,ZFMISC_1:87;
ConsecutiveDelta(q,o1) in rng Ls by A8,A9,A13,A20,FUNCT_1:def 3;
then
A34: h1 c= f by A20,ZFMISC_1:74;
reconsider x9=x, y9=y as Element of ConsecutiveSet(A,o1) by A9,A11,A13
,A14,A24,A32;
[x,y] in dom h1 by A19,A24,A23,A32,ZFMISC_1:87;
hence f.(x,y) = h1.(x9,y9) by A34,GRFUNC_1:2
.= h1.(y9,x9) by A21
.= f.(y,x) by A34,A33,GRFUNC_1:2;
end;
end;
hence thesis by A6,A8,Th28;
end;
A35: X[0]
proof
let x,y be Element of ConsecutiveSet(A,0);
reconsider x9 = x, y9 = y as Element of A by Th21;
thus ConsecutiveDelta(q,0).(x,y) = d.(x9,y9) by Th26
.= d.(y9,x9) by A1
.= ConsecutiveDelta(q,0).(y,x) by Th26;
end;
for O holds X[O] from ORDINAL2:sch 1(A35,A2,A5);
hence thesis;
end;
theorem Th35:
for d be BiFunction of A,L st d is symmetric u.t.i. for q being
QuadrSeq of d st O c= DistEsti(d) holds ConsecutiveDelta(q,O) is u.t.i.
proof
let d be BiFunction of A,L;
assume that
A1: d is symmetric and
A2: d is u.t.i.;
let q be QuadrSeq of d;
defpred X[Ordinal] means $1 c= DistEsti(d) implies ConsecutiveDelta(q,$1) is
u.t.i.;
A3: for O1 st X[O1] holds X[succ O1]
proof
let O1;
assume that
A4: O1 c= DistEsti(d) implies ConsecutiveDelta(q,O1) is u.t.i. and
A5: succ O1 c= DistEsti(d);
A6: O1 in DistEsti(d) by A5,ORDINAL1:21;
then
A7: O1 in dom q by Th25;
then q.O1 in rng q by FUNCT_1:def 3;
then
A8: q.O1 in {[u,v,a9,b9] where u is Element of A, v is Element of A, a9
is Element of L, b9 is Element of L: d.(u,v) <= a9"\/"b9} by Def13;
let x,y,z be Element of ConsecutiveSet(A,succ O1);
A9: ConsecutiveDelta(q,O1) is symmetric by A1,Th34;
reconsider x9 = x, y9 = y, z9 = z as Element of new_set ConsecutiveSet(A,
O1) by Th22;
set f = new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1));
set X = Quadr(q,O1)`1_4, Y = Quadr(q,O1)`2_4;
reconsider a = Quadr(q,O1)`3_4, b = Quadr(q,O1)`4_4 as Element of L;
A10: dom d = [:A,A:] & d c= ConsecutiveDelta(q,O1) by Th31,FUNCT_2:def 1;
consider u,v be Element of A, a9,b9 be Element of L such that
A11: q.O1 = [u,v,a9,b9] and
A12: d.(u,v) <= a9"\/"b9 by A8;
A13: Quadr(q,O1) = [u,v,a9,b9] by A7,A11,Def14;
then
A14: u = X & v = Y;
A15: a9 = a & b9 = b by A13;
d.(u,v) = d.[u,v] .= ConsecutiveDelta(q,O1).(X,Y) by A14,A10,GRFUNC_1:2;
then
new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) is u.t.i. by A4,A6,A9,A12
,A15,Th18,ORDINAL1:def 2;
then
A16: f.(x9,z9) <= f.(x9,y9) "\/" f.(y9,z9);
ConsecutiveDelta(q,succ O1) = new_bi_fun(BiFun(ConsecutiveDelta(q,O1)
, ConsecutiveSet(A,O1),L),Quadr(q,O1)) by Th27
.= new_bi_fun(ConsecutiveDelta(q,O1),Quadr(q,O1)) by Def15;
hence
ConsecutiveDelta(q,succ O1).(x,z) <= ConsecutiveDelta(q,succ O1).(x,y
) "\/" ConsecutiveDelta(q,succ O1).(y,z) by A16;
end;
A17: for O2 st O2 <> 0 & O2 is limit_ordinal & for O1 st O1 in O2 holds X[
O1] holds X[O2]
proof
deffunc U(Ordinal) = ConsecutiveDelta(q,$1);
let O2;
assume that
A18: O2 <> 0 & O2 is limit_ordinal and
A19: for O1 st O1 in O2 holds (O1 c= DistEsti(d) implies
ConsecutiveDelta(q,O1) is u.t.i.) and
A20: O2 c= DistEsti(d);
set CS = ConsecutiveSet(A,O2);
consider Ls being Sequence such that
A21: dom Ls = O2 & for O1 being Ordinal st O1 in O2 holds Ls.O1 = U(O1
) from ORDINAL2:sch 2;
ConsecutiveDelta(q,O2) = union rng Ls by A18,A21,Th28;
then reconsider f = union rng Ls as BiFunction of CS,L;
deffunc U(Ordinal) = ConsecutiveSet(A,$1);
consider Ts being Sequence such that
A22: dom Ts = O2 & for O1 being Ordinal st O1 in O2 holds Ts.O1 = U(O1
) from ORDINAL2:sch 2;
A23: ConsecutiveSet(A,O2) = union rng Ts by A18,A22,Th23;
f is u.t.i.
proof
let x,y,z be Element of CS;
consider X being set such that
A24: x in X and
A25: X in rng Ts by A23,TARSKI:def 4;
consider o1 being object such that
A26: o1 in dom Ts and
A27: X = Ts.o1 by A25,FUNCT_1:def 3;
consider Y being set such that
A28: y in Y and
A29: Y in rng Ts by A23,TARSKI:def 4;
consider o2 being object such that
A30: o2 in dom Ts and
A31: Y = Ts.o2 by A29,FUNCT_1:def 3;
consider Z being set such that
A32: z in Z and
A33: Z in rng Ts by A23,TARSKI:def 4;
consider o3 being object such that
A34: o3 in dom Ts and
A35: Z = Ts.o3 by A33,FUNCT_1:def 3;
reconsider o1,o2,o3 as Ordinal by A26,A30,A34;
A36: x in ConsecutiveSet(A,o1) by A22,A24,A26,A27;
A37: Ls.o3 = ConsecutiveDelta(q,o3) by A21,A22,A34;
then reconsider h3 = Ls.o3 as BiFunction of ConsecutiveSet(A,o3),L;
A38: h3 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet(A,o3);
o3 c= DistEsti(d) by A20,A22,A34,ORDINAL1:def 2;
then
A39: ConsecutiveDelta(q,o3) is u.t.i. by A19,A22,A34;
ConsecutiveDelta(q,o3) = h3 by A21,A22,A34;
hence h3.(x,z) <= h3.(x,y) "\/" h3.(y,z) by A39;
end;
A40: dom h3 = [:ConsecutiveSet(A,o3),ConsecutiveSet(A,o3):] by FUNCT_2:def 1;
A41: z in ConsecutiveSet(A,o3) by A22,A32,A34,A35;
A42: Ls.o2 = ConsecutiveDelta(q,o2) by A21,A22,A30;
then reconsider h2 = Ls.o2 as BiFunction of ConsecutiveSet(A,o2),L;
A43: h2 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet(A,o2);
o2 c= DistEsti(d) by A20,A22,A30,ORDINAL1:def 2;
then
A44: ConsecutiveDelta(q,o2) is u.t.i. by A19,A22,A30;
ConsecutiveDelta(q,o2) = h2 by A21,A22,A30;
hence h2.(x,z) <= h2.(x,y) "\/" h2.(y,z) by A44;
end;
A45: dom h2 = [:ConsecutiveSet(A,o2),ConsecutiveSet(A,o2):] by FUNCT_2:def 1;
A46: Ls.o1 = ConsecutiveDelta(q,o1) by A21,A22,A26;
then reconsider h1 = Ls.o1 as BiFunction of ConsecutiveSet(A,o1),L;
A47: h1 is u.t.i.
proof
let x,y,z be Element of ConsecutiveSet(A,o1);
o1 c= DistEsti(d) by A20,A22,A26,ORDINAL1:def 2;
then
A48: ConsecutiveDelta(q,o1) is u.t.i. by A19,A22,A26;
ConsecutiveDelta(q,o1) = h1 by A21,A22,A26;
hence h1.(x,z) <= h1.(x,y) "\/" h1.(y,z) by A48;
end;
A49: dom h1 = [:ConsecutiveSet(A,o1),ConsecutiveSet(A,o1):] by FUNCT_2:def 1;
A50: y in ConsecutiveSet(A,o2) by A22,A28,A30,A31;
per cases;
suppose
A51: o1 c= o3;
then
A52: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o3) by Th29;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose
A53: o2 c= o3;
reconsider z9 = z as Element of ConsecutiveSet(A,o3) by A22,A32,A34
,A35;
reconsider x9 = x as Element of ConsecutiveSet(A,o3) by A36,A52;
ConsecutiveDelta(q,o3) in rng Ls by A21,A22,A34,A37,FUNCT_1:def 3;
then
A54: h3 c= f by A37,ZFMISC_1:74;
A55: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o3) by A53,Th29;
then reconsider y9 = y as Element of ConsecutiveSet(A,o3) by A50;
[y,z] in dom h3 by A50,A41,A40,A55,ZFMISC_1:87;
then
A56: f.(y,z) = h3.(y9,z9) by A54,GRFUNC_1:2;
[x,z] in dom h3 by A36,A41,A40,A52,ZFMISC_1:87;
then
A57: f.(x,z) = h3.(x9,z9) by A54,GRFUNC_1:2;
[x,y] in dom h3 by A36,A50,A40,A52,A55,ZFMISC_1:87;
then f.(x,y) = h3.(x9,y9) by A54,GRFUNC_1:2;
hence thesis by A38,A56,A57;
end;
suppose
A58: o3 c= o2;
reconsider y9 = y as Element of ConsecutiveSet(A,o2) by A22,A28,A30
,A31;
ConsecutiveDelta(q,o2) in rng Ls by A21,A22,A30,A42,FUNCT_1:def 3;
then
A59: h2 c= f by A42,ZFMISC_1:74;
A60: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o2) by A58,Th29;
then reconsider z9 = z as Element of ConsecutiveSet(A,o2) by A41;
[y,z] in dom h2 by A50,A41,A45,A60,ZFMISC_1:87;
then
A61: f.(y,z) = h2.(y9,z9) by A59,GRFUNC_1:2;
ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o3) by A51,Th29;
then
A62: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by A60;
then reconsider x9 = x as Element of ConsecutiveSet(A,o2) by A36;
[x,y] in dom h2 by A36,A50,A45,A62,ZFMISC_1:87;
then
A63: f.(x,y) = h2.(x9,y9) by A59,GRFUNC_1:2;
[x,z] in dom h2 by A36,A41,A45,A60,A62,ZFMISC_1:87;
then f.(x,z) = h2.(x9,z9) by A59,GRFUNC_1:2;
hence thesis by A43,A63,A61;
end;
end;
end;
suppose
A64: o3 c= o1;
then
A65: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o1) by Th29;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose
A66: o1 c= o2;
reconsider y9 = y as Element of ConsecutiveSet(A,o2) by A22,A28,A30
,A31;
ConsecutiveDelta(q,o2) in rng Ls by A21,A22,A30,A42,FUNCT_1:def 3;
then
A67: h2 c= f by A42,ZFMISC_1:74;
A68: ConsecutiveSet(A,o1) c= ConsecutiveSet(A,o2) by A66,Th29;
then reconsider x9 = x as Element of ConsecutiveSet(A,o2) by A36;
[x,y] in dom h2 by A36,A50,A45,A68,ZFMISC_1:87;
then
A69: f.(x,y) = h2.(x9,y9) by A67,GRFUNC_1:2;
ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o1) by A64,Th29;
then
A70: ConsecutiveSet(A,o3) c= ConsecutiveSet(A,o2) by A68;
then reconsider z9 = z as Element of ConsecutiveSet(A,o2) by A41;
[y,z] in dom h2 by A50,A41,A45,A70,ZFMISC_1:87;
then
A71: f.(y,z) = h2.(y9,z9) by A67,GRFUNC_1:2;
[x,z] in dom h2 by A36,A41,A45,A68,A70,ZFMISC_1:87;
then f.(x,z) = h2.(x9,z9) by A67,GRFUNC_1:2;
hence thesis by A43,A69,A71;
end;
suppose
A72: o2 c= o1;
reconsider x9 = x as Element of ConsecutiveSet(A,o1) by A22,A24,A26
,A27;
reconsider z9 = z as Element of ConsecutiveSet(A,o1) by A41,A65;
ConsecutiveDelta(q,o1) in rng Ls by A21,A22,A26,A46,FUNCT_1:def 3;
then
A73: h1 c= f by A46,ZFMISC_1:74;
A74: ConsecutiveSet(A,o2) c= ConsecutiveSet(A,o1) by A72,Th29;
then reconsider y9 = y as Element of ConsecutiveSet(A,o1) by A50;
[x,y] in dom h1 by A36,A50,A49,A74,ZFMISC_1:87;
then
A75: f.(x,y) = h1.(x9,y9) by A73,GRFUNC_1:2;
[x,z] in dom h1 by A36,A41,A49,A65,ZFMISC_1:87;
then
A76: f.(x,z) = h1.(x9,z9) by A73,GRFUNC_1:2;
[y,z] in dom h1 by A50,A41,A49,A65,A74,ZFMISC_1:87;
then f.(y,z) = h1.(y9,z9) by A73,GRFUNC_1:2;
hence thesis by A47,A75,A76;
end;
end;
end;
end;
hence thesis by A18,A21,Th28;
end;
A77: X[0]
proof
assume 0 c= DistEsti(d);
let x,y,z be Element of ConsecutiveSet(A,0);
reconsider x9 = x, y9 = y, z9 = z as Element of A by Th21;
ConsecutiveDelta(q,0) = d & d.(x9,z9) <= d.(x9,y9) "\/" d.(y9,z9) by A2
,Th26;
hence ConsecutiveDelta(q,0).(x,z) <= ConsecutiveDelta(q,0).(x,y) "\/"
ConsecutiveDelta(q,0).(y,z);
end;
for O holds X[O] from ORDINAL2:sch 1(A77,A3,A17);
hence thesis;
end;
theorem
for d being distance_function of A,L for q being QuadrSeq of d st O c=
DistEsti(d) holds ConsecutiveDelta(q,O) is distance_function of ConsecutiveSet(
A,O),L by Th33,Th34,Th35;
definition
let A,L;
let d be BiFunction of A,L;
func NextSet(d) -> set equals
ConsecutiveSet(A,DistEsti(d));
correctness;
end;
registration
let A,L;
let d be BiFunction of A,L;
cluster NextSet(d) -> non empty;
coherence;
end;
definition
let A,L;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
func NextDelta(q) -> set equals
ConsecutiveDelta(q,DistEsti(d));
correctness;
end;
definition
let A,L;
let d be distance_function of A,L;
let q be QuadrSeq of d;
redefine func NextDelta(q) -> distance_function of NextSet(d),L; :: redefines NextDelta (LATTICE5, definition)
coherence by Th33,Th34,Th35;
end;
definition
let A,L;
let d be distance_function of A,L;
let Aq be non empty set, dq be distance_function of Aq,L;
pred Aq, dq is_extension_of A,d means
ex q being QuadrSeq of d st Aq = NextSet(d) & dq = NextDelta(q);
end;
theorem Th37:
for d be distance_function of A,L for Aq be non empty set, dq be
distance_function of Aq,L st Aq, dq is_extension_of A,d for x,y being Element
of A, a,b being Element of L st d.(x,y) <= a "\/" b ex z1,z2,z3 being Element
of Aq st dq.(x,z1) = a & dq.(z2,z3) = a & dq.(z1,z2) = b & dq.(z3,y) = b
proof
let d be distance_function of A,L;
let Aq be non empty set, dq be distance_function of Aq,L;
assume Aq, dq is_extension_of A,d;
then consider q being QuadrSeq of d such that
A1: Aq = NextSet(d) and
A2: dq = NextDelta(q);
let x,y be Element of A;
let a,b be Element of L;
assume
A3: d.(x,y) <= a "\/" b;
rng q = {[x9,y9,a9,b9] where x9 is Element of A, y9 is Element of A, a9
is Element of L, b9 is Element of L: d.(x9,y9) <= a9"\/"b9} by Def13;
then [x,y,a,b] in rng q by A3;
then consider o being object such that
A4: o in dom q and
A5: q.o = [x,y,a,b] by FUNCT_1:def 3;
reconsider o as Ordinal by A4;
A6: q.o = Quadr(q,o) by A4,Def14;
then
A7: x = Quadr(q,o)`1_4 by A5;
A8: b = Quadr(q,o)`4_4 by A5,A6;
A9: y = Quadr(q,o)`2_4 by A5,A6;
A10: a = Quadr(q,o)`3_4 by A5,A6;
reconsider B = ConsecutiveSet(A,o) as non empty set;
{B} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:def 1;
then
A11: {B} in B \/ {{B}, {{B}}, {{{B}}} } by XBOOLE_0:def 3;
reconsider cd = ConsecutiveDelta(q,o) as BiFunction of B,L;
reconsider Q = Quadr(q,o) as Element of [:B,B,the carrier of L,the carrier
of L:];
A12: {{B}} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:def 1;
then
A13: {{B}} in new_set B by XBOOLE_0:def 3;
A c= B by Th24;
then reconsider xo = x, yo = y as Element of B;
A14: B c= new_set B by XBOOLE_1:7;
reconsider x1 = xo, y1 = yo as Element of new_set B by A14;
A15: cd is zeroed by Th33;
A16: {{{B}}} in {{B}, {{B}}, {{{B}}} } by ENUMSET1:def 1;
then
A17: {{{B}}} in new_set B by XBOOLE_0:def 3;
o in DistEsti(d) by A4,Th25;
then
A18: succ o c= DistEsti(d) by ORDINAL1:21;
then
A19: ConsecutiveDelta(q,succ o) c= ConsecutiveDelta(q,DistEsti(d)) by Th32;
ConsecutiveSet(A,succ o) = new_set B by Th22;
then new_set B c= ConsecutiveSet(A,DistEsti(d)) by A18,Th29;
then reconsider
z1={B},z2={{B}},z3={{{B}}} as Element of Aq by A1,A11,A13,A17;
take z1,z2,z3;
A20: ConsecutiveDelta(q,succ o) = new_bi_fun(BiFun(ConsecutiveDelta(q,o),
ConsecutiveSet(A,o),L),Quadr(q,o)) by Th27
.= new_bi_fun(cd,Q) by Def15;
A21: dom new_bi_fun(cd,Q) = [:new_set B,new_set B:] by FUNCT_2:def 1;
then [x1,{B}] in dom new_bi_fun(cd,Q) by A11,ZFMISC_1:87;
hence dq.(x,z1) = new_bi_fun(cd,Q).(x1,{B}) by A2,A19,A20,GRFUNC_1:2
.= cd.(xo,xo)"\/"a by A7,A10,Def10
.= Bottom L"\/" a by A15
.= a by WAYBEL_1:3;
{{B}} in B \/ {{B}, {{B}}, {{{B}}} } by A12,XBOOLE_0:def 3;
then [{{B}},{{{B}}}] in dom new_bi_fun(cd,Q) by A17,A21,ZFMISC_1:87;
hence dq.(z2,z3) = new_bi_fun(cd,Q).({{B}},{{{B}}}) by A2,A19,A20,GRFUNC_1:2
.= a by A10,Def10;
[{B},{{B}}] in dom new_bi_fun(cd,Q) by A11,A13,A21,ZFMISC_1:87;
hence dq.(z1,z2) = new_bi_fun(cd,Q).({B},{{B}}) by A2,A19,A20,GRFUNC_1:2
.= b by A8,Def10;
{{{B}}} in B \/ {{B}, {{B}}, {{{B}}} } by A16,XBOOLE_0:def 3;
then [{{{B}}},y1] in dom new_bi_fun(cd,Q) by A21,ZFMISC_1:87;
hence dq.(z3,y) = new_bi_fun(cd,Q).({{{B}}},y1) by A2,A19,A20,GRFUNC_1:2
.= cd.(yo,yo)"\/"b by A9,A8,Def10
.= Bottom L"\/" b by A15
.= b by WAYBEL_1:3;
end;
definition
let A,L;
let d be distance_function of A,L;
mode ExtensionSeq of A,d -> Function means
:Def20:
dom it = NAT & it.0 = [A,
d] & for n being Nat holds ex A9 being non empty set, d9 being
distance_function of A9,L, Aq being non empty set, dq being distance_function
of Aq,L st Aq, dq is_extension_of A9,d9 & it.n = [A9,d9] & it.(n+1) = [Aq,dq];
existence
proof
defpred P[set,set,set] means (ex A9 being non empty set, d9 being
distance_function of A9,L, Aq being non empty set, dq being distance_function
of Aq,L st Aq, dq is_extension_of A9,d9 & $2 = [A9,d9] & $3 = [Aq,dq]) or $3= 0
& not ex A9 being non empty set, d9 being distance_function of A9,L, Aq being
non empty set, dq being distance_function of Aq,L st Aq, dq is_extension_of A9,
d9 & $2 = [A9,d9];
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 A9 being non empty set, d9 being distance_function of A9,L,
Aq being non empty set, dq being distance_function of Aq,L st Aq, dq
is_extension_of A9,d9 & x = [A9,d9];
then consider
A9 being non empty set, d9 being distance_function of A9,L,
Aq being non empty set, dq being distance_function of Aq,L such that
A2: Aq, dq is_extension_of A9,d9 & x = [A9,d9];
take [Aq,dq];
thus thesis by A2;
end;
suppose
A3: not ex A9 being non empty set, d9 being distance_function of
A9,L, Aq being non empty set, dq being distance_function of Aq,L st Aq, dq
is_extension_of A9,d9 & x = [A9,d9];
take 0;
thus thesis by A3;
end;
end;
consider f being Function such that
A4: dom f = NAT and
A5: f.0 = [A,d] and
A6: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:
sch 1( A1);
take f;
thus dom f = NAT by A4;
thus f.0 = [A,d] by A5;
defpred X[Nat] means ex A9 being non empty set, d9 being
distance_function of A9,L, Aq being non empty set, dq being distance_function
of Aq,L st Aq, dq is_extension_of A9,d9 & f.$1 = [A9,d9] & f.($1+1) = [Aq,dq];
A7: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
given A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L such that
Aq, dq is_extension_of A9,d9 and
f.k = [A9,d9] and
A8: f.(k+1) = [Aq,dq];
ex A1 being non empty set, d1 being distance_function of A1,L, AQ
being non empty set, DQ being distance_function of AQ,L st AQ, DQ
is_extension_of A1,d1 & f.(k+1) = [A1,d1]
proof
set Q = the QuadrSeq of dq;
set AQ = NextSet(dq);
take Aq,dq;
set DQ = NextDelta(Q);
take AQ,DQ;
thus AQ, DQ is_extension_of Aq,dq;
thus thesis by A8;
end;
hence thesis by A6;
end;
ex A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L st Aq, dq
is_extension_of A9,d9 & f.0 = [A9,d9]
proof
set Aq = NextSet(d);
set q = the QuadrSeq of d;
take A,d;
consider dq being distance_function of Aq,L such that
A9: dq = NextDelta(q);
take Aq,dq;
thus Aq, dq is_extension_of A,d by A9;
thus thesis by A5;
end;
then
A10: X[ 0 ] by A6;
thus for k being Nat holds X[k] from NAT_1:sch 2(A10, A7);
end;
end;
theorem Th38:
for d be distance_function of A,L for S being ExtensionSeq of A,
d for k,l being Nat st k <= l holds (S.k)`1 c= (S.l)`1
proof
let d be distance_function of A,L;
let S be ExtensionSeq of A,d;
let k be Nat;
defpred X[Nat] means k <= $1 implies (S.k)`1 c= (S.$1)`1;
A1: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat;
assume that
A2: k <= i implies (S.k)`1 c= (S.i)`1 and
A3: k <= i+1;
per cases by A3,NAT_1:8;
suppose
k = i+1;
hence thesis;
end;
suppose
A4: k <= i;
consider A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L such that
A5: Aq, dq is_extension_of A9,d9 and
A6: S.i = [A9,d9] and
A7: S.(i+1) = [Aq,dq] by Def20;
A8: (S.i)`1 c= ConsecutiveSet(A9,DistEsti(d9)) by Th24,A6;
ex q being QuadrSeq of d9 st Aq = NextSet(d9) & dq = NextDelta(q)
by A5;
then (S.(i+1))`1 = ConsecutiveSet(A9,DistEsti(d9)) by A7;
hence thesis by A2,A4,A8;
end;
end;
A9: X[ 0 ] by NAT_1:3;
thus for l being Nat holds X[l] from NAT_1:sch 2(A9, A1);
end;
theorem Th39:
for d be distance_function of A,L for S being ExtensionSeq of A,
d for k,l being Nat st k <= l holds (S.k)`2 c= (S.l)`2
proof
let d be distance_function of A,L;
let S be ExtensionSeq of A,d;
let k be Nat;
defpred X[Nat] means k <= $1 implies (S.k)`2 c= (S.$1)`2;
A1: for i being Nat st X[i] holds X[i+1]
proof
let i be Nat;
assume that
A2: k <= i implies (S.k)`2 c= (S.i)`2 and
A3: k <= i+1;
per cases by A3,NAT_1:8;
suppose
k = i+1;
hence thesis;
end;
suppose
A4: k <= i;
consider A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L such that
A5: Aq, dq is_extension_of A9,d9 and
A6: S.i = [A9,d9] and
A7: S.(i+1) = [Aq,dq] by Def20;
consider q being QuadrSeq of d9 such that
Aq = NextSet(d9) and
A8: dq = NextDelta(q) by A5;
A9: (S.i)`2 c= ConsecutiveDelta(q,DistEsti(d9)) by Th31,A6;
(S.(i+1))`2 = ConsecutiveDelta(q,DistEsti(d9)) by A7,A8;
hence thesis by A2,A4,A9;
end;
end;
A10: X[ 0 ] by NAT_1:3;
thus for l being Nat holds X[l] from NAT_1:sch 2(A10, A1);
end;
definition
let L;
func BasicDF(L) -> distance_function of the carrier of L,L means
:Def21:
for x,y being Element of L holds (x <> y implies it.(x,y) = x"\/"y) & (x = y
implies it.(x,y) = Bottom L);
existence
proof
defpred X[Element of L,Element of L,set] means ($1 = $2 implies $3 =
Bottom L) & ($1 <> $2 implies $3 = $1"\/"$2);
set A = the carrier of L;
A1: for x,y being Element of L ex z being Element of L st X[x,y,z]
proof
let x,y be Element of L;
per cases;
suppose
A2: x = y;
take Bottom L;
thus thesis by A2;
end;
suppose
A3: x <> y;
take x"\/"y;
thus thesis by A3;
end;
end;
consider f being Function of [:the carrier of L,the carrier of L:],the
carrier of L such that
A4: for x,y being Element of L holds X[x,y,f.(x,y)] from BINOP_1:sch 3
(A1 );
reconsider f as BiFunction of A,L;
A5: f is zeroed
by A4;
A6: f is u.t.i.
proof
let x,y,z be Element of A;
reconsider x9 = x, y9 = y, z9 = z as Element of L;
per cases;
suppose
A7: x = z;
f.(x,y) "\/" f.(y,z) >= Bottom L by YELLOW_0:44;
hence thesis by A4,A7;
end;
suppose
A8: x <> z;
thus f.(x,y) "\/" f.(y,z) >= f.(x,z)
proof
per cases;
suppose
A9: x = y;
x9 "\/" z9 >= x9 "\/" z9 by ORDERS_2:1;
then f.(x,z) >= x9 "\/" z9 by A4,A8;
then Bottom L "\/" f.(x,z) >= x9 "\/" z9 by WAYBEL_1:3;
then f.(x,y) "\/" f.(y,z) >= x9 "\/" z9 by A4,A9;
hence thesis by A4,A8;
end;
suppose
A10: x <> y;
(x9 "\/" y9) "\/" f.(y,z) >= x9 "\/" z9
proof
per cases;
suppose
A11: y = z;
(x9 "\/" y9) >= x9 "\/" y9 by ORDERS_2:1;
then Bottom L "\/" (x9 "\/" y9) >= x9 "\/" z9 by A11,WAYBEL_1:3
;
hence thesis by A4,A11;
end;
suppose
A12: y <> z;
(x9 "\/" z9) "\/" y9 = (x9 "\/" z9) "\/" (y9 "\/" y9) by
YELLOW_5:1
.= x9 "\/" (z9 "\/" (y9 "\/" y9)) by LATTICE3:14
.= x9 "\/" (y9 "\/" (y9 "\/" z9)) by LATTICE3:14
.= (x9 "\/" y9) "\/" (y9 "\/" z9) by LATTICE3:14;
then (x9 "\/" y9) "\/" (y9 "\/" z9) >= x9 "\/" z9 by
YELLOW_0:22;
hence thesis by A4,A12;
end;
end;
then f.(x,y) "\/" f.(y,z) >= x9 "\/" z9 by A4,A10;
hence thesis by A4,A8;
end;
end;
end;
end;
f is symmetric
proof
let x,y be Element of A;
reconsider x9 = x, y9 = y as Element of L;
per cases;
suppose
x = y;
hence thesis;
end;
suppose
A13: x <> y;
hence f.(x,y) = y9 "\/" x9 by A4
.= f.(y,x) by A4,A13;
end;
end;
then reconsider f as distance_function of A,L by A5,A6;
take f;
thus thesis by A4;
end;
uniqueness
proof
let f1,f2 be distance_function of the carrier of L,L such that
A14: for x,y being Element of L holds (x <> y implies f1.(x,y) = x"\/"
y) & (x = y implies f1.(x,y) = Bottom L) and
A15: for x,y being Element of L holds (x <> y implies f2.(x,y) = x"\/"
y) & (x = y implies f2.(x,y) = Bottom L);
A16: for z being object st z in dom f1 holds f1.z = f2.z
proof
let z be object;
assume
A17: z in dom f1;
then consider x,y being object such that
A18: z = [x,y] by RELAT_1:def 1;
reconsider x,y as Element of L by A17,A18,ZFMISC_1:87;
per cases;
suppose
A19: x = y;
thus f1.z = f1.(x,y) by A18
.= Bottom L by A14,A19
.= f2.(x,y) by A15,A19
.= f2.z by A18;
end;
suppose
A20: x <> y;
thus f1.z = f1.(x,y) by A18
.= x"\/"y by A14,A20
.= f2.(x,y) by A15,A20
.= f2.z by A18;
end;
end;
dom f1 = [:the carrier of L,the carrier of L:] by FUNCT_2:def 1
.= dom f2 by FUNCT_2:def 1;
hence f1 = f2 by A16,FUNCT_1:2;
end;
end;
theorem Th40:
BasicDF(L) is onto
proof
set X = the carrier of L, f = BasicDF(L);
for w being object st w in X ex z being object st z in [:X,X:] & w = f.z
proof
let w be object;
assume
A1: w in X;
then reconsider w9 = w as Element of L;
reconsider w99 = w as Element of L by A1;
per cases;
suppose
A2: w = Bottom L;
reconsider z = [w,w] as set;
take z;
thus z in [:X,X:] by A1,ZFMISC_1:87;
thus f.z = f.(w9,w9) .= w by A2,Def21;
end;
suppose
A3: w <> Bottom L;
reconsider z = [Bottom L,w] as set;
take z;
thus z in [:X,X:] by A1,ZFMISC_1:87;
thus f.z = f.(Bottom L,w9) .= Bottom L "\/" w99 by A3,Def21
.= w by WAYBEL_1:3;
end;
end;
then rng f = the carrier of L by FUNCT_2:10;
hence thesis by FUNCT_2:def 3;
end;
Lm2: now
let j be Nat;
assume that
A1: 1 <= j and
A2: j < 5;
j < 4+1 by A2;
then j <= 4 by NAT_1:13;
then j = 0 or ... or j = 4 by NAT_1:60;
hence j = 1 or ... or j = 4 by A1;
end;
Lm3: now
let m be Element of NAT;
assume
A1: m in Seg 5;
then m <= 5 by FINSEQ_1:1;
then m = 0 or ... or m = 5 by NAT_1:60;
hence m = 1 or ... or m = 5 by A1,FINSEQ_1:1;
end;
Lm4: now
let A,L;
let d be distance_function of A,L;
succ {} c= DistEsti(d) or DistEsti(d) in succ {} by ORDINAL1:16;
then succ {} c= DistEsti(d) or DistEsti(d) c= {} by ORDINAL1:22;
hence succ {} c= DistEsti(d) by Th20,XBOOLE_1:3;
end;
theorem Th41:
for S being ExtensionSeq of the carrier of L, BasicDF(L) for FS
being non empty set st FS = union the set of all
(S.i)`1 where i is Element of NAT holds union the set of all
(S.i)`2 where i is Element of NAT is distance_function of FS,L
proof
let S be ExtensionSeq of the carrier of L, BasicDF(L);
let FS be non empty set;
assume
A1: FS = union the set of all (S.i)`1 where i is Element of NAT;
reconsider FS as non empty set;
set A = the carrier of L;
set FD = union the set of all (S.i)`2 where i is Element of NAT;
now
let x,y be set;
assume that
A2: x in the set of all (S.i)`2 where i is Element of NAT and
A3: y in the set of all (S.i)`2 where i is Element of NAT;
consider k being Element of NAT such that
A4: x = (S.k)`2 by A2;
consider l being Element of NAT such that
A5: y = (S.l)`2 by A3;
k <= l or l <= k;
then x c= y or y c= x by A4,A5,Th39;
hence x,y are_c=-comparable;
end;
then
A6: the set of all (S.i)`2 where i is Element of NAT is c=-linear;
the set of all (S.i)`2 where i is Element of NAT c= PFuncs([:FS,
FS:],A)
proof
let z be object;
assume z in the set of all (S.i)`2 where i is Element of NAT;
then consider j being Element of NAT such that
A7: z = (S.j)`2;
consider A9 being non empty set, d9 being distance_function of A9,L, Aq
being non empty set, dq being distance_function of Aq,L such that
Aq, dq is_extension_of A9,d9 and
A8: S.j = [A9,d9] and
S.(j+1) = [Aq,dq] by Def20;
A9 = [A9,d9]`1;
then A9 in the set of all (S.i)`1 where i is Element of NAT
by A8;
then dom d9 = [:A9,A9:] & A9 c= FS by A1,FUNCT_2:def 1,ZFMISC_1:74;
then
A9: rng d9 c= A & dom d9 c= [:FS,FS:] by ZFMISC_1:96;
z = d9 by A7,A8;
hence thesis by A9,PARTFUN1:def 3;
end;
then FD in PFuncs([:FS,FS:],A) by A6,TREES_2:40;
then
A10: ex g being Function st FD = g & dom g c= [:FS,FS:] & rng g c= A by
PARTFUN1:def 3;
(S.0)`1 in the set of all (S.i)`1 where i is Element of NAT;
then reconsider
X = the set of all (S.i)`1 where i is Element of NAT as
non empty set;
set LL = { [:I,I:] where I is Element of X : I in X },
PP = the set of all [:(S.i)`1,(S.i
)`1:] where i is Element of NAT;
defpred X[object,object] means $2 = (S.$1)`2;
A11: LL = PP
proof
thus LL c= PP
proof
let x be object;
assume x in LL;
then consider J being Element of X such that
A12: x = [:J,J:] and
A13: J in X;
ex j being Element of NAT st J = (S.j)`1 by A13;
hence thesis by A12;
end;
let x be object;
assume x in PP;
then consider j being Element of NAT such that
A14: x = [:(S.j)`1,(S.j)`1:];
(S.j)`1 in X;
hence thesis by A14;
end;
reconsider FD as Function by A10;
A15: for x being object st x in NAT ex y being object st X[x,y];
consider F being Function such that
A16: dom F = NAT and
A17: for x being object st x in NAT holds X[x,F.x] from CLASSES1:sch 1(A15);
A18: rng F = the set of all (S.i)`2 where i is Element of NAT
proof
thus rng F c= the set of all (S.i)`2 where i is Element of NAT
proof
let x be object;
assume x in rng F;
then consider j being object such that
A19: j in dom F and
A20: F.j = x by FUNCT_1:def 3;
reconsider j as Element of NAT by A16,A19;
x = (S.j)`2 by A17,A20;
hence thesis;
end;
let x be object;
assume x in the set of all (S.i)`2 where i is Element of NAT;
then consider j being Element of NAT such that
A21: x = (S.j)`2;
x = F.j by A17,A21;
hence thesis by A16,FUNCT_1:def 3;
end;
F is Function-yielding
proof
let x be object;
assume x in dom F;
then reconsider j = x as Element of NAT by A16;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension_of A1,d1 and
A22: S.j = [A1,d1] and
S.(j+1) = [Aq1,dq1] by Def20;
[A1,d1]`2 = d1;
hence thesis by A17,A22;
end;
then reconsider F as Function-yielding Function;
A23: rng doms F = PP
proof
thus rng doms F c= PP
proof
let x be object;
assume x in rng doms F;
then consider j being object such that
A24: j in dom doms F and
A25: x = (doms F).j by FUNCT_1:def 3;
A26: j in dom F by A24,FUNCT_6:59;
reconsider j as Element of NAT by A16,A24,FUNCT_6:59;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension_of A1,d1 and
A27: S.j = [A1,d1] and
S.(j+1) = [Aq1,dq1] by Def20;
A28: [A1,d1]`2 = d1;
x = dom (F.j) by A25,A26,FUNCT_6:22
.= dom d1 by A17,A28,A27
.= [:(S.j)`1,(S.j)`1:] by A27,FUNCT_2:def 1;
hence thesis;
end;
let x be object;
assume x in PP;
then consider j being Element of NAT such that
A29: x = [:(S.j)`1,(S.j)`1:];
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension_of A1,d1 and
A30: S.j = [A1,d1] and
S.(j+1) = [Aq1,dq1] by Def20;
A31: [A1,d1]`2 = d1;
j in NAT;
then
A32: j in dom doms F by A16,FUNCT_6:59;
x = dom d1 by A29,A30,FUNCT_2:def 1
.= dom (F.j) by A17,A31,A30
.= (doms F).j by A16,FUNCT_6:22;
hence thesis by A32,FUNCT_1:def 3;
end;
now
let x,y be set;
assume that
A33: x in X and
A34: y in X;
consider k being Element of NAT such that
A35: x = (S.k)`1 by A33;
consider l being Element of NAT such that
A36: y = (S.l)`1 by A34;
k <= l or l <= k;
then x c= y or y c= x by A35,A36,Th38;
hence x,y are_c=-comparable;
end;
then X is c=-linear;
then [:FS,FS:] = union rng doms F by A1,A23,A11,Th3
.= dom FD by A18,Th1;
then reconsider FD as BiFunction of FS,L by A10,FUNCT_2:def 1,RELSET_1:4;
A37: FD is symmetric
proof
let x,y be Element of FS;
consider x1 being set such that
A38: x in x1 and
A39: x1 in X by A1,TARSKI:def 4;
consider k being Element of NAT such that
A40: x1 = (S.k)`1 by A39;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension_of A1,d1 and
A41: S.k = [A1,d1] and
S.(k+1) = [Aq1,dq1] by Def20;
A42: [A1,d1]`1 = A1;
A43: x in A1 by A38,A40,A41;
[A1,d1]`2 = d1;
then d1 in the set of all (S.i)`2 where i is Element of NAT
by A41;
then
A44: d1 c= FD by ZFMISC_1:74;
consider y1 being set such that
A45: y in y1 and
A46: y1 in X by A1,TARSKI:def 4;
consider l being Element of NAT such that
A47: y1 = (S.l)`1 by A46;
consider A2 being non empty set, d2 being distance_function of A2,L, Aq2
being non empty set, dq2 being distance_function of Aq2,L such that
Aq2, dq2 is_extension_of A2,d2 and
A48: S.l = [A2,d2] and
S.(l+1) = [Aq2,dq2] by Def20;
A49: [A2,d2]`1 = A2;
A50: y in A2 by A45,A47,A48;
[A2,d2]`2 = d2;
then d2 in the set of all (S.i)`2 where i is Element of NAT
by A48;
then
A51: d2 c= FD by ZFMISC_1:74;
per cases;
suppose
k <= l;
then A1 c= A2 by A42,A49,Th38,A41,A48;
then reconsider x9=x,y9=y as Element of A2
by A43,A50;
A52: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
hence FD.(x,y) = d2.[x9,y9] by A51,GRFUNC_1:2
.= d2.(x9,y9)
.= d2.(y9,x9) by Def5
.= FD.[y9,x9] by A51,A52,GRFUNC_1:2
.= FD.(y,x);
end;
suppose
l <= k;
then A2 c= A1 by A42,A49,Th38,A48,A41;
then reconsider x9=x,y9=y as Element of A1 by A38,A40,A41,A50;
A53: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD.(x,y) = d1.[x9,y9] by A44,GRFUNC_1:2
.= d1.(x9,y9)
.= d1.(y9,x9) by Def5
.= FD.[y9,x9] by A44,A53,GRFUNC_1:2
.= FD.(y,x);
end;
end;
A54: FD is u.t.i.
proof
let x,y,z be Element of FS;
consider x1 being set such that
A55: x in x1 and
A56: x1 in X by A1,TARSKI:def 4;
consider k being Element of NAT such that
A57: x1 = (S.k)`1 by A56;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension_of A1,d1 and
A58: S.k = [A1,d1] and
S.(k+1) = [Aq1,dq1] by Def20;
A59: x in A1 by A55,A57,A58;
[A1,d1]`2 = d1;
then d1 in the set of all (S.i)`2 where i is Element of NAT
by A58;
then
A60: d1 c= FD by ZFMISC_1:74;
A61: dom d1 = [:A1,A1:] by FUNCT_2:def 1;
A62: (S.k)`1 = A1 by A58;
consider y1 being set such that
A63: y in y1 and
A64: y1 in X by A1,TARSKI:def 4;
consider l being Element of NAT such that
A65: y1 = (S.l)`1 by A64;
consider A2 being non empty set, d2 being distance_function of A2,L, Aq2
being non empty set, dq2 being distance_function of Aq2,L such that
Aq2, dq2 is_extension_of A2,d2 and
A66: S.l = [A2,d2] and
S.(l+1) = [Aq2,dq2] by Def20;
A67: y in A2 by A63,A65,A66;
[A2,d2]`2 = d2;
then d2 in the set of all (S.i)`2 where i is Element of NAT
by A66;
then
A68: d2 c= FD by ZFMISC_1:74;
A69: dom d2 = [:A2,A2:] by FUNCT_2:def 1;
A70: [A2,d2]`1 = A2;
consider z1 being set such that
A71: z in z1 and
A72: z1 in X by A1,TARSKI:def 4;
consider n being Element of NAT such that
A73: z1 = (S.n)`1 by A72;
consider A3 being non empty set, d3 being distance_function of A3,L, Aq3
being non empty set, dq3 being distance_function of Aq3,L such that
Aq3, dq3 is_extension_of A3,d3 and
A74: S.n = [A3,d3] and
S.(n+1) = [Aq3,dq3] by Def20;
A75: [A3,d3]`1 = A3;
A76: z in A3 by A71,A73,A74;
[A3,d3]`2 = d3;
then d3 in the set of all (S.i)`2 where i is Element of NAT
by A74;
then
A77: d3 c= FD by ZFMISC_1:74;
A78: dom d3 = [:A3,A3:] by FUNCT_2:def 1;
per cases;
suppose
k <= l;
then
A79: A1 c= A2 by A62,A70,Th38,A66;
thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z)
proof
per cases;
suppose
l <= n;
then
A80: A2 c= A3 by A70,A75,Th38,A74,A66;
then
A1 c= A3 by A79;
then reconsider x9 = x, y9 = y as Element of A3 by A59,A67,A80;
reconsider z9 = z as Element of A3 by A76;
A81: FD.(y,z) = d3.[y9,z9] by A77,A78,GRFUNC_1:2
.= d3.(y9,z9);
A82: FD.(x,z) = d3.[x9,z9] by A77,A78,GRFUNC_1:2
.= d3.(x9,z9);
FD.(x,y) = d3.[x9,y9] by A77,A78,GRFUNC_1:2
.= d3.(x9,y9);
hence thesis by A81,A82,Def7;
end;
suppose
n <= l;
then
A83: A3 c= A2 by A70,A75,Th38,A74,A66;
reconsider y9 = y as Element of A2 by A67;
reconsider x9 = x as Element of A2 by A59,A79;
reconsider z9 = z as Element of A2 by A76,A83;
A84: FD.(y,z) = d2.[y9,z9] by A68,A69,GRFUNC_1:2
.= d2.(y9,z9);
A85: FD.(x,z) = d2.[x9,z9] by A68,A69,GRFUNC_1:2
.= d2.(x9,z9);
FD.(x,y) = d2.[x9,y9] by A68,A69,GRFUNC_1:2
.= d2.(x9,y9);
hence thesis by A84,A85,Def7;
end;
end;
end;
suppose
l <= k;
then
A86: A2 c= A1 by A62,A70,Th38,A66;
thus FD.(x,y) "\/" FD.(y,z) >= FD.(x,z)
proof
per cases;
suppose
k <= n;
then
A87: A1 c= A3 by A62,A75,Th38,A74;
then
A88: A2 c= A3 by A86;
reconsider x9 = x as Element of A3 by A59,A87;
reconsider z9 = z as Element of A3 by A71,A73,A74;
reconsider y9 = y as Element of A3 by A67,A88;
A89: FD.(y,z) = d3.[y9,z9] by A77,A78,GRFUNC_1:2
.= d3.(y9,z9);
A90: FD.(x,z) = d3.[x9,z9] by A77,A78,GRFUNC_1:2
.= d3.(x9,z9);
FD.(x,y) = d3.[x9,y9] by A77,A78,GRFUNC_1:2
.= d3.(x9,y9);
hence thesis by A89,A90,Def7;
end;
suppose
n <= k;
then A3 c= A1 by A62,A75,Th38,A74;
then reconsider
x9 = x, y9 = y, z9 = z as Element of A1
by A55,A57,A58,A67,A76,A86;
A91: FD.(y,z) = d1.[y9,z9] by A60,A61,GRFUNC_1:2
.= d1.(y9,z9);
A92: FD.(x,z) = d1.[x9,z9] by A60,A61,GRFUNC_1:2
.= d1.(x9,z9);
FD.(x,y) = d1.[x9,y9] by A60,A61,GRFUNC_1:2
.= d1.(x9,y9);
hence thesis by A91,A92,Def7;
end;
end;
end;
end;
FD is zeroed
proof
let x be Element of FS;
consider y being set such that
A93: x in y and
A94: y in X by A1,TARSKI:def 4;
consider j being Element of NAT such that
A95: y = (S.j)`1 by A94;
consider A1 being non empty set, d1 being distance_function of A1,L, Aq1
being non empty set, dq1 being distance_function of Aq1,L such that
Aq1, dq1 is_extension_of A1,d1 and
A96: S.j = [A1,d1] and
S.(j+1) = [Aq1,dq1] by Def20;
reconsider x9 = x as Element of A1 by A93,A95,A96;
[A1,d1]`2 = d1;
then d1 in the set of all (S.i)`2 where i is Element of NAT
by A96;
then
A97: d1 c= FD by ZFMISC_1:74;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
hence FD.(x,x) = d1.[x9,x9] by A97,GRFUNC_1:2
.= d1.(x9,x9)
.=Bottom L by Def6;
end;
hence thesis by A37,A54;
end;
theorem Th42:
for S being ExtensionSeq of the carrier of L, BasicDF(L) for FS
being non empty set, FD being distance_function of FS,L for x,y being Element
of FS for a,b being Element of L
st FS = union the set of all (S.i)`1 where i is Element of
NAT &
FD = union the set of all (S.i)`2 where i is Element of NAT
& FD.(x,y) <= a"\/"b ex z1,z2,z3 being Element of FS st FD.(x,z1
) = a & FD.(z2,z3) = a & FD.(z1,z2) = b & FD.(z3,y) = b
proof
let S be ExtensionSeq of the carrier of L, BasicDF(L);
let FS be non empty set, FD be distance_function of FS,L;
let x,y be Element of FS;
let a,b be Element of L;
assume that
A1: FS = union the set of all (S.i)`1 where i is Element of NAT and
A2: FD = union the set of all (S.i)`2 where i is Element of NAT and
A3: FD.(x,y) <= a"\/"b;
(S.0)`1 in the set of all (S.i)`1 where i is Element of NAT;
then reconsider
X = the set of all (S.i)`1 where i is Element of NAT as
non empty set;
consider x1 being set such that
A4: x in x1 and
A5: x1 in X by A1,TARSKI:def 4;
consider k being Element of NAT such that
A6: x1 = (S.k)`1 by A5;
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
A7: Aq1, dq1 is_extension_of A1,d1 and
A8: S.k = [A1,d1] and
A9: S.(k+1) = [Aq1,dq1] by Def20;
A10: [A1,d1]`1 = A1;
A11: x in A1 by A4,A6,A8;
[A1,d1]`2 = d1;
then d1 in the set of all (S.i)`2 where i is Element of NAT by A8;
then
A12: d1 c= FD by A2,ZFMISC_1:74;
A13: [Aq1,dq1]`1 = Aq1;
then Aq1 in the set of all (S.i)`1 where i is Element of NAT by A9;
then
A14: Aq1 c= FS by A1,ZFMISC_1:74;
[Aq1,dq1]`2 = dq1;
then dq1 in the set of all (S.i)`2 where i is Element of NAT by A9;
then
A15: dq1 c= FD by A2,ZFMISC_1:74;
consider y1 being set such that
A16: y in y1 and
A17: y1 in X by A1,TARSKI:def 4;
consider l being Element of NAT such that
A18: y1 = (S.l)`1 by A17;
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
A19: Aq2, dq2 is_extension_of A2,d2 and
A20: S.l = [A2,d2] and
A21: S.(l+1) = [Aq2,dq2] by Def20;
A22: [A2,d2]`1 = A2;
A23: y in A2 by A16,A18,A20;
[A2,d2]`2 = d2;
then d2 in the set of all (S.i)`2 where i is Element of NAT by A20;
then
A24: d2 c= FD by A2,ZFMISC_1:74;
A25: [Aq2,dq2]`1 = Aq2;
then Aq2 in the set of all (S.i)`1 where i is Element of NAT by A21;
then
A26: Aq2 c= FS by A1,ZFMISC_1:74;
[Aq2,dq2]`2 = dq2;
then dq2 in the set of all (S.i)`2 where i is Element of NAT by A21;
then
A27: dq2 c= FD by A2,ZFMISC_1:74;
per cases;
suppose
k <= l;
then
A1 c= A2 by A10,A22,Th38,A20,A8;
then reconsider x9=x,y9=y as Element of A2 by A11,A16,A18,A20;
A2 c= Aq2 by A22,A25,Th38,A20,A21,NAT_1:11;
then reconsider x99 = x9,y99 = y9 as Element of Aq2;
dom d2 = [:A2,A2:] by FUNCT_2:def 1;
then FD.(x,y) = d2.[x9,y9] by A24,GRFUNC_1:2
.= d2.(x9,y9);
then consider z1,z2,z3 being Element of Aq2 such that
A28: dq2.(x,z1) = a and
A29: dq2.(z2,z3) = a and
A30: dq2.(z1,z2) = b and
A31: dq2.(z3,y) = b by A3,A19,Th37;
reconsider z19 = z1, z29 = z2, z39 = z3 as Element of FS by A26;
take z19,z29,z39;
A32: dom dq2 = [:Aq2,Aq2:] by FUNCT_2:def 1;
hence FD.(x,z19) = dq2.[x99,z1] by A27,GRFUNC_1:2
.= a by A28;
thus FD.(z29,z39) = dq2.[z2,z3] by A27,A32,GRFUNC_1:2
.= a by A29;
thus FD.(z19,z29) = dq2.[z1,z2] by A27,A32,GRFUNC_1:2
.= b by A30;
thus FD.(z39,y) = dq2.[z3,y99] by A27,A32,GRFUNC_1:2
.= b by A31;
end;
suppose
l <= k;
then A2 c= A1 by A10,A22,Th38,A20,A8;
then reconsider x9=x,y9=y as Element of A1 by A4,A6,A8,A23;
A1 c= Aq1 by A10,A13,Th38,A8,A9,NAT_1:11;
then reconsider x99 = x9,y99 = y9 as Element of Aq1;
dom d1 = [:A1,A1:] by FUNCT_2:def 1;
then FD.(x,y) = d1.[x9,y9] by A12,GRFUNC_1:2
.= d1.(x9,y9);
then consider z1,z2,z3 being Element of Aq1 such that
A33: dq1.(x,z1) = a and
A34: dq1.(z2,z3) = a and
A35: dq1.(z1,z2) = b and
A36: dq1.(z3,y) = b by A3,A7,Th37;
reconsider z19 = z1, z29 = z2, z39 = z3 as Element of FS by A14;
take z19,z29,z39;
A37: dom dq1 = [:Aq1,Aq1:] by FUNCT_2:def 1;
hence FD.(x,z19) = dq1.[x99,z1] by A15,GRFUNC_1:2
.= a by A33;
thus FD.(z29,z39) = dq1.[z2,z3] by A15,A37,GRFUNC_1:2
.= a by A34;
thus FD.(z19,z29) = dq1.[z1,z2] by A15,A37,GRFUNC_1:2
.= b by A35;
thus FD.(z39,y) = dq1.[z3,y99] by A15,A37,GRFUNC_1:2
.= b by A36;
end;
end;
theorem Th43:
for S being ExtensionSeq of the carrier of L, BasicDF(L) for FS
being non empty set for FD being distance_function of FS,L for f being
Homomorphism of L,EqRelLATT FS for x, y being Element of FS for e1,e2 being
Equivalence_Relation of FS,x,y being object st f = alpha FD &
FS = union the set of all (S.i)`1 where i
is Element of NAT &
FD = union the set of all (S.i)`2 where i is Element
of NAT & e1 in the carrier of Image f & e2 in the carrier
of Image f & [x,y] in e1 "\/" e2 ex F being non empty FinSequence of FS st len
F = 3+2 & x,y are_joint_by F,e1,e2
proof
let S be ExtensionSeq of the carrier of L, BasicDF(L);
let FS be non empty set;
let FD be distance_function of FS,L;
let f be Homomorphism of L,EqRelLATT FS;
let x, y be Element of FS;
let e1,e2 be Equivalence_Relation of FS,x,y be object;
assume that
A1: f = alpha FD and
A2: FS = union the set of all (S.i)`1 where i is Element of NAT &
FD = union the set of all (S.i)`2 where i is Element of NAT and
A3: e1 in the carrier of Image f and
A4: e2 in the carrier of Image f and
A5: [x,y] in e1 "\/" e2;
A6: 4 in Seg 5;
field (e1 "\/" e2) = FS by ORDERS_1:12;
then reconsider u = x, v = y as Element of FS by A5,RELAT_1:15;
A7: 1 in Seg 5;
Image f = subrelstr rng f by YELLOW_2:def 2;
then
A8: the carrier of Image f = rng f by YELLOW_0:def 15;
then consider a being object such that
A9: a in dom f and
A10: e1 = f.a by A3,FUNCT_1:def 3;
consider b being object such that
A11: b in dom f and
A12: e2 = f.b by A4,A8,FUNCT_1:def 3;
reconsider a,b as Element of L by A9,A11;
reconsider a,b as Element of L;
consider e being Equivalence_Relation of FS such that
A13: e = f.(a"\/"b) and
A14: for u,v being Element of FS holds [u,v] in e iff FD.(u,v) <= a"\/"b
by A1,Def8;
consider e19 being Equivalence_Relation of FS such that
A15: e19 = f.a and
A16: for u,v being Element of FS holds [u,v] in e19 iff FD.(u,v) <= a by A1
,Def8;
consider e29 being Equivalence_Relation of FS such that
A17: e29 = f.b and
A18: for u,v being Element of FS holds [u,v] in e29 iff FD.(u,v) <= b by A1
,Def8;
A19: 3 in Seg 5;
e = f.a"\/"f.b by A13,WAYBEL_6:2
.= e1 "\/" e2 by A10,A12,Th10;
then FD.(u,v) <= a"\/"b by A5,A14;
then consider z1,z2,z3 being Element of FS such that
A20: FD.(u,z1) = a and
A21: FD.(z2,z3) = a and
A22: FD.(z1,z2) = b and
A23: FD.(z3,v) = b by A2,Th42;
defpred P[set,object] means
($1 = 1 implies $2 = u) & ($1 = 2 implies $2 = z1)
& ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = z3) & ($1 = 5 implies $2 = v)
;
A24: for m being Nat st m in Seg 5 ex w being object st P[m,w]
proof
let m be Nat;
assume m in Seg 5;
then m = 1 or ... or m = 5 by Lm3;
then per cases;
suppose
A25: m = 1;
take x;
thus thesis by A25;
end;
suppose
A26: m = 2;
take z1;
thus thesis by A26;
end;
suppose
A27: m = 3;
take z2;
thus thesis by A27;
end;
suppose
A28: m = 4;
take z3;
thus thesis by A28;
end;
suppose
A29: m = 5;
take y;
thus thesis by A29;
end;
end;
ex p being FinSequence st dom p = Seg 5 & for k being Nat st k in Seg 5
holds P[k,p.k] from FINSEQ_1:sch 1(A24);
then consider h being FinSequence such that
A30: dom h = Seg 5 and
A31: for m being Nat st m in Seg 5 holds (m = 1 implies h.m = u) & (m =
2 implies h.m = z1) & (m = 3 implies h.m = z2) & (m = 4 implies h.m = z3) & (m
= 5 implies h.m = v);
A32: len h = 5 by A30,FINSEQ_1:def 3;
A33: 5 in Seg 5;
A34: 2 in Seg 5;
rng h c= FS
proof
let w be object;
assume w in rng h;
then consider j be object such that
A35: j in dom h and
A36: w = h.j by FUNCT_1:def 3;
j = 1 or ... or j = 5 by A30,A35,Lm3;
then per cases;
suppose
j = 1;
then h.j = u by A31,A7;
hence thesis by A36;
end;
suppose
j = 2;
then h.j = z1 by A31,A34;
hence thesis by A36;
end;
suppose
j = 3;
then h.j = z2 by A31,A19;
hence thesis by A36;
end;
suppose
j = 4;
then h.j = z3 by A31,A6;
hence thesis by A36;
end;
suppose
j = 5;
then h.j = v by A31,A33;
hence thesis by A36;
end;
end;
then reconsider h as FinSequence of FS by FINSEQ_1:def 4;
reconsider h as non empty FinSequence of FS by A30;
A37: h.1 = x by A31,A7;
A38: for j being Element of 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 Element of NAT;
assume 1 <= j & j < len h;
then j = 1 or ... or j = 4 by A32,Lm2;
then per cases;
suppose
A39: j = 1;
[u,z1] in e19 by A16,A20;
then [h.1,z1] in e19 by A31,A7;
hence thesis by A10,A15,A31,A34,A39;
end;
suppose
A40: j = 3;
[z2,z3] in e19 by A16,A21;
then
A41: [h.3,z3] in e19 by A31,A19;
2*1+1 = j by A40;
hence thesis by A10,A15,A31,A6,A41;
end;
suppose
A42: j = 2;
[z1,z2] in e29 by A18,A22;
then
A43: [h.2,z2] in e29 by A31,A34;
2*1 = j by A42;
hence thesis by A12,A17,A31,A19,A43;
end;
suppose
A44: j = 4;
[z3,v] in e29 by A18,A23;
then
A45: [h.4,v] in e29 by A31,A6;
2*2 = j by A44;
hence thesis by A12,A17,A31,A33,A45;
end;
end;
take h;
thus len h = 3+2 by A30,FINSEQ_1:def 3;
h.(len h) = h.5 by A30,FINSEQ_1:def 3
.= y by A31,A33;
hence thesis by A37,A38;
end;
::$N Jonsson Theorem for lattices
theorem
ex A being non empty set, f being Homomorphism of L,EqRelLATT A st f
is one-to-one & type_of Image f <= 3
proof
set A = the carrier of L, D = BasicDF(L);
set S = the ExtensionSeq of A,D;
set FS = union the set of all (S.i)`1 where i is Element of NAT;
A1: (S.0)`1 in the set of all (S.i)`1 where i is Element of NAT;
A2: S.0 = [A,D] by Def20;
A c= FS by A1,A2,ZFMISC_1:74;
then reconsider FS as non empty set;
reconsider FD
= union the set of all (S.i)`2 where i is Element of NAT
as distance_function of FS,L by Th41;
alpha FD is join-preserving
proof
set f = alpha FD;
let a,b be Element of L;
A3: ex_sup_of f.:{a,b},EqRelLATT FS by YELLOW_0:17;
consider e3 being Equivalence_Relation of FS such that
A4: e3 = f.(a "\/" b) and
A5: for x,y being Element of FS holds [x,y] in e3 iff FD.(x,y) <= a
"\/"b by Def8;
consider e2 being Equivalence_Relation of FS such that
A6: e2 = f.b and
A7: for x,y being Element of FS holds [x,y] in e2 iff FD.(x,y) <= b by Def8;
consider e1 being Equivalence_Relation of FS such that
A8: e1 = f.a and
A9: for x,y being Element of FS holds [x,y] in e1 iff FD.(x,y) <= a by Def8;
A10: field e2 = FS by ORDERS_1:12;
now
let x,y be object;
A11: b <= b "\/" a by YELLOW_0:22;
assume
A12: [x,y] in e2;
then reconsider x9 = x, y9 = y as Element of FS by A10,RELAT_1:15;
FD.(x9,y9) <= b by A7,A12;
then FD.(x9,y9) <= b "\/" a by A11,ORDERS_2:3;
hence [x,y] in e3 by A5;
end;
then
A13: e2 c= e3 by RELAT_1:def 3;
A14: field e3 = FS by ORDERS_1:12;
for u,v being object holds [u,v] in e3 implies [u,v] in e1 "\/" e2
proof
let u,v be object;
A15: 3 in Seg 5;
assume
A16: [u,v] in e3;
then reconsider x = u, y = v as Element of FS by A14,RELAT_1:15;
FD.(x,y) <= a"\/"b by A5,A16;
then consider z1,z2,z3 being Element of FS such that
A17: FD.(x,z1) = a and
A18: FD.(z2,z3) = a and
A19: FD.(z1,z2) = b and
A20: FD.(z3,y) = b by Th42;
A21: u in FS by A14,A16,RELAT_1:15;
defpred P[set,object] means
($1 = 1 implies $2 = x) & ($1 = 2 implies $2 =
z1) & ($1 = 3 implies $2 = z2) & ($1 = 4 implies $2 = z3) & ($1 = 5 implies $2
= y);
A22: for m being Nat st m in Seg 5 ex w being object st P[m,w]
proof
let m be Nat;
assume m in Seg 5;
then m = 1 or ... or m = 5 by Lm3;
then per cases;
suppose
A23: m = 1;
take x;
thus thesis by A23;
end;
suppose
A24: m = 2;
take z1;
thus thesis by A24;
end;
suppose
A25: m = 3;
take z2;
thus thesis by A25;
end;
suppose
A26: m = 4;
take z3;
thus thesis by A26;
end;
suppose
A27: m = 5;
take y;
thus thesis by A27;
end;
end;
ex p being FinSequence st dom p = Seg 5 & for k being Nat st k in
Seg 5 holds P[k,p.k] from FINSEQ_1:sch 1(A22);
then consider h being FinSequence such that
A28: dom h = Seg 5 and
A29: for m being Nat st m in Seg 5 holds (m = 1 implies h.m = x) & (
m = 2 implies h.m = z1) & (m = 3 implies h.m = z2) & (m = 4 implies h.m = z3) &
(m = 5 implies h.m = y);
A30: len h = 5 by A28,FINSEQ_1:def 3;
A31: 5 in Seg 5;
A32: 4 in Seg 5;
A33: 1 in Seg 5;
then
A34: u = h.1 by A29;
A35: 2 in Seg 5;
A36: 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 1 <= j & j < len h;
then j = 1 or ... or j = 4 by A30,Lm2;
then per cases;
suppose
A37: j = 1;
[x,z1] in e1 by A9,A17;
then [h.1,z1] in e1 by A29,A33;
then [h.1,h.2] in e1 by A29,A35;
hence thesis by A37,XBOOLE_0:def 3;
end;
suppose
A38: j = 3;
[z2,z3] in e1 by A9,A18;
then [h.3,z3] in e1 by A29,A15;
then [h.3,h.4] in e1 by A29,A32;
hence thesis by A38,XBOOLE_0:def 3;
end;
suppose
A39: j = 2;
[z1,z2] in e2 by A7,A19;
then [h.2,z2] in e2 by A29,A35;
then [h.2,h.3] in e2 by A29,A15;
hence thesis by A39,XBOOLE_0:def 3;
end;
suppose
A40: j = 4;
[z3,y] in e2 by A7,A20;
then [h.4,y] in e2 by A29,A32;
then [h.4,h.5] in e2 by A29,A31;
hence thesis by A40,XBOOLE_0:def 3;
end;
end;
v = h.5 by A29,A31
.= h.(len h) by A28,FINSEQ_1:def 3;
hence thesis by A21,A30,A34,A36,EQREL_1:28;
end;
then
A41: e3 c= e1 "\/" e2 by RELAT_1:def 3;
A42: field e1 = FS by ORDERS_1:12;
now
let x,y be object;
A43: a <= a "\/" b by YELLOW_0:22;
assume
A44: [x,y] in e1;
then reconsider x9 = x, y9 = y as Element of FS by A42,RELAT_1:15;
FD.(x9,y9) <= a by A9,A44;
then FD.(x9,y9) <= a "\/" b by A43,ORDERS_2:3;
hence [x,y] in e3 by A5;
end;
then e1 c= e3 by RELAT_1:def 3;
then e1 \/ e2 c= e3 by A13,XBOOLE_1:8;
then
A45: e1 "\/" e2 c= e3 by EQREL_1:def 2;
dom f = the carrier of L by FUNCT_2:def 1;
then sup (f.:{a,b}) = sup {f.a,f.b} by FUNCT_1:60
.= f.a "\/" f.b by YELLOW_0:41
.= e1 "\/" e2 by A8,A6,Th10
.= f.(a "\/" b) by A4,A45,A41
.= f.sup {a,b} by YELLOW_0:41;
hence thesis by A3;
end;
then reconsider f = alpha FD as Homomorphism of L,EqRelLATT FS by Th14;
A46: dom f = the carrier of L by FUNCT_2:def 1;
A47: Image f = subrelstr rng f by YELLOW_2:def 2;
A48: ex e being Equivalence_Relation of FS st e in the carrier of Image f &
e <> id FS
proof
A49: {A} <> {{A}}
proof
assume {A} = {{A}};
then {A} in {A} by TARSKI:def 1;
hence contradiction;
end;
consider A9 being non empty set, d9 being distance_function of A9,L, Aq9
being non empty set, dq9 being distance_function of Aq9,L such that
A50: Aq9, dq9 is_extension_of A9,d9 and
A51: S.0 = [A9,d9] and
A52: S.(0+1) = [Aq9,dq9] by Def20;
A9 = A & d9 = D by A2,A51,XTUPLE_0:1;
then consider q being QuadrSeq of D such that
A53: Aq9 = NextSet(D) and
A54: dq9 = NextDelta(q) by A50;
ConsecutiveSet(A,{}) = A by Th21;
then reconsider Q = Quadr(q,{}) as Element of [:A,A,the carrier of L,the
carrier of L:];
A55: (S.1)`2 in the set of all (S.i)`2 where i is Element of NAT;
succ {} c= DistEsti(D) by Lm4;
then {} in DistEsti(D) by ORDINAL1:21;
then
A56: {} in dom q by Th25;
then q.{} in rng q by FUNCT_1:def 3;
then q.{} in {[u,v,a9,b9] where u is Element of A, v is Element of A, a9
is Element of L, b9 is Element of L: D.(u,v) <= a9"\/"b9} by Def13;
then consider u,v be Element of A, a,b be Element of L such that
A57: q.{} = [u,v,a,b] and
D.(u,v) <= a"\/"b;
consider e being Equivalence_Relation of FS such that
A58: e = f.b and
A59: for x,y being Element of FS holds [x,y] in e iff FD.(x,y) <= b by Def8;
A60: Quadr(q,{}) = [u,v,a,b] by A56,A57,Def14;
[Aq9,dq9]`2 = NextDelta(q) by A54;
then
A61: NextDelta(q) c= FD by A55,A52,ZFMISC_1:74;
A62: {{A}} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:def 1;
then
A63: {{A}} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 3;
take e;
e in rng f by A46,A58,FUNCT_1:def 3;
hence e in the carrier of Image f by A47,YELLOW_0:def 15;
A64: (S.1)`1 in the set of all (S.i)`1 where i is Element of NAT;
[Aq9,dq9]`1 = NextSet(D) by A53;
then
A65: NextSet(D) c= FS by A64,A52,ZFMISC_1:74;
new_set A = new_set ConsecutiveSet(A,{}) by Th21
.= ConsecutiveSet(A,succ {}) by Th22;
then new_set A c= NextSet(D) by Lm4,Th29;
then
A66: new_set A c= FS by A65;
A67: {{A}} in new_set A by A62,XBOOLE_0:def 3;
A68: {A} in {{A}, {{A}}, {{{A}}} } by ENUMSET1:def 1;
then {A} in A \/ {{A}, {{A}}, {{{A}}}} by XBOOLE_0:def 3;
then reconsider W = {A}, V = {{A}} as Element of FS by A66,A67;
A69: ConsecutiveSet(A,{}) = A & ConsecutiveDelta(q,{}) = D by Th21,Th26;
ConsecutiveDelta(q,succ {}) = new_bi_fun(BiFun(ConsecutiveDelta(q,{}
), ConsecutiveSet(A,{}),L),Quadr(q,{})) by Th27
.= new_bi_fun(D,Q) by A69,Def15;
then new_bi_fun(D,Q) c= NextDelta(q) by Lm4,Th32;
then
A70: new_bi_fun(D,Q) c= FD by A61;
dom new_bi_fun(D,Q) = [:new_set A,new_set A:] & {A} in new_set A by A68,
FUNCT_2:def 1,XBOOLE_0:def 3;
then [{A},{{A}}] in dom new_bi_fun(D,Q) by A63,ZFMISC_1:87;
then FD.(W,V) = new_bi_fun(D,Q).({A},{{A}}) by A70,GRFUNC_1:2
.= Q`4_4 by Def10
.= b by A60;
then [{A},{{A}}] in e by A59;
hence thesis by A49,RELAT_1:def 10;
end;
take FS,f;
D is onto by Th40;
then
A71: rng D = A by FUNCT_2:def 3;
for w being object st w in A
ex z being object st z in [:FS,FS:] & w = FD.z
proof
let w be object;
A72: (S.0)`1 in the set of all (S.i)`1 where i is Element of NAT;
A73: (S.0)`2 in the set of all (S.i)`2 where i is Element of NAT;
A74: S.0 = [A,D] by Def20;
A75: D c= FD by A73,A74,ZFMISC_1:74;
assume w in A;
then consider z being object such that
A76: z in [:A,A:] and
A77: D.z = w by A71,FUNCT_2:11;
take z;
A c= FS by A72,A74,ZFMISC_1:74;
then [:A,A:] c= [:FS,FS:] by ZFMISC_1:96;
hence z in [:FS,FS:] by A76;
z in dom D by A76,FUNCT_2:def 1;
hence thesis by A77,A75,GRFUNC_1:2;
end;
then rng FD = A by FUNCT_2:10;
then FD is onto by FUNCT_2:def 3;
hence f is one-to-one by Th15;
for e1,e2 being Equivalence_Relation of FS,
x,y being object st e1 in the carrier of
Image f & e2 in the carrier of Image f & [x,y] in e1 "\/" e2 ex F being non
empty FinSequence of FS st len F = 3+2 & x,y are_joint_by F,e1,e2 by Th43;
hence thesis by A48,Th13;
end;