Copyright (c) 1996 Association of Mizar Users
environ
vocabulary WAYBEL_0, ORDINAL2, WAYBEL_3, FILTER_2, QUANTAL1, YELLOW_0,
LATTICE3, LATTICES, YELLOW_2, WAYBEL_1, YELLOW_1, PRE_TOPC, FUNCT_1,
RELAT_1, BHSP_3, PBOOLE, PRALG_1, FUNCOP_1, ZF_REFLE, FUNCT_6, CARD_3,
FINSEQ_4, BOOLE, ORDERS_1, TARSKI, YELLOW_6, CLASSES1, ZF_LANG, FUNCT_5,
FUNCT_2, FINSUB_1, FINSET_1, REALSET1, RELAT_2, LATTICE2, CAT_1, SGRAPH1,
MSUALG_3, SEQM_3, WAYBEL_5;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FINSET_1, FINSUB_1,
FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCT_5, FUNCT_6, FUNCOP_1,
STRUCT_0, ORDERS_1, LATTICE3, CARD_3, REALSET1, PBOOLE, PRALG_1, PRALG_2,
MSUALG_1, MSUALG_3, PRE_TOPC, PRE_CIRC, BORSUK_1, CLASSES1, CLASSES2,
GRCAT_1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0, WAYBEL_3,
YELLOW_6;
constructors FINSUB_1, LATTICE3, TOPS_2, PRE_CIRC, BORSUK_1, PRALG_2,
MSUALG_3, ORDERS_3, WAYBEL_1, WAYBEL_3, YELLOW_6, CLASSES1, GRCAT_1;
clusters STRUCT_0, FINSET_1, LATTICE3, ORDERS_1, PBOOLE, MSUALG_1, CIRCCOMB,
PRVECT_1, FRAENKEL, PRALG_1, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3,
CLASSES2, YELLOW_6, CANTOR_1, FUNCT_2, FUNCOP_1, RELSET_1, SUBSET_1,
FUNCT_4, PARTFUN1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICE3;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, FUNCT_5, CARD_3, ORDERS_1,
LATTICE3, FUNCT_6, FUNCOP_1, FINSET_1, PBOOLE, PRALG_1, PRALG_2,
MSUALG_1, MSUALG_3, EXTENS_1, AUTALG_1, RELAT_1, UNIALG_1, REALSET1,
FINSUB_1, COMPTS_1, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_0,
WAYBEL_3, CLASSES2, YELLOW_6, CLASSES1, GRCAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, FUNCT_4;
schemes FUNCT_1, FUNCT_2, MSSUBFAM, YELLOW_2, COMPTS_1;
begin :: The Continuity of Lattices
reserve x, y, i for set,
L for up-complete Semilattice;
Lm1: ::Theorem 2.1 (1) implies (2)
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 set;
assume y in waybelow x;
then y in {y' where y' is Element of L: y' << x} by WAYBEL_3:def 3;
then consider y' being Element of L such that
A2: y = y' & y' << x;
thus y in I by A1,A2,WAYBEL_3:20;
end;
hence thesis;
end;
end;
Lm2: ::Theorem 2.1 (2) implies (1)
(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 L is continuous 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: ::Theorem 2.1 (1) implies (3)
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,WAYBEL_3:def 6;
take I;
thus x <= sup I & for J being Ideal of L st x <= sup J holds
I c= J by A1,Lm1;
end;
Lm4: ::Theorem 2.1 (3) implies (1)
(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 set;
assume
A4: y in I;
then reconsider y'= 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 y in J by A4;
end;
then y' << x by WAYBEL_3:21;
hence y in waybelow x by WAYBEL_3:7;
end;
then A5: I c= waybelow x by TARSKI:def 3;
now
let y be set;
assume
A6: y in waybelow x;
then reconsider y'= y as Element of L;
y' << x by A6,WAYBEL_3:7;
hence y in I by A2,WAYBEL_3:20;
end;
then waybelow x c= I by TARSKI:def 3;
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 L is continuous 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 has_a_lower_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 map of L, InclPoset(Ids L) st
for t being Element of L holds d.t = F(t) from LambdaMD;
then consider d being map 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));
A2: ex_inf_of r"(uparrow t),InclPoset(Ids L) by YELLOW_0:17;
A3: 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 A4: I in dom r by YELLOW_2:51;
reconsider I'= I as Ideal of L by YELLOW_2:43;
consider J being Ideal of L such that
A5: t <= sup J and
A6: for K being Ideal of L st t <= sup K holds J c= K by Lm3;
reconsider J'= J as Element of P by YELLOW_2:43;
A7: r"(uparrow t) is_>=_than J'
proof
let K be Element of P;
reconsider K'= K as Ideal of L by YELLOW_2:43;
assume K in r"(uparrow t);
then K in dom r & r.K in uparrow t by FUNCT_1:def 13;
then t <= r.K by WAYBEL_0:18;
then t <= sup K' by YELLOW_2:def 3;
then J' c= K' by A6;
hence J' <= K by YELLOW_1:3;
end;
for K being Element of P st r"(uparrow t) is_>=_than K holds K <= J'
proof
let K be Element of P;
assume
A8: r"(uparrow t) is_>=_than K;
J' in the carrier of P;
then J' in Ids L by YELLOW_1:1;
then A9: J in dom r by YELLOW_2:51;
t <= r.J' by A5,YELLOW_2:def 3;
then r.J in uparrow t by WAYBEL_0:18;
then J in r"(uparrow t) by A9,FUNCT_1:def 13;
hence K <= J' by A8,LATTICE3:def 8;
end;
then t <= sup I' by A5,A7,YELLOW_0:31;
then t <= r.I by YELLOW_2:def 3;
then r.I in uparrow t by WAYBEL_0:18;
then I in r"(uparrow t) by A4,FUNCT_1:def 13;
hence thesis by A2,A3,WAYBEL_1:def 6;
end;
then [r, d] is Galois by WAYBEL_1:11;
hence r is upper_adjoint 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;
assume
A1: SupMap L is upper_adjoint;
set P = InclPoset(Ids L);
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
let x be Element of L;
set r = SupMap L;
set I' = inf(r"(uparrow x));
reconsider I = I' as Ideal of L by YELLOW_2:43;
consider d being map of L, P such that
A2: [r,d] is Galois by A1,WAYBEL_1:def 11;
d.x is_minimum_of r"(uparrow x) by A2,WAYBEL_1:11;
then ex_inf_of r"(uparrow x),P & d.x = I & I in r"(uparrow x)
by WAYBEL_1:def 6;
then r.I in uparrow x by FUNCT_1:def 13;
then x <= r.I' by WAYBEL_0:18;
then A3: x <= sup I by YELLOW_2:def 3;
for J being Ideal of L st x <= sup J holds I c= J
proof
let J be Ideal of L;
reconsider J'= J as Element of P by YELLOW_2:43;
A4: J in dom r by YELLOW_2:52;
assume x <= sup J;
then x <= r.J' by YELLOW_2:def 3;
then r.J' in uparrow x by WAYBEL_0:18;
then J' in r"(uparrow x) by A4,FUNCT_1:def 13;
then I' <= J' by YELLOW_2:24;
hence I c= J by YELLOW_1:3;
end;
hence thesis by A3;
end;
hence L is continuous 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 has_a_lower_adjoint
proof
let L be complete Semilattice;
set r = SupMap L;
assume r is infs-preserving sups-preserving;
then ex d being map 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:15;
hence r is upper_adjoint 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:13;
hence F.j is Function of K.j, D by A1,MSUALG_1:def 2;
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;
coherence by Th6;
end;
definition
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
proof
dom(F.j) = K.j by FUNCT_2:def 1;
hence rng(F.j) is non empty by RELAT_1:65;
end;
end;
definition
let J be set, D be non empty set;
let K be non-empty ManySortedSet of J;
cluster -> non-empty DoubleIndexedSet of K, D;
correctness
proof
let F be DoubleIndexedSet of K, D;
for j being set st j in dom F holds F.j is non empty
proof
let j be set;
assume j in dom F;
then A1: j in J by PBOOLE:def 3;
then A2: K.j is non empty by PBOOLE:def 16;
consider k being Element of K.j;
F.j is Function of K.j, D by A1,Th6;
then dom(F.j) = K.j by FUNCT_2:def 1;
then [k, (F.j).k] in F.j by A2,FUNCT_1:def 4;
hence thesis;
end;
hence thesis by UNIALG_1:def 6;
end;
end;
theorem Th7:
for F being Function-yielding Function
for f being set
holds
f in dom(Frege F) implies f is Function
proof
let F be Function-yielding Function;
let f be set;
assume f in dom(Frege F);
then f in product doms F by PBOOLE:def 3;
then ex g being Function st g = f & dom g = dom(doms F) &
for x st x in dom(doms F) holds g.x in (doms F).x by CARD_3:def 5;
hence thesis;
end;
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 by PBOOLE:def 3;
then consider g being Function such that
A2: g = f and
A3: dom g = dom(doms F) and
for x st x in dom(doms F) holds g.x in (doms F).x by CARD_3:def 5;
thus dom f = dom F by A2,A3,EXTENS_1:3;
thus dom ((Frege F).f) = dom(F..f) by A1,PRALG_2:def 8
.= dom F by PRALG_1:def 18;
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;
set G = (Frege F).f;
let i be set such that
A2: i in dom F;
A3: f in product doms F by A1,PBOOLE:def 3;
then A4: G = F..f by PRALG_2:def 8;
i in dom(doms F) by A2,EXTENS_1:3;
then f.i in (doms F).i by A3,CARD_3:18;
hence f.i in dom(F.i) by A2,FUNCT_6:31;
thus
A5: G.i = (F.i).(f.i) by A2,A4,PRALG_1:def 18;
dom G = dom F by A1,Th8;
hence (F.i).(f.i) in rng((Frege F).f) by A2,A5,FUNCT_1:def 5;
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);
A2: dom F = J by PBOOLE:def 3;
set G = (Frege F).f;
A3: dom G = dom F by A1,Th8;
rng G c= D
proof
let y be set;
assume y in rng G;
then consider x such that
A4: x in dom G and
A5: y = G.x by FUNCT_1:def 5;
A6: G.x = (F.x).(f.x) by A1,A3,A4,Th9;
f.x in dom(F.x) by A1,A3,A4,Th9;
then A7: y in rng(F.x) by A5,A6,FUNCT_1:def 5;
F.x is Function of K.x, D by A2,A3,A4,Th6;
then rng(F.x) c= D by RELSET_1:12;
hence y in D by A7;
end;
hence G is Function of J, D by A2,A3,FUNCT_2:4;
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 PBOOLE:def 3;
hence
((Frege F).f).j = (F.j).(f.j) by A1,Th9;
thus (F.j).(f.j) in rng((Frege F).f) 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;
dom F = J by PBOOLE:def 3;
then A3: f.j in dom(F.j) by A1,A2,Th9;
F.j is Function of K.j, D by A2,Th6;
hence f.j in K.j by A3,FUNCT_2:def 1;
end;
definition
let f be non-empty Function;
cluster doms f -> non-empty;
correctness
proof
for j being set st j in dom doms f holds (doms f).j is non empty
proof
let j be set;
assume that
A1: j in dom doms f and
A2: (doms f).j is empty;
A3: j in f"SubFuncs rng f by A1,FUNCT_6:def 2;
then A4: j in dom f & f.j is Function by FUNCT_6:28;
reconsider fj = f.j as Function by A3,FUNCT_6:28;
{} = dom fj by A2,A4,FUNCT_6:31;
then f.j = {} by RELAT_1:64;
hence contradiction by A4,UNIALG_1:def 6;
end;
hence thesis by UNIALG_1:def 6;
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;
coherence
proof
set PD = product doms F;
set A = (PD --> J), B = (PD --> D);
set G = Frege F;
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 A2: i in dom G by PBOOLE:def 3;
then reconsider f = i as Function by Th7;
A.i = J & B.i = D by A1,FUNCOP_1:13;
then G.f is Function of A.i, B.i by A2,Th10;
hence G.i is Function of A.i, B.i;
end;
hence thesis by MSUALG_1:def 2;
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;
coherence
proof
(product doms F --> J).f = J by FUNCOP_1:13;
hence 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(set) = \\/(F.$1, L);
ex f being Function st dom f = dom F &
for x st x in dom F holds f.x = F(x) from Lambda;
then consider f being Function such that
A1: dom f = dom F and
A2: for x st x in dom F holds f.x = \\/(F.x, L);
rng f c= the carrier of L
proof
let y;
assume y in rng f;
then consider x such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 5;
y = \\/(F.x, L) by A1,A2,A3,A4;
hence y in the carrier of L;
end;
then reconsider f as Function of dom F, the carrier of L by A1,FUNCT_2:4;
take f;
thus thesis by A2;
end;
uniqueness
proof
let f, g be Function of dom F, the carrier of L such that
A5: for x st x in dom F holds f.x = \\/(F.x, L) and
A6: for x st x in dom F holds g.x = \\/(F.x, L);
A7: dom f = dom F & dom g = dom F by FUNCT_2:def 1;
now
let x;
assume
A8: x in dom F;
hence f.x = \\/(F.x, L) by A5
.= g.x by A6,A8;
end;
hence thesis by A7,FUNCT_1:9;
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(set) = //\(F.$1, L);
ex f being Function st dom f = dom F &
for x st x in dom F holds f.x = F(x) from Lambda;
then consider f being Function such that
A9: dom f = dom F and
A10: for x st x in dom F holds f.x = //\(F.x, L);
rng f c= the carrier of L
proof
let y;
assume y in rng f;
then consider x such that
A11: x in dom f and
A12: y = f.x by FUNCT_1:def 5;
y = //\(F.x, L) by A9,A10,A11,A12;
hence y in the carrier of L;
end;
then reconsider f as Function of dom F, the carrier of L by A9,FUNCT_2:4;
take f;
thus thesis by A10;
end;
uniqueness
proof
let f, g be Function of dom F, the carrier of L such that
A13: for x st x in dom F holds f.x = //\(F.x, L) and
A14: for x st x in dom F holds g.x = //\(F.x, L);
A15: dom f = dom F & dom g = dom F by FUNCT_2:def 1;
now
let x;
assume
A16: x in dom F;
hence f.x = //\(F.x, L) by A13
.= g.x by A14,A16;
end;
hence thesis by A15,FUNCT_1:9;
end;
end;
definition
let J be set, K be ManySortedSet of J, L be non empty RelStr;
let F be DoubleIndexedSet of K, L;
redefine func \//(F, L);
synonym Sups F;
redefine func /\\(F, L);
synonym Infs F;
end;
definition
let I, J be set, L be non empty RelStr;
let F be DoubleIndexedSet of (I --> J), L;
redefine func \//(F, L);
synonym Sups F;
redefine func /\\(F, L);
synonym Infs F;
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: dom \//(F, L) = dom F & dom \//(G, L) = dom G by FUNCT_2:def 1;
for x st x in dom F holds \//(F, L).x = \//(G, L).x
proof
let x;
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;
hence thesis by A1,A3,FUNCT_1:9;
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: dom /\\(F, L) = dom F & dom /\\(G, L) = dom G by FUNCT_2:def 1;
for x st x in dom F holds /\\(F, L).x = /\\(G, L).x
proof
let x;
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;
hence thesis by A1,A3,FUNCT_1:9;
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 such that
A1: x in dom \//(F, L) and
A2: y = \//(F, L).x by FUNCT_1:def 5;
take x;
x in dom F by A1,FUNCT_2:def 1;
hence x in dom F & y = \\/(F.x, L) by A2,Def1;
end;
given x such that
A3: x in dom F and
A4: y = \\/(F.x, L);
x in dom \//(F, L) & y = \//(F, L).x by A3,A4,Def1,FUNCT_2:def 1;
hence y in rng \//(F, L) by FUNCT_1:def 5;
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 such that
A5: x in dom /\\(F, L) and
A6: y = /\\(F, L).x by FUNCT_1:def 5;
take x;
x in dom F by A5,FUNCT_2:def 1;
hence x in dom F & y = //\(F.x, L) by A6,Def2;
end;
given x such that
A7: x in dom F and
A8: y = //\(F.x, L);
x in dom /\\(F, L) & y = /\\(F, L).x by A7,A8,Def2,FUNCT_2:def 1;
hence y in rng /\\(F, L) by FUNCT_1:def 5;
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 PBOOLE:def 3;
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 set such that
A2: j in dom F and
A3: x = \\/(F.j, L) by Th13;
reconsider j as Element of J by A2,PBOOLE:def 3;
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 set such that
A4: j in dom F and
A5: x = //\(F.j, L) by Th13;
reconsider j as Element of J by A4,PBOOLE:def 3;
take j;
thus x = Inf(F.j) by A5;
end;
thus thesis by A1,Th13;
end;
definition
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
proof
consider j being Element of J;
Sup(F.j) in rng Sups F by Th14;
hence thesis;
end;
cluster rng Infs F -> non empty;
correctness
proof
consider j being Element of J;
Inf(F.j) in rng Infs F by Th14;
hence thesis;
end;
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 PBOOLE:def 3;
end;
thus thesis by PBOOLE:def 3;
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 set such that
A2: f in dom(Frege F) and
A3: c = //\((Frege F).f, L) by Th13;
reconsider f as Function by A2,Th7;
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 Sup /\\(Frege F, L) <= a 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;
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:55;
(F.j).k <= Sup(F.j) by YELLOW_2:55;
hence Sup(F.j) >= Inf((Frege F).f) by A3,ORDERS_1:26;
end;
set a = Sup Infs Frege F;
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
proof
let f be Function;
assume f in dom(Frege F);
then reconsider f'= f as Element of product doms F by Lm7;
Sup(F.j) >= Inf((Frege F).f') by A1;
hence //\((Frege F).f, L) <= c by A4;
end;
hence a <= c by Th15;
end;
then a <= inf rng Sups F by YELLOW_0:33;
hence Inf Sups F >= Sup Infs Frege F 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;
A3: L is complete satisfying_axiom_of_approximation by A1,WAYBEL_3:def 6;
now
let c;
assume c in waybelow a;
then c << a by WAYBEL_3:7;
hence c <= b by A2;
end;
then waybelow a is_<=_than b by LATTICE3:def 9;
then sup waybelow a <= b by YELLOW_0:32;
hence a <= b by A3,WAYBEL_3:def 5;
end;
Lm8: ::Theorem 2.3 (1) implies (2)
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:24;
then Inf Sups F <= Sup(F.j) by YELLOW_2:def 6;
hence c << Sup(F.j) 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
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: rng(F.j) is non empty directed Subset of L by A2;
A7: c << Sup(F.j) by A4;
Sup(F.j) <= sup(rng(F.j)) by YELLOW_2:def 5;
then consider d being Element of L such that
A8: d in rng(F.j) and
A9: c <= d by A6,A7,WAYBEL_3:def 1;
consider k being set such that
A10: k in dom(F.j) and
A11: d = (F.j).k by A8,FUNCT_1:def 5;
reconsider k as Element of K.j by A10,FUNCT_2:def 1;
take k;
thus thesis by A9,A11;
end;
defpred P[set, set] means
$1 in J & $2 in K.$1 & ex b st b = (F.$1).$2 & c <= b;
A12:
for j being set st j in J ex k being set st k in union rng K & P[j, k]
proof
let j be set;
assume j in J;
then reconsider j'= j as Element of J;
consider k being Element of K.j' such that
A13: c <= (F.j').k by A5;
take k;
j' in J;
then j' in dom K by PBOOLE:def 3;
then k in K.j' & K.j' in rng K by FUNCT_1:def 5;
hence k in union rng K by TARSKI:def 4;
thus P[j, k] by A13;
end;
consider f being Function such that
A14: dom f = J and rng f c= union rng K and
A15: for j being set st j in J holds P[j, f.j]
from NonUniqBoundFuncEx(A12);
A16: for j being Element of J holds
f.j in K.j & ex b st b = (F.j).(f.j) & c <= b by A15;
A17: dom f = dom F by A14,PBOOLE:def 3
.= dom doms F by EXTENS_1:3;
now
let x be set;
assume x in dom doms F;
then A18: x in dom F by EXTENS_1:3;
then reconsider j = x as Element of J by PBOOLE:def 3;
(doms F).x = dom(F.j) by A18,FUNCT_6:31
.= K.j by FUNCT_2:def 1;
hence f.x in (doms F).x by A15;
end;
then f in product doms F by A17,CARD_3:18;
then f in dom(Frege F) by PBOOLE:def 3;
hence thesis by A16;
end;
then consider f being Function such that
A19: f in dom(Frege F) and
A20: 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 A19,Lm7;
reconsider G = (Frege F).f as Function of J, the carrier of L;
now
let j be Element of J;
j in J;
then A21: j in dom F by PBOOLE:def 3;
ex b st b = (F.j).(f.j) & c <= b by A20;
hence c <= G.j by A19,A21,Th9;
end;
then A22: c <= Inf((Frege F).f) by YELLOW_2:57;
set a = Inf((Frege F).f);
a in rng Infs Frege F by Th14;
then a <= sup rng Infs Frege F by YELLOW_2:24;
then a <= Sup Infs Frege F by YELLOW_2:def 5;
hence c <= Sup Infs Frege F by A22,YELLOW_0:def 2;
end;
then A23: Inf Sups F <= Sup Infs Frege F by A1,Th17;
Inf Sups F >= Sup Infs Frege F by Th16;
hence thesis by A23,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
let x be Element of L;
set J = {j where j is directed non empty Subset of L : x <= sup j};
set UN = the_universe_of the carrier of L;
A2: UN = Tarski-Class the_transitive-closure_of the carrier of L by YELLOW_6:
def 3;
reconsider UN as universal set;
A3:the carrier of L c= the_transitive-closure_of the carrier of L
by CLASSES1:59;
the_transitive-closure_of the carrier of L in UN by A2,CLASSES1:5;
then A4: the carrier of L in UN by A3,CLASSES1:def 1;
then A5: bool the carrier of L in UN by CLASSES2:65;
A6: J c= bool the carrier of L
proof let u be set;
assume u in J;
then ex j being directed non empty Subset of L st u = j & x <= sup j;
hence u in bool the carrier of L;
end;
then A7: J in UN by A5,CLASSES1:def 1;
A8: {x} is directed non empty Subset of L by WAYBEL_0:5;
x <= sup {x} by YELLOW_0:39;
then A9: {x} in J by A8;
then reconsider J as non empty set;
A10:
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 consider j' being directed non empty Subset of L such that
A11: j'= j and
x <= sup j';
thus thesis by A11;
end;
set K = id J;
dom K = J by FUNCT_1:34;
then reconsider K as ManySortedSet of J by PBOOLE:def 3;
A12: for j being Element of J holds K.j in UN
proof let j be Element of J;
K.j = j by FUNCT_1:35;
then K.j in J;
hence K.j in UN by A4,A6,CLASSES1:def 1;
end;
for i st i in J holds K.i is non empty
proof
let i;
assume i in J;
then reconsider i'= i as Element of J;
K.i = i' by FUNCT_1:35;
hence K.i is non empty by A10;
end;
then reconsider K as non-empty ManySortedSet of J by PBOOLE:def 16;
deffunc F(set) = id(K.$1);
ex F being Function st dom F = J &
for j being set st j in J holds F.j = F(j) from Lambda;
then consider F being Function such that
A13: dom F = J and
A14: for j being set st j in J holds F.j = id(K.j);
reconsider F as ManySortedSet of J by A13,PBOOLE:def 3;
for j being set st j in dom F holds F.j is Function
proof
let j be set;
assume j in dom F;
then F.j = id(K.j) by A13,A14;
hence F.j is Function;
end;
then reconsider F as ManySortedFunction of J by PRALG_1:def 15;
for j being set st j in J holds
F.j is Function of K.j, (J --> the carrier of L).j
proof
let j be set;
assume j in J;
then reconsider j as Element of J;
A15: F.j = id(K.j) by A14;
then A16: dom(F.j) = K.j by FUNCT_2:def 1;
A17: rng(F.j) c= K.j by A15,RELSET_1:12;
K.j = j by FUNCT_1:35;
then K.j is Subset of L by A10;
then rng(F.j) c= the carrier of L by A17,XBOOLE_1:1;
then rng(F.j) c= (J --> the carrier of L).j by FUNCOP_1:13;
hence thesis by A16,FUNCT_2:4;
end;
then reconsider F as DoubleIndexedSet of K, L by MSUALG_1:def 2;
A18: 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 A14;
hence thesis by FUNCT_1:35;
end;
A19:
for j being Element of J holds rng(F.j) = j
proof
let j be Element of J;
now
let y;
assume y in rng(F.j);
then consider x such that
A20: x in dom(F.j) and
A21: y = (F.j).x by FUNCT_1:def 5;
A22: x in K.j by A20,FUNCT_2:def 1;
then x in j by FUNCT_1:35;
hence y in j by A18,A21,A22;
end;
then A23: rng(F.j) c= j by TARSKI:def 3;
now
let x;
assume x in j;
then A24: x in K.j by FUNCT_1:35;
then A25: (F.j).x = x by A18;
x in dom(F.j) by A24,FUNCT_2:def 1;
hence x in rng(F.j) by A25,FUNCT_1:def 5;
end;
then j c= rng(F.j) by TARSKI:def 3;
hence rng(F.j) = j by A23,XBOOLE_0:def 10;
end;
A26:
for j being Element of J holds rng(F.j) is directed
proof
let j be Element of J;
rng(F.j) = j by A19;
hence thesis by A10;
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
A27: 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
let D be non empty directed Subset of L;
assume x <= sup D;
then D in J;
then reconsider D'= D as Element of J;
A28: 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 PBOOLE:def 3;
then f.j in dom(F.j) by A27,Th9;
hence thesis by FUNCT_2:def 1;
end;
A29: dom f = dom F by A27,Th8
.= J by PBOOLE:def 3;
now
let y be set;
assume y in rng f;
then consider j being set such that
A30: j in dom f and
A31: y = f.j by FUNCT_1:def 5;
reconsider j as Element of J by A29,A30;
y in K.j by A28,A31;
then A32: y in j by FUNCT_1:35;
j is Subset of L by A10;
hence y in the carrier of L by A32;
end;
then rng f c= the carrier of L by TARSKI:def 3;
then reconsider f as Function of J, the carrier of L by A29,FUNCT_2:4;
A33: Inf f <= f.D' by YELLOW_2:55;
A34: dom f = dom F by A27,Th8
.= dom((Frege F).f) by A27,Th8;
now
let j be set;
assume j in dom f;
then A35: j in dom F by A27,Th8;
then reconsider j'= j as Element of J by PBOOLE:def 3;
A36: f.j' is Element of K.j' by A28;
thus ((Frege F).f).j = (F.j').(f.j') by A27,A35,Th9
.= f.j by A18,A36;
end;
then A37: a <= f.D' by A33,A34,FUNCT_1:9;
f.D' in K.D' by A28;
then f.D' in D' by FUNCT_1:35;
hence ex d being Element of L st d in D & a <= d by A37;
end;
then a << x by WAYBEL_3:def 1;
then a in waybelow x by WAYBEL_3:7;
hence //\((Frege F).f, L) <= sup waybelow x by YELLOW_2:24;
end;
then A38: 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
A39: b = Sup(F.j) by Th14;
j in J;
then consider j' being directed non empty Subset of L such that
A40: j'= j and
A41: x <= sup j';
b = sup rng(F.j) by A39,YELLOW_2:def 5
.= sup j' by A19,A40;
hence x <= b by A41;
end;
then x <= inf rng Sups F by YELLOW_0:33;
then A42: x <= Inf Sups F by YELLOW_2:def 6;
reconsider j = {x} as Element of J by A9;
Sup(F.j) = sup rng(F.j) by YELLOW_2:def 5
.= sup {x} by A19
.= x by YELLOW_0:39;
then x in rng Sups F by Th14;
then inf rng Sups F <= x by YELLOW_2:24;
then Inf Sups F <= x by YELLOW_2:def 6;
then A43: x = Inf Sups F by A42,ORDERS_1:25
.= Sup Infs Frege F by A1,A7,A12,A26;
x is_>=_than waybelow x by WAYBEL_3:9;
then x >= sup waybelow x by YELLOW_0:32;
hence x = sup waybelow x by A38,A43,ORDERS_1:25;
end;
then A44: L is up-complete satisfying_axiom_of_approximation by WAYBEL_3:def 5;
for x being Element of L holds waybelow x is non empty directed;
hence L is continuous by A44,WAYBEL_3:def 6;
end;
Lm9: ::Theorem 2.3 (2) implies (1)
(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;
coherence
proof
A1: dom F = [:J, K:] by FUNCT_2:def 1;
then reconsider F'= F as ManySortedSet of [:J, K:] by PBOOLE:def 3;
for j being set st j in J holds
(curry F').j is Function of (J --> K).j, (J --> D).j
proof
let j be set;
assume
A2: j in J;
then A3: (J --> K).j = K & (J --> D).j = D by FUNCOP_1:13;
J = dom curry F by A1,FUNCT_5:31;
then reconsider G = (curry F').j as Function by A2,FUNCT_5:37;
consider g being Function such that
A4: (curry F').j = g and
A5: dom g = K and
A6: rng g c= rng F' and
for k being set st k in K holds g.k = F'.[j, k]
by A1,A2,FUNCT_5:36;
rng F c= D by RELSET_1:12;
then rng g c= D by A6,XBOOLE_1:1;
then reconsider g as Function of K, D by A5,FUNCT_2:def 1,RELSET_1:11;
G = g by A4;
hence (curry F').j is Function of (J --> K).j, (J --> D).j by A3;
end;
hence thesis by MSUALG_1:def 2;
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 3
.= proj1 [:J, K:] by FUNCT_2:def 1
.= J by FUNCT_5:11;
[:J, K:] <> {} & dom F = [:J, K:] & j in J 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 set st i in K holds g.i = F.[j, i]
by FUNCT_5:36;
hence dom((curry F).j) = K;
[j, k] in [:J, K:] by ZFMISC_1:106;
then [j, k] in dom F by FUNCT_2:def 1;
hence F.[j, k] = ((curry F).j).k by FUNCT_5:27;
end;
Lm10: ::Theorem 2.3 (2') implies (1)
(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;
assume
A2: for j being Element of J holds rng(F.j) is directed;
consider j being Element of J;
consider k being Element of K.j;
j in J;
then j in dom K by PBOOLE:def 3;
then k in K.j & K.j in rng K by FUNCT_1:def 5;
then reconsider K'= union rng K as non empty set by TARSKI:def 4;
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));
A3:
for j being Element of J for k' being Element of K'
ex z being Element of L st P[j, k', z]
proof
let j be Element of J;
let k' be Element of K';
per cases;
suppose k' in K.j;
then reconsider k = k' as Element of K.j;
take (F.j).k;
thus thesis;
suppose
A4: not k' in K.j;
take Bottom L;
thus thesis by A4;
end;
ex G being Function of [:J, K':], the carrier of L st
for j being Element of J
for k being Element of K' holds P[j, k, G.[j, k]] from FuncEx2D(A3);
then consider G being Function of [:J, K':], the carrier of L such that
A5: for j being Element of J for k being Element of K' holds
P[j, k, G.[j, k]];
A6: for j being Element of J holds K.j c= K'
proof
let j be Element of J;
hereby
let k be set;
assume
A7: k in K.j;
j in J;
then j in dom K by PBOOLE:def 3;
then K.j in rng K by FUNCT_1:def 5;
hence k in K' by A7,TARSKI:def 4;
end;
thus thesis;
end;
A8: 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 set;
assume y in rng(F.j);
then consider k being set such that
A9: k in dom(F.j) and
A10: y = (F.j).k by FUNCT_1:def 5;
A11: k in K.j & K.j c= K' by A6,A9,FUNCT_2:def 1;
then reconsider k as Element of K';
[j, k] in [:J, K':] by ZFMISC_1:106;
then A12: [j, k] in dom G by FUNCT_2:def 1;
k in K' & dom((curry G).j) = (J --> K').j by FUNCT_2:def 1;
then A13: k in dom((curry G).j) by FUNCOP_1:13;
y = G.[j, k] by A5,A10,A11
.= ((curry G).j).k by A12,FUNCT_5:27;
hence y in rng((curry G).j) by A13,FUNCT_1:def 5;
end;
thus thesis;
end;
A14: 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
let x, y be Element of L;
A15: rng(F.j) is directed by A2;
assume
A16: x in X & y in X;
then consider a being set such that
A17: a in dom((curry G).j) and
A18: ((curry G).j).a = x by FUNCT_1:def 5;
consider b being set such that
A19: b in dom((curry G).j) and
A20: ((curry G).j).b = y by A16,FUNCT_1:def 5;
reconsider a'= a, b'= b as Element of K' by A17,A19,Th20;
A21: x = G.[j, a'] & y = G.[j, b'] by A18,A20,Th20;
per cases;
suppose
A22: a in K.j & b in K.j;
then A23: a in dom(F.j) & b in dom(F.j) by FUNCT_2:def 1;
x = (F.j).a' & y = (F.j).b' by A5,A21,A22;
then x in rng(F.j) & y in rng(F.j) by A23,FUNCT_1:def 5;
then consider z being Element of L such that
A24: z in rng(F.j) and
A25: x <= z & y <= z by A15,WAYBEL_0:def 1;
take z;
rng(F.j) c= X by A8;
hence thesis by A24,A25;
suppose a in K.j & not b in K.j;
then A26: y = Bottom L by A5,A21;
take x;
thus thesis by A16,A26,YELLOW_0:44;
suppose not a in K.j & b in K.j;
then A27: x = Bottom L by A5,A21;
take y;
thus thesis by A16,A27,YELLOW_0:44;
suppose not a in K.j & not b in K.j;
then A28: x = Bottom L & y = Bottom L by A5,A21;
take x;
thus thesis by A16,A28;
end;
hence rng((curry G).j) is directed by WAYBEL_0:def 1;
end;
A29: dom doms F = dom F by EXTENS_1:3;
A30: dom F = J by PBOOLE:def 3;
A31: dom doms curry G = dom curry G by EXTENS_1:3;
A32: dom curry G = J by Th20;
product doms F c= product doms curry G
proof
let x be set;
assume x in product doms F;
then consider g being Function such that
A33: x = g and
A34: dom g = dom doms F and
A35: for j being set st j in dom doms F holds g.j in (doms F).j
by CARD_3:def 5;
A36: dom g = dom doms curry G by A29,A30,A31,A34,Th20;
for j being set st j in dom doms curry G holds g.j in (doms curry G).j
proof
let j be set;
assume A37: j in dom doms curry G;
then A38: j in J by A31,Th20;
reconsider j' = j as Element of J by A31,A37,Th20;
A39: g.j in (doms F).j by A29,A30,A35,A38;
A40: (doms F).j = dom(F.j') by A30,FUNCT_6:31
.= K.j' by FUNCT_2:def 1;
A41: K.j' c= K' by A6;
(doms curry G).j = dom((curry G).j') by A32,FUNCT_6:31
.= K' by Th20;
hence g.j in (doms curry G).j by A39,A40,A41;
end;
hence x in product doms curry G by A33,A36,CARD_3:def 5;
end;
then dom(Frege F) c= product doms curry G by PBOOLE:def 3;
then A42: dom(Frege F) c= dom(Frege curry G) by PBOOLE:def 3;
A43:
for f being set st f in dom(Frege F)
holds //\((Frege F).f, L) = //\((Frege curry G).f, L)
proof
let f' be set;
assume
A44: f' in dom(Frege F);
then reconsider f= f' as Element of product doms F by PBOOLE:def 3;
A45: dom((Frege F).f) = dom F by A44,Th8
.= J by PBOOLE:def 3;
A46: dom((Frege curry G).f) = dom(curry G) by A42,A44,Th8
.= proj1 dom G by FUNCT_5:def 3
.= proj1 [:J, K':] by FUNCT_2:def 1
.= J by FUNCT_5:11;
for j being set st j in J holds ((Frege F).f).j = ((Frege curry G).f).j
proof
let j' be set;
assume j' in J;
then reconsider j = j' as Element of J;
A47: f.j in K.j & K.j c= K' by A6,A44,Lm6;
then reconsider fj = f.j as Element of K';
((Frege F).f).j = (F.j).fj by A44,Lm5
.= G.[j, fj] by A5,A47
.= ((curry G).j).(f.j) by Th20
.= ((Frege curry G).f).j by A42,A44,Lm5;
hence thesis;
end;
hence //\((Frege F).f', L) = //\((Frege curry G).f', L)
by A45,A46,FUNCT_1:9;
end;
:: Unfortunately there are two cases: K = J --> K' or not.
A48: Sup Infs(Frege curry G) = Sup Infs(Frege F)
proof
per cases;
:: case I
suppose
A49: for j being Element of J holds K.j = K';
for j being set st j in J holds (doms F).j = (doms curry G).j
proof
let j be set;
assume j in J;
then reconsider j' = j as Element of J;
A50: (doms F).j = dom(F.j') by A30,FUNCT_6:31
.= K.j' by FUNCT_2:def 1;
(doms curry G).j = dom((curry G).j') by A32,FUNCT_6:31
.= K' by Th20;
hence (doms F).j = (doms curry G).j by A49,A50;
end;
then doms F = doms curry G by A29,A30,A31,A32,FUNCT_1:9;
then dom(Frege F) = product doms curry G by PBOOLE:def 3;
then dom(Frege F) = dom(Frege curry G) by PBOOLE:def 3;
hence thesis by A43,Th12;
:: case II
suppose ex j being Element of J st K.j <> K';
then consider j being Element of J such that
A51: K.j <> K';
K.j c= K' by A6;
then not K' c= K.j by A51,XBOOLE_0:def 10;
then consider k being set such that
A52: k in K' & not k in K.j by TARSKI:def 3;
reconsider k as Element of K' by A52;
A53: rng Infs(Frege curry G) c= rng Infs(Frege F) \/ {Bottom L}
proof
let x be set;
assume x in rng Infs(Frege curry G);
then consider f being set such that
A54: f in dom Frege curry G and
A55: x = //\((Frege curry G).f, L) by Th13;
reconsider f as Function by A54,Th7;
per cases;
suppose
A56: for j being Element of J holds f.j in K.j;
A57: dom f = dom curry G by A54,Th8
.= dom doms F by A29,A30,Th20;
for x st x in dom doms F holds f.x in (doms F).x
proof
let x;
assume x in dom doms F;
then reconsider j = x as Element of J by A30,EXTENS_1:3;
(doms F).j = dom(F.j) by A30,FUNCT_6:31
.= K.j by FUNCT_2:def 1;
hence thesis by A56;
end;
then f in product doms F by A57,CARD_3:18;
then A58: f in dom Frege F by PBOOLE:def 3;
then x = //\((Frege F).f, L) by A43,A55;
then x in rng Infs(Frege F) by A58,Th13;
hence thesis by XBOOLE_0:def 2;
suppose ex j being Element of J st not f.j in K.j;
then consider j being Element of J such that
A59: 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 A54,Th9;
then reconsider k = f.j as Element of K' by Th20;
Bottom L = G.[j, k] by A5,A59
.= ((curry G).j).(f.j) by Th20;
then Bottom L in rng((Frege curry G).f) by A54,Lm5;
then Bottom L >= "/\"(rng((Frege curry G).f), L) by YELLOW_2:24;
then A60: 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 A55,A60,ORDERS_1:25;
then x in {Bottom L} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 2;
end;
A61: rng Infs(Frege F) \/ {Bottom L} c= rng Infs(Frege curry G)
proof
let x be set;
assume
A62: x in rng Infs(Frege F) \/ {Bottom L};
per cases by A62,XBOOLE_0:def 2;
suppose x in rng Infs(Frege F);
then consider f being set such that
A63: f in dom Frege F and
A64: x = //\((Frege F).f, L) by Th13;
x = //\((Frege curry G).f, L) by A43,A63,A64;
hence x in rng Infs(Frege curry G) by A42,A63,Th13;
suppose A65: x in {Bottom L};
then A66: x = Bottom L by TARSKI:def 1;
reconsider x' = x as Element of L by A65;
set f = J --> k;
A67: dom f = J by FUNCOP_1:19
.= dom doms curry G by A31,Th20;
for x st x in dom doms curry G holds f.x in (doms curry G).x
proof
let x;
assume x in dom doms curry G;
then reconsider j = x as Element of J by A31,Th20;
A68: f.j = k by FUNCOP_1:13;
(doms curry G).j = dom((curry G).j) by A32,FUNCT_6:31
.= K' by Th20;
hence thesis by A68;
end;
then f in product doms curry G by A67,CARD_3:18;
then A69: f in dom Frege curry G by PBOOLE:def 3;
x = G.[j, k] by A5,A52,A66
.= ((curry G).j).k by Th20
.= ((curry G).j).(f.j) by FUNCOP_1:13;
then x in rng((Frege curry G).f) by A69,Lm5;
then x' >= "/\"(rng((Frege curry G).f), L) by YELLOW_2:24;
then A70: x' >= //\((Frege curry G).f, L) by YELLOW_2:def 6;
x' <= //\((Frege curry G).f, L) by A66,YELLOW_0:44;
then x' = //\((Frege curry G).f, L) by A70,ORDERS_1:25;
hence x in rng Infs(Frege curry G) by A69,Th13;
end;
A71: ex_sup_of rng Infs(Frege F), L & ex_sup_of {Bottom
L}, L by YELLOW_0:17;
A72: 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 A53,A61,XBOOLE_0:def
10
.= sup rng Infs(Frege F) "\/" sup{Bottom L} by A71,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 A72,YELLOW_0:24;
hence thesis;
end;
A73: dom F = J by PBOOLE:def 3
.= dom curry G by PBOOLE:def 3;
for j being set st j in dom F holds \\/(F.j, L) = \\/((curry G).j, L)
proof
let j' be set;
assume
j' in dom F;
then reconsider j = j' as Element of J by PBOOLE:def 3;
reconsider H = (curry G).j as Function of (J --> K').j, the carrier of L;
(J --> K').j = K' by FUNCOP_1:13;
then reconsider H as Function of K', the carrier of L;
A74: ex_sup_of rng(F.j),L & ex_sup_of rng((curry G).j), L by YELLOW_0:17;
rng(F.j) c= rng((curry G).j) by A8;
then sup rng(F.j) <= sup rng((curry G).j) by A74,YELLOW_0:34;
then Sup(F.j) <= sup(rng H) by YELLOW_2:def 5;
then A75: Sup(F.j) <= Sup H by YELLOW_2:def 5;
for k being Element of K' holds H.k <= Sup(F.j)
proof
let k be Element of K';
per cases;
suppose
A76: k in K.j;
then A77: (F.j).k = G.[j, k] by A5
.= H.k by Th20;
k in dom(F.j) by A76,FUNCT_2:def 1;
then H.k in rng(F.j) by A77,FUNCT_1:def 5;
then H.k <= sup rng(F.j) by YELLOW_2:24;
hence H.k <= Sup(F.j) by YELLOW_2:def 5;
suppose not k in K.j;
then Bottom L = G.[j, k] by A5
.= H.k by Th20;
hence H.k <= Sup(F.j) by YELLOW_0:44;
end;
then Sup H <= Sup(F.j) by YELLOW_2:56;
hence \\/(F.j', L) = \\/((curry G).j', L) by A75,ORDERS_1:25;
end;
hence Inf Sups F = Inf Sups(curry G) by A73,Th11
.= Sup Infs(Frege F) by A1,A14,A48;
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 consider f' being Function such that
A1: f' = f and
A2: dom f' = J and
A3: rng f' 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,A2,FUNCT_1:def 5;
hence f.j is finite Subset of K by A1,A3,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 such that
A1: f in Funcs(J, Fin K);
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];
A3: f.j is finite Subset of K by A1,Lm11;
A4:
rng(G.j) c= rng((curry F).j)
proof
let y be set;
assume y in rng(G.j);
then consider k being set such that
A5: k in dom(G.j) and
A6: y = (G.j).k by FUNCT_1:def 5;
A7: k in f.j by A5,FUNCT_2:def 1;
then A8: k in K by A3;
reconsider k as Element of K by A3,A7;
A9: k in dom((curry F).j) by A8,Th20;
y = F.[j, k] by A2,A6,A7
.= ((curry F).j).k by Th20;
hence y in rng((curry F).j) by A9,FUNCT_1:def 5;
end;
dom(G.j) is finite by A3,FUNCT_2:def 1;
then A10: (G.j).:(dom(G.j)) is finite by FINSET_1:17;
rng(G.j) c= (G.j).:(dom(G.j))
proof
let y be set;
assume y in rng(G.j);
then consider k being set such that
A11: k in dom(G.j) and
A12: y = (G.j).k by FUNCT_1:def 5;
thus y in (G.j).:(dom(G.j)) by A11,A12,FUNCT_1:def 12;
end;
hence thesis by A4,A10,FINSET_1:13;
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;
assume
A1: 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};
A2:
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
A3: f in Funcs(J, Fin K);
let G be DoubleIndexedSet of f, L such that
A4: for j, x st x in f.j holds (G.j).x = F.[j, x];
let j;
A5: 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 A3,A4,Lm12;
then sup rng((curry F).j) >= sup rng(G.j) by A5,YELLOW_0:34;
then Sup((curry F).j) >= sup rng(G.j) by YELLOW_2:def 5;
hence Sup((curry F).j) >= Sup(G.j) by YELLOW_2:def 5;
end;
A6:
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
A7: f in Funcs(J, Fin K);
let G be DoubleIndexedSet of f, L such that
A8: 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
A9: a = Sup((curry F).j) by Th14;
A10: Sup((curry F).j) >= Sup(G.j) by A2,A7,A8;
Sup(G.j) in rng Sups G by Th14;
then Sup(G.j) >= inf rng Sups G by YELLOW_2:24;
then Sup(G.j) >= Inf Sups G by YELLOW_2:def 6;
hence a >= Inf Sups G by A9,A10,ORDERS_1:26;
end;
then inf rng Sups curry F >= Inf Sups G by YELLOW_0:33;
hence Inf Sups curry F >= Inf Sups G by YELLOW_2:def 6;
end;
Inf Sups curry F is_>=_than X
proof
let a;
assume a in X;
then consider a' being Element of L such that
A11: a' = a and
A12: 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 by A1;
consider f being non-empty ManySortedSet of J such that
A13: f in Funcs(J, Fin K) and
A14: 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 A12;
consider G being DoubleIndexedSet of f, L such that
A15: for j, x st x in f.j holds (G.j).x = F.[j, x] and
A16: a' = Inf Sups G by A14;
thus Inf Sups curry F >= a by A6,A11,A13,A15,A16;
end;
hence thesis by YELLOW_0:32;
end;
Lm13: ::Theorem 2.3 (1) implies (3)
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;
let F be Function of [:J, K:], the carrier of L;
let X be Subset of L;
assume
A2: 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};
set FIK = {A where A is Subset of K: A is finite & A <> {}};
consider k being Element of K;
{k} c= K & {k} <> {} by ZFMISC_1:37;
then {k} in FIK;
then reconsider FIK as non empty set;
A3: FIK c= Fin K
proof
let x be set;
assume x in FIK;
then consider A being Subset of K such that
A4: x = A & A is finite & A <> {};
thus x in Fin K by A4,FINSUB_1:def 5;
end;
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 Lambda2D;
then consider H being Function of [:J, N:], the carrier of L such that
A5: 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;
A6: 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 set such that
A7: g in dom Hj and
A8: Hj.g = x by FUNCT_1:def 5;
reconsider g as Element of N by A7,Th20;
A9: x = H.[j, g] by A8,Th20
.= sup(Fj.:(g.j)) by A5;
consider g' being Function such that
A10: g' = g and
A11: dom g' = J and
A12: rng g' c= FIK by FUNCT_2:def 2;
g.j in rng g by A10,A11,FUNCT_1:def 5;
then g.j in FIK by A10,A12;
then consider A being Subset of K such that
A13: A = g.j & A is finite & A <> {};
reconsider Y = Fj.:(g.j) as finite Subset of R
by A13,FINSET_1:17,RELAT_1:144;
take Y;
thus thesis by A9,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;
assume
A14: Y <> {};
consider Z being set such that
A15: Z c= dom Fj and
A16: Z is finite and
A17: Fj.:Z = Y by COMPTS_1:1;
A18: Z <> {} by A14,A17,RELAT_1:149;
Z c= K by A15,Th20;
then Z in FIK by A16,A18;
then A19: {Z} c= FIK by ZFMISC_1:37;
A20: dom(J --> Z) = J by FUNCOP_1:19;
rng(J --> Z) = {Z} by FUNCOP_1:14;
then reconsider g = J --> Z as Element of N by A19,A20,FUNCT_2:def 2;
g in N;
then A21: g in dom Hj by Th20;
A22: g.j = Z by FUNCOP_1:13;
Hj.g = H.[j, g] by Th20
.= "\/"(Y, L) by A5,A17,A22;
hence "\/"(Y, L) in D by A21,FUNCT_1:def 5;
end;
end;
for j holds rng((curry H).j) is directed
proof
let j;
(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) by A6;
hence rng(cH.j) is directed by WAYBEL_0:51;
end;
then A23: Inf Sups curry H = Sup Infs Frege curry H by A1,Lm8;
A24: dom curry F = J by Th20
.= dom curry H by Th20;
for j being set st j in dom curry F holds
\\/((curry F).j, L) = \\/((curry H).j, L)
proof
let j' be set;
assume j' in dom curry F;
then reconsider j = j' as Element of J by Th20;
A25: ex_sup_of rng(cF.j),L by YELLOW_0:17;
(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) by A6;
then sup(rng(cF.j)) = sup(rng(cH.j)) by A25,WAYBEL_0:54;
then Sup(cF.j) = sup(rng(cH.j)) by YELLOW_2:def 5;
hence thesis by YELLOW_2:def 5;
end;
then A26: Inf Sups curry F = Inf Sups curry H by A24,Th11;
A27: 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 A28: h in dom Frege curry H by PBOOLE:def 3;
A29: dom id J = J by FUNCT_1:34;
A30: dom doms h = dom h by EXTENS_1:3;
A31: dom h = dom curry H by A28,Th8
.= J by Th20;
for x st x in dom doms h holds (id J).x in (doms h).x
proof
let x;
assume x in dom doms h;
then reconsider j = x as Element of J by A31,EXTENS_1:3;
A32: (id J).j = j by FUNCT_1:35;
h.j in (J --> N).j by A28,Lm6;
then h.j in N by FUNCOP_1:13;
then consider g being Function such that
A33: g = h.j and
A34: dom g = J and
rng g c= FIK by FUNCT_2:def 2;
(doms h).j = J by A31,A33,A34,FUNCT_6:31;
hence thesis by A32;
end;
then id J in product doms h by A29,A30,A31,CARD_3:18;
then A35: id J in dom Frege h by PBOOLE:def 3;
thus
A36: 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
A37: ((Frege h).(id J)).j = (h.j).((id J).j) by A31,A35,Th9
.= (h.j).j by FUNCT_1:35;
h.j in (J --> N).j by A28,Lm6;
hence
h.j in N by FUNCOP_1:13;
then consider g being Function such that
A38: g = h.j and
A39: dom g = J and
A40: rng g c= FIK by FUNCT_2:def 2;
f.j in rng g by A37,A38,A39,FUNCT_1:def 5;
then f.j in FIK by A40;
then consider A being Subset of K such that
A41: f.j = A & A is finite & A <> {};
thus f.j is finite non empty Subset of K by A41;
end;
A42: dom f = J by A31,A35,Th8;
then reconsider f'= f as ManySortedSet of J by PBOOLE:def 3;
for j being set st j in J holds f'.j is non empty by A36;
hence f is non-empty ManySortedSet of J by PBOOLE:def 16;
A43: rng f c= FIK
proof
let y be set;
assume y in rng f;
then consider j being set such that
A44: j in dom f and
A45: y = f.j by FUNCT_1:def 5;
f.j is finite non empty Subset of K by A36,A42,A44;
hence y in FIK by A45;
end;
hence f in Funcs(J, FIK) by A42,FUNCT_2:def 2;
rng f c= Fin K by A3,A43,XBOOLE_1:1;
hence f in Funcs(J, Fin K) by A42,FUNCT_2:def 2;
end;
A46: for h being Element of product doms curry H holds
Inf((Frege curry H).h) <= sup X
proof
let h be Element of product doms curry H;
h in product doms curry H;
then A47: h in dom Frege curry H by PBOOLE:def 3;
for x st x in dom h holds h.x is Function
proof
let x;
assume
A48: x in dom h;
dom h = dom curry H by A47,Th8
.= J by Th20;
then reconsider j = x as Element of J by A48;
h.j in (J --> N).j by A47,Lm6;
then h.j in N by FUNCOP_1:13;
then ex f being Function st h.j = f & dom f = J & rng f c= FIK
by FUNCT_2:def 2;
hence thesis;
end;
then reconsider h'= h as Function-yielding Function by PRALG_1:def 15;
reconsider f = (Frege h').(id J) as non-empty ManySortedSet of J by A27;
A49: f in Funcs(J, Fin K) by A27;
defpred P[set,set,set] means $1 = F.[$3, $2];
A50: for j being set st j in J holds
for x st x in f.j ex y st y in (J --> the carrier of L).j & P[y,x,j]
proof
let i;
assume i in J;
then reconsider j = i as Element of J;
let x;
assume
A51: x in f.i;
f.j is Subset of K by A27;
then reconsider k = x as Element of K by A51;
take y = F.[j, k];
[j, k] in [:J, K:] by ZFMISC_1:106;
then y in the carrier of L by FUNCT_2:7;
hence thesis by FUNCOP_1:13;
end;
ex G being ManySortedFunction of f, (J --> the carrier of L) st
for j being set st j in J holds
ex g being Function of f.j, (J --> the carrier of L).j st g = G.j &
for x st x in f.j holds P[g.x,x,j] from MSFExFunc(A50);
then consider G being ManySortedFunction of f, (J --> the carrier of L)
such that
A52: for j being set st j in J holds
ex g being Function of f.j, (J --> the carrier of L).j st g = G.j &
for x st x in f.j holds g.x = F.[j, x];
reconsider G as DoubleIndexedSet of f, L;
A53: for j, x st x in f.j holds (G.j).x = F.[j, x]
proof
let j, x;
assume
A54: x in f.j;
consider g being Function of f.j, (J --> the carrier of L).j such that
A55: g = G.j and
A56: for x st x in f.j holds g.x = F.[j, x] by A52;
thus thesis by A54,A55,A56;
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
A57: y = Sup(G.j) by Th14;
A58: ex_sup_of ((curry F.j).:(f.j)),L & ex_sup_of rng(G.j),L
by YELLOW_0:17;
(curry F.j).:(f.j) c= rng(G.j)
proof
let y be set;
assume y in (curry F.j).:(f.j);
then consider x being set such that
A59: x in dom((curry F).j) and
A60: x in f.j and
A61: y = ((curry F).j).x by FUNCT_1:def 12;
reconsider k = x as Element of K by A59,Th20;
A62: y = F.[j, k] by A61,Th20
.= (G.j).k by A53,A60;
k in dom(G.j) by A60,FUNCT_2:def 1;
hence y in rng(G.j) by A62,FUNCT_1:def 5;
end;
then sup((curry F.j).:(f.j)) <= sup rng(G.j) by A58,YELLOW_0:34;
then A63: sup((curry F.j).:(f.j)) <= Sup(G.j) by YELLOW_2:def 5;
j in J;
then A64: j in dom curry H by Th20;
h.j in (J --> N).j by A47,Lm6;
then reconsider hj = h.j as Element of N by FUNCOP_1:13;
A65: sup((curry F.j).:(f.j)) = sup((curry F.j).:(hj.j)) by A27
.= H.[j, hj] by A5
.= ((curry H).j).(h.j) by Th20
.= ((Frege curry H).h).j by A47,A64,Th9;
Inf((Frege curry H).h) <= ((Frege curry H).h).j by YELLOW_2:55;
hence Inf((Frege curry H).h) <= y by A57,A63,A65,ORDERS_1:26;
end;
then Inf((Frege curry H).h) <= inf rng Sups G by YELLOW_0:33;
then A66: Inf((Frege curry H).h) <= Inf Sups G by YELLOW_2:def 6;
Inf Sups G in X by A2,A49,A53;
then Inf Sups G <= sup X by YELLOW_2:24;
hence Inf((Frege curry H).h) <= sup X by A66,ORDERS_1:26;
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 set such that
A67: h in dom Frege curry H and
A68: x = //\((Frege curry H).h, L) by Th13;
reconsider h as Element of product doms curry H by A67,PBOOLE:def 3;
Inf((Frege curry H).h) <= sup X by A46;
hence thesis by A68;
end;
then sup rng Infs Frege curry H <= sup X by YELLOW_0:32;
then A69: Inf Sups curry F <= sup X by A23,A26,YELLOW_2:def 5;
Inf Sups curry F >= sup X by A2,Th22;
hence Inf Sups curry F = sup X by A69,ORDERS_1:25;
end;
thus thesis;
end;
Lm14: ::Theorem 2.3 (3) implies (1)
(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 RelStrSubset;
X is_<=_than Sup Infs Frege curry F
proof
let a' be Element of L;
assume a' in X;
then consider a being Element of L such that
A3: a' = 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;
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;
defpred P[set, set] means
$1 in J & $2 in K & ex b st b = ((curry F).$1).$2 & a <= b;
A9: for x st x in J ex y st y in K & P[x, y]
proof
let x;
assume
x in J;
then reconsider j = x as Element of J;
A10: rng((curry F).j) is non empty directed by A2;
rng(G.j) is finite Subset of rng((curry F).j) by 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 A10,WAYBEL_0:1;
consider k being set such that
A13: k in dom((curry F).j) and
A14: y = ((curry F).j).k by A11,FUNCT_1:def 5;
reconsider k as Element of K by A13,Th20;
take k;
sup rng(G.j) <= y by A12,YELLOW_0:32;
then A15: Sup(G.j) <= y by YELLOW_2:def 5;
Sup(G.j) in rng Sups G by Th14;
then inf rng Sups G <= Sup(G.j) by YELLOW_2:24;
then Inf Sups G <= Sup(G.j) by YELLOW_2:def 6;
then a <= y by A8,A15,ORDERS_1:26;
hence thesis by A14;
end;
consider g being Function such that
A16: dom g = J and rng g c= K and
A17: for x st x in J holds P[x, g.x] from NonUniqBoundFuncEx(A9);
A18: dom doms curry F = dom curry F by EXTENS_1:3;
then A19: dom g = dom doms curry F by A16,Th20;
for x st x in dom doms curry F holds g.x in (doms curry F).x
proof
let x;
assume x in dom doms curry F;
then reconsider j = x as Element of J by A18,Th20;
dom curry F = J by Th20;
then (doms curry F).j = dom((curry F).j) by FUNCT_6:31
.= K by Th20;
hence thesis by A17;
end;
then reconsider g as Element of product doms curry F by A19,CARD_3:18;
for j holds a <= ((Frege curry F).g).j
proof
let j;
A20: dom Frege curry F = product doms curry F by PBOOLE:def 3;
A21: J = dom curry F by Th20;
consider b such that
A22: b = ((curry F).j).(g.j) & a <= b by A17;
thus thesis by A20,A21,A22,Th9;
end;
then A23: a <= Inf((Frege curry F).g) by YELLOW_2:57;
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:24
;
then Inf((Frege curry F).g) <= Sup Infs Frege curry F by YELLOW_2:def 5;
hence a' <= Sup Infs Frege curry F by A3,A23,ORDERS_1:26;
end;
then sup X <= Sup Infs Frege curry F by YELLOW_0:32;
then A24: Inf Sups curry F <= Sup Infs Frege curry F by A1;
Inf Sups curry F >= Sup Infs Frege curry F by Th16;
hence Inf Sups curry F = Sup Infs Frege curry F by A24,ORDERS_1:25;
end;
hence L is continuous 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 ::Definition 2.4
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;
definition
cluster trivial -> completely-distributive (non empty Poset);
coherence
proof
let L be non empty Poset;
assume
A1: L is trivial;
consider x being Element of L;
thus L is complete
proof
let X be set;
take x;
thus X is_<=_than x
proof
let y be Element of L;
thus y in X implies y <= x by A1,REALSET1:def 20;
end;
let y be Element of L;
y = x by A1,REALSET1:def 20;
hence thesis by ORDERS_1:24;
end;
then L is complete (non empty Poset);
then reconsider L'= L as complete LATTICE;
for x being Element of L' holds x = sup waybelow x
by A1,REALSET1:def 20;
then A2: L' is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
for x being Element of L' holds waybelow x is non empty directed;
then reconsider L' as continuous LATTICE by A2,WAYBEL_3:def 6;
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)
proof
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K, L';
for j being Element of J holds rng(F.j) is directed
proof
let j be Element of J;
for x, y being Element of L st x in rng(F.j) & y in rng(F.j)
ex z being Element of L st z in rng(F.j) & x <= z & y <= z
proof
let x, y be Element of L;
assume x in rng(F.j) & y in rng(F.j);
consider z being Element of rng(F.j);
reconsider z as Element of L;
take z;
thus thesis by A1,REALSET1:def 20;
end;
hence rng(F.j) is directed by WAYBEL_0:def 1;
end;
hence Inf Sups F = Sup Infs(Frege F) by Lm8;
end;
hence thesis;
end;
end;
definition
cluster completely-distributive LATTICE;
existence
proof
consider x being set, R be Order of {x};
RelStr(#{x},R#) is trivial non empty 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;
L is complete & (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;
hence L is continuous by Lm9;
end;
definition
cluster completely-distributive -> complete continuous LATTICE;
correctness by Def3,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;
X is_<=_than sup X by A1,YELLOW_0:30;
then y <= z & z <= sup X by A4,A5,LATTICE3:def 9,YELLOW_0:23;
then y <= x & y <= sup X by A4,YELLOW_0:23,def 2;
hence y <= x "/\" sup X by YELLOW_0:23;
end;
hence sup Y <= x "/\" sup X 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 & F.2 = id X by FUNCT_4:66;
A2: K.1 = {1} & K.2 = X by FUNCT_4:66;
reconsider j1 = 1, j2 = 2 as Element of J by TARSKI:def 2;
dom K = J by FUNCT_4:65;
then reconsider K as ManySortedSet of J by PBOOLE:def 3;
i in J implies K.i is non empty by A2,TARSKI:def 2;
then reconsider K as non-empty ManySortedSet of J by PBOOLE:def 16;
dom F = J by FUNCT_4:65;
then reconsider F as ManySortedSet of J by PBOOLE:def 3;
for j being set st j in J holds F.j is
Function of K.j, (J --> the carrier of L).j
proof
let j be set;
assume
A3: j in J;
then A4: (J --> the carrier of L).j = the carrier of L by FUNCOP_1:13;
per cases by A3,TARSKI:def 2;
suppose j = 1;
hence F.j is Function of K.j, (J --> the carrier of L).j
by A2,A4,FUNCT_4:66;
suppose j = 2;
hence F.j is Function of K.j, (J --> the carrier of L).j
by A1,A2,A4,FUNCT_2:9;
end;
then reconsider F as DoubleIndexedSet of K, L by MSUALG_1:def 2;
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
A5: y = Sup(F.j) by Th14;
per cases by TARSKI:def 2;
suppose j = 1;
then rng(F.j) = {x} by A1,FUNCOP_1:14;
then Sup(F.j) = sup{x} by YELLOW_2:def 5;
then y = x by A5,YELLOW_0:39;
hence x "/\" sup X <= y by YELLOW_0:23;
suppose j = 2;
then rng(F.j) = X by A1,RELAT_1:71;
then y = sup X by A5,YELLOW_2:def 5;
hence x "/\" sup X <= y by YELLOW_0:23;
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 A6: x "/\" sup X <= Sup Infs Frege F by Def3;
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 set such that
A7: f in dom Frege F and
A8: y = //\(((Frege F).f), L) by Th13;
reconsider f as Function by A7,Th7;
A9: f.j1 in K.j1 & f.j2 in K.j2 by A7,Lm6;
then reconsider f2 = f.2 as Element of X by FUNCT_4:66;
A10: y = "/\"(rng((Frege F).f), L) by A8,YELLOW_2:def 6;
A11: ex_inf_of rng((Frege F).f),L & ex_inf_of {x, f.2},L by YELLOW_0:17;
{x, f2} c= rng((Frege F).f)
proof
let z be set;
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,A2,A9,FUNCOP_1:13,FUNCT_1:35;
hence z in rng((Frege F).f) by A7,Lm5;
end;
then y <= inf{x, f2} by A10,A11,YELLOW_0:35;
then A12: y <= x"/\"f2 by YELLOW_0:40;
x"/\"f2 in A;
then x"/\"f2 <= "\/"(A, L) by YELLOW_2:24;
hence thesis by A12,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 Sup Infs Frege F <= "\/"({x"/\"y where y is Element of L: y in X}, L)
by YELLOW_2:def 5;
then A13: x "/\" sup X <= "\/"({x"/\"y where y is Element of L: y in X}, L) by
A6,YELLOW_0:def 2;
(x "/\").:X = A by WAYBEL_1:64;
then reconsider A'= A as Subset of L;
ex_sup_of X,L & ex_sup_of A',L by YELLOW_0:17;
then x "/\" sup X >= sup A' by Th25;
hence thesis by A13,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
assume
A2: A <> {};
consider z being Element of A;
z in A by A2;
then consider y being Element of L such that
A3: z = x"/\"y & y in X;
thus contradiction by A1,A3;
end;
then sup X = Bottom L & "\/"(A, L) = Bottom
L by A1,YELLOW_0:def 11; hence thesis by WAYBEL_1:4;
suppose X is non empty;
hence thesis by Lm15;
end;
definition
cluster completely-distributive -> Heyting 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 "/\" has_an_upper_adjoint by
WAYBEL_1:67;
hence thesis by WAYBEL_1:def 19;
end;
end;
:: For distributivity confer WAYBEL_1.
begin :: SubFrames of Continuous Lattices
definition ::Definition 2.6
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;
assume
A1: for j being Element of J holds rng(F.j) is directed;
set X = rng Infs Frege F;
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 g being set such that
A4: g in dom(Frege F) and
A5: x = //\((Frege F).g, L) by A2,Th13;
reconsider g as Function by A4,Th7;
reconsider G = (Frege F).g as Function of J, the carrier of L
by A4,Th10;
A6: x = "/\"(rng((Frege F).g), L) by A5,YELLOW_2:def 6;
A7: ex_inf_of rng((Frege F).g),L by YELLOW_0:17;
consider h being set such that
A8: h in dom(Frege F) and
A9: y = //\((Frege F).h, L) by A3,Th13;
reconsider h as Function by A8,Th7;
reconsider H = (Frege F).h as Function of J, the carrier of L
by A8,Th10;
A10: y = "/\"(rng((Frege F).h), L) by A9,YELLOW_2:def 6;
A11: ex_inf_of rng((Frege F).h),L by YELLOW_0:17;
A12:
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 j in dom F by PBOOLE:def 3;
then A13: G.j = (F.j).(g.j) & H.j = (F.j).(h.j) by A4,A8,Th9;
A14: rng(F.j) is directed Subset of L by A1;
j in J;
then j in dom F by PBOOLE:def 3;
then g.j in dom(F.j) & h.j in dom(F.j) by A4,A8,Th9;
then G.j in rng(F.j) & H.j in rng(F.j) by A13,FUNCT_1:def 5;
then consider c being Element of L such that
A15: c in rng(F.j) and
A16: G.j <= c & H.j <= c by A14,WAYBEL_0:def 1;
consider k being set such that
A17: k in dom(F.j) and
A18: c = (F.j).k by A15,FUNCT_1:def 5;
reconsider k as Element of K.j by A17,FUNCT_2:def 1;
take k;
thus G.j <= (F.j).k & H.j <= (F.j).k by A16,A18;
end;
defpred P[set, set] 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);
A19:
for j being set st j in J ex k being set st k in union rng K & P[j, k]
proof
let j' be set;
assume j' in J;
then reconsider j = j' as Element of J;
consider k being Element of K.j such that
A20: G.j <= (F.j).k and
A21: H.j <= (F.j).k by A12;
take k;
j in J;
then j in dom K by PBOOLE:def 3;
then k in K.j & K.j in rng K by FUNCT_1:def 5;
hence k in union rng K by TARSKI:def 4;
thus P[j', k] by A20,A21;
end;
consider f being Function such that
A22: dom f = J and rng f c= union rng K and
A23: for j being set st j in J holds P[j, f.j] from NonUniqBoundFuncEx(A19);
A24: dom f = dom F by A22,PBOOLE:def 3
.= dom doms F by EXTENS_1:3;
now
let x be set;
assume x in dom doms F;
then A25: x in dom F by EXTENS_1:3;
then reconsider j = x as Element of J by PBOOLE:def 3;
(doms F).x = dom(F.j) by A25,FUNCT_6:31
.= K.j by FUNCT_2:def 1;
hence f.x in (doms F).x by A23;
end;
then f in product doms F by A24,CARD_3:18;
then A26: f in dom(Frege F) by PBOOLE:def 3;
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;
now
let j be Element of J;
A27: j in J;
then j in dom G by FUNCT_2:def 1;
then A28: G.j in rng G by FUNCT_1:def 5;
x is_<=_than rng G by A6,A7,YELLOW_0:def 10;
then A29: x <= G.j by A28,LATTICE3:def 8;
j in dom F by A27,PBOOLE:def 3;
then (F.j).(f.j) = ((Frege F).f).j by A26,Th9;
then G.j <= Ff.j by A23;
hence x <= Ff.j by A29,ORDERS_1:26;
end;
hence x <= z by YELLOW_2:57;
now
let j be Element of J;
A30: j in J;
then j in dom H by FUNCT_2:def 1;
then A31: H.j in rng H by FUNCT_1:def 5;
y is_<=_than rng H by A10,A11,YELLOW_0:def 10;
then A32: y <= H.j by A31,LATTICE3:def 8;
j in dom F by A30,PBOOLE:def 3;
then (F.j).(f.j) = ((Frege F).f).j by A26,Th9;
then H.j <= Ff.j by A23;
hence y <= Ff.j by A32,ORDERS_1:26;
end;
hence y <= z by YELLOW_2:57;
end;
hence X is directed 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;
reconsider L'= L as complete LATTICE;
let S be CLSubFrame of L;
A2: S is complete LATTICE by YELLOW_2:32;
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 set;
assume
A4: j in J;
then reconsider j'= j as Element of J;
A5: F.j' is Function of K.j', the carrier of S;
A6: the carrier of S c= the carrier of L by YELLOW_0:def 13;
(J --> the carrier of L).j = the carrier of L by A4,FUNCOP_1:13;
hence F.j is Function of K.j, (J --> the carrier of L).j by A5,A6,FUNCT_2
:9;
end;
then reconsider F'= F as DoubleIndexedSet of K, L by MSUALG_1:def 2;
for j being Element of J holds rng(F'.j) is directed
proof
let j be Element of J;
rng(F.j) is directed by A3;
hence rng(F'.j) is directed by YELLOW_2:7;
end;
then A7: Inf Sups F' = Sup Infs Frege F' by A1,Lm8;
A8: ex_inf_of (rng Sups F'),L' by YELLOW_0:17;
now
let x;
assume x in rng Sups F;
then consider j being Element of J such that
A9: x = Sup(F.j) by Th14;
A10: ex_sup_of rng(F.j),L' by YELLOW_0:17;
A11: rng(F.j) is directed Subset of S by A3;
x = sup rng(F.j) by A9,YELLOW_2:def 5
.= sup rng(F'.j) by A10,A11,WAYBEL_0:7
.= Sup(F'.j) by YELLOW_2:def 5;
hence x in rng Sups F' by Th14;
end;
then A12: rng Sups F c= rng Sups F' by TARSKI:def 3;
now
let x;
assume x in rng Sups F';
then consider j being Element of J such that
A13: x = Sup(F'.j) by Th14;
A14: ex_sup_of rng(F.j),L' by YELLOW_0:17;
A15: rng(F.j) is directed Subset of S by A3;
x = sup rng(F'.j) by A13,YELLOW_2:def 5
.= sup rng(F.j) by A14,A15,WAYBEL_0:7
.= Sup(F.j) by YELLOW_2:def 5;
hence x in rng Sups F by Th14;
end;
then rng Sups F' c= rng Sups F by TARSKI:def 3;
then A16: rng Sups F' = rng Sups F by A12,XBOOLE_0:def 10;
ex_inf_of rng Sups F,L by YELLOW_0:17;
then "/\"(rng Sups F,L) in the carrier of S by YELLOW_0:def 18;
then inf rng Sups F' = inf rng Sups F by A8,A16,YELLOW_0:64;
then A17: Inf Sups F' = inf rng Sups F by YELLOW_2:def 6;
A18: ex_sup_of rng /\\(Frege F', L),L' by YELLOW_0:17;
A19: rng Infs Frege F is non empty directed Subset of S by A2,A3,Th27;
now
let x;
assume x in rng /\\(Frege F', L);
then consider f being set such that
A20: f in dom(Frege F') and
A21: x = //\((Frege F').f, L) by Th13;
reconsider f as Element of product doms F' by A20,Lm7;
(Frege F).f is Function of J, the carrier of S by A20,Th10;
then rng((Frege F).f) c= the carrier of S by RELSET_1:12;
then A22: rng((Frege F).f) is Subset of S;
A23: ex_inf_of rng((Frege F).f),L' by YELLOW_0:17;
then A24: "/\"(rng((Frege F).f), L) in the carrier of S by A22,YELLOW_0:def 18;
x = "/\"(rng((Frege F').f), L) by A21,YELLOW_2:def 6
.= "/\"(rng((Frege F).f), S) by A22,A23,A24,YELLOW_0:64
.= //\((Frege F).f, S) by YELLOW_2:def 6;
hence x in rng Infs Frege F by A20,Th13;
end;
then A25: rng /\\(Frege F', L) c= rng /\\(Frege F, S) by TARSKI:def 3;
now
let x;
assume x in rng Infs Frege F;
then consider f being set such that
A26: f in dom(Frege F) and
A27: x = //\((Frege F).f, S) by Th13;
reconsider f as Function by A26,Th7;
(Frege F).f is Function of J, the carrier of S by A26,Th10;
then rng((Frege F).f) c= the carrier of S by RELSET_1:12;
then A28: rng((Frege F).f) is Subset of S;
A29: ex_inf_of rng((Frege F).f),L' by YELLOW_0:17;
then A30: "/\"(rng((Frege F).f), L) in the carrier of S by A28,YELLOW_0:def 18;
x = "/\"(rng((Frege F).f), S) by A27,YELLOW_2:def 6
.= "/\"(rng((Frege F').f), L) by A28,A29,A30,YELLOW_0:64
.= //\((Frege F').f, L) by YELLOW_2:def 6;
hence x in rng Infs Frege F' by A26,Th13;
end;
then rng Infs Frege F c= rng Infs Frege F' by TARSKI:def 3;
then rng Infs Frege F' = rng Infs Frege F by A25,XBOOLE_0:def 10;
then sup rng Infs Frege F' = sup rng Infs Frege F by A18,A19,WAYBEL_0:7;
then Sup Infs Frege F' = sup rng Infs Frege F by YELLOW_2:def 5
.= Sup Infs Frege F by YELLOW_2:def 5;
hence Inf Sups F = Sup Infs Frege F by A7,A17,YELLOW_2:def 6;
end;
hence S is continuous LATTICE by A2,Lm9;
end;
theorem Th29:
for S being non empty Poset st ex g being map of L, S st
g is infs-preserving onto
holds
S is complete LATTICE
proof
let S be non empty Poset;
given g being map 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:147;
A4: ex_inf_of Y,L by YELLOW_0:17;
g preserves_inf_of Y by A1,WAYBEL_0:def 32;
hence thesis by A3,A4,WAYBEL_0:def 30;
end;
then S is complete (non empty Poset) by YELLOW_2:30;
hence S is complete LATTICE;
end;
definition
let J be set, y be set;
redefine func J --> y;
synonym J => y;
end;
definition
let J be set, y be set;
redefine func J --> y -> ManySortedSet of J;
coherence
proof
dom (J --> y) = J by FUNCOP_1:19;
hence thesis by PBOOLE:def 3;
end;
synonym J => y;
end;
definition
let A, B, J be set, f be Function of A, B;
redefine func J => f -> ManySortedFunction of (J --> A), (J --> B);
coherence
proof
set JA = J --> A, JB = J --> B;
for j being set st j in J holds (J => f).j is Function of JA.j, JB.j
proof
let j be set;
assume j in J;
then (J => f).j = f & JA.j = A & JB.j = B by FUNCOP_1:13;
hence (J => f).j is Function of JA.j, JB.j;
end;
hence thesis by MSUALG_1:def 2;
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;
assume
A1: g*f = id A;
set F = (J => g)**(J => f);
dom F = J by MSUALG_3:2;
then reconsider F as ManySortedSet of J by PBOOLE:def 3;
A2:
for j being set st j in J holds F.j = id ((J --> A).j)
proof
let j be set;
assume
A3: j in J;
then (J => g).j = g & (J => f).j = f & (J --> A).j = A by FUNCOP_1:13;
hence F.j = id ((J --> A).j) by A1,A3,MSUALG_3:2;
end;
now
let j be set;
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 MSUALG_1:
def 2;
for j being set st j in J holds F.j = id ((J --> A).j) by A2;
hence (J => g)**(J => f) = id (J --> A) 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 PBOOLE:def 3;
for j being set st j in J holds fF.j is Function of K.j, (J --> B).j
proof
let j be set;
assume
A1: j in J;
then reconsider j'= j as Element of J;
reconsider Fj = F.j' as Function of K.j, A;
A2: (J --> B).j = B by A1,FUNCOP_1:13;
fF.j = ((J => f).j)*(F.j) by A1,MSUALG_3:2
.= f*Fj by FUNCOP_1:13;
hence fF.j is Function of K.j, (J --> B).j by A2;
end;
hence (J --> f)**F is DoubleIndexedSet of K, B by MSUALG_1:def 2;
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 EXTENS_1:3
.= J by MSUALG_3:2;
A2:
dom doms F = dom F by EXTENS_1:3
.= J by PBOOLE:def 3;
now
let x be set;
assume
A3: x in J;
then reconsider j = x as Element of J;
A4: rng(F.j) c= A & dom f = A by FUNCT_2:def 1,RELSET_1:12;
A5: j in dom F by A3,PBOOLE:def 3;
j in dom((J => f)**F) by A1,A3,EXTENS_1:3;
then (doms((J => f)**F)).j = dom(((J => f)**F).j) by FUNCT_6:31
.= dom(((J => f).j)*(F.j)) by MSUALG_3:2
.= dom(f*(F.j)) by FUNCOP_1:13
.= dom(F.j) by A4,RELAT_1:46
.= (doms F).j by A5,FUNCT_6:31;
hence (doms((J => f)**F)).x = (doms F).x;
end;
hence thesis by A1,A2,FUNCT_1:9;
end;
theorem ::Theorem 2.7 (iii)
L is continuous implies
for S being non empty Poset st ex g being map 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 map of L, S such that
A2: g is infs-preserving directed-sups-preserving and
A3: g is onto;
reconsider S'= S as complete LATTICE by A2,A3,Th29;
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
A4: for j being Element of J holds rng(F.j) is directed;
consider d being map 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:15;
for t being Element of S holds d.t is_minimum_of g"{t}
by A3,A5,WAYBEL_1:23;
then g*d = id S by WAYBEL_1:24;
then A6: g*d = id the carrier of S by GRCAT_1:def 11;
A7: d is monotone by A5,WAYBEL_1:9;
reconsider dF = (J => d)**F as DoubleIndexedSet of K, L by Th31;
A8: for j being Element of J holds rng(dF.j) is directed
proof
let j be Element of J;
(J => d).j = d by FUNCOP_1:13;
then A9: rng(dF.j) = rng(d*(F.j)) by MSUALG_3:2
.= d.:(rng(F.j)) by RELAT_1:160;
rng(F.j) is directed by A4;
hence rng(dF.j) is directed by A7,A9,YELLOW_2:17;
end;
reconsider gdF = (J => g)**dF as DoubleIndexedSet of K, S;
A10:
F = (id (J --> the carrier of S))**F by MSUALG_3:4
.= ((J --> g)**(J --> d))**F by A6,Th30
.= gdF by AUTALG_1:13;
A11: rng Sups gdF c= g.:(rng Sups dF)
proof
let y be set;
assume y in rng Sups gdF;
then consider j being Element of J such that
A12: y = Sup(gdF.j) by Th14;
gdF.j = ((J => g).j)*(dF.j) by MSUALG_3:2
.= g*(dF.j) by FUNCOP_1:13;
then rng(gdF.j) = g.:(rng(dF.j)) by RELAT_1:160;
then A13: y = sup(g.:(rng(dF.j))) by A12,YELLOW_2:def 5;
rng(dF.j) is directed by A8;
then A14: 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 A14,WAYBEL_0:def 31;
then A15: y = g.Sup(dF.j) by A13,YELLOW_2:def 5;
Sup(dF.j) in the carrier of L & Sup(dF.j) in rng Sups dF by Th14;
hence y in g.:(rng Sups dF) by A15,FUNCT_2:43;
end;
A16: g.:(rng Sups dF) c= rng Sups gdF
proof
let y be set;
assume y in g.:(rng Sups dF);
then consider x being set such that
x in the carrier of L and
A17: x in rng Sups dF and
A18: y = g.x by FUNCT_2:115;
consider j being Element of J such that
A19: x = Sup(dF.j) by A17,Th14;
rng(dF.j) is directed by A8;
then A20: 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 A20,WAYBEL_0:def 31;
then A21: y = sup(g.:(rng(dF.j))) by A18,A19,YELLOW_2:def 5;
gdF.j = ((J => g).j)*(dF.j) by MSUALG_3:2
.= g*(dF.j) by FUNCOP_1:13;
then rng(gdF.j) = g.:(rng(dF.j)) by RELAT_1:160;
then y = Sup(gdF.j) by A21,YELLOW_2:def 5;
hence y in rng Sups gdF by Th14;
end;
A22: ex_inf_of (rng Sups dF),L by YELLOW_0:17;
A23: g preserves_inf_of (rng Sups dF) by A2,WAYBEL_0:def 32;
rng Infs Frege dF is directed non empty by A8,Th27;
then A24: g preserves_sup_of rng Infs Frege dF by A2,WAYBEL_0:def 37;
A25: ex_sup_of rng Infs Frege dF,L by YELLOW_0:17;
A26: 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
A27: f in dom(Frege dF);
then reconsider f as Element of product doms dF by PBOOLE:def 3;
A28: dom(Frege dF) = product(doms dF) by PBOOLE:def 3
.= product(doms F) by Th32
.= dom(Frege F) by PBOOLE:def 3;
A29: dom((Frege dF).f) = dom dF by A27,Th8
.= J by PBOOLE:def 3;
A30: dom((Frege F).f) = dom F by A27,A28,Th8
.= J by PBOOLE:def 3;
dom g = the carrier of L by FUNCT_2:def 1;
then rng((Frege dF).f) c= dom g;
then A31: dom(g*((Frege dF).f)) = dom((Frege dF).f) by RELAT_1:46;
now
let i be set;
assume
A32: i in J;
then reconsider j = i as Element of J;
A33: j in dom dF by A32,PBOOLE:def 3;
then f.j in dom(dF.j) by A27,Th9;
then f.j in dom(((J => d).j)*(F.j)) by MSUALG_3:2;
then A34: f.j in dom(d*(F.j)) by FUNCOP_1:13;
A35: j in dom F by A32,PBOOLE:def 3;
(g*((Frege dF).f)).j = g.(((Frege dF).f).j) by A29,FUNCT_1:23
.= g.((dF.j).(f.j)) by A27,A33,Th9
.= g.((((J => d).j)*(F.j)).(f.j)) by MSUALG_3:2
.= g.((d*(F.j)).(f.j)) by FUNCOP_1:13
.= (g*(d*(F.j))).(f.j) by A34,FUNCT_1:23
.= ((id the carrier of S)*(F.j)).(f.j) by A6,
RELAT_1:55
.= (F.j).(f.j) by FUNCT_2:23
.= ((Frege F).f).j by A27,A28,A35,Th9;
hence (g*((Frege dF).f)).i = ((Frege F).f).i;
end;
then rng((Frege F).f) = rng(g*((Frege dF).f)) by A29,A30,A31,FUNCT_1:9
.= g.:(rng((Frege dF).f)) by RELAT_1:160;
hence thesis;
end;
A36: g.:(rng Infs Frege dF) c= rng Infs Frege F
proof
let y be set;
assume y in g.:(rng Infs Frege dF);
then consider x being set such that
x in the carrier of L and
A37: x in rng Infs Frege dF and
A38: y = g.x by FUNCT_2:115;
consider f being set such that
A39: f in dom(Frege dF) and
A40: x = //\((Frege dF).f, L) by A37,Th13;
reconsider f as Element of product doms dF by A39,PBOOLE:def 3;
reconsider f'= f as Element of product doms F by Th32;
set X = rng((Frege dF).f);
A41: g preserves_inf_of X by A2,WAYBEL_0:def 32;
ex_inf_of X,L by YELLOW_0:17;
then inf(g.:X) = g.inf X by A41,WAYBEL_0:def 30;
then A42: y = inf(g.:X) by A38,A40,YELLOW_2:def 6;
A43: dom(Frege dF) = product(doms dF) by PBOOLE:def 3
.= product(doms F) by Th32
.= dom(Frege F) by PBOOLE:def 3;
rng((Frege F).f) = g.:(rng((Frege dF).f)) by A26,A39;
then y = Inf((Frege F).f') by A42,YELLOW_2:def 6;
hence y in rng Infs Frege F by A39,A43,Th13;
end;
A44: rng Infs Frege F c= g.:(rng Infs Frege dF)
proof
let y be set;
assume y in rng Infs Frege F;
then consider f being set such that
A45: f in dom(Frege F) and
A46: y = //\((Frege F).f, S) by Th13;
reconsider f as Element of product doms F by A45,PBOOLE:def 3;
reconsider f'= f as Element of product doms dF by Th32;
A47: dom(Frege dF) = product(doms dF) by PBOOLE:def 3
.= product(doms F) by Th32
.= dom(Frege F) by PBOOLE:def 3;
then rng((Frege F).f) = g.:(rng((Frege dF).f)) by A26,A45;
then A48: y = "/\"(g.:(rng((Frege dF).f)), S) by A46,YELLOW_2:def 6;
set X = rng((Frege dF).f');
A49: g preserves_inf_of X by A2,WAYBEL_0:def 32;
ex_inf_of X,L by YELLOW_0:17;
then A50: y = g.inf X by A48,A49,WAYBEL_0:def 30
.= g.Inf((Frege dF).f') by YELLOW_2:def 6;
Inf((Frege dF).f') in rng Infs Frege dF by A45,A47,Th13;
hence y in g.:(rng Infs Frege dF) by A50,FUNCT_2:43;
end;
Inf Sups F = inf rng Sups gdF by A10,YELLOW_2:def 6
.= inf (g.:(rng Sups dF)) by A11,A16,XBOOLE_0:def 10
.= g.(inf rng Sups dF) by A22,A23,WAYBEL_0:def 30
.= g.(Inf Sups dF) by YELLOW_2:def 6
.= g.(Sup Infs Frege dF) by A1,A8,Lm8
.= g.(sup rng Infs Frege dF) by YELLOW_2:def 5
.= sup(g.:(rng Infs Frege dF)) by A24,A25,WAYBEL_0:def 31
.= sup rng Infs Frege F by A36,A44,XBOOLE_0:def 10
.= Sup Infs Frege F by YELLOW_2:def 5;
hence thesis;
end;
hence S is continuous LATTICE by Lm9;
end;