:: The Equational Characterization of Continuous Lattices
:: by Mariusz \.Zynel
::
:: Received October 25, 1996
:: Copyright (c) 1996-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 WAYBEL_0, ORDINAL2, SUBSET_1, WAYBEL_3, CARD_FIL, XXREAL_0,
TARSKI, XBOOLE_0, YELLOW_0, LATTICE3, LATTICES, YELLOW_2, WAYBEL_1,
YELLOW_1, RELAT_1, FUNCT_1, STRUCT_0, REWRITE1, PBOOLE, FUNCOP_1,
FUNCT_6, CARD_3, FINSEQ_4, ORDERS_2, YELLOW_6, CLASSES1, CLASSES2,
ZFMISC_1, FUNCT_5, EQREL_1, FUNCT_2, FINSUB_1, FINSET_1, ORDERS_1,
RELAT_2, LATTICE2, CAT_1, XBOOLEAN, PARTFUN1, MEMBER_1, SEQM_3, WAYBEL_5,
CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, FINSET_1,
FINSUB_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4,
FUNCT_5, FUNCT_6, FUNCOP_1, ORDERS_1, DOMAIN_1, STRUCT_0, ORDERS_2,
LATTICE3, CARD_3, PBOOLE, PRALG_1, PRALG_2, MSUALG_3, CLASSES1, CLASSES2,
YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_3, YELLOW_6;
constructors FINSUB_1, CLASSES1, CLASSES2, BORSUK_1, LATTICE3, PRALG_1,
PRALG_2, MSUALG_3, ORDERS_3, WAYBEL_1, WAYBEL_3, YELLOW_6, FUNCT_5,
XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1,
FUNCT_4, FINSET_1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, ORDERS_2,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_3, YELLOW_6,
PRALG_1, RELAT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICE3;
equalities BINOP_1, STRUCT_0;
expansions TARSKI, LATTICE3;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_5, CARD_3, ORDERS_2,
FUNCT_6, FUNCOP_1, PBOOLE, PRALG_1, PRALG_2, MSUALG_3, RELAT_1, FINSUB_1,
YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_3, CLASSES2,
YELLOW_6, CLASSES1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCT_4, ORDERS_1,
PARTFUN1;
schemes FUNCT_1, FUNCT_2, MSSUBFAM, DOMAIN_1, BINOP_1;
begin :: The Continuity of Lattices
reserve x, y, i for object,
L for up-complete Semilattice;
Lm1: for L being continuous Semilattice for x being Element of L holds
waybelow x is Ideal of L & x <= sup waybelow x & for I being Ideal of L st x <=
sup I holds waybelow x c= I
proof
let L be continuous Semilattice;
let x be Element of L;
thus waybelow x is Ideal of L;
thus x <= sup waybelow x by WAYBEL_3:def 5;
thus for I being Ideal of L st x <= sup I holds waybelow x c= I
proof
let I be Ideal of L;
assume
A1: x <= sup I;
waybelow x c= I
proof
let y be object;
assume y in waybelow x;
then y in {y9 where y9 is Element of L: y9 << x} by WAYBEL_3:def 3;
then ex y9 being Element of L st y = y9 & y9 << x;
hence thesis by A1,WAYBEL_3:20;
end;
hence thesis;
end;
end;
Lm2: (for x being Element of L holds waybelow x is Ideal of L & x <= sup
waybelow x & for I being Ideal of L st x <= sup I holds waybelow x c= I)
implies L is continuous
proof
assume
A1: for x being Element of L holds waybelow x is Ideal of L & x <= sup
waybelow x & for I being Ideal of L st x <= sup I holds waybelow x c= I;
now
let x be Element of L;
A2: x <= sup waybelow x by A1;
waybelow x is non empty directed by A1;
then
A3: ex_sup_of waybelow x,L by WAYBEL_0:75;
waybelow x is_<=_than x by WAYBEL_3:9;
then sup waybelow x <= x by A3,YELLOW_0:def 9;
hence x = sup waybelow x by A2,YELLOW_0:def 3;
end;
then
A4: L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
for x being Element of L holds waybelow x is non empty directed by A1;
hence thesis by A4,WAYBEL_3:def 6;
end;
theorem ::Theorem 2.1 (1) iff (2)
L is continuous iff for x being Element of L holds waybelow x is Ideal
of L & x <= sup waybelow x & for I being Ideal of L st x <= sup I holds
waybelow x c= I by Lm1,Lm2;
Lm3: L is continuous implies for x being Element of L ex I being Ideal of L st
x <= sup I & for J being Ideal of L st x <= sup J holds I c= J
proof
assume
A1: L is continuous;
let x be Element of L;
reconsider I = waybelow x as Ideal of L by A1;
take I;
thus thesis by A1,Lm1;
end;
Lm4: (for x being Element of L ex I being Ideal of L st x <= sup I & for J
being Ideal of L st x <= sup J holds I c= J) implies L is continuous
proof
assume
A1: for x being Element of L ex I being Ideal of L st x <= sup I & for J
being Ideal of L st x <= sup J holds I c= J;
now
let x be Element of L;
consider I being Ideal of L such that
A2: x <= sup I and
A3: for J being Ideal of L st x <= sup J holds I c= J by A1;
now
let y be object;
assume
A4: y in I;
then reconsider y9= y as Element of L;
for J being Ideal of L st x <= sup J holds y in J
proof
let J be Ideal of L;
assume x <= sup J;
then I c= J by A3;
hence thesis by A4;
end;
then y9 << x by WAYBEL_3:21;
hence y in waybelow x by WAYBEL_3:7;
end;
then
A5: I c= waybelow x;
for y being object st y in waybelow x holds y in I by A2,WAYBEL_3:7,20;
then waybelow x c= I;
then waybelow x = I by A5,XBOOLE_0:def 10;
hence
waybelow x is Ideal of L & x <= sup waybelow x & for I being Ideal of
L st x <= sup I holds waybelow x c= I by A2,A3;
end;
hence thesis by Lm2;
end;
theorem ::Theorem 2.1 (1) iff (3)
L is continuous iff for x being Element of L ex I being Ideal of L st
x <= sup I & for J being Ideal of L st x <= sup J holds I c= J by Lm3,Lm4;
theorem ::Theorem 2.1 (1) implies (4)
for L being continuous lower-bounded sup-Semilattice holds SupMap L is
upper_adjoint
proof
let L be continuous lower-bounded sup-Semilattice;
set P = InclPoset(Ids L);
set r = SupMap L;
deffunc F(Element of L) = inf(r"(uparrow {$1}));
ex d being Function of L, InclPoset(Ids L) st for t being Element of L
holds d.t = F(t) from FUNCT_2:sch 4;
then consider d being Function of L, InclPoset(Ids L) such that
A1: for t being Element of L holds d.t = inf(r"(uparrow {t}));
for t being Element of L holds d.t is_minimum_of r"(uparrow t)
proof
let t be Element of L;
set I = inf(r"(uparrow t));
reconsider I9= I as Ideal of L by YELLOW_2:41;
A2: d.t = inf(r"(uparrow {t})) by A1
.= I by WAYBEL_0:def 18;
I in the carrier of P;
then I in Ids L by YELLOW_1:1;
then
A3: I in dom r by YELLOW_2:49;
consider J being Ideal of L such that
A4: t <= sup J and
A5: for K being Ideal of L st t <= sup K holds J c= K by Lm3;
reconsider J9= J as Element of P by YELLOW_2:41;
A6: for K being Element of P st r"(uparrow t) is_>=_than K holds K <= J9
proof
J9 in the carrier of P;
then J9 in Ids L by YELLOW_1:1;
then
A7: J in dom r by YELLOW_2:49;
let K be Element of P;
assume
A8: r"(uparrow t) is_>=_than K;
t <= r.J9 by A4,YELLOW_2:def 3;
then r.J in uparrow t by WAYBEL_0:18;
then J in r"(uparrow t) by A7,FUNCT_1:def 7;
hence thesis by A8;
end;
r"(uparrow t) is_>=_than J9
proof
let K be Element of P;
reconsider K9= K as Ideal of L by YELLOW_2:41;
assume K in r"(uparrow t);
then r.K in uparrow t by FUNCT_1:def 7;
then t <= r.K by WAYBEL_0:18;
then t <= sup K9 by YELLOW_2:def 3;
then J9 c= K9 by A5;
hence J9 <= K by YELLOW_1:3;
end;
then t <= sup I9 by A4,A6,YELLOW_0:31;
then t <= r.I by YELLOW_2:def 3;
then r.I in uparrow t by WAYBEL_0:18;
then ex_inf_of r"(uparrow t),InclPoset(Ids L) & I in r"(uparrow t) by A3,
FUNCT_1:def 7,YELLOW_0:17;
hence thesis by A2,WAYBEL_1:def 6;
end;
then [r, d] is Galois by WAYBEL_1:10;
hence thesis by WAYBEL_1:def 11;
end;
theorem ::Theorem 2.1 (4) implies (1)
for L being up-complete lower-bounded LATTICE holds SupMap L is
upper_adjoint implies L is continuous
proof
let L be up-complete lower-bounded LATTICE;
set P = InclPoset(Ids L);
assume
A1: SupMap L is upper_adjoint;
for x being Element of L ex I being Ideal of L st x <= sup I & for J
being Ideal of L st x <= sup J holds I c= J
proof
set r = SupMap L;
let x be Element of L;
set I9 = inf(r"(uparrow x));
reconsider I = I9 as Ideal of L by YELLOW_2:41;
A2: for J being Ideal of L st x <= sup J holds I c= J
proof
let J be Ideal of L;
reconsider J9= J as Element of P by YELLOW_2:41;
assume x <= sup J;
then x <= r.J9 by YELLOW_2:def 3;
then J in dom r & r.J9 in uparrow x by WAYBEL_0:18,YELLOW_2:50;
then J9 in r"(uparrow x) by FUNCT_1:def 7;
then I9 <= J9 by YELLOW_2:22;
hence thesis by YELLOW_1:3;
end;
consider d being Function of L, P such that
A3: [r,d] is Galois by A1,WAYBEL_1:def 11;
d.x is_minimum_of r"(uparrow x) by A3,WAYBEL_1:10;
then I in r"(uparrow x) by WAYBEL_1:def 6;
then r.I in uparrow x by FUNCT_1:def 7;
then x <= r.I9 by WAYBEL_0:18;
then x <= sup I by YELLOW_2:def 3;
hence thesis by A2;
end;
hence thesis by Lm4;
end;
theorem ::Theorem 2.1 (5) implies (4)
for L being complete Semilattice holds SupMap L is infs-preserving
sups-preserving implies SupMap L is upper_adjoint
proof
let L be complete Semilattice;
set r = SupMap L;
assume r is infs-preserving sups-preserving;
then ex d being Function of L, InclPoset(Ids L) st [r, d] is Galois & for t
being Element of L holds d.t is_minimum_of r"(uparrow t) by WAYBEL_1:14;
hence thesis by WAYBEL_1:def 11;
end;
:: Corollary 2.2 can be found in WAYBEL_4.
definition
let J, D be set, K be ManySortedSet of J;
mode DoubleIndexedSet of K, D is ManySortedFunction of K, (J --> D);
end;
definition
let J be set, K be ManySortedSet of J, S be 1-sorted;
mode DoubleIndexedSet of K, S is DoubleIndexedSet of K, the carrier of S;
end;
theorem Th6:
for J, D being set, K being ManySortedSet of J for F being
DoubleIndexedSet of K, D for j being set st j in J holds F.j is Function of K.j
, D
proof
let J, D be set, K be ManySortedSet of J;
let F be DoubleIndexedSet of K, D;
let j be set;
assume
A1: j in J;
then (J --> D).j = D by FUNCOP_1:7;
hence thesis by A1,PBOOLE:def 15;
end;
definition
let J, D be non empty set, K be ManySortedSet of J;
let F be DoubleIndexedSet of K, D;
let j be Element of J;
redefine func F.j -> Function of K.j, D; :: redefines . (FUNCT_1, definition)
coherence by Th6;
end;
registration
let J, D be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, D;
let j be Element of J;
cluster rng(F.j) -> non empty;
correctness;
end;
registration
let J be set, D be non empty set;
let K be non-empty ManySortedSet of J;
cluster -> non-empty for DoubleIndexedSet of K, D;
correctness
proof
let F be DoubleIndexedSet of K, D;
for j being object st j in dom F holds F.j is non empty
proof
let j be object;
set k = the Element of K.j;
assume j in dom F;
then
A1: j in J;
then F.j is Function of K.j, D by Th6;
then dom(F.j) = K.j by FUNCT_2:def 1;
then [k, (F.j).k] in F.j by A1,FUNCT_1:def 2;
hence thesis;
end;
hence thesis by FUNCT_1:def 9;
end;
end;
registration let F be Function-yielding Function;
cluster dom Frege F -> functional;
coherence;
end;
::$CT
theorem Th8:
for F being Function-yielding Function
for f being Function st f in dom Frege F holds
dom f = dom F & dom F = dom((Frege F).f)
proof
let F be Function-yielding Function;
let f be Function;
assume f in dom Frege F ;
then
A1: f in product doms F;
then ex g being Function st g = f & dom g = dom(doms F) &
for x being object st x in dom doms F holds g.x in (doms F).x
by CARD_3:def 5;
hence
A2: dom f = dom F by FUNCT_6:59;
thus dom ((Frege F).f) = dom(F..f) by A1,PRALG_2:def 2
.= dom F /\ dom f by PRALG_1:def 19
.= dom F by A2;
end;
theorem Th9:
for F being Function-yielding Function
for f being Function st f in dom Frege F
for i being set st i in dom F holds f.i in dom(F.i) &
((Frege F).f).i = (F.i).(f.i) & (F.i).(f.i) in rng((Frege F).f)
proof
let F be Function-yielding Function;
let f be Function such that
A1: f in dom Frege F;
A2: f in product doms F by A1;
set G = (Frege F).f;
let i be set such that
A3: i in dom F;
i in dom f by Th8,A1,A3; then
i in dom F /\ dom f by A3,XBOOLE_0:def 4; then
a3: i in dom (F..f) by PRALG_1:def 19;
i in dom doms F by A3,FUNCT_6:59;
then f.i in (doms F).i by A2,CARD_3:9;
hence f.i in dom(F.i) by A3,FUNCT_6:22;
G = F..f by A2,PRALG_2:def 2;
hence
A4: G.i = (F.i).(f.i) by a3,PRALG_1:def 19;
dom G = dom F by A1,Th8;
hence thesis by A3,A4,FUNCT_1:def 3;
end;
theorem Th10:
for J, D being set, K being ManySortedSet of J
for F being DoubleIndexedSet of K, D
for f being Function st f in dom(Frege F) holds
(Frege F).f is Function of J, D
proof
let J, D be set, K be ManySortedSet of J;
let F be DoubleIndexedSet of K, D;
let f be Function such that
A1: f in dom(Frege F);
set G = (Frege F).f;
A2: dom G = dom F by A1,Th8;
A3: dom F = J by PARTFUN1:def 2;
rng G c= D
proof
let y be object;
assume y in rng G;
then consider x being object such that
A4: x in dom G and
A5: y = G.x by FUNCT_1:def 3;
F.x is Function of K.x, D by A2,A4,Th6;
then
A6: rng(F.x) c= D by RELAT_1:def 19;
G.x = (F.x).(f.x) & f.x in dom(F.x) by A1,A2,A4,Th9;
then y in rng(F.x) by A5,FUNCT_1:def 3;
hence thesis by A6;
end;
hence thesis by A3,A2,FUNCT_2:2;
end;
Lm5: for J, D being set, K being ManySortedSet of J for F being
DoubleIndexedSet of K, D for f being Function st f in dom(Frege F) for j being
set st j in J holds ((Frege F).f).j = (F.j).(f.j) & (F.j).(f.j) in rng((Frege F
).f)
proof
let J, D be set, K be ManySortedSet of J;
let F be DoubleIndexedSet of K, D;
let f be Function such that
A1: f in dom(Frege F);
let j be set;
assume j in J;
then
A2: j in dom F by PARTFUN1:def 2;
hence ((Frege F).f).j = (F.j).(f.j) by A1,Th9;
thus thesis by A1,A2,Th9;
end;
Lm6: for J being set, K being ManySortedSet of J, D being non empty set for F
being DoubleIndexedSet of K, D for f being Function st f in dom(Frege F) for j
being set st j in J holds f.j in K.j
proof
let J be set, K be ManySortedSet of J, D be non empty set;
let F be DoubleIndexedSet of K, D;
let f be Function such that
A1: f in dom(Frege F);
let j be set such that
A2: j in J;
A3: F.j is Function of K.j, D by A2,Th6;
dom F = J by PARTFUN1:def 2;
then f.j in dom(F.j) by A1,A2,Th9;
hence thesis by A3,FUNCT_2:def 1;
end;
registration
let f be non-empty Function-yielding Function;
cluster doms f -> non-empty;
correctness
proof
for j being object st j in dom doms f holds (doms f).j is non empty
proof
let j be object;
assume that
A1: j in dom doms f and
A2: (doms f).j is empty;
A3: j in dom f by A1,FUNCT_6:def 2;
reconsider fj = f.j as Function;
A4: j in dom f by A3;
then {} = dom fj by A2,FUNCT_6:22;
then f.j = {};
hence contradiction by A4,FUNCT_1:def 9;
end;
hence thesis by FUNCT_1:def 9;
end;
end;
definition
let J, D be set, K be ManySortedSet of J;
let F be DoubleIndexedSet of K, D;
redefine func Frege F -> DoubleIndexedSet of (product doms F --> J), D; :: redefines Frege (FUNCT_6, definition)
coherence
proof
set G = Frege F;
set PD = product doms F;
set A = (PD --> J), B = (PD --> D);
for i st i in PD holds G.i is Function of A.i, B.i
proof
let i;
assume
A1: i in PD;
then reconsider f = i as Function;
A2: B.i = D by A1,FUNCOP_1:7;
i in dom G & A.i = J by A1,FUNCOP_1:7,PARTFUN1:def 2;
then G.f is Function of A.i, B.i by A2,Th10;
hence thesis;
end;
hence thesis by PBOOLE:def 15;
end;
end;
definition
let J, D be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, D;
let G be DoubleIndexedSet of (product doms F --> J), D;
let f be Element of product doms F;
redefine func G.f -> Function of J, D; :: redefines . (FUNCT_1, definition)
coherence
proof
thus G.f is Function of J, D;
end;
end;
definition
let L be non empty RelStr;
let F be Function-yielding Function;
func \//(F, L) -> Function of dom F, the carrier of L means
:Def1:
for x st x in dom F holds it.x = \\/(F.x, L);
existence
proof
deffunc F(object) = \\/(F.$1, L);
ex f being Function st dom f = dom F &
for x being object st x in dom F holds f.x =
F(x) from FUNCT_1:sch 3;
then consider f being Function such that
A1: dom f = dom F and
A2: for x being object st x in dom F holds f.x = \\/(F.x, L);
rng f c= the carrier of L
proof
let y be object;
assume y in rng f;
then consider x being object such that
A3: x in dom f & y = f.x by FUNCT_1:def 3;
y = \\/(F.x, L) by A1,A2,A3;
hence thesis;
end;
then reconsider f as Function of dom F, the carrier of L by A1,FUNCT_2:2;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f, g be Function of dom F, the carrier of L such that
A4: for x st x in dom F holds f.x = \\/(F.x, L) and
A5: for x st x in dom F holds g.x = \\/(F.x, L);
A6: now
let x be object;
assume
A7: x in dom F;
hence f.x = \\/(F.x, L) by A4
.= g.x by A5,A7;
end;
dom f = dom F & dom g = dom F by FUNCT_2:def 1;
hence thesis by A6,FUNCT_1:2;
end;
func /\\(F, L) -> Function of dom F, the carrier of L means
:Def2:
for x st x in dom F holds it.x = //\(F.x, L);
existence
proof
deffunc F(object) = //\(F.$1, L);
ex f being Function st dom f = dom F &
for x being object st x in dom F holds f.x = F(x) from FUNCT_1:sch 3;
then consider f being Function such that
A8: dom f = dom F and
A9: for x being object st x in dom F holds f.x = //\(F.x, L);
rng f c= the carrier of L
proof
let y be object;
assume y in rng f;
then consider x being object such that
A10: x in dom f & y = f.x by FUNCT_1:def 3;
y = //\(F.x, L) by A8,A9,A10;
hence thesis;
end;
then reconsider f as Function of dom F, the carrier of L by A8,FUNCT_2:2;
take f;
thus thesis by A9;
end;
uniqueness
proof
let f, g be Function of dom F, the carrier of L such that
A11: for x st x in dom F holds f.x = //\(F.x, L) and
A12: for x st x in dom F holds g.x = //\(F.x, L);
A13: now
let x be object;
assume
A14: x in dom F;
hence f.x = //\(F.x, L) by A11
.= g.x by A12,A14;
end;
dom f = dom F & dom g = dom F by FUNCT_2:def 1;
hence thesis by A13,FUNCT_1:2;
end;
end;
notation
let J be set, K be ManySortedSet of J, L be non empty RelStr;
let F be DoubleIndexedSet of K, L;
synonym Sups F for \//(F, L);
synonym Infs F for /\\(F, L);
end;
notation
let I, J be set, L be non empty RelStr;
let F be DoubleIndexedSet of (I --> J), L;
synonym Sups F for \//(F, L);
synonym Infs F for /\\(F, L);
end;
theorem Th11:
for L being non empty RelStr for F, G being Function-yielding
Function st dom F = dom G & (for x st x in dom F holds \\/(F.x, L) = \\/(G.x, L
)) holds \//(F, L) = \//(G, L)
proof
let L be non empty RelStr;
let F, G be Function-yielding Function such that
A1: dom F = dom G and
A2: for x st x in dom F holds \\/(F.x, L) = \\/(G.x, L);
A3: for x being object st x in dom F holds \//(F, L).x = \//(G, L).x
proof
let x be object;
assume
A4: x in dom F;
hence \//(F, L).x = \\/(F.x, L) by Def1
.= \\/(G.x, L) by A2,A4
.= \//(G, L).x by A1,A4,Def1;
end;
dom \//(F, L) = dom F & dom \//(G, L) = dom G by FUNCT_2:def 1;
hence thesis by A1,A3,FUNCT_1:2;
end;
theorem Th12:
for L being non empty RelStr for F, G being Function-yielding
Function st dom F = dom G & (for x st x in dom F holds //\(F.x, L) = //\(G.x, L
)) holds /\\(F, L) = /\\(G, L)
proof
let L be non empty RelStr;
let F, G be Function-yielding Function such that
A1: dom F = dom G and
A2: for x st x in dom F holds //\(F.x, L) = //\(G.x, L);
A3: for x being object st x in dom F holds /\\(F, L).x = /\\(G, L).x
proof
let x be object;
assume
A4: x in dom F;
hence /\\(F, L).x = //\(F.x, L) by Def2
.= //\(G.x, L) by A2,A4
.= /\\(G, L).x by A1,A4,Def2;
end;
dom /\\(F, L) = dom F & dom /\\(G, L) = dom G by FUNCT_2:def 1;
hence thesis by A1,A3,FUNCT_1:2;
end;
theorem Th13:
for L being non empty RelStr for F being Function-yielding
Function holds (y in rng \//(F, L) iff ex x st x in dom F & y = \\/(F.x, L)) &
(y in rng /\\(F, L) iff ex x st x in dom F & y = //\(F.x, L))
proof
let L be non empty RelStr;
let F be Function-yielding Function;
thus y in rng \//(F, L) iff ex x st x in dom F & y = \\/(F.x, L)
proof
hereby
assume y in rng \//(F, L);
then consider x being object such that
A1: x in dom \//(F, L) & y = \//(F, L).x by FUNCT_1:def 3;
take x;
thus x in dom F & y = \\/(F.x, L) by A1,Def1;
end;
given x such that
A2: x in dom F & y = \\/(F.x, L);
x in dom \//(F, L) & y = \//(F, L).x by A2,Def1,FUNCT_2:def 1;
hence thesis by FUNCT_1:def 3;
end;
thus y in rng /\\(F, L) iff ex x st x in dom F & y = //\(F.x, L)
proof
hereby
assume y in rng /\\(F, L);
then consider x being object such that
A3: x in dom /\\(F, L) & y = /\\(F, L).x by FUNCT_1:def 3;
take x;
thus x in dom F & y = //\(F.x, L) by A3,Def2;
end;
given x such that
A4: x in dom F & y = //\(F.x, L);
x in dom /\\(F, L) & y = /\\(F, L).x by A4,Def2,FUNCT_2:def 1;
hence thesis by FUNCT_1:def 3;
end;
end;
theorem Th14:
for L being non empty RelStr for J being non empty set, K being
ManySortedSet of J for F being DoubleIndexedSet of K, L holds (x in rng Sups F
iff ex j being Element of J st x = Sup(F.j)) & (x in rng Infs F iff ex j being
Element of J st x = Inf(F.j))
proof
let L be non empty RelStr;
let J be non empty set, K be ManySortedSet of J;
let F be DoubleIndexedSet of K, L;
A1: dom F = J by PARTFUN1:def 2;
thus x in rng Sups F iff ex j being Element of J st x = Sup(F.j)
proof
hereby
assume x in rng Sups F;
then consider j being object such that
A2: j in dom F and
A3: x = \\/(F.j, L) by Th13;
reconsider j as Element of J by A2;
take j;
thus x = Sup(F.j) by A3;
end;
thus thesis by A1,Th13;
end;
hereby
assume x in rng Infs F;
then consider j being object such that
A4: j in dom F and
A5: x = //\(F.j, L) by Th13;
reconsider j as Element of J by A4;
take j;
thus x = Inf(F.j) by A5;
end;
thus thesis by A1,Th13;
end;
registration
let J be non empty set, K be ManySortedSet of J, L be non empty RelStr;
let F be DoubleIndexedSet of K, L;
cluster rng Sups F -> non empty;
correctness;
cluster rng Infs F -> non empty;
correctness;
end;
reserve L for complete LATTICE,
a, b, c for Element of L,
J for non empty set,
K for non-empty ManySortedSet of J;
Lm7: for F being DoubleIndexedSet of K, L for f being set holds f is Element
of product doms F iff f in dom(Frege F)
proof
let F be DoubleIndexedSet of K, L;
let f be set;
hereby
assume f is Element of product doms F;
then f in product doms F;
hence f in dom(Frege F) by PARTFUN1:def 2;
end;
thus thesis;
end;
theorem Th15:
for F being Function-yielding Function holds (for f being
Function st f in dom Frege F holds //\((Frege F).f, L) <= a) implies Sup /\\(
Frege F, L) <= a
proof
let F be Function-yielding Function;
assume
A1: for f being Function st f in dom(Frege F) holds //\((Frege F).f, L) <= a;
rng /\\(Frege F, L) is_<=_than a
proof
let c;
assume c in rng /\\(Frege F, L);
then consider f being object such that
A2: f in dom(Frege F) and
A3: c = //\((Frege F).f, L) by Th13;
reconsider f as Function by A2;
f in dom(Frege F) by A2;
hence c <= a by A1,A3;
end;
then sup rng /\\(Frege F, L) <= a by YELLOW_0:32;
hence thesis by YELLOW_2:def 5;
end;
theorem Th16:
for F being DoubleIndexedSet of K, L holds Inf Sups F >= Sup Infs Frege F
proof
let F be DoubleIndexedSet of K, L;
set a = Sup Infs Frege F;
A1: for j being Element of J for f being Element of product doms F holds Sup
(F.j) >= Inf((Frege F).f)
proof
let j be Element of J;
let f be Element of product doms F;
A2: f in dom(Frege F) by Lm7;
then reconsider k = f.j as Element of K.j by Lm6;
(F.j).k = ((Frege F).f).j by A2,Lm5;
then
A3: Inf((Frege F).f) <= (F.j).k by YELLOW_2:53;
(F.j).k <= Sup(F.j) by YELLOW_2:53;
hence thesis by A3,ORDERS_2:3;
end;
a is_<=_than rng Sups F
proof
let c;
assume c in rng Sups F;
then consider j being Element of J such that
A4: c = Sup(F.j) by Th14;
for f being Function st f in dom(Frege F) holds //\((Frege F).f, L) <= c
by A1,A4;
hence a <= c by Th15;
end;
then a <= inf rng Sups F by YELLOW_0:33;
hence thesis by YELLOW_2:def 6;
end;
theorem Th17:
(L is continuous & for c st c << a holds c <= b) implies a <= b
proof
assume that
A1: L is continuous and
A2: for c st c << a holds c <= b;
for c st c in waybelow a holds c <= b by A2,WAYBEL_3:7;
then waybelow a is_<=_than b;
then sup waybelow a <= b by YELLOW_0:32;
hence thesis by A1,WAYBEL_3:def 5;
end;
Lm8: L is continuous implies for J, K for F being DoubleIndexedSet of K, L st
for j being Element of J holds rng(F.j) is directed holds Inf Sups F = Sup Infs
Frege F
proof
assume
A1: L is continuous;
let J, K;
let F be DoubleIndexedSet of K, L such that
A2: for j being Element of J holds rng(F.j) is directed;
now
let c;
assume
A3: c << Inf Sups F;
A4: for j being Element of J holds c << Sup(F.j)
proof
let j be Element of J;
Sup(F.j) in rng Sups F by Th14;
then inf rng Sups F <= Sup(F.j) by YELLOW_2:22;
then Inf Sups F <= Sup(F.j) by YELLOW_2:def 6;
hence thesis by A3,WAYBEL_3:2;
end;
ex f being Function st f in dom(Frege F) & for j being Element of J ex
b st b = (F.j).(f.j) & c <= b
proof
defpred P[object, object] means
$1 in J & $2 in K.$1 & ex b st b = (F.$1).$2 &
c <= b;
A5: for j being Element of J ex k being Element of K.j st c <= (F.j).k
proof
let j be Element of J;
A6: Sup(F.j) <= sup(rng(F.j)) by YELLOW_2:def 5;
rng(F.j) is non empty directed Subset of L & c << Sup(F.j) by A2,A4;
then consider d being Element of L such that
A7: d in rng(F.j) and
A8: c <= d by A6,WAYBEL_3:def 1;
consider k being object such that
A9: k in dom(F.j) and
A10: d = (F.j).k by A7,FUNCT_1:def 3;
reconsider k as Element of K.j by A9;
take k;
thus thesis by A8,A10;
end;
A11: for j being object st j in J
ex k being object st k in union rng K & P[j, k]
proof
let j be object;
assume j in J;
then reconsider j9= j as Element of J;
consider k being Element of K.j9 such that
A12: c <= (F.j9).k by A5;
take k;
j9 in J;
then j9 in dom K by PARTFUN1:def 2;
then K.j9 in rng K by FUNCT_1:def 3;
hence k in union rng K by TARSKI:def 4;
thus thesis by A12;
end;
consider f being Function such that
A13: dom f = J and
rng f c= union rng K and
A14: for j being object st j in J holds P[j, f.j] from FUNCT_1:sch 6(
A11);
A15: now
let x be object;
assume x in dom doms F;
then
A16: x in dom F by FUNCT_6:59;
then reconsider j = x as Element of J;
(doms F).x = dom(F.j) by A16,FUNCT_6:22
.= K.j by FUNCT_2:def 1;
hence f.x in (doms F).x by A14;
end;
dom f = dom F by A13,PARTFUN1:def 2
.= dom doms F by FUNCT_6:59;
then f in product doms F by A15,CARD_3:9;
then
A17: f in dom(Frege F) by PARTFUN1:def 2;
for j being Element of J holds f.j in K.j & ex b st b = (F.j).(f.j)
& c <= b by A14;
hence thesis by A17;
end;
then consider f being Function such that
A18: f in dom(Frege F) and
A19: for j being Element of J ex b st b = (F.j).(f.j) & c <= b;
reconsider f as Element of product doms F by A18;
reconsider G = (Frege F).f as Function of J, the carrier of L;
now
let j be Element of J;
j in J;
then
A20: j in dom F by PARTFUN1:def 2;
ex b st b = (F.j).(f.j) & c <= b by A19;
hence c <= G.j by A18,A20,Th9;
end;
then
A21: c <= Inf((Frege F).f) by YELLOW_2:55;
set a = Inf((Frege F).f);
a in rng Infs Frege F by Th14;
then a <= sup rng Infs Frege F by YELLOW_2:22;
then a <= Sup Infs Frege F by YELLOW_2:def 5;
hence c <= Sup Infs Frege F by A21,YELLOW_0:def 2;
end;
then
A22: Inf Sups F <= Sup Infs Frege F by A1,Th17;
Inf Sups F >= Sup Infs Frege F by Th16;
hence thesis by A22,YELLOW_0:def 3;
end;
theorem Th18: ::Theorem 2.3 (2) implies (1)
(for J being non empty set st J in the_universe_of the carrier
of L for K being non-empty ManySortedSet of J st for j being Element of J holds
K.j in the_universe_of the carrier of L for F being DoubleIndexedSet of K, L st
for j being Element of J holds rng(F.j) is directed holds Inf Sups F = Sup Infs
Frege F) implies L is continuous
proof
assume
A1: for J being non empty set st J in the_universe_of the carrier of L
for K being non-empty ManySortedSet of J st for j being Element of J holds K.j
in the_universe_of the carrier of L for F being DoubleIndexedSet of K, L st (
for j being Element of J holds rng(F.j) is directed) holds Inf Sups F = Sup
Infs Frege F;
now
set UN = the_universe_of the carrier of L;
let x be Element of L;
set J = {j where j is directed non empty Subset of L : x <= sup j};
A2: UN = Tarski-Class the_transitive-closure_of the carrier of L by
YELLOW_6:def 1;
reconsider UN as universal set;
A3: J c= bool the carrier of L
proof
let u be object;
assume u in J;
then ex j being directed non empty Subset of L st u = j & x <= sup j;
hence thesis;
end;
the carrier of L c= the_transitive-closure_of the carrier of L &
the_transitive-closure_of the carrier of L in UN by A2,CLASSES1:2,52;
then
A4: the carrier of L in UN by CLASSES1:def 1;
then bool the carrier of L in UN by CLASSES2:59;
then
A5: J in UN by A3,CLASSES1:def 1;
x is_>=_than waybelow x by WAYBEL_3:9;
then
A6: x >= sup waybelow x by YELLOW_0:32;
{x} is directed non empty Subset of L & x <= sup {x} by WAYBEL_0:5
,YELLOW_0:39;
then
A7: {x} in J;
then reconsider J as non empty set;
set K = id J;
reconsider K as ManySortedSet of J;
A8: for j being Element of J holds K.j in UN
proof
let j be Element of J;
K.j in J;
hence thesis by A4,A3,CLASSES1:def 1;
end;
reconsider j = {x} as Element of J by A7;
A9: for j being Element of J holds j is directed non empty Subset of L
proof
let j be Element of J;
j in J;
then
ex j9 being directed non empty Subset of L st j9= j & x <= sup j9;
hence thesis;
end;
for i being object st i in J holds K.i is non empty
proof
let i be object;
assume i in J;
then reconsider i9= i as Element of J;
K.i = i9;
hence thesis by A9;
end;
then reconsider K as non-empty ManySortedSet of J by PBOOLE:def 13;
deffunc F(object) = id(K.$1);
ex F being Function st dom F = J & for j being object st j in J holds F.
j = F(j) from FUNCT_1:sch 3;
then consider F being Function such that
A10: dom F = J and
A11: for j being object st j in J holds F.j = id(K.j);
reconsider F as ManySortedSet of J by A10,PARTFUN1:def 2,RELAT_1:def 18;
for j being object st j in dom F holds F.j is Function
proof
let j be object;
assume j in dom F;
then F.j = id(K.j) by A11;
hence thesis;
end;
then reconsider F as ManySortedFunction of J by FUNCOP_1:def 6;
for j being object st j in J holds F.j is Function of K.j, (J --> the
carrier of L).j
proof
let j be object;
assume j in J;
then reconsider j as Element of J;
A12: K.j is Subset of L by A9;
A13: F.j = id(K.j) by A11;
then rng(F.j) c= K.j;
then rng(F.j) c= the carrier of L by A12,XBOOLE_1:1;
then
A14: rng(F.j) c= (J --> the carrier of L).j;
dom(F.j) = K.j by A13;
hence thesis by A14,FUNCT_2:2;
end;
then reconsider F as DoubleIndexedSet of K, L by PBOOLE:def 15;
A15: for j being Element of J, k being Element of K.j holds (F.j).k = k
proof
let j be Element of J;
let k be Element of K.j;
F.j = id(K.j) by A11;
hence thesis;
end;
A16: for j being Element of J holds rng(F.j) = j
proof
let j be Element of J;
now
let y be object;
assume y in rng(F.j);
then consider x being object such that
A17: x in dom(F.j) and
A18: y = (F.j).x by FUNCT_1:def 3;
x in K.j by A17;
then x in j;
hence y in j by A15,A18;
end;
then
A19: rng(F.j) c= j;
now
let x be object;
assume x in j;
then x in K.j;
then (F.j).x = x & x in dom(F.j) by A15,FUNCT_2:def 1;
hence x in rng(F.j) by FUNCT_1:def 3;
end;
then j c= rng(F.j);
hence thesis by A19,XBOOLE_0:def 10;
end;
A20: for j being Element of J holds rng(F.j) is directed
proof
let j be Element of J;
rng(F.j) = j by A16;
hence thesis by A9;
end;
for f being Function st f in dom(Frege F) holds //\((Frege F).f, L)
<= sup waybelow x
proof
let f be Function such that
A21: f in dom(Frege F);
set a = //\((Frege F).f, L);
for D being non empty directed Subset of L st x <= sup D ex d being
Element of L st d in D & a <= d
proof
A22: for j being Element of J holds f.j in K.j
proof
let j be Element of J;
j in J;
then j in dom F by PARTFUN1:def 2;
then f.j in dom(F.j) by A21,Th9;
hence thesis;
end;
A23: dom f = dom F by A21,Th8
.= J by PARTFUN1:def 2;
now
let y be object;
assume y in rng f;
then consider j being object such that
A24: j in dom f and
A25: y = f.j by FUNCT_1:def 3;
reconsider j as Element of J by A23,A24;
y in K.j by A22,A25;
then
A26: y in j;
j is Subset of L by A9;
hence y in the carrier of L by A26;
end;
then rng f c= the carrier of L;
then reconsider f as Function of J, the carrier of L by A23,FUNCT_2:2;
let D be non empty directed Subset of L;
assume x <= sup D;
then D in J;
then reconsider D9= D as Element of J;
A27: Inf f <= f.D9 by YELLOW_2:53;
f.D9 in K.D9 by A22;
then
A28: f.D9 in D9;
A29: now
let j be object;
assume
A30: j in dom f;
then reconsider j9= j as Element of J;
A31: f.j9 is Element of K.j9 by A22;
j in dom F by A21,A30,Th8;
hence ((Frege F).f).j = (F.j9).(f.j9) by A21,Th9
.= f.j by A15,A31;
end;
dom f = dom F by A21,Th8
.= dom((Frege F).f) by A21,Th8;
then a <= f.D9 by A27,A29,FUNCT_1:2;
hence thesis by A28;
end;
then a << x by WAYBEL_3:def 1;
then a in waybelow x by WAYBEL_3:7;
hence thesis by YELLOW_2:22;
end;
then
A32: Sup Infs Frege F <= sup waybelow x by Th15;
x is_<=_than rng Sups F
proof
let b be Element of L;
assume b in rng Sups F;
then consider j being Element of J such that
A33: b = Sup(F.j) by Th14;
j in J;
then consider j9 being directed non empty Subset of L such that
A34: j9= j and
A35: x <= sup j9;
b = sup rng(F.j) by A33,YELLOW_2:def 5
.= sup j9 by A16,A34;
hence x <= b by A35;
end;
then x <= inf rng Sups F by YELLOW_0:33;
then
A36: x <= Inf Sups F by YELLOW_2:def 6;
Sup(F.j) = sup rng(F.j) by YELLOW_2:def 5
.= sup {x} by A16
.= x by YELLOW_0:39;
then x in rng Sups F by Th14;
then inf rng Sups F <= x by YELLOW_2:22;
then Inf Sups F <= x by YELLOW_2:def 6;
then x = Inf Sups F by A36,ORDERS_2:2
.= Sup Infs Frege F by A1,A5,A8,A20;
hence x = sup waybelow x by A32,A6,ORDERS_2:2;
end;
then L is up-complete satisfying_axiom_of_approximation by WAYBEL_3:def 5;
hence thesis;
end;
Lm9: (for J, K for F being DoubleIndexedSet of K, L st for j being Element of
J holds rng(F.j) is directed holds Inf Sups F = Sup Infs Frege F) implies L is
continuous
proof
assume for J, K for F being DoubleIndexedSet of K, L st for j being Element
of J holds rng(F.j) is directed holds Inf Sups F = Sup Infs Frege F;
then
for J being non empty set st J in the_universe_of the carrier of L for K
being non-empty ManySortedSet of J st for j being Element of J holds K.j in
the_universe_of the carrier of L for F being DoubleIndexedSet of K, L st (for j
being Element of J holds rng(F.j) is directed) holds Inf Sups F = Sup Infs
Frege F;
hence thesis by Th18;
end;
theorem ::Theorem 2.3 (1) iff (2)
L is continuous iff for J, K for F being DoubleIndexedSet of K, L st
for j being Element of J holds rng(F.j) is directed holds Inf Sups F = Sup Infs
Frege F by Lm8,Lm9;
definition
let J, K, D be non empty set;
let F be Function of [:J, K:], D;
redefine func curry F -> DoubleIndexedSet of (J --> K), D; :: redefines curry (FUNCT_5, definition)
coherence
proof
reconsider F9= F as ManySortedSet of [:J, K:];
A1: dom F = [:J, K:] by FUNCT_2:def 1;
for j being object st j in J holds (curry F9).j is Function of (J --> K).
j, (J --> D).j
proof
let j be object;
assume
A2: j in J;
then consider g being Function such that
A3: (curry F9).j = g and
A4: dom g = K and
A5: rng g c= rng F9 and
for k being object st k in K holds g.k = F9.(j, k) by A1,FUNCT_5:29;
J = dom curry F by A1,FUNCT_5:24;
then reconsider G = (curry F9).j as Function;
rng F c= D;
then rng g c= D by A5;
then reconsider g as Function of K, D by A4,FUNCT_2:def 1,RELSET_1:4;
A6: G = g by A3;
(J --> K).j = K by A2,FUNCOP_1:7;
hence thesis by A2,A6,FUNCOP_1:7;
end;
hence thesis by PBOOLE:def 15;
end;
end;
reserve J, K, D for non empty set,
j for Element of J,
k for Element of K;
theorem Th20:
for F being Function of [:J, K:], D holds dom curry F = J & dom(
(curry F).j) = K & F.(j, k) = ((curry F).j).k
proof
let F be Function of [:J, K:], D;
thus dom curry F = proj1 dom F by FUNCT_5:def 1
.= proj1 [:J, K:] by FUNCT_2:def 1
.= J by FUNCT_5:9;
dom F = [:J, K:] by FUNCT_2:def 1;
then ex g being Function st (curry F).j = g & dom g = K & rng g c= rng F &
for i being object st i in K holds g.i = F.(j, i) by FUNCT_5:29;
hence dom((curry F).j) = K;
[j, k] in [:J, K:];
then [j, k] in dom F by FUNCT_2:def 1;
hence thesis by FUNCT_5:20;
end;
Lm10: (for J, K for F being Function of [:J, K:], the carrier of L st for j
being Element of J holds rng((curry F).j) is directed holds Inf Sups curry F =
Sup Infs Frege curry F) implies L is continuous
proof
assume
A1: for J, K for F being Function of [:J, K:], the carrier of L st for j
being Element of J holds rng((curry F).j) is directed holds Inf Sups (curry F)
= Sup Infs (Frege curry F);
for J for K being non-empty ManySortedSet of J for F being
DoubleIndexedSet of K, L st for j being Element of J holds rng(F.j) is directed
holds Inf Sups F = Sup Infs(Frege F)
proof
let J;
let K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, L;
set j = the Element of J;
set k = the Element of K.j;
defpred P[set, set, set] means $1 in J & (($2 in K.$1 & $3 = (F.$1).$2) or
(not $2 in K.$1 & $3 = Bottom L));
A2: dom doms F = dom F by FUNCT_6:59;
j in J;
then j in dom K by PARTFUN1:def 2;
then k in K.j & K.j in rng K by FUNCT_1:def 3;
then reconsider K9= union rng K as non empty set by TARSKI:def 4;
A3: dom F = J by PARTFUN1:def 2;
A4: for j being Element of J for k9 being Element of K9 ex z being Element
of L st P[j, k9, z]
proof
let j be Element of J;
let k9 be Element of K9;
per cases;
suppose
k9 in K.j;
then reconsider k = k9 as Element of K.j;
take (F.j).k;
thus thesis;
end;
suppose
A5: not k9 in K.j;
take Bottom L;
thus thesis by A5;
end;
end;
ex G being Function of [:J, K9:], the carrier of L st for j being
Element of J for k being Element of K9 holds P[j, k, G.(j, k)] from BINOP_1:sch
3(A4);
then consider G being Function of [:J, K9:], the carrier of L such that
A6: for j being Element of J for k being Element of K9 holds P[j, k, G.(j, k)];
A7: for j being Element of J holds K.j c= K9
proof
let j be Element of J;
hereby
let k be object;
j in J;
then j in dom K by PARTFUN1:def 2;
then
A8: K.j in rng K by FUNCT_1:def 3;
assume k in K.j;
hence k in K9 by A8,TARSKI:def 4;
end;
end;
A9: for j being Element of J holds rng(F.j) c= rng((curry G).j)
proof
let j be Element of J;
hereby
let y be object;
assume y in rng(F.j);
then consider k being object such that
A10: k in dom(F.j) and
A11: y = (F.j).k by FUNCT_1:def 3;
A12: k in K.j by A10;
K.j c= K9 by A7;
then reconsider k as Element of K9 by A12;
[j, k] in [:J, K9:];
then
A13: [j, k] in dom G by FUNCT_2:def 1;
k in K9 & dom((curry G).j) = (J --> K9).j by FUNCT_2:def 1;
then
A14: k in dom((curry G).j);
y = G.(j, k) by A6,A10,A11
.= ((curry G).j).k by A13,FUNCT_5:20;
hence y in rng((curry G).j) by A14,FUNCT_1:def 3;
end;
end;
A15: for j being object st j in dom F holds \\/(F.j, L) = \\/((curry G).j, L)
proof
let j9 be object;
assume j9 in dom F;
then reconsider j = j9 as Element of J;
reconsider H = (curry G).j as Function of (J --> K9).j, the carrier of L;
reconsider H as Function of K9, the carrier of L;
for k being Element of K9 holds H.k <= Sup(F.j)
proof
let k be Element of K9;
per cases;
suppose
A16: k in K.j;
then
A17: k in dom(F.j) by FUNCT_2:def 1;
(F.j).k = G.(j, k) by A6,A16
.= H.k by Th20;
then H.k in rng(F.j) by A17,FUNCT_1:def 3;
then H.k <= sup rng(F.j) by YELLOW_2:22;
hence thesis by YELLOW_2:def 5;
end;
suppose
not k in K.j;
then Bottom L = G.(j, k) by A6
.= H.k by Th20;
hence thesis by YELLOW_0:44;
end;
end;
then
A18: Sup H <= Sup(F.j) by YELLOW_2:54;
ex_sup_of rng(F.j),L & ex_sup_of rng((curry G).j), L by YELLOW_0:17;
then sup rng(F.j) <= sup rng((curry G).j) by A9,YELLOW_0:34;
then Sup(F.j) <= sup(rng H) by YELLOW_2:def 5;
then Sup(F.j) <= Sup H by YELLOW_2:def 5;
hence thesis by A18,ORDERS_2:2;
end;
A19: dom doms curry G = dom curry G by FUNCT_6:59;
A20: dom curry G = J by Th20;
product doms F c= product doms curry G
proof
let x be object;
assume x in product doms F;
then consider g being Function such that
A21: x = g and
A22: dom g = dom doms F and
A23: for j being object st j in dom doms F holds g.j in (doms F).j by
CARD_3:def 5;
A24: for j being object st j in dom doms curry G
holds g.j in (doms curry G ) . j
proof
let j be object;
assume
A25: j in dom doms curry G;
then reconsider j9 = j as Element of J by A19;
j in J by A19,A25;
then
A26: g.j in (doms F).j by A2,A3,A23;
A27: (doms F).j = dom(F.j9) by A3,FUNCT_6:22
.= K.j9 by FUNCT_2:def 1;
A28: K.j9 c= K9 by A7;
(doms curry G).j = dom((curry G).j9) by A20,FUNCT_6:22
.= K9 by Th20;
hence thesis by A26,A27,A28;
end;
dom g = dom doms curry G by A2,A3,A19,A22,Th20;
hence thesis by A21,A24,CARD_3:def 5;
end;
then dom(Frege F) c= product doms curry G;
then
A29: dom(Frege F) c= dom(Frege curry G) by PARTFUN1:def 2;
A30: for f being object st f in dom(Frege F) holds //\((Frege F).f, L) = //\(
(Frege curry G).f, L)
proof
let f9 be object;
assume
A31: f9 in dom(Frege F);
then reconsider f= f9 as Element of product doms F;
A32: dom((Frege F).f) = dom F by A31,Th8
.= J by PARTFUN1:def 2;
A33: for j being object st j in J holds ((Frege F).f).j = ((Frege curry G).
f ) . j
proof
let j9 be object;
assume j9 in J;
then reconsider j = j9 as Element of J;
A34: f.j in K.j by A31,Lm6;
K.j c= K9 by A7;
then reconsider fj = f.j as Element of K9 by A34;
((Frege F).f).j = (F.j).fj by A31,Lm5
.= G.(j, fj) by A6,A34
.= ((curry G).j).(f.j) by Th20
.= ((Frege curry G).f).j by A29,A31,Lm5;
hence thesis;
end;
dom((Frege curry G).f) = dom(curry G) by A29,A31,Th8
.= proj1 dom G by FUNCT_5:def 1
.= proj1 [:J, K9:] by FUNCT_2:def 1
.= J by FUNCT_5:9;
hence thesis by A32,A33,FUNCT_1:2;
end;
A35: Sup Infs(Frege curry G) = Sup Infs(Frege F)
proof
per cases;
suppose
A36: for j being Element of J holds K.j = K9;
for j being object st j in J holds (doms F).j = (doms curry G).j
proof
let j be object;
assume j in J;
then reconsider j9 = j as Element of J;
A37: (doms F).j = dom(F.j9) by A3,FUNCT_6:22
.= K.j9 by FUNCT_2:def 1;
(doms curry G).j = dom((curry G).j9) by A20,FUNCT_6:22
.= K9 by Th20;
hence thesis by A36,A37;
end;
then doms F = doms curry G by A2,A3,A19,A20,FUNCT_1:2;
then dom(Frege F) = product doms curry G by PARTFUN1:def 2;
then dom(Frege F) = dom(Frege curry G) by PARTFUN1:def 2;
hence thesis by A30,Th12;
end;
suppose
ex j being Element of J st K.j <> K9;
then consider j being Element of J such that
A38: K.j <> K9;
K.j c= K9 by A7;
then not K9 c= K.j by A38,XBOOLE_0:def 10;
then consider k being object such that
A39: k in K9 and
A40: not k in K.j;
reconsider k as Element of K9 by A39;
A41: rng Infs(Frege F) \/ {Bottom L} c= rng Infs(Frege curry G)
proof
let x be object;
assume
A42: x in rng Infs(Frege F) \/ {Bottom L};
per cases by A42,XBOOLE_0:def 3;
suppose
x in rng Infs(Frege F);
then consider f being object such that
A43: f in dom Frege F and
A44: x = //\((Frege F).f, L) by Th13;
x = //\((Frege curry G).f, L) by A30,A43,A44;
hence thesis by A29,A43,Th13;
end;
suppose
A45: x in {Bottom L};
then reconsider x9 = x as Element of L;
set f = J --> k;
A46: for x being object st x in dom doms curry G
holds f.x in (doms curry G).x
proof
let x be object;
assume x in dom doms curry G;
then reconsider j = x as Element of J by A19;
(doms curry G).j = dom((curry G).j) by A20,FUNCT_6:22
.= K9 by Th20;
hence thesis;
end;
dom f = J
.= dom doms curry G by A19,Th20;
then f in product doms curry G by A46,CARD_3:9;
then
A48: f in dom Frege curry G by PARTFUN1:def 2;
A49: x = Bottom L by A45,TARSKI:def 1;
then x = G.(j, k) by A6,A40
.= ((curry G).j).k by Th20
.= ((curry G).j).(f.j);
then x in rng((Frege curry G).f) by A48,Lm5;
then x9 >= "/\"(rng((Frege curry G).f), L) by YELLOW_2:22;
then
A50: x9 >= //\((Frege curry G).f, L) by YELLOW_2:def 6;
x9 <= //\((Frege curry G).f, L) by A49,YELLOW_0:44;
then x9 = //\((Frege curry G).f, L) by A50,ORDERS_2:2;
hence thesis by A48,Th13;
end;
end;
A51: ex_sup_of rng Infs(Frege F), L & ex_sup_of {Bottom L}, L by YELLOW_0:17
;
A52: rng Infs(Frege curry G) c= rng Infs(Frege F) \/ {Bottom L}
proof
let x be object;
assume x in rng Infs(Frege curry G);
then consider f being object such that
A53: f in dom Frege curry G and
A54: x = //\((Frege curry G).f, L) by Th13;
reconsider f as Function by A53;
per cases;
suppose
A55: for j being Element of J holds f.j in K.j;
A56: for x being object st x in dom doms F holds f.x in (doms F).x
proof
let x be object;
assume x in dom doms F;
then reconsider j = x as Element of J by A3,FUNCT_6:59;
(doms F).j = dom(F.j) by A3,FUNCT_6:22
.= K.j by FUNCT_2:def 1;
hence thesis by A55;
end;
dom f = dom curry G by A53,Th8
.= dom doms F by A2,A3,Th20;
then f in product doms F by A56,CARD_3:9;
then
A57: f in dom Frege F by PARTFUN1:def 2;
then x = //\((Frege F).f, L) by A30,A54;
then x in rng Infs(Frege F) by A57,Th13;
hence thesis by XBOOLE_0:def 3;
end;
suppose
ex j being Element of J st not f.j in K.j;
then consider j being Element of J such that
A58: not f.j in K.j;
j in J;
then j in dom curry G by Th20;
then f.j in dom((curry G).j) by A53,Th9;
then reconsider k = f.j as Element of K9;
Bottom L = G.(j, k) by A6,A58
.= ((curry G).j).(f.j) by Th20;
then Bottom L in rng((Frege curry G).f) by A53,Lm5;
then Bottom L >= "/\"(rng((Frege curry G).f), L) by YELLOW_2:22;
then
A59: Bottom L >= //\((Frege curry G).f, L) by YELLOW_2:def 6;
Bottom L <= //\((Frege curry G).f, L) by YELLOW_0:44;
then x = Bottom L by A54,A59,ORDERS_2:2;
then x in {Bottom L} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
A60: Bottom L <= Sup Infs(Frege F) by YELLOW_0:44;
Sup Infs Frege curry G = sup rng Infs Frege curry G by YELLOW_2:def 5
.= sup(rng Infs(Frege F) \/ {Bottom L}) by A52,A41,XBOOLE_0:def 10
.= sup rng Infs(Frege F) "\/" sup{Bottom L} by A51,YELLOW_2:3
.= sup rng Infs(Frege F) "\/" Bottom L by YELLOW_0:39
.= Sup Infs(Frege F) "\/" Bottom L by YELLOW_2:def 5
.= Sup Infs(Frege F) by A60,YELLOW_0:24;
hence thesis;
end;
end;
assume
A61: for j being Element of J holds rng(F.j) is directed;
A62: for j being Element of J holds rng((curry G).j) is directed
proof
let j be Element of J;
set X = rng((curry G).j);
for x, y being Element of L st x in X & y in X ex z being Element
of L st z in X & x <= z & y <= z
proof
A63: rng(F.j) is directed by A61;
let x, y be Element of L;
assume that
A64: x in X and
A65: y in X;
consider b being object such that
A66: b in dom((curry G).j) and
A67: ((curry G).j).b = y by A65,FUNCT_1:def 3;
consider a being object such that
A68: a in dom((curry G).j) and
A69: ((curry G).j).a = x by A64,FUNCT_1:def 3;
reconsider a9= a, b9= b as Element of K9 by A68,A66;
A70: x = G.(j, a9) by A69,Th20;
A71: y = G.(j, b9) by A67,Th20;
per cases;
suppose
A72: a in K.j & b in K.j;
then b in dom(F.j) & y = (F.j).b9 by A6,A71,FUNCT_2:def 1;
then
A73: y in rng(F.j) by FUNCT_1:def 3;
a in dom(F.j) & x = (F.j).a9 by A6,A70,A72,FUNCT_2:def 1;
then x in rng(F.j) by FUNCT_1:def 3;
then consider z being Element of L such that
A74: z in rng(F.j) & x <= z & y <= z by A63,A73,WAYBEL_0:def 1;
take z;
rng(F.j) c= X by A9;
hence thesis by A74;
end;
suppose
A75: a in K.j & not b in K.j;
take x;
y = Bottom L by A6,A71,A75;
hence thesis by A64,YELLOW_0:44;
end;
suppose
A76: not a in K.j & b in K.j;
take y;
x = Bottom L by A6,A70,A76;
hence thesis by A65,YELLOW_0:44;
end;
suppose
A77: not a in K.j & not b in K.j;
take x;
x = Bottom L by A6,A70,A77;
hence thesis by A6,A64,A71,A77;
end;
end;
hence thesis by WAYBEL_0:def 1;
end;
dom F = J by PARTFUN1:def 2
.= dom curry G by PARTFUN1:def 2;
hence Inf Sups F = Inf Sups(curry G) by A15,Th11
.= Sup Infs(Frege F) by A1,A62,A35;
end;
hence thesis by Lm9;
end;
theorem ::Theorem 2.3 (1) iff (2')
L is continuous iff for J, K being non empty set for F being Function
of [:J, K:], the carrier of L st for j being Element of J holds rng((curry F).j
) is directed holds Inf Sups curry F = Sup Infs Frege curry F by Lm8,Lm10;
Lm11: for f being Function st f in Funcs(J, Fin K) holds for j holds f.j is
finite Subset of K
proof
let f be Function;
assume f in Funcs(J, Fin K);
then
A1: ex f9 being Function st f9 = f & dom f9 = J & rng f9 c= Fin K by
FUNCT_2:def 2;
for j holds f.j is finite Subset of K
proof
let j;
f.j in rng f by A1,FUNCT_1:def 3;
hence thesis by A1,FINSUB_1:def 5;
end;
hence thesis;
end;
Lm12: for F being Function of [:J, K:], D for f being non-empty ManySortedSet
of J st f in Funcs(J, Fin K) for G being DoubleIndexedSet of f, L st for j, x
st x in f.j holds (G.j).x = F.(j, x) holds rng(G.j) is finite Subset of rng((
curry F).j)
proof
let F be Function of [:J, K:], D;
let f be non-empty ManySortedSet of J;
assume f in Funcs(J, Fin K);
then
A1: f.j is finite Subset of K by Lm11;
let G be DoubleIndexedSet of f, L such that
A2: for j, x st x in f.j holds (G.j).x = F.(j, x);
rng(G.j) c= rng((curry F).j)
proof
let y be object;
assume y in rng(G.j);
then consider k being object such that
A3: k in dom(G.j) and
A4: y = (G.j).k by FUNCT_1:def 3;
A5: k in f.j by A3;
then
A6: k in K by A1;
reconsider k as Element of K by A1,A5;
A7: k in dom((curry F).j) by A6,Th20;
y = F.(j, k) by A2,A3,A4
.= ((curry F).j).k by Th20;
hence thesis by A7,FUNCT_1:def 3;
end;
hence thesis by A1;
end;
theorem Th22:
for F being Function of [:J, K:], the carrier of L for X being
Subset of L st X = {a where a is Element of L: ex f being non-empty
ManySortedSet of J st f in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f,
L st (for j, x st x in f.j holds (G.j).x = F.(j, x)) & a = Inf Sups G} holds
Inf Sups curry F >= sup X
proof
let F be Function of [:J, K:], the carrier of L;
let X be Subset of L;
A1: for f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) for G
being DoubleIndexedSet of f, L st for j, x st x in f.j holds (G.j).x = F.(j, x)
for j holds Sup((curry F).j) >= Sup(G.j)
proof
let f be non-empty ManySortedSet of J such that
A2: f in Funcs(J, Fin K);
let G be DoubleIndexedSet of f, L such that
A3: for j, x st x in f.j holds (G.j).x = F.(j, x);
let j;
A4: ex_sup_of rng((curry F).j), L & ex_sup_of rng(G.j),L by YELLOW_0:17;
rng(G.j) is Subset of rng((curry F).j) by A2,A3,Lm12;
then sup rng((curry F).j) >= sup rng(G.j) by A4,YELLOW_0:34;
then Sup((curry F).j) >= sup rng(G.j) by YELLOW_2:def 5;
hence thesis by YELLOW_2:def 5;
end;
A5: for f being non-empty ManySortedSet of J st f in Funcs(J, Fin K) for G
being DoubleIndexedSet of f, L st for j, x st x in f.j holds (G.j).x = F.(j, x)
holds Inf Sups curry F >= Inf Sups G
proof
let f be non-empty ManySortedSet of J such that
A6: f in Funcs(J, Fin K);
let G be DoubleIndexedSet of f, L such that
A7: for j, x st x in f.j holds (G.j).x = F.(j, x);
rng Sups curry F is_>=_than Inf Sups G
proof
let a;
assume a in rng Sups curry F;
then consider j being Element of J such that
A8: a = Sup((curry F).j) by Th14;
Sup(G.j) in rng Sups G by Th14;
then Sup(G.j) >= inf rng Sups G by YELLOW_2:22;
then
A9: Sup(G.j) >= Inf Sups G by YELLOW_2:def 6;
Sup((curry F).j) >= Sup(G.j) by A1,A6,A7;
hence thesis by A8,A9,ORDERS_2:3;
end;
then inf rng Sups curry F >= Inf Sups G by YELLOW_0:33;
hence thesis by YELLOW_2:def 6;
end;
assume
A10: X = {a where a is Element of L: ex f being non-empty ManySortedSet
of J st f in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f, L st (for j, x
st x in f.j holds (G.j).x = F.(j, x)) & a = Inf Sups G};
Inf Sups curry F is_>=_than X
proof
let a;
assume a in X;
then ex a9 being Element of L st a9 = a & ex f being non-empty
ManySortedSet of J st f in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f,
L st (for j, x st x in f.j holds (G.j).x = F.(j, x)) & a9 = Inf Sups G by A10;
hence thesis by A5;
end;
hence thesis by YELLOW_0:32;
end;
Lm13: L is continuous implies for J, K for F being Function of [:J, K:], the
carrier of L for X being Subset of L st X = {a where a is Element of L: ex f
being non-empty ManySortedSet of J st f in Funcs(J, Fin K) & ex G being
DoubleIndexedSet of f, L st (for j, x st x in f.j holds (G.j).x = F.(j, x)) & a
= Inf Sups G} holds Inf Sups curry F = sup X
proof
assume
A1: L is continuous;
hereby
let J, K;
set FIK = {A where A is Subset of K: A is finite & A <> {}};
set k = the Element of K;
{k} in FIK;
then reconsider FIK as non empty set;
let F be Function of [:J, K:], the carrier of L;
let X be Subset of L;
set N = Funcs(J, FIK);
deffunc F(Element of J, Element of N) = sup(((curry F).$1).:($2.$1));
ex H being Function of [:J, N:], the carrier of L st for j being
Element of J for g being Element of N holds H.(j, g) = F(j,g) from BINOP_1:sch
4;
then consider H being Function of [:J, N:], the carrier of L such that
A2: for j for g being Element of N holds H.(j, g) = sup(((curry F).j) .:(g.j));
set cF = curry F, cH = curry H;
A3: for j holds (for Y being finite Subset of rng(cF.j) st Y <> {} holds
ex_sup_of Y,L) & (for x being Element of L st x in rng(cH.j) ex Y being finite
Subset of rng(cF.j) st ex_sup_of Y,L & x = "\/"(Y,L)) & for Y being finite
Subset of rng(cF.j) st Y <> {} holds "\/"(Y,L) in rng(cH.j)
proof
let j;
set D = rng((curry H).j), R = rng((curry F).j);
set Hj = (curry H).j, Fj = (curry F).j;
thus for Y being finite Subset of R st Y <> {} holds ex_sup_of Y,L by
YELLOW_0:17;
thus for x being Element of L st x in D ex Y being finite Subset of R st
ex_sup_of Y,L & x = "\/"(Y,L)
proof
let x be Element of L;
assume x in D;
then consider g being object such that
A4: g in dom Hj and
A5: Hj.g = x by FUNCT_1:def 3;
reconsider g as Element of N by A4;
g.j in FIK;
then ex A being Subset of K st A = g.j & A is finite & A <> {};
then reconsider Y = Fj.:(g.j) as finite Subset of R by RELAT_1:111;
take Y;
x = H.(j, g) by A5,Th20
.= sup(Fj.:(g.j)) by A2;
hence thesis by YELLOW_0:17;
end;
thus for Y being finite Subset of R st Y <> {} holds "\/"(Y,L) in D
proof
let Y be finite Subset of R;
consider Z being set such that
A6: Z c= dom Fj and
A7: Z is finite and
A8: Fj.:Z = Y by ORDERS_1:85;
A9: Z c= K by A6,Th20;
assume Y <> {};
then Z <> {} by A8;
then Z in FIK by A7,A9;
then
A10: {Z} c= FIK by ZFMISC_1:31;
dom(J --> Z) = J & rng(J --> Z) = {Z} by FUNCOP_1:8;
then reconsider g = J --> Z as Element of N by A10,FUNCT_2:def 2;
A11: g.j = Z;
g in N;
then
A12: g in dom Hj by Th20;
Hj.g = H.(j, g) by Th20
.= "\/"(Y, L) by A2,A8,A11;
hence thesis by A12,FUNCT_1:def 3;
end;
end;
for j holds rng((curry H).j) is directed
proof
let j;
A13: for Y being finite Subset of rng(cF.j) st Y <> {} holds "\/"(Y,L)
in rng(cH.j) by A3;
( for Y being finite Subset of rng(cF.j) st Y <> {} holds ex_sup_of
Y,L)& for x being Element of L st x in rng(cH.j) ex Y being finite Subset of
rng(cF.j) st ex_sup_of Y,L & x = "\/"(Y,L) by A3;
hence thesis by A13,WAYBEL_0:51;
end;
then
A14: Inf Sups curry H = Sup Infs Frege curry H by A1,Lm8;
A15: for j being object st j in dom curry F holds \\/((curry F).j, L) = \\/((
curry H).j, L)
proof
let j9 be object;
assume j9 in dom curry F;
then reconsider j = j9 as Element of J;
A16: ( for x being Element of L st x in rng(cH.j) ex Y being finite
Subset of rng(cF .j) st ex_sup_of Y,L & x = "\/"(Y,L))& for Y being finite
Subset of rng(cF.j) st Y <> {} holds "\/"(Y,L) in rng(cH.j) by A3;
ex_sup_of rng(cF.j),L & for Y being finite Subset of rng(cF.j) st Y
<> {} holds ex_sup_of Y,L by YELLOW_0:17;
then sup(rng(cF.j)) = sup(rng(cH.j)) by A16,WAYBEL_0:54;
then Sup(cF.j) = sup(rng(cH.j)) by YELLOW_2:def 5;
hence thesis by YELLOW_2:def 5;
end;
assume
A17: X = {a where a is Element of L: ex f being non-empty ManySortedSet
of J st f in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f, L st (for j, x
st x in f.j holds (G.j).x = F.(j, x)) & a = Inf Sups G};
then
A18: Inf Sups curry F >= sup X by Th22;
A19: FIK c= Fin K
proof
let x be object;
assume x in FIK;
then ex A being Subset of K st x = A & A is finite & A <> {};
hence thesis by FINSUB_1:def 5;
end;
A20: for h being Function-yielding Function st h in product doms curry H
holds (for j holds ((Frege h).(id J)).j = (h.j).j & h.j in N & ((Frege h).(id J
)).j is finite non empty Subset of K) & (Frege h).(id J) is non-empty
ManySortedSet of J & (Frege h).(id J) in Funcs(J, FIK) & (Frege h).(id J) in
Funcs(J, Fin K)
proof
let h be Function-yielding Function;
set f = (Frege h).(id J);
assume h in product doms curry H;
then
A21: h in dom Frege curry H by PARTFUN1:def 2;
then
A22: dom h = dom curry H by Th8
.= J by Th20;
A23: for x being object st x in dom doms h holds (id J).x in (doms h).x
proof
let x be object;
assume x in dom doms h;
then reconsider j = x as Element of J by A22,FUNCT_6:59;
h.j in (J --> N).j by A21,Lm6;
then h.j in N;
then ex g being Function st g = h.j & dom g = J & rng g c= FIK by
FUNCT_2:def 2;
then (id J).j = j & (doms h).j = J by A22,FUNCT_6:22;
hence thesis;
end;
dom id J = J & dom doms h = dom h by FUNCT_6:59;
then id J in product doms h by A22,A23,CARD_3:9;
then
A24: id J in dom Frege h by PARTFUN1:def 2;
then
A25: dom f = J by A22,Th8;
then reconsider f9= f as ManySortedSet of J by PARTFUN1:def 2
,RELAT_1:def 18;
thus
A26: for j holds ((Frege h).(id J)).j = (h.j).j & h.j in N & ((
Frege h).(id J)).j is finite non empty Subset of K
proof
let j;
thus
A27: ((Frege h).(id J)).j = (h.j).((id J).j) by A22,A24,Th9
.= (h.j).j;
h.j in (J --> N).j by A21,Lm6;
hence h.j in N;
then consider g being Function such that
A28: g = h.j & dom g = J and
A29: rng g c= FIK by FUNCT_2:def 2;
f.j in rng g by A27,A28,FUNCT_1:def 3;
then f.j in FIK by A29;
then ex A being Subset of K st f.j = A & A is finite & A <> {};
hence thesis;
end;
then for j being object st j in J holds f9.j is non empty;
hence f is non-empty ManySortedSet of J by PBOOLE:def 13;
A30: rng f c= FIK
proof
let y be object;
assume y in rng f;
then consider j being object such that
A31: j in dom f and
A32: y = f.j by FUNCT_1:def 3;
f.j is finite non empty Subset of K by A26,A25,A31;
hence thesis by A32;
end;
hence f in Funcs(J, FIK) by A25,FUNCT_2:def 2;
rng f c= Fin K by A19,A30;
hence thesis by A25,FUNCT_2:def 2;
end;
A33: for h being Element of product doms curry H holds Inf((Frege curry H)
.h) <= sup X
proof
defpred P[object,object,object] means $1 = F.($3, $2);
let h be Element of product doms curry H;
h in product doms curry H;
then
A34: h in dom Frege curry H by PARTFUN1:def 2;
for x being object st x in dom h holds h.x is Function
proof
let x be object;
assume
A35: x in dom h;
dom h = dom curry H by A34,Th8
.= J by Th20;
then reconsider j = x as Element of J by A35;
h.j in (J --> N).j by A34,Lm6;
then h.j in N;
hence thesis;
end;
then reconsider h9= h as Function-yielding Function by FUNCOP_1:def 6;
reconsider f = (Frege h9).(id J) as non-empty ManySortedSet of J by A20;
A36: for j being object st j in J
for x being object st x in f.j ex y being object st y in (J
--> the carrier of L).j & P[y,x,j]
proof
let i be object;
assume i in J;
then reconsider j = i as Element of J;
let x be object;
assume
A37: x in f.i;
f.j is Subset of K by A20;
then reconsider k = x as Element of K by A37;
take y = F.[j, k];
thus thesis;
end;
ex G being ManySortedFunction of f, (J --> the carrier of L) st
for
j being object st j in J
ex g being Function of f.j, (J --> the carrier of L
).j st g = G.j & for x being object st x in f.j holds P[g.x,x,j]
from MSSUBFAM:sch 1(A36);
then consider
G being ManySortedFunction of f, (J --> the carrier of L) such
that
A38: for j being object st j in J holds ex g being Function of f.j, (J
--> the carrier of L).j st g = G.j &
for x being object st x in f.j holds g.x = F.(j, x);
reconsider G as DoubleIndexedSet of f, L;
A39: for j, x st x in f.j holds (G.j).x = F.(j, x)
proof
let j, x;
assume
A40: x in f.j;
ex g being Function of f.j, (J --> the carrier of L).j st g = G.j
& for x being object st x in f.j holds g.x = F.(j, x) by A38;
hence thesis by A40;
end;
Inf((Frege curry H).h) is_<=_than rng Sups G
proof
let y be Element of L;
assume y in rng Sups G;
then consider j such that
A41: y = Sup(G.j) by Th14;
j in J;
then
A42: j in dom curry H by Th20;
A43: (curry F.j).:(f.j) c= rng(G.j)
proof
let y be object;
assume y in (curry F.j).:(f.j);
then consider x being object such that
A44: x in dom((curry F).j) and
A45: x in f.j and
A46: y = ((curry F).j).x by FUNCT_1:def 6;
reconsider k = x as Element of K by A44;
A47: k in dom(G.j) by A45,FUNCT_2:def 1;
y = F.(j, k) by A46,Th20
.= (G.j).k by A39,A45;
hence thesis by A47,FUNCT_1:def 3;
end;
ex_sup_of ((curry F.j).:(f.j)),L & ex_sup_of rng(G.j),L by YELLOW_0:17;
then sup((curry F.j).:(f.j)) <= sup rng(G.j) by A43,YELLOW_0:34;
then
A48: sup((curry F.j).:(f.j)) <= Sup(G.j) by YELLOW_2:def 5;
h.j in (J --> N).j by A34,Lm6;
then reconsider hj = h.j as Element of N;
A49: Inf((Frege curry H).h) <= ((Frege curry H).h).j by YELLOW_2:53;
sup((curry F.j).:(f.j)) = sup((curry F.j).:(hj.j)) by A20
.= H.(j, hj) by A2
.= ((curry H).j).(h.j) by Th20
.= ((Frege curry H).h).j by A34,A42,Th9;
hence Inf((Frege curry H).h) <= y by A41,A48,A49,ORDERS_2:3;
end;
then Inf((Frege curry H).h) <= inf rng Sups G by YELLOW_0:33;
then
A50: Inf((Frege curry H).h) <= Inf Sups G by YELLOW_2:def 6;
f in Funcs(J, Fin K) by A20;
then Inf Sups G in X by A17,A39;
then Inf Sups G <= sup X by YELLOW_2:22;
hence thesis by A50,ORDERS_2:3;
end;
rng Infs Frege curry H is_<=_than sup X
proof
let x be Element of L;
assume x in rng Infs Frege curry H;
then consider h being object such that
A51: h in dom Frege curry H and
A52: x = //\((Frege curry H).h, L) by Th13;
reconsider h as Element of product doms curry H by A51;
Inf((Frege curry H).h) <= sup X by A33;
hence thesis by A52;
end;
then
A53: sup rng Infs Frege curry H <= sup X by YELLOW_0:32;
dom curry F = J by Th20
.= dom curry H by Th20;
then Inf Sups curry F = Inf Sups curry H by A15,Th11;
then Inf Sups curry F <= sup X by A14,A53,YELLOW_2:def 5;
hence Inf Sups curry F = sup X by A18,ORDERS_2:2;
end;
end;
Lm14: (for J, K for F being Function of [:J, K:], the carrier of L for X being
Subset of L st X = {a where a is Element of L: ex f being non-empty
ManySortedSet of J st f in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f,
L st (for j, x st x in f.j holds (G.j).x = F.(j, x)) & a = Inf Sups G} holds
Inf Sups curry F = sup X) implies L is continuous
proof
assume
A1: for J, K for F being Function of [:J, K:], the carrier of L for X
being Subset of L st X = {a where a is Element of L: ex f being non-empty
ManySortedSet of J st f in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f,
L st (for j, x st x in f.j holds (G.j).x = F.(j, x)) & a = Inf Sups G} holds
Inf Sups curry F = sup X;
for J, K for F being Function of [:J, K:], the carrier of L st for j
being Element of J holds rng((curry F).j) is directed holds Inf Sups curry F =
Sup Infs Frege curry F
proof
let J, K;
let F be Function of [:J, K:], the carrier of L such that
A2: for j being Element of J holds rng((curry F).j) is directed;
defpred P[Element of L] means ex f being non-empty ManySortedSet of J st f
in Funcs(J, Fin K) & ex G being DoubleIndexedSet of f, L st (for j, x st x in f
.j holds (G.j).x = F.(j, x)) & $1 = Inf Sups G;
reconsider X = {a where a is Element of L: P[a]} as Subset of L from
DOMAIN_1:sch 7;
X is_<=_than Sup Infs Frege curry F
proof
let a9 be Element of L;
assume a9 in X;
then consider a being Element of L such that
A3: a9 = a and
A4: ex f being non-empty ManySortedSet of J st f in Funcs(J, Fin K)
& ex G being DoubleIndexedSet of f, L st (for j, x st x in f.j holds (G.j).x =
F.(j, x)) & a = Inf Sups G;
defpred P[object, object] means
$1 in J & $2 in K & ex b st b = ((curry F).$1)
.$2 & a <= b;
consider f being non-empty ManySortedSet of J such that
A5: f in Funcs(J, Fin K) and
A6: ex G being DoubleIndexedSet of f, L st (for j, x st x in f.j
holds (G.j).x = F.(j, x)) & a = Inf Sups G by A4;
consider G being DoubleIndexedSet of f, L such that
A7: for j, x st x in f.j holds (G.j).x = F.(j, x) and
A8: a = Inf Sups G by A6;
A9: for x being object st x in J ex y being object st y in K & P[x, y]
proof
let x be object;
assume x in J;
then reconsider j = x as Element of J;
Sup(G.j) in rng Sups G by Th14;
then inf rng Sups G <= Sup(G.j) by YELLOW_2:22;
then
A10: Inf Sups G <= Sup(G.j) by YELLOW_2:def 6;
rng((curry F).j) is non empty directed & rng(G.j) is finite
Subset of rng(( curry F).j) by A2,A5,A7,Lm12;
then consider y being Element of L such that
A11: y in rng((curry F).j) and
A12: rng(G.j) is_<=_than y by WAYBEL_0:1;
consider k being object such that
A13: k in dom((curry F).j) and
A14: y = ((curry F).j).k by A11,FUNCT_1:def 3;
reconsider k as Element of K by A13;
take k;
sup rng(G.j) <= y by A12,YELLOW_0:32;
then Sup(G.j) <= y by YELLOW_2:def 5;
hence thesis by A8,A14,A10,ORDERS_2:3;
end;
consider g being Function such that
A15: dom g = J and
rng g c= K and
A16: for x being object st x in J holds P[x, g.x] from FUNCT_1:sch 6(A9);
A17: dom doms curry F = dom curry F by FUNCT_6:59;
then
A18: dom g = dom doms curry F by A15,Th20;
for x being object st x in dom doms curry F
holds g.x in (doms curry F).x
proof
let x be object;
assume x in dom doms curry F;
then reconsider j = x as Element of J by A17;
dom curry F = J by Th20;
then (doms curry F).j = dom((curry F).j) by FUNCT_6:22
.= K by Th20;
hence thesis by A16;
end;
then reconsider g as Element of product doms curry F by A18,CARD_3:9;
for j holds a <= ((Frege curry F).g).j
proof
let j;
A19: ex b st b = ((curry F).j).(g.j) & a <= b by A16;
dom Frege curry F = product doms curry F & J = dom curry F by
PARTFUN1:def 2;
hence thesis by A19,Th9;
end;
then
A20: a <= Inf((Frege curry F).g) by YELLOW_2:55;
Inf((Frege curry F).g) in rng Infs Frege curry F by Th14;
then Inf((Frege curry F).g) <= sup rng Infs Frege curry F by YELLOW_2:22;
then Inf((Frege curry F).g) <= Sup Infs Frege curry F by YELLOW_2:def 5;
hence a9 <= Sup Infs Frege curry F by A3,A20,ORDERS_2:3;
end;
then sup X <= Sup Infs Frege curry F by YELLOW_0:32;
then
A21: Inf Sups curry F <= Sup Infs Frege curry F by A1;
Inf Sups curry F >= Sup Infs Frege curry F by Th16;
hence thesis by A21,ORDERS_2:2;
end;
hence thesis by Lm10;
end;
theorem ::Theorem 2.3 (1) iff (3)
L is continuous iff for J, K for F being Function of [:J, K:], the
carrier of L for X being Subset of L st X = {a where a is Element of L: ex f
being non-empty ManySortedSet of J st f in Funcs(J, Fin K) & ex G being
DoubleIndexedSet of f, L st (for j, x st x in f.j holds (G.j).x = F.(j, x)) & a
= Inf Sups G} holds Inf Sups curry F = sup X by Lm13,Lm14;
begin :: Completely-Distributive Lattices
definition
let L be non empty RelStr;
attr L is completely-distributive means
:Def3:
L is complete & for J being
non empty set, K being non-empty ManySortedSet of J for F being
DoubleIndexedSet of K, L holds Inf Sups F = Sup Infs Frege F;
end;
reserve J for non empty set,
K for non-empty ManySortedSet of J;
registration
cluster -> completely-distributive for 1-element Poset;
coherence
proof
let L be 1-element Poset;
reconsider L9= L as complete LATTICE;
thus L is complete;
reconsider L9 as continuous LATTICE;
for J being non empty set, K being non-empty ManySortedSet of J for F
being DoubleIndexedSet of K, L9 holds Inf Sups F = Sup Infs(Frege F)
proof
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, L9;
for j being Element of J holds rng(F.j) is directed;
hence thesis by Lm8;
end;
hence thesis;
end;
end;
registration
cluster completely-distributive for LATTICE;
existence
proof
set x = the set,R = the Order of {x};
RelStr(#{x},R#) is 1-element RelStr;
hence thesis;
end;
end;
theorem Th24: ::Corollary 2.5
for L being completely-distributive LATTICE holds L is continuous
proof
let L be completely-distributive LATTICE;
A1: for F being DoubleIndexedSet of K, L st for j being Element of J holds
rng(F.j) is directed holds Inf Sups F = Sup Infs Frege F by Def3;
L is complete by Def3;
hence thesis by A1,Lm9;
end;
registration
cluster completely-distributive -> complete continuous for LATTICE;
correctness by Th24;
end;
theorem Th25:
for L being non empty antisymmetric transitive with_infima
RelStr for x being Element of L for X, Y being Subset of L st ex_sup_of X,L &
ex_sup_of Y,L & Y = {x"/\"y where y is Element of L: y in X} holds x "/\" sup X
>= sup Y
proof
let L be non empty antisymmetric transitive with_infima RelStr;
let x be Element of L;
let X, Y be Subset of L such that
A1: ex_sup_of X,L and
A2: ex_sup_of Y,L and
A3: Y = {x"/\"y where y is Element of L: y in X};
Y is_<=_than (x "/\" sup X)
proof
let y be Element of L;
assume y in Y;
then consider z being Element of L such that
A4: y = x "/\" z and
A5: z in X by A3;
A6: y <= z by A4,YELLOW_0:23;
X is_<=_than sup X by A1,YELLOW_0:30;
then z <= sup X by A5;
then
A7: y <= sup X by A6,YELLOW_0:def 2;
y <= x by A4,YELLOW_0:23;
hence thesis by A7,YELLOW_0:23;
end;
hence thesis by A2,YELLOW_0:30;
end;
Lm15: for L being completely-distributive LATTICE for X being non empty Subset
of L for x being Element of L holds x "/\" sup X = "\/"({x"/\"y where y is
Element of L: y in X}, L)
proof
let L be completely-distributive LATTICE;
let X be non empty Subset of L;
let x be Element of L;
set A = {x"/\"y where y is Element of L: y in X};
set J = {1, 2}, K = (1, 2) --> ({1}, X);
set F = (1, 2) --> ({1} --> x, id X);
A1: F.1 = {1} --> x by FUNCT_4:63;
A2: dom K = J by FUNCT_4:62;
A3: K.2 = X by FUNCT_4:63;
A4: dom F = J by FUNCT_4:62;
reconsider j1 = 1, j2 = 2 as Element of J by TARSKI:def 2;
A5: F.2 = id X by FUNCT_4:63;
reconsider F as ManySortedSet of J by A4,PARTFUN1:def 2,RELAT_1:def 18;
A6: K.1 = {1} by FUNCT_4:63;
reconsider K as ManySortedSet of J by A2,PARTFUN1:def 2,RELAT_1:def 18;
for i being object holds i in J implies K.i is non empty
by A6,A3,TARSKI:def 2;
then reconsider K as non-empty ManySortedSet of J by PBOOLE:def 13;
for j being object st j in J holds F.j is Function of K.j, (J --> the
carrier of L).j
proof
let j be object;
assume
A7: j in J;
then
A8: (J --> the carrier of L).j = the carrier of L by FUNCOP_1:7;
per cases by A7,TARSKI:def 2;
suppose
j = 1;
hence thesis by A1,A6,A7,FUNCOP_1:7;
end;
suppose
j = 2;
hence thesis by A5,A3,A8,FUNCT_2:7;
end;
end;
then reconsider F as DoubleIndexedSet of K, L by PBOOLE:def 15;
rng Infs Frege F is_<=_than "\/"({x"/\"y where y is Element of L: y in
X } , L )
proof
let y be Element of L;
assume y in rng Infs Frege F;
then consider f being object such that
A9: f in dom Frege F and
A10: y = //\(((Frege F).f), L) by Th13;
reconsider f as Function by A9;
A11: f.j2 in K.j2 by A9,Lm6;
then reconsider f2 = f.2 as Element of X by FUNCT_4:63;
A12: f.j1 in K.j1 by A9,Lm6;
A13: {x, f2} c= rng((Frege F).f)
proof
let z be object;
assume z in {x, f2};
then z = x or z = f.2 by TARSKI:def 2;
then z = (F.j1).(f.j1) or z = (F.j2).(f.j2) by A1,A5,A6,A3,A12,A11,
FUNCOP_1:7,FUNCT_1:18;
hence thesis by A9,Lm5;
end;
x"/\"f2 in A;
then
A14: x"/\"f2 <= "\/"(A, L) by YELLOW_2:22;
A15: ex_inf_of rng((Frege F).f),L & ex_inf_of {x, f.2},L by YELLOW_0:17;
y = "/\"(rng((Frege F).f), L) by A10,YELLOW_2:def 6;
then y <= inf{x, f2} by A15,A13,YELLOW_0:35;
then y <= x"/\"f2 by YELLOW_0:40;
hence thesis by A14,YELLOW_0:def 2;
end;
then sup rng Infs Frege F <= "\/"({x"/\"y where y is Element of L: y in X},
L) by YELLOW_0:32;
then
A16: Sup Infs Frege F <= "\/"({x"/\"y where y is Element of L: y in X}, L)
by YELLOW_2:def 5;
(x "/\").:X = A by WAYBEL_1:61;
then reconsider A9= A as Subset of L;
ex_sup_of X,L & ex_sup_of A9,L by YELLOW_0:17;
then
A17: x "/\" sup X >= sup A9 by Th25;
x "/\" sup X is_<=_than rng Sups F
proof
let y be Element of L;
assume y in rng Sups F;
then consider j being Element of J such that
A18: y = Sup(F.j) by Th14;
per cases by TARSKI:def 2;
suppose
j = 1;
then rng(F.j) = {x} by A1,FUNCOP_1:8;
then Sup(F.j) = sup{x} by YELLOW_2:def 5;
then y = x by A18,YELLOW_0:39;
hence x "/\" sup X <= y by YELLOW_0:23;
end;
suppose
j = 2;
then rng(F.j) = X by A5;
then y = sup X by A18,YELLOW_2:def 5;
hence x "/\" sup X <= y by YELLOW_0:23;
end;
end;
then x "/\" sup X <= inf rng Sups F by YELLOW_0:33;
then x "/\" sup X <= Inf Sups F by YELLOW_2:def 6;
then x "/\" sup X <= Sup Infs Frege F by Def3;
then x "/\" sup X <= "\/"({x"/\"y where y is Element of L: y in X}, L) by A16
,YELLOW_0:def 2;
hence thesis by A17,YELLOW_0:def 3;
end;
theorem Th26:
for L being completely-distributive LATTICE for X being Subset
of L for x being Element of L holds x "/\" sup X = "\/"({x"/\"y where y is
Element of L: y in X}, L)
proof
let L be completely-distributive LATTICE;
let X be Subset of L;
let x be Element of L;
set A = {x"/\"y where y is Element of L: y in X};
per cases;
suppose
A1: X is empty;
now
set z = the Element of A;
assume A <> {};
then z in A;
then ex y being Element of L st z = x"/\"y & y in X;
hence contradiction by A1;
end;
then
A2: "\/"(A, L) = Bottom L by YELLOW_0:def 11;
sup X = Bottom L by A1,YELLOW_0:def 11;
hence thesis by A2,WAYBEL_1:3;
end;
suppose
X is non empty;
hence thesis by Lm15;
end;
end;
registration
cluster completely-distributive -> Heyting for LATTICE;
correctness
proof
let L be LATTICE;
assume L is completely-distributive;
then reconsider L as completely-distributive LATTICE;
for X being Subset of L for x being Element of L holds x"/\" sup X =
"\/"({x"/\" y where y is Element of L: y in X}, L) by Th26;
then for x being Element of L holds x "/\" is lower_adjoint by WAYBEL_1:64;
hence thesis by WAYBEL_1:def 19;
end;
end;
:: For distributivity confer WAYBEL_1.
begin :: SubFrames of Continuous Lattices
definition
let L be non empty RelStr;
mode CLSubFrame of L is infs-inheriting directed-sups-inheriting non empty
full SubRelStr of L;
end;
theorem Th27:
for F being DoubleIndexedSet of K, L st for j being Element of J
holds rng(F.j) is directed holds rng Infs Frege F is directed
proof
let F be DoubleIndexedSet of K, L;
set X = rng Infs Frege F;
assume
A1: for j being Element of J holds rng(F.j) is directed;
for x, y being Element of L st x in X & y in X ex z being Element of L
st z in X & x <= z & y <= z
proof
let x, y be Element of L;
assume that
A2: x in X and
A3: y in X;
consider h being object such that
A4: h in dom(Frege F) and
A5: y = //\((Frege F).h, L) by A3,Th13;
reconsider h as Function by A4;
reconsider H = (Frege F).h as Function of J, the carrier of L by A4,Th10;
consider g being object such that
A6: g in dom(Frege F) and
A7: x = //\((Frege F).g, L) by A2,Th13;
reconsider g as Function by A6;
reconsider G = (Frege F).g as Function of J, the carrier of L by A6,Th10;
A8: ex_inf_of rng((Frege F).g),L by YELLOW_0:17;
defpred P[object, object] means
$1 in J & $2 in K.$1 & for c being Element of L
st c = (F.$1).$2 holds (for a being Element of L st a = G.$1 holds a <= c) & (
for b being Element of L st b = H.$1 holds b <= c);
A9: for j being Element of J ex k being Element of K.j st G.j <= (F.j).k
& H.j <= (F.j).k
proof
let j be Element of J;
j in J;
then
A10: j in dom F by PARTFUN1:def 2;
then
A11: g.j in dom(F.j) by A6,Th9;
j in J;
then
A12: j in dom F by PARTFUN1:def 2;
then G.j = (F.j).(g.j) by A6,Th9;
then
A13: G.j in rng(F.j) by A11,FUNCT_1:def 3;
A14: h.j in dom(F.j) by A4,A10,Th9;
H.j = (F.j).(h.j) by A4,A12,Th9;
then
A15: H.j in rng(F.j) by A14,FUNCT_1:def 3;
rng(F.j) is directed Subset of L by A1;
then consider c being Element of L such that
A16: c in rng(F.j) and
A17: G.j <= c & H.j <= c by A13,A15,WAYBEL_0:def 1;
consider k being object such that
A18: k in dom(F.j) and
A19: c = (F.j).k by A16,FUNCT_1:def 3;
reconsider k as Element of K.j by A18;
take k;
thus thesis by A17,A19;
end;
A20: for j being object st j in J
ex k being object st k in union rng K & P[j, k ]
proof
let j9 be object;
assume j9 in J;
then reconsider j = j9 as Element of J;
consider k being Element of K.j such that
A21: G.j <= (F.j).k & H.j <= (F.j).k by A9;
take k;
j in J;
then j in dom K by PARTFUN1:def 2;
then K.j in rng K by FUNCT_1:def 3;
hence k in union rng K by TARSKI:def 4;
thus thesis by A21;
end;
consider f being Function such that
A22: dom f = J and
rng f c= union rng K and
A23: for j being object st j in J holds P[j, f.j] from FUNCT_1:sch 6(A20
);
A24: now
let x be object;
assume x in dom doms F;
then
A25: x in dom F by FUNCT_6:59;
then reconsider j = x as Element of J;
(doms F).x = dom(F.j) by A25,FUNCT_6:22
.= K.j by FUNCT_2:def 1;
hence f.x in (doms F).x by A23;
end;
dom f = dom F by A22,PARTFUN1:def 2
.= dom doms F by FUNCT_6:59;
then f in product doms F by A24,CARD_3:9;
then
A26: f in dom(Frege F) by PARTFUN1:def 2;
then reconsider Ff = (Frege F).f as Function of J, the carrier of L by Th10
;
take z = Inf Ff;
thus z in X by A26,Th13;
A27: x = "/\"(rng((Frege F).g), L) by A7,YELLOW_2:def 6;
now
let j be Element of J;
A28: j in J;
then j in dom G by FUNCT_2:def 1;
then
A29: G.j in rng G by FUNCT_1:def 3;
j in dom F by A28,PARTFUN1:def 2;
then (F.j).(f.j) = ((Frege F).f).j by A26,Th9;
then
A30: G.j <= Ff.j by A23;
x is_<=_than rng G by A27,A8,YELLOW_0:def 10;
then x <= G.j by A29;
hence x <= Ff.j by A30,ORDERS_2:3;
end;
hence x <= z by YELLOW_2:55;
A31: ex_inf_of rng((Frege F).h),L by YELLOW_0:17;
A32: y = "/\"(rng((Frege F).h), L) by A5,YELLOW_2:def 6;
now
let j be Element of J;
A33: j in J;
then j in dom H by FUNCT_2:def 1;
then
A34: H.j in rng H by FUNCT_1:def 3;
j in dom F by A33,PARTFUN1:def 2;
then (F.j).(f.j) = ((Frege F).f).j by A26,Th9;
then
A35: H.j <= Ff.j by A23;
y is_<=_than rng H by A32,A31,YELLOW_0:def 10;
then y <= H.j by A34;
hence y <= Ff.j by A35,ORDERS_2:3;
end;
hence thesis by YELLOW_2:55;
end;
hence thesis by WAYBEL_0:def 1;
end;
theorem ::Theorem 2.7 (ii)
L is continuous implies for S being CLSubFrame of L holds S is
continuous LATTICE
proof
assume
A1: L is continuous;
let S be CLSubFrame of L;
reconsider L9= L as complete LATTICE;
A2: S is complete LATTICE by YELLOW_2:30;
for J, K for F being DoubleIndexedSet of K, S st for j being Element of
J holds rng(F.j) is directed holds Inf Sups F = Sup Infs Frege F
proof
let J, K;
let F be DoubleIndexedSet of K, S such that
A3: for j being Element of J holds rng(F.j) is directed;
now
let j be object;
assume
j in J;
then reconsider j9= j as Element of J;
A5: F.j9 is Function of K.j9, the carrier of S & the carrier of S c= the
carrier of L by YELLOW_0:def 13;
thus F.j is Function of K.j, (J --> the carrier of L).j by A5,FUNCT_2:7;
end;
then reconsider F9= F as DoubleIndexedSet of K, L by PBOOLE:def 15;
ex_inf_of rng Sups F,L by YELLOW_0:17;
then
A6: "/\"(rng Sups F,L) in the carrier of S by YELLOW_0:def 18;
now
let x be object;
assume x in rng Sups F9;
then consider j being Element of J such that
A7: x = Sup(F9.j) by Th14;
A8: ex_sup_of rng(F.j),L9 & rng(F.j) is directed Subset of S by A3,
YELLOW_0:17;
x = sup rng(F9.j) by A7,YELLOW_2:def 5
.= sup rng(F.j) by A8,WAYBEL_0:7
.= Sup(F.j) by YELLOW_2:def 5;
hence x in rng Sups F by Th14;
end;
then
A9: rng Sups F9 c= rng Sups F;
now
let x be object;
assume x in rng Sups F;
then consider j being Element of J such that
A10: x = Sup(F.j) by Th14;
A11: ex_sup_of rng(F.j),L9 & rng(F.j) is directed Subset of S by A3,
YELLOW_0:17;
x = sup rng(F.j) by A10,YELLOW_2:def 5
.= sup rng(F9.j) by A11,WAYBEL_0:7
.= Sup(F9.j) by YELLOW_2:def 5;
hence x in rng Sups F9 by Th14;
end;
then rng Sups F c= rng Sups F9;
then ex_inf_of (rng Sups F9),L9 & rng Sups F9 = rng Sups F by A9,
XBOOLE_0:def 10,YELLOW_0:17;
then inf rng Sups F9 = inf rng Sups F by A6,YELLOW_0:63;
then
A12: Inf Sups F9 = inf rng Sups F by YELLOW_2:def 6;
now
let x be object;
assume x in rng Infs Frege F;
then consider f being object such that
A13: f in dom(Frege F) and
A14: x = //\((Frege F).f, S) by Th13;
reconsider f as Function by A13;
(Frege F).f is Function of J, the carrier of S by A13,Th10;
then
A15: rng((Frege F).f) c= the carrier of S by RELAT_1:def 19;
A16: ex_inf_of rng((Frege F).f),L9 by YELLOW_0:17;
then
A17: "/\"(rng((Frege F).f), L) in the carrier of S by A15,YELLOW_0:def 18;
x = "/\"(rng((Frege F).f), S) by A14,YELLOW_2:def 6
.= "/\"(rng((Frege F9).f), L) by A15,A16,A17,YELLOW_0:63
.= //\((Frege F9).f, L) by YELLOW_2:def 6;
hence x in rng Infs Frege F9 by A13,Th13;
end;
then
A18: rng Infs Frege F c= rng Infs Frege F9;
now
let x be object;
assume x in rng /\\(Frege F9, L);
then consider f being object such that
A19: f in dom(Frege F9) and
A20: x = //\((Frege F9).f, L) by Th13;
reconsider f as Element of product doms F9 by A19;
(Frege F).f is Function of J, the carrier of S by A19,Th10;
then
A21: rng((Frege F).f) c= the carrier of S by RELAT_1:def 19;
A22: ex_inf_of rng((Frege F).f),L9 by YELLOW_0:17;
then
A23: "/\"(rng((Frege F).f), L) in the carrier of S by A21,YELLOW_0:def 18;
x = "/\"(rng((Frege F9).f), L) by A20,YELLOW_2:def 6
.= "/\"(rng((Frege F).f), S) by A21,A22,A23,YELLOW_0:63
.= //\((Frege F).f, S) by YELLOW_2:def 6;
hence x in rng Infs Frege F by A19,Th13;
end;
then rng /\\(Frege F9, L) c= rng /\\(Frege F, S);
then
A24: rng Infs Frege F9 = rng Infs Frege F by A18,XBOOLE_0:def 10;
for j being Element of J holds rng(F9.j) is directed
proof
let j be Element of J;
rng(F.j) is directed by A3;
hence thesis by YELLOW_2:7;
end;
then
A25: Inf Sups F9 = Sup Infs Frege F9 by A1,Lm8;
ex_sup_of rng /\\(Frege F9, L),L9 & rng Infs Frege F is non empty
directed Subset of S by A2,A3,Th27,YELLOW_0:17;
then sup rng Infs Frege F9 = sup rng Infs Frege F by A24,WAYBEL_0:7;
then Sup Infs Frege F9 = sup rng Infs Frege F by YELLOW_2:def 5
.= Sup Infs Frege F by YELLOW_2:def 5;
hence thesis by A25,A12,YELLOW_2:def 6;
end;
hence thesis by A2,Lm9;
end;
theorem Th29:
for S being non empty Poset st ex g being Function of L, S st g
is infs-preserving onto holds S is complete LATTICE
proof
let S be non empty Poset;
given g being Function of L, S such that
A1: g is infs-preserving and
A2: g is onto;
for A being Subset of S holds ex_inf_of A,S
proof
let A be Subset of S;
set Y = g"A;
rng g = the carrier of S by A2,FUNCT_2:def 3;
then
A3: A = g.:Y by FUNCT_1:77;
ex_inf_of Y,L & g preserves_inf_of Y by A1,WAYBEL_0:def 32,YELLOW_0:17;
hence thesis by A3,WAYBEL_0:def 30;
end;
then S is complete non empty Poset by YELLOW_2:28;
hence thesis;
end;
notation
let J be set, y be set;
synonym J => y for J --> y;
end;
registration
let J be set, y be set;
cluster J => y -> total for J-defined Function;
coherence;
end;
definition
let A, B, J be set, f be Function of A, B;
redefine func J => f -> ManySortedFunction of (J --> A), (J --> B); :: redefines => (WAYBEL_5, synonym) → --> (FUNCOP_1, definition)
coherence
proof
set JA = J --> A, JB = J --> B;
for j being object st j in J holds (J => f).j is Function of JA.j, JB.j
proof
let j be object;
assume
A1: j in J;
then JA.j = A & JB.j = B by FUNCOP_1:7;
hence thesis by A1,FUNCOP_1:7;
end;
hence thesis by PBOOLE:def 15;
end;
end;
theorem Th30:
for A, B being set for f being Function of A, B, g being
Function of B, A st g*f = id A holds (J => g)**(J => f) = id (J --> A)
proof
let A, B be set;
let f be Function of A, B;
let g be Function of B, A;
set F = (J => g)**(J => f);
dom F = J by MSUALG_3:2;
then reconsider F as ManySortedSet of J by PARTFUN1:def 2,RELAT_1:def 18;
assume
A1: g*f = id A;
A2: for j being object st j in J holds F.j = id ((J --> A).j)
proof
let j be object;
assume
A3: j in J;
then
A4: (J --> A).j = A by FUNCOP_1:7;
(J => g).j = g & (J => f).j = f by A3,FUNCOP_1:7;
hence thesis by A1,A3,A4,MSUALG_3:2;
end;
now
let j be object;
assume j in J;
then F.j = id ((J --> A).j) by A2;
hence F.j is Function of (J --> A).j, (J --> A).j;
end;
then reconsider F as ManySortedFunction of (J --> A), (J --> A) by
PBOOLE:def 15;
for j being set st j in J holds F.j = id ((J --> A).j) by A2;
hence thesis by MSUALG_3:def 1;
end;
theorem Th31:
for J, A being non empty set, B being set, K being ManySortedSet
of J for F being DoubleIndexedSet of K, A for f being Function of A, B holds (J
=> f)**F is DoubleIndexedSet of K, B
proof
let J, A be non empty set;
let B be set;
let K be ManySortedSet of J;
let F be DoubleIndexedSet of K, A;
let f be Function of A, B;
set fF = (J => f)**F;
dom fF = J by MSUALG_3:2;
then reconsider fF as ManySortedSet of J by PARTFUN1:def 2,RELAT_1:def 18;
for j being object st j in J holds fF.j is Function of K.j, (J --> B).j
proof
let j be object;
assume
A1: j in J;
then reconsider j9= j as Element of J;
reconsider Fj = F.j9 as Function of K.j, A;
A2: fF.j = ((J => f).j)*(F.j) by A1,MSUALG_3:2
.= f*Fj;
thus thesis by A2;
end;
hence (J --> f)**F is DoubleIndexedSet of K, B by PBOOLE:def 15;
end;
theorem Th32:
for J, A, B being non empty set, K being ManySortedSet of J for
F being DoubleIndexedSet of K, A for f being Function of A, B holds doms((J =>
f)**F) = doms F
proof
let J, A, B be non empty set;
let K be ManySortedSet of J;
let F be DoubleIndexedSet of K, A;
let f be Function of A, B;
A1: dom doms((J => f)**F) = dom((J => f)**F) by FUNCT_6:59
.= J by MSUALG_3:2;
A2: now
let x be object;
assume
A3: x in J;
then reconsider j = x as Element of J;
A4: j in dom F by A3,PARTFUN1:def 2;
A5: rng(F.j) c= A & dom f = A by FUNCT_2:def 1;
j in dom((J => f)**F) by A1,A3,FUNCT_6:59;
then (doms((J => f)**F)).j = dom(((J => f)**F).j) by FUNCT_6:22
.= dom(((J => f).j)*(F.j)) by MSUALG_3:2
.= dom(f*(F.j))
.= dom(F.j) by A5,RELAT_1:27
.= (doms F).j by A4,FUNCT_6:22;
hence (doms((J => f)**F)).x = (doms F).x;
end;
dom doms F = dom F by FUNCT_6:59
.= J by PARTFUN1:def 2;
hence thesis by A1,A2,FUNCT_1:2;
end;
theorem ::Theorem 2.7 (iii)
L is continuous implies for S being non empty Poset st ex g being
Function of L, S st g is infs-preserving directed-sups-preserving & g is onto
holds S is continuous LATTICE
proof
assume
A1: L is continuous;
let S be non empty Poset;
given g being Function of L, S such that
A2: g is infs-preserving directed-sups-preserving and
A3: g is onto;
reconsider S9= S as complete LATTICE by A2,A3,Th29;
for J, K for F being DoubleIndexedSet of K, S9 st for j being Element of
J holds rng(F.j) is directed holds Inf Sups F = Sup Infs(Frege F)
proof
let J, K;
let F be DoubleIndexedSet of K, S9 such that
A4: for j being Element of J holds rng(F.j) is directed;
consider d being Function of S, L such that
A5: [g, d] is Galois and
for t being Element of S holds d.t is_minimum_of g"(uparrow t) by A2,
WAYBEL_1:14;
reconsider dF = (J => d)**F as DoubleIndexedSet of K, L by Th31;
A6: ex_inf_of (rng Sups dF),L & g preserves_inf_of (rng Sups dF) by A2,
WAYBEL_0:def 32,YELLOW_0:17;
for t being Element of S holds d.t is_minimum_of g"{t} by A3,A5,WAYBEL_1:22
;
then
A7: g*d = id S by WAYBEL_1:23;
A8: for f being set st f in dom(Frege dF) holds rng((Frege F).f) = g.:(
rng((Frege dF).f))
proof
let f be set;
assume
A9: f in dom(Frege dF);
then reconsider f as Element of product doms dF;
A10: dom(Frege dF) = product(doms dF) by PARTFUN1:def 2
.= product(doms F) by Th32
.= dom(Frege F) by PARTFUN1:def 2;
A11: dom((Frege dF).f) = dom dF by A9,Th8
.= J by PARTFUN1:def 2;
A12: now
let i be object;
assume
A13: i in J;
then reconsider j = i as Element of J;
A14: j in dom F by A13,PARTFUN1:def 2;
A15: j in dom dF by A13,PARTFUN1:def 2;
then f.j in dom(dF.j) by A9,Th9;
then f.j in dom(((J => d).j)*(F.j)) by MSUALG_3:2;
then
A16: f.j in dom(d*(F.j));
(g*((Frege dF).f)).j = g.(((Frege dF).f).j) by A11,FUNCT_1:13
.= g.((dF.j).(f.j)) by A9,A15,Th9
.= g.((((J => d).j)*(F.j)).(f.j)) by MSUALG_3:2
.= g.((d*(F.j)).(f.j))
.= (g*(d*(F.j))).(f.j) by A16,FUNCT_1:13
.= ((id the carrier of S)*(F.j)).(f.j) by A7,RELAT_1:36
.= (F.j).(f.j) by FUNCT_2:17
.= ((Frege F).f).j by A9,A10,A14,Th9;
hence (g*((Frege dF).f)).i = ((Frege F).f).i;
end;
dom g = the carrier of L by FUNCT_2:def 1;
then rng((Frege dF).f) c= dom g;
then
A17: dom(g*((Frege dF).f)) = dom((Frege dF).f) by RELAT_1:27;
dom((Frege F).f) = dom F by A9,A10,Th8
.= J by PARTFUN1:def 2;
then rng((Frege F).f) = rng(g*((Frege dF).f)) by A11,A17,A12,FUNCT_1:2
.= g.:(rng((Frege dF).f)) by RELAT_1:127;
hence thesis;
end;
A18: rng Infs Frege F c= g.:(rng Infs Frege dF)
proof
let y be object;
assume y in rng Infs Frege F;
then consider f being object such that
A19: f in dom(Frege F) and
A20: y = //\((Frege F).f, S) by Th13;
reconsider f as Element of product doms F by A19;
reconsider f9= f as Element of product doms dF by Th32;
set X = rng((Frege dF).f9);
A21: g preserves_inf_of X & ex_inf_of X,L by A2,WAYBEL_0:def 32,YELLOW_0:17;
A22: dom(Frege dF) = product(doms dF) by PARTFUN1:def 2
.= product(doms F) by Th32
.= dom(Frege F) by PARTFUN1:def 2;
then rng((Frege F).f) = g.:(rng((Frege dF).f)) by A8,A19;
then y = "/\"(g.:(rng((Frege dF).f)), S) by A20,YELLOW_2:def 6;
then
A23: y = g.inf X by A21,WAYBEL_0:def 30
.= g.Inf((Frege dF).f9) by YELLOW_2:def 6;
Inf((Frege dF).f9) in rng Infs Frege dF by A19,A22,Th13;
hence thesis by A23,FUNCT_2:35;
end;
A24: g.:(rng Infs Frege dF) c= rng Infs Frege F
proof
let y be object;
assume y in g.:(rng Infs Frege dF);
then consider x being object such that
x in the carrier of L and
A25: x in rng Infs Frege dF and
A26: y = g.x by FUNCT_2:64;
consider f being object such that
A27: f in dom(Frege dF) and
A28: x = //\((Frege dF).f, L) by A25,Th13;
reconsider f as Element of product doms dF by A27;
set X = rng((Frege dF).f);
g preserves_inf_of X & ex_inf_of X,L by A2,WAYBEL_0:def 32,YELLOW_0:17;
then inf(g.:X) = g.inf X by WAYBEL_0:def 30;
then
A29: y = inf(g.:X) by A26,A28,YELLOW_2:def 6;
A30: dom(Frege dF) = product(doms dF) by PARTFUN1:def 2
.= product(doms F) by Th32
.= dom(Frege F) by PARTFUN1:def 2;
reconsider f9= f as Element of product doms F by Th32;
rng((Frege F).f) = g.:(rng((Frege dF).f)) by A8,A27;
then y = Inf((Frege F).f9) by A29,YELLOW_2:def 6;
hence thesis by A27,A30,Th13;
end;
A31: d is monotone by A5,WAYBEL_1:8;
A32: for j being Element of J holds rng(dF.j) is directed
proof
let j be Element of J;
(J => d).j = d;
then
A33: rng(dF.j) = rng(d*(F.j)) by MSUALG_3:2
.= d.:(rng(F.j)) by RELAT_1:127;
rng(F.j) is directed by A4;
hence thesis by A31,A33,YELLOW_2:15;
end;
then rng Infs Frege dF is directed non empty by Th27;
then
A34: g preserves_sup_of rng Infs Frege dF by A2,WAYBEL_0:def 37;
reconsider gdF = (J => g)**dF as DoubleIndexedSet of K, S;
A35: ex_sup_of rng Infs Frege dF,L by YELLOW_0:17;
A36: rng Sups gdF c= g.:(rng Sups dF)
proof
let y be object;
assume y in rng Sups gdF;
then consider j being Element of J such that
A37: y = Sup(gdF.j) by Th14;
gdF.j = ((J => g).j)*(dF.j) by MSUALG_3:2
.= g*(dF.j);
then rng(gdF.j) = g.:(rng(dF.j)) by RELAT_1:127;
then
A38: y = sup(g.:(rng(dF.j))) by A37,YELLOW_2:def 5;
rng(dF.j) is directed by A32;
then
A39: g preserves_sup_of rng(dF.j) by A2,WAYBEL_0:def 37;
ex_sup_of rng(dF.j),L by YELLOW_0:17;
then sup(g.:(rng(dF.j))) = g.sup(rng(dF.j)) by A39,WAYBEL_0:def 31;
then
A40: y = g.Sup(dF.j) by A38,YELLOW_2:def 5;
Sup(dF.j) in rng Sups dF by Th14;
hence thesis by A40,FUNCT_2:35;
end;
A41: g.:(rng Sups dF) c= rng Sups gdF
proof
let y be object;
assume y in g.:(rng Sups dF);
then consider x being object such that
x in the carrier of L and
A42: x in rng Sups dF and
A43: y = g.x by FUNCT_2:64;
consider j being Element of J such that
A44: x = Sup(dF.j) by A42,Th14;
rng(dF.j) is directed by A32;
then
A45: g preserves_sup_of rng(dF.j) by A2,WAYBEL_0:def 37;
ex_sup_of rng(dF.j),L by YELLOW_0:17;
then sup(g.:(rng(dF.j))) = g.sup(rng(dF.j)) by A45,WAYBEL_0:def 31;
then
A46: y = sup(g.:(rng(dF.j))) by A43,A44,YELLOW_2:def 5;
gdF.j = ((J => g).j)*(dF.j) by MSUALG_3:2
.= g*(dF.j);
then rng(gdF.j) = g.:(rng(dF.j)) by RELAT_1:127;
then y = Sup(gdF.j) by A46,YELLOW_2:def 5;
hence thesis by Th14;
end;
F = (id (J --> the carrier of S))**F by MSUALG_3:4
.= ((J --> g)**(J --> d))**F by A7,Th30
.= gdF by PBOOLE:140;
then Inf Sups F = inf rng Sups gdF by YELLOW_2:def 6
.= inf (g.:(rng Sups dF)) by A36,A41,XBOOLE_0:def 10
.= g.(inf rng Sups dF) by A6,WAYBEL_0:def 30
.= g.(Inf Sups dF) by YELLOW_2:def 6
.= g.(Sup Infs Frege dF) by A1,A32,Lm8
.= g.(sup rng Infs Frege dF) by YELLOW_2:def 5
.= sup(g.:(rng Infs Frege dF)) by A34,A35,WAYBEL_0:def 31
.= sup rng Infs Frege F by A24,A18,XBOOLE_0:def 10
.= Sup Infs Frege F by YELLOW_2:def 5;
hence thesis;
end;
hence thesis by Lm9;
end;