:: Representation theorem for free continuous lattices
:: by Piotr Rudnicki
::
:: Received July 21, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REWRITE1, WAYBEL_0, TARSKI, ZFMISC_1, STRUCT_0, LATTICES,
ORDINAL2, SUBSET_1, EQREL_1, XBOOLE_0, YELLOW_1, ARYTM_0, ORDERS_2,
WAYBEL16, RELAT_1, YELLOW_0, LATTICE3, WAYBEL_5, WELLORD2, CARD_FIL,
WELLORD1, CAT_1, SETFAM_1, XXREAL_0, FUNCT_1, CARD_1, SEQM_3, PBOOLE,
FUNCOP_1, YELLOW_2, CARD_3, FUNCT_6, WAYBEL22, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_6, ORDERS_1, STRUCT_0,
WELLORD1, CARD_1, CARD_3, ORDERS_2, LATTICE3, FUNCOP_1, YELLOW_0,
YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5,
WAYBEL16;
constructors DOMAIN_1, TOLER_1, ORDERS_3, PRALG_3, WAYBEL_5, WAYBEL_8,
WAYBEL16, RELSET_1, WAYBEL20;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3, PBOOLE,
STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_5, YELLOW_7,
WAYBEL_8, WAYBEL16, FUNCT_1, RELAT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, ORDERS_3, LATTICE3, WELLORD2, YELLOW_0, WAYBEL_0;
equalities LATTICE3, YELLOW_0, WAYBEL_0, STRUCT_0;
expansions FUNCT_1, LATTICE3, WELLORD2, WAYBEL_0;
theorems TARSKI, CARD_1, ZFMISC_1, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_3, FUNCT_4, FUNCT_6, FUNCOP_1, WELLORD1, WELLORD2, CARD_3,
LATTICE3, PBOOLE, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1,
WAYBEL_5, WAYBEL11, WAYBEL13, WAYBEL14, WAYBEL15, WAYBEL16, WAYBEL17,
RELSET_1, WAYBEL_4, WAYBEL20, XBOOLE_0, XBOOLE_1, PARTFUN1;
schemes CLASSES1, FUNCT_2, MSSUBFAM, YELLOW_3;
begin :: Preliminaries
Lm1: for L being complete LATTICE, X being set st X c= bool the carrier of L
holds "/\"(union X, L) = "/\"({inf Y where Y is Subset of L: Y in X}, L)
proof
let L be complete LATTICE, X be set such that
A1: X c= bool the carrier of L;
defpred P[Subset of L] means $1 in X;
set XX = {Z where Z is Subset of L : P[Z]};
A2: now
let x be object;
hereby
assume x in XX;
then ex Z being Subset of L st x = Z & Z in X;
hence x in X;
end;
assume
A3: x in X;
then reconsider x9 = x as Subset of L by A1;
x9 in XX by A3;
hence x in XX;
end;
"/\"({"/\"(Y, L) where Y is Subset of L: P[Y]}, L) = "/\"(union XX, L)
from YELLOW_3:sch 3;
hence thesis by A2,TARSKI:2;
end;
Lm2: for L being complete LATTICE, X being set st X c= bool the carrier of L
holds "\/"(union X, L) = "\/"({sup Y where Y is Subset of L: Y in X}, L)
proof
let L be complete LATTICE, X be set such that
A1: X c= bool the carrier of L;
defpred P[set] means $1 in X;
set XX = {Z where Z is Subset of L : P[Z]};
A2: now
let x be object;
hereby
assume x in XX;
then ex Z being Subset of L st x = Z & Z in X;
hence x in X;
end;
assume
A3: x in X;
then reconsider x9 = x as Subset of L by A1;
x9 in XX by A3;
hence x in XX;
end;
"\/"({"\/"(Y, L) where Y is Subset of L: P[Y]}, L) = "\/"(union XX, L)
from YELLOW_3:sch 5;
hence thesis by A2,TARSKI:2;
end;
theorem Th1: :: cf. WAYBEL13:9
for L being upper-bounded Semilattice, F being non empty directed
Subset of InclPoset Filt L holds sup F = union F
proof
let L be upper-bounded Semilattice, F be non empty directed Subset of
InclPoset Filt L;
Filt L = Ids (L opp) by WAYBEL16:7;
hence thesis by WAYBEL13:9;
end;
theorem Th2:
for L, S, T being complete non empty Poset, f being
CLHomomorphism of L, S, g being CLHomomorphism of S, T holds g*f is
CLHomomorphism of L, T
proof
let L, S, T be complete non empty Poset, f be CLHomomorphism of L, S, g be
CLHomomorphism of S, T;
f is directed-sups-preserving & g is directed-sups-preserving by
WAYBEL16:def 1;
then
A1: g*f is directed-sups-preserving by WAYBEL20:28;
f is infs-preserving & g is infs-preserving by WAYBEL16:def 1;
then g*f is infs-preserving by WAYBEL20:25;
hence thesis by A1,WAYBEL16:def 1;
end;
theorem Th3:
for L being non empty RelStr holds id L is infs-preserving
proof
let L be non empty RelStr;
let X be Subset of L;
set f = id L;
assume ex_inf_of X, L;
hence ex_inf_of f.:X, L by FUNCT_1:92;
f.:X = X by FUNCT_1:92;
hence thesis;
end;
theorem Th4:
for L being non empty RelStr holds id L is directed-sups-preserving
proof
let L be non empty RelStr;
let X be Subset of L such that
X is non empty directed;
set f = id L;
assume ex_sup_of X, L;
hence ex_sup_of f.:X, L by FUNCT_1:92;
f.:X = X by FUNCT_1:92;
hence thesis;
end;
theorem Th5:
for L being complete non empty Poset holds id L is CLHomomorphism of L, L
proof
let L be complete non empty Poset;
id L is directed-sups-preserving & id L is infs-preserving by Th3,Th4;
hence thesis by WAYBEL16:def 1;
end;
theorem Th6:
for L being upper-bounded with_infima non empty Poset holds
InclPoset Filt L is CLSubFrame of BoolePoset the carrier of L
proof
let L be upper-bounded with_infima non empty Poset;
set cL = the carrier of L;
set BP = BoolePoset cL;
set cBP = the carrier of BP;
set rBP = the InternalRel of BP;
set IP = InclPoset Filt L;
set cIP = the carrier of IP;
set rIP = the InternalRel of IP;
A1: InclPoset bool cL = RelStr(#bool cL, RelIncl bool cL#) by YELLOW_1:def 1;
A2: InclPoset Filt L = RelStr(#Filt L, RelIncl Filt L#) by YELLOW_1:def 1;
A3: BoolePoset cL = InclPoset bool cL by YELLOW_1:4;
A4: cIP c= cBP
proof
let x be object;
assume x in cIP;
then ex X being Filter of L st x = X by A2;
hence thesis by A3,A1;
end;
A5: field rIP = Filt L by A2,WELLORD2:def 1;
rIP c= rBP
proof
let p be object;
assume
A6: p in rIP;
then consider x, y being object such that
A7: p = [x, y] by RELAT_1:def 1;
A8: y in field rIP by A6,A7,RELAT_1:15;
then consider Y being Filter of L such that
A9: y = Y by A5;
A10: x in field rIP by A6,A7,RELAT_1:15;
then consider X being Filter of L such that
A11: x = X by A5;
X c= Y by A2,A5,A6,A7,A10,A8,A11,A9,WELLORD2:def 1;
hence thesis by A3,A1,A7,A11,A9,WELLORD2:def 1;
end;
then reconsider IP as SubRelStr of BP by A4,YELLOW_0:def 13;
now
let p be object;
A12: rBP|_2 cIP = rBP /\ [:cIP, cIP:] by WELLORD1:def 6;
hereby
assume
A13: p in rIP;
then consider x, y being object such that
A14: p = [x, y] by RELAT_1:def 1;
A15: y in field rIP by A13,A14,RELAT_1:15;
then consider Y being Filter of L such that
A16: y = Y by A5;
A17: x in field rIP by A13,A14,RELAT_1:15;
then consider X being Filter of L such that
A18: x = X by A5;
X c= Y by A2,A5,A13,A14,A17,A15,A18,A16,WELLORD2:def 1;
then p in rBP by A3,A1,A14,A18,A16,WELLORD2:def 1;
hence p in rBP|_2 cIP by A12,A13,XBOOLE_0:def 4;
end;
assume
A19: p in rBP|_2 cIP;
then
A20: p in rBP by A12,XBOOLE_0:def 4;
p in [:cIP, cIP:] by A12,A19,XBOOLE_0:def 4;
then consider x, y being object such that
A21: x in cIP & y in cIP and
A22: p = [x, y] by ZFMISC_1:def 2;
reconsider x,y as set by TARSKI:1;
(ex X being Filter of L st x = X )& ex Y being Filter of L st y = Y
by A2,A21;
then x c= y by A3,A1,A20,A22,WELLORD2:def 1;
hence p in rIP by A2,A21,A22,WELLORD2:def 1;
end;
then rIP = rBP|_2 cIP by TARSKI:2;
then reconsider IP as full SubRelStr of BP by YELLOW_0:def 14;
A23: Filt L c= bool cL
proof
let x be object;
assume x in Filt L;
then ex X being Filter of L st x = X;
hence thesis;
end;
A24: IP is directed-sups-inheriting
proof
let X be directed Subset of IP such that
A25: X <> {} and
ex_sup_of X, BP;
consider Y being object such that
A26: Y in X by A25,XBOOLE_0:def 1;
reconsider F = X as Subset-Family of cL by A2,A23,XBOOLE_1:1;
A27: for P, R being Subset of L st P in F & R in F ex Z being Subset of L
st Z in F & P \/ R c= Z
proof
let P, R be Subset of L;
assume
A28: P in F & R in F;
then reconsider P9 = P, R9 = R as Element of IP;
consider Z being Element of IP such that
A29: Z in X and
A30: P9 <= Z & R9 <= Z by A28,WAYBEL_0:def 1;
Z in the carrier of IP by A29;
then consider Z9 being Filter of L such that
A31: Z9 = Z by A2;
take Z9;
thus Z9 in F by A29,A31;
P9 c= Z & R9 c= Z by A30,YELLOW_1:3;
hence thesis by A31,XBOOLE_1:8;
end;
reconsider X9 = X as Subset of BP by A3,A1,A2,A23,XBOOLE_1:1;
set sX = "\/"(X, BP);
A32: sup X9 = union X by YELLOW_1:21;
reconsider sX as Subset of L by A1,YELLOW_1:4;
A33: for X being Subset of L st X in F holds X is upper filtered
proof
let X be Subset of L;
assume X in F;
then X in Filt L by A2;
then ex Y being Filter of L st X = Y;
hence thesis;
end;
then for X being Subset of L st X in F holds X is upper;
then
A34: sX is upper by A32,WAYBEL_0:28;
for X being Subset of L st X in F holds X is filtered by A33;
then
A35: sX is filtered by A32,A27,WAYBEL_0:47;
reconsider Y as set by TARSKI:1;
Y in Filt L by A2,A26;
then ex Z being Filter of L st Y = Z;
then Top L in Y by WAYBEL_4:22;
then sX is non empty by A32,A26,TARSKI:def 4;
hence thesis by A2,A34,A35;
end;
IP is infs-inheriting
proof
let X be Subset of IP such that
ex_inf_of X, BP;
set sX = "/\"(X, BP);
per cases;
suppose
A36: X is empty;
A37: [#]L = cL;
"/\"(X, BP) = Top BP by A36
.= cL by YELLOW_1:19;
hence thesis by A2,A37;
end;
suppose
A38: X is non empty;
reconsider F = X as Subset-Family of cL by A2,A23,XBOOLE_1:1;
reconsider sX as Subset of L by A1,YELLOW_1:4;
reconsider X9 = X as Subset of BP by A3,A1,A2,A23,XBOOLE_1:1;
A39: inf X9 = meet X by A38,YELLOW_1:20;
A40: for X being Subset of L st X in F holds X is upper filtered
proof
let X be Subset of L;
assume X in F;
then X in Filt L by A2;
then ex Y being Filter of L st X = Y;
hence thesis;
end;
then
A41: sX is filtered by A39,YELLOW_2:39;
for X being Subset of L st X in F holds X is upper by A40;
then
A42: sX is upper by A39,YELLOW_2:37;
for Y being set st Y in X holds Top L in Y
proof
let Y be set;
assume Y in X;
then Y in Filt L by A2;
then ex Z being Filter of L st Y = Z;
hence thesis by WAYBEL_4:22;
end;
then sX is non empty by A38,A39,SETFAM_1:def 1;
hence thesis by A2,A42,A41;
end;
end;
hence thesis by A24;
end;
registration
let L be upper-bounded with_infima non empty Poset;
cluster InclPoset Filt L -> continuous;
coherence
proof
InclPoset Filt L is CLSubFrame of BoolePoset the carrier of L by Th6;
hence thesis by WAYBEL_5:28;
end;
end;
registration
let L be upper-bounded non empty Poset;
cluster -> non empty for Element of InclPoset Filt L;
coherence
proof
let x be Element of InclPoset Filt L;
InclPoset Filt L = RelStr(#Filt L, RelIncl Filt L#) by YELLOW_1:def 1;
then x in Filt L;
then ex X being Filter of L st x = X;
hence thesis;
end;
end;
begin :: Free generators of continuous lattices
definition
let S be continuous complete non empty Poset;
let A be set;
pred A is_FreeGen_set_of S means
for T be continuous complete non
empty Poset for f be Function of A, the carrier of T ex h be CLHomomorphism of
S, T st h|A = f & for h9 being CLHomomorphism of S,T st h9|A = f holds h9 = h;
end;
theorem Th7:
for S being continuous complete non empty Poset, A being set st
A is_FreeGen_set_of S holds A is Subset of S
proof
set T = the continuous complete non empty Poset;
let S be continuous complete non empty Poset, A be set such that
A1: A is_FreeGen_set_of S;
set f = the Function of A, the carrier of T;
consider h being CLHomomorphism of S, T such that
A2: h|A = f and
for h9 being CLHomomorphism of S, T st h9|A = f holds h9 = h by A1;
dom (h|A) = dom h /\ A by RELAT_1:61;
hence thesis by A2,FUNCT_2:def 1;
end;
theorem Th8:
for S being continuous complete non empty Poset, A being set st
A is_FreeGen_set_of S for h9 being CLHomomorphism of S, S st h9|A = id A holds
h9 = id S
proof
let S be continuous complete non empty Poset, A be set such that
A1: A is_FreeGen_set_of S;
set L = S;
A2: A is Subset of L by A1,Th7;
then
A3: (id L)|A = id A by FUNCT_3:1;
dom id A = A & rng id A = A;
then reconsider f = id A as Function of A,the carrier of L by A2,RELSET_1:4;
consider h being CLHomomorphism of L, L such that
h|A = f and
A4: for h9 being CLHomomorphism of L,L st h9|A = f holds h9 = h by A1;
A5: id L is CLHomomorphism of L, L by Th5;
let h9 be CLHomomorphism of S, S;
assume h9|A = id A;
hence h9 = h by A4
.= id L by A4,A5,A3;
end;
begin :: Representation theorem for free continuous lattices
reserve X for set,
F for Filter of BoolePoset X,
x for Element of BoolePoset X ,
z for Element of X;
definition :: See proof of Theorem 4.17, p. 90
let X;
func FixedUltraFilters X -> Subset-Family of BoolePoset X equals
{ uparrow x
: ex z st x = {z} };
coherence
proof
set FUF = { uparrow x where x is Element of BoolePoset X : ex y being
Element of X st x = {y} };
FUF c= bool the carrier of BoolePoset X
proof
let z be object;
assume z in FUF;
then ex x being Element of BoolePoset X st z = uparrow x & ex y being
Element of X st x = {y};
hence thesis;
end;
hence thesis;
end;
end;
theorem Th9:
FixedUltraFilters X c= Filt BoolePoset X
proof
let F be object;
assume F in FixedUltraFilters X;
then
ex x being Element of BoolePoset X st F = uparrow x & ex y being Element
of X st x = {y};
hence thesis;
end;
theorem Th10:
card FixedUltraFilters X = card X
proof
set FUF = { uparrow x : ex z st x = {z} };
A1: BoolePoset X = InclPoset bool X by YELLOW_1:4;
A2: InclPoset bool X = RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
then
A3: the carrier of BoolePoset X = bool X by YELLOW_1:4;
X,FUF are_equipotent
proof
defpred P[object, object] means
ex y being Element of X, x being Element of
BoolePoset X st x = {y} & $1 = y & $2 = uparrow x;
A4: for x being object st x in X ex y being object st P[x,y]
proof
let x be object;
assume
A5: x in X;
then reconsider x9 = x as Element of X;
reconsider bx = {x} as Element of BoolePoset X by A1,A2,A5,ZFMISC_1:31;
take uparrow bx;
take x9;
take bx;
thus thesis;
end;
consider f being Function such that
A6: dom f = X & for x being object st x in X holds P[x, f.x] from
CLASSES1:sch 1(A4);
take f;
thus f is one-to-one
proof
let x1, x2 be object such that
A7: x1 in dom f and
A8: x2 in dom f and
A9: f.x1 = f.x2;
consider x29 being Element of X, bx2 being Element of BoolePoset X such
that
A10: bx2 = {x29} & x2 = x29 and
A11: f.x2 = uparrow bx2 by A6,A8;
consider x19 being Element of X, bx1 being Element of BoolePoset X such
that
A12: bx1 = {x19} & x1 = x19 and
A13: f.x1 = uparrow bx1 by A6,A7;
bx1 = bx2 by A9,A13,A11,WAYBEL_0:20;
hence thesis by A12,A10,ZFMISC_1:3;
end;
thus dom f = X by A6;
now
let z be object;
hereby
assume z in rng f;
then consider x1 being object such that
A14: x1 in dom f and
A15: z = f.x1 by FUNCT_1:def 3;
ex x19 being Element of X, bx1 being Element of BoolePoset X st
bx1 = {x19} & x1 = x19 & f.x1 = uparrow bx1 by A6,A14;
hence z in FUF by A15;
end;
assume z in FUF;
then consider bx being Element of BoolePoset X such that
A16: z = uparrow bx and
A17: ex y being Element of X st bx = {y};
consider y being Element of X such that
A18: bx = {y} by A17;
A19: y in X by A3,A18,ZFMISC_1:31;
then ex x19 being Element of X, bx1 being Element of BoolePoset X st bx1
= {x19} & y = x19 & f.y = uparrow bx1 by A6;
hence z in rng f by A6,A16,A18,A19,FUNCT_1:def 3;
end;
hence thesis by TARSKI:2;
end;
hence thesis by CARD_1:5;
end;
theorem Th11:
F = "\/"({"/\"({uparrow x : ex z st x = {z} & z in Y}, InclPoset
Filt BoolePoset X) where Y is Subset of X : Y in F}, InclPoset Filt BoolePoset
X)
proof
set BP = BoolePoset X;
set IP = InclPoset Filt BP;
set cIP = the carrier of IP;
set Xs = {"/\"({uparrow x : ex z st x = {z} & z in Y }, IP ) where Y is
Subset of X : Y in F};
set RS = "\/"(Xs, IP);
A1: InclPoset Filt BP = RelStr(#Filt BP, RelIncl Filt BP#) by YELLOW_1:def 1;
F in Filt BP;
then reconsider F9 = F as Element of IP by A1;
A2: Xs c= cIP
proof
let p be object;
assume p in Xs;
then
ex YY being Subset of X st p = "/\"({uparrow x : ex z st x = {z} & z in
YY}, IP) & YY in F;
hence thesis;
end;
A3: the carrier of BP = the carrier of LattPOSet BooleLatt X by YELLOW_1:def 2
.= bool X by LATTICE3:def 1;
now
consider YY being object such that
A4: YY in F by XBOOLE_0:def 1;
reconsider YY as set by TARSKI:1;
"/\"({uparrow x : ex z st x = {z} & z in YY}, IP) in Xs by A3,A4;
hence Xs is non empty;
end;
then reconsider Xs9 = Xs as non empty Subset of IP by A2;
A5: ex_sup_of Xs9, IP by YELLOW_0:17;
F c= RS
proof
let p be object;
assume
A6: p in F;
then reconsider Y = p as Element of F;
set Xsi = {uparrow x where x is Element of BP : ex z being Element of X st
x = {z} & z in Y};
A7: "/\"(Xsi, IP) in Xs by A3;
per cases;
suppose
A8: Xsi is empty;
A9: p in the carrier of BP by A6;
Xs9 is_<=_than RS by A5,YELLOW_0:def 9;
then
A10: "/\"(Xsi, IP) <= RS by A7;
"/\"(Xsi, IP) = Top IP by A8
.= bool X by WAYBEL16:15;
then bool X c= RS by A10,YELLOW_1:3;
hence thesis by A3,A9;
end;
suppose
A11: Xsi is non empty;
Xsi c= cIP
proof
let r be object;
assume r in Xsi;
then ex xz being Element of BP st r = uparrow xz & ex z being Element
of X st xz = {z} & z in Y;
hence thesis by A1;
end;
then reconsider Xsi as non empty Subset of IP by A11;
for yy being set st yy in Xsi holds Y in yy
proof
reconsider Y9 = Y as Element of BP;
let yy be set;
assume yy in Xsi;
then consider r being Element of BP such that
A12: yy = uparrow r and
A13: ex z being Element of X st r = {z} & z in Y;
r c= Y by A13,ZFMISC_1:31;
then r <= Y9 by YELLOW_1:2;
hence thesis by A12,WAYBEL_0:18;
end;
then "/\"(Xsi, IP) = meet Xsi & Y in meet Xsi by SETFAM_1:def 1
,WAYBEL16:10;
then
A14: p in union Xs by A7,TARSKI:def 4;
union Xs9 c= RS by WAYBEL16:17,YELLOW_0:17;
hence thesis by A14;
end;
end;
then
A15: F9 <= RS by YELLOW_1:3;
Xs is_<=_than F9
proof
let b be Element of IP;
assume b in Xs;
then consider Y being Subset of X such that
A16: b = "/\"({uparrow x : ex z st x = {z} & z in Y}, IP) and
A17: Y in F;
reconsider Y9 = Y as Element of F by A17;
set Xsi = {uparrow x : ex z st x = {z} & z in Y};
per cases;
suppose
A18: Y is empty;
now
assume Xsi is non empty;
then consider p being object such that
A19: p in Xsi by XBOOLE_0:def 1;
ex x being Element of BP st p = uparrow x & ex z being Element of
X st x = {z} & z in Y by A19;
hence contradiction by A18;
end;
then
A20: "/\"(Xsi, IP) = Top IP .= bool X by WAYBEL16:15;
Bottom BP = {} by YELLOW_1:18;
then uparrow Bottom BP c= F by A17,A18,WAYBEL11:42;
then bool X c= F by A3,WAYBEL14:10;
hence b <= F9 by A3,A16,A20,XBOOLE_0:def 10;
end;
suppose
A21: Y is non empty;
A22: now
consider z being object such that
A23: z in Y by A21,XBOOLE_0:def 1;
reconsider z as Element of X by A23;
reconsider x = {z} as Element of BP by A3,A23,ZFMISC_1:31;
uparrow x in Xsi by A23;
hence Xsi is non empty;
end;
Xsi c= cIP
proof
let r be object;
assume r in Xsi;
then ex xz being Element of BP st r = uparrow xz & ex z being Element
of X st xz = {z} & z in Y;
hence thesis by A1;
end;
then reconsider Xsi as non empty Subset of IP by A22;
A24: "/\"(Xsi, IP) = meet Xsi by WAYBEL16:10;
b c= F9
proof
let yy be object;
b in Filt BP by A1;
then consider bf being Filter of BP such that
A25: b = bf;
assume
A26: yy in b;
then reconsider yy9 = yy as Element of bf by A25;
reconsider yy9 as Element of BP;
Y c= yy9
proof
let zz be object;
assume
A27: zz in Y;
then reconsider z = zz as Element of X;
reconsider xz = {z} as Element of BP by A3,A27,ZFMISC_1:31;
uparrow xz in Xsi by A27;
then yy in uparrow xz by A16,A24,A26,SETFAM_1:def 1;
then xz <= yy9 by WAYBEL_0:18;
then {z} c= yy9 by YELLOW_1:2;
hence thesis by ZFMISC_1:31;
end;
then Y9 <= yy9 by YELLOW_1:2;
then uparrow Y9 c= F9 & yy in uparrow Y9 by WAYBEL11:42,WAYBEL_0:18;
hence thesis;
end;
hence b <= F9 by YELLOW_1:3;
end;
end;
then RS <= F9 by A5,YELLOW_0:def 9;
hence thesis by A15,YELLOW_0:def 3;
end;
definition :: See proof of Theorem 4.17, p. 90
let X;
let L be continuous complete non empty Poset;
let f be Function of FixedUltraFilters X, the carrier of L;
func f-extension_to_hom -> Function of InclPoset Filt BoolePoset X, L means
:Def3:
for Fi being Element of InclPoset Filt BoolePoset X holds it.Fi = "\/"({
"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y is Subset of X : Y
in Fi }, L);
existence
proof
set IP = InclPoset Filt BoolePoset X;
deffunc F(Element of IP) = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z
in Y }, L) where Y is Subset of X : Y in $1 }, L);
consider F being Function of the carrier of IP, the carrier of L such that
A1: for Fi being Element of IP holds F.Fi = F(Fi) from FUNCT_2:sch 4;
reconsider F as Function of IP, L;
take F;
thus thesis by A1;
end;
uniqueness
proof
set IP = InclPoset Filt BoolePoset X;
let it1, it2 be Function of IP, L such that
A2: for Fi being Element of IP holds it1.Fi = "\/"({"/\"({f.(uparrow x
) : ex z st x = {z} & z in Y }, L) where Y is Subset of X : Y in Fi }, L)
and
A3: for Fi being Element of IP holds it2.Fi = "\/"({"/\"({f.(uparrow x
) : ex z st x = {z} & z in Y }, L) where Y is Subset of X : Y in Fi }, L);
reconsider it29 = it2 as Function of the carrier of IP, the carrier of L;
reconsider it19 = it1 as Function of the carrier of IP, the carrier of L;
now
let Fi be Element of IP;
thus it19.Fi = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L
) where Y is Subset of X : Y in Fi }, L) by A2
.= it29.Fi by A3;
end;
hence it1 = it2 by FUNCT_2:63;
end;
end;
theorem
for L being continuous complete non empty Poset, f being Function of
FixedUltraFilters X, the carrier of L holds f-extension_to_hom is monotone
proof
let L be continuous complete non empty Poset, f be Function of
FixedUltraFilters X, the carrier of L;
let F1, F2 be Element of InclPoset Filt BoolePoset X;
set F = f-extension_to_hom;
set F1s = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y is
Subset of X : Y in F1};
set F2s = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y is
Subset of X : Y in F2 };
A1: ex_sup_of F1s, L & ex_sup_of F2s, L by YELLOW_0:17;
A2: F.F1 = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where
Y is Subset of X : Y in F1}, L) by Def3;
assume F1 <= F2;
then
A3: F1 c= F2 by YELLOW_1:3;
A4: F1s c= F2s
proof
let s be object;
assume s in F1s;
then
ex Y being Subset of X st s = "/\"({f.(uparrow x) : ex z st x = {z} & z
in Y}, L) & Y in F1;
hence thesis by A3;
end;
A5: F.F2 = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where
Y is Subset of X : Y in F2}, L) by Def3;
let FF1, FF2 be Element of L;
assume FF1 = F.F1 & FF2 = F.F2;
hence FF1 <= FF2 by A2,A5,A1,A4,YELLOW_0:34;
end;
theorem Th13:
for L being continuous complete non empty Poset, f being
Function of FixedUltraFilters X, the carrier of L holds (f-extension_to_hom).
Top (InclPoset Filt BoolePoset X) = Top L
proof
let L be continuous complete non empty Poset, f be Function of
FixedUltraFilters X, the carrier of L;
set IP = InclPoset Filt BoolePoset X;
set F = f-extension_to_hom;
reconsider T = Top IP as Element of IP;
reconsider E = {} as Subset of X by XBOOLE_1:2;
set Z = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y is
Subset of X : Y in T};
A1: {f.(uparrow x) : ex z st x = {z} & z in E} = {}
proof
assume not thesis;
then consider r being object such that
A2: r in {f.(uparrow x) : ex z st x = {z} & z in E} by XBOOLE_0:def 1;
ex x st r = f.(uparrow x) & ex z st x = {z} & z in E by A2;
hence contradiction;
end;
A3: F.T = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y
is Subset of X : Y in T}, L) by Def3;
T = bool X by WAYBEL16:15;
then
A4: "/\"({f.(uparrow x) : ex z st x = {z} & z in E}, L) in Z;
Z is_<=_than "\/"(Z, L) by YELLOW_0:32;
then Top L <= "\/"(Z, L) by A4,A1;
hence thesis by A3,WAYBEL15:3;
end;
registration :: See proof of Theorem 4.17, p. 91
let X;
let L be continuous complete non empty Poset, f be Function of
FixedUltraFilters X, the carrier of L;
cluster f-extension_to_hom -> directed-sups-preserving;
coherence
proof
set F = f-extension_to_hom;
set IP = InclPoset Filt BoolePoset X;
let Fs be Subset of IP such that
A1: Fs is non empty directed;
reconsider Fs9 = Fs as non empty Subset of IP by A1;
set FFsU = the set of all
{"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) where Y
is Subset of X : Y in YY } where YY is Element of Fs9;
reconsider sFs = sup Fs as Element of IP;
set FFs = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y is
Subset of X : Y in sFs };
A2: sup Fs = union Fs by A1,Th1;
now
let p be object;
hereby
assume p in FFs;
then consider Y being Subset of X such that
A3: p = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A4: Y in sFs;
consider YY being set such that
A5: Y in YY and
A6: YY in Fs by A2,A4,TARSKI:def 4;
A7: {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y1}, L) where Y1 is
Subset of X : Y1 in YY} in FFsU by A6;
p in {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y1}, L) where
Y1 is Subset of X : Y1 in YY} by A3,A5;
hence p in union FFsU by A7,TARSKI:def 4;
end;
assume p in union FFsU;
then consider r being set such that
A8: p in r and
A9: r in FFsU by TARSKI:def 4;
consider YY being Element of Fs9 such that
A10: r = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) where
Y is Subset of X: Y in YY} by A9;
consider Y being Subset of X such that
A11: p = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A12: Y in YY by A8,A10;
Y in sFs by A2,A12,TARSKI:def 4;
hence p in FFs by A11;
end;
then
A13: FFs = union FFsU by TARSKI:2;
set Zs = {sup Z where Z is Subset of L : Z in FFsU};
assume ex_sup_of Fs, IP;
thus ex_sup_of F.:Fs, L by YELLOW_0:17;
FFsU c= bool the carrier of L
proof
let r be object;
reconsider rr=r as set by TARSKI:1;
assume r in FFsU;
then consider YY being Element of Fs9 such that
A14: r = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) where Y
is Subset of X : Y in YY};
rr c= the carrier of L
proof
let s be object;
assume s in rr;
then
ex Y being Subset of X st s = "/\"({f.(uparrow x) : ex z st x = {z}
& z in Y}, L) & Y in YY by A14;
hence thesis;
end;
hence thesis;
end;
then
A15: "\/"(union FFsU, L) = "\/"(Zs, L) by Lm2;
A16: now
let r be object;
hereby
assume r in F.:Fs;
then consider YY being object such that
A17: YY in the carrier of IP and
A18: YY in Fs and
A19: F.YY = r by FUNCT_2:64;
reconsider YY as Element of Fs by A18;
reconsider YY9 = YY as Element of IP by A17;
set Zi = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) where Y
is Subset of X : Y in YY9 };
Zi c= the carrier of L
proof
let t be object;
assume t in Zi;
then ex Y being Subset of X st t = "/\"({f.(uparrow x) : ex z st x =
{z} & z in Y}, L) & Y in YY9;
hence thesis;
end;
then reconsider Zi as Subset of L;
A20: Zi in FFsU;
F.YY9 = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L
) where Y is Subset of X : Y in YY9}, L) by Def3;
hence r in Zs by A19,A20;
end;
assume r in Zs;
then consider Z being Subset of L such that
A21: r = sup Z and
A22: Z in FFsU;
consider YY being Element of Fs such that
A23: Z = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) where
Y is Subset of X : Y in YY} by A22;
reconsider YY as Element of Fs9;
reconsider YY9 = YY as Element of IP;
F.YY9 = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L)
where Y is Subset of X : Y in YY9}, L) by Def3;
hence r in F.:Fs by A21,A23,FUNCT_2:35;
end;
F.sFs = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L)
where Y is Subset of X : Y in sFs }, L) by Def3;
hence thesis by A15,A13,A16,TARSKI:2;
end;
end;
registration :: See proof of Theorem 4.17, p. 91
let X;
let L be continuous complete non empty Poset, f be Function of
FixedUltraFilters X, the carrier of L;
cluster f-extension_to_hom -> infs-preserving;
coherence
proof
set FUF = FixedUltraFilters X;
set cL = the carrier of L;
set F = f-extension_to_hom;
set BP = BoolePoset X;
set IP = InclPoset Filt BP;
set cIP = the carrier of IP;
A1: InclPoset Filt BP = RelStr(#Filt BP, RelIncl Filt BP#) by YELLOW_1:def 1;
let Fs be Subset of IP;
assume ex_inf_of Fs, IP;
thus ex_inf_of F.:Fs, L by YELLOW_0:17;
A2: BoolePoset X = InclPoset bool X by YELLOW_1:4;
A3: InclPoset bool X = RelStr(#bool X, RelIncl bool X#) by YELLOW_1:def 1;
then
A4: the carrier of BoolePoset X = bool X by YELLOW_1:4;
per cases;
suppose
Fs is empty;
then "/\"(F.:Fs, L) = Top L & "/\"(Fs, IP) = Top IP;
hence thesis by Th13;
end;
suppose
Fs is non empty;
then reconsider Fs9 = Fs as non empty Subset of IP;
defpred P[object, object, object] means
ex D2 being set st D2 = $2 &
$1 = "/\"({f.(uparrow x) : ex z st x = {z} & z in D2}, L);
deffunc FDi(Element of Fs9) = {"/\"({f.(uparrow x) : ex z st x = {z} & z
in Y }, L) where Y is Subset of X : Y in $1};
not {} in Fs9;
then Fs9 is with_non-empty_elements by SETFAM_1:def 8;
then reconsider K = id Fs9 as non-empty ManySortedSet of Fs9;
A5: for i be object st i in Fs9 for s be object st s in K.i
ex y be object st y in (Fs9 --> cL).i & P[y, s, i]
proof
let i be object such that
A6: i in Fs9;
let s be object such that
s in K.i;
reconsider D2 = s as set by TARSKI:1;
take y = "/\"({f.(uparrow x) : ex z st x = {z} & z in D2}, L);
y in cL;
hence y in (Fs9 --> cL).i by A6,FUNCOP_1:7;
take D2;
thus D2 = s;
thus y = "/\"({f.(uparrow x) : ex z st x = {z} & z in D2}, L);
end;
consider FD being ManySortedFunction of K, (Fs9 --> cL) such that
A7: for i being object st i in Fs9
ex g being Function of K.i, (Fs9 --> cL).i st g = FD.i &
for s being object st s in K.i holds P[g.s, s, i]
from
MSSUBFAM:sch 1(A5);
defpred rFD[Element of Fs9] means rng (FD.$1) = FDi($1);
A8: for s being Element of Fs9 holds rFD[s]
proof
let s be Element of Fs9;
now
let t be object;
consider g being Function of K.s, (Fs9 --> cL).s such that
A9: g = FD.s and
A10: for u being object st u in K.s holds P[g.u, u, s] by A7;
hereby
assume t in rng (FD.s);
then consider u being object such that
A11: u in dom (FD.s) and
A12: t = (FD.s).u by FUNCT_1:def 3;
consider g being Function of K.s, (Fs9 --> cL).s such that
A13: g = FD.s and
A14: for u being object st u in K.s holds P[g.u, u, s] by A7;
A15: dom (FD.s) = K.s by FUNCT_2:def 1;
reconsider u as set by TARSKI:1;
P[g.u, u, s] by A11,A14;
then
A16: g.u = "/\"({f.(uparrow x) : ex z st x = {z} & z in u}, L);
s in cIP;
then K.s = s & ex FF being Filter of BP st s = FF by A1;
then reconsider u as Subset of X by A3,A11,A15,YELLOW_1:4;
u in s by A11;
then t in {"/\"({f.(uparrow x) :
ex z st x = {z} & z in Y }, L) where Y is Subset of X : Y in s}
by A12,A13,A16;
hence t in FDi(s);
end;
assume t in FDi(s);
then consider Y being Subset of X such that
A17: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A18: Y in s;
dom (FD.s) = K.s by FUNCT_2:def 1;
then
A19: Y in dom (FD.s) by A18;
P[g.Y, Y, s] by A10,A18;
then g.Y = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L);
hence t in rng (FD.s) by A17,A19,A9,FUNCT_1:def 3;
end;
hence thesis by TARSKI:2;
end;
meet Fs9 is Filter of BoolePoset X by WAYBEL16:9;
then meet Fs9 in Filt BP;
then reconsider mFs = meet Fs9 as Element of cIP by A1;
set smFs = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y
is Subset of X : Y in mFs};
A20: dom FD = Fs9 by PARTFUN1:def 2;
reconsider FD as DoubleIndexedSet of K, L;
now
let r be object;
hereby
assume r in F.:Fs;
then consider s being object such that
A21: s in cIP and
A22: s in Fs and
A23: F.s = r by FUNCT_2:64;
reconsider s9 = s as Element of cIP by A21;
reconsider s as Element of Fs9 by A22;
A24: rFD[s] by A8;
F.s9 = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y },
L) where Y is Subset of X : Y in s9 }, L) by Def3;
then r = Sup (FD.s) by A23,A24,YELLOW_2:def 5;
hence r in rng Sups FD by WAYBEL_5:14;
end;
assume r in rng Sups FD;
then consider s being Element of Fs9 such that
A25: r = Sup (FD.s) by WAYBEL_5:14;
rFD[s] by A8;
then F.s = "\/"(rng (FD.s), L) by Def3
.= Sup (FD.s) by YELLOW_2:def 5;
hence r in F.:Fs by A25,FUNCT_2:35;
end;
then F.:Fs = rng Sups FD by TARSKI:2;
then
A26: inf (F.:Fs) = Inf Sups FD by YELLOW_2:def 6;
A27: now
reconsider pdFD = product doms FD as non empty functional set;
let r be object;
reconsider dFFD = product doms FD --> Fs9 as ManySortedSet of pdFD;
reconsider FFD = Frege FD as DoubleIndexedSet of dFFD, L;
deffunc rFFDs(Element of pdFD) = {"/\"({f.(uparrow x) : ex z st x = {z
} & z in $1.u}, L) where u is Element of Fs9 : u in dom (FFD.$1) };
A28: dom FFD = pdFD by PARTFUN1:def 2;
A29: now
let s be Element of pdFD;
A30: dom FD = dom (FFD.s) by A28,WAYBEL_5:8;
now
let t be object;
hereby
assume t in rng (FFD.s);
then consider u being object such that
A31: u in dom (FFD.s) and
A32: t = FFD.s.u by FUNCT_1:def 3;
A33: FFD.s.u = (FD.u).(s.u) by A28,A30,A31,WAYBEL_5:9;
reconsider u as Element of Fs9 by A31;
consider g being Function of K.u, (Fs9 --> cL).u such that
A34: g = FD.u and
A35: for v being object st v in K.u holds P[g.v, v, u] by A7;
dom (FD.u) = K.u by FUNCT_2:def 1;
then P[g.(s.u), s.u, s] by A20,A28,A35,WAYBEL_5:9;
then
g.(s.u) = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}
, L);
hence t in rFFDs(s) by A31,A32,A33,A34;
end;
assume t in rFFDs(s);
then consider u being Element of Fs9 such that
A36: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L)
& u in dom (FFD.s);
reconsider u as Element of Fs9;
consider g being Function of K.u, (Fs9 --> cL).u such that
A37: g = FD.u and
A38: for v being object st v in K.u holds P[g.v, v, u] by A7;
dom (FD.u) = K.u by FUNCT_2:def 1;
then P[g.(s.u), s.u, s] by A20,A28,A38,WAYBEL_5:9;
then g.(s.u) = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u},
L);
hence t in rng(FFD.s) by A28,A30,A36,A37,WAYBEL_5:9;
end;
hence rng (FFD.s) = rFFDs(s) by TARSKI:2;
end;
hereby
assume r in rng Infs Frege FD;
then consider s being Element of pdFD such that
A39: r = Inf (FFD.s) by WAYBEL_5:14;
set idFFDs = {{f.(uparrow x) : ex z st x = {z} & z in s.u} where u
is Element of Fs9 : u in dom (FFD.s)};
A40: idFFDs c= bool the carrier of L
proof
let t be object;
reconsider tt=t as set by TARSKI:1;
assume t in idFFDs;
then consider u being Element of Fs9 such that
A41: t = {f.(uparrow x) : ex z st x = {z} & z in s.u} and
u in dom (FFD.s);
tt c= cL
proof
let v be object;
assume v in tt;
then consider x such that
A42: v = f.(uparrow x) and
A43: ex z st x = {z} & z in s.u by A41;
uparrow x in FUF by A43;
hence thesis by A42,FUNCT_2:5;
end;
hence thesis;
end;
now
let t be object;
hereby
assume t in rFFDs(s);
then consider u being Element of Fs9 such that
A44: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L) and
A45: u in dom (FFD.s);
{f.(uparrow x) : ex z st x = {z} & z in s.u} c= cL
proof
let v be object;
assume v in {f.(uparrow x) : ex z st x = {z} & z in s.u};
then consider x such that
A46: v = f.(uparrow x) and
A47: ex z st x = {z} & z in s.u;
uparrow x in FUF by A47;
hence thesis by A46,FUNCT_2:5;
end;
then reconsider
Y1 ={f.(uparrow x) : ex z st x = {z} & z in s.u} as
Subset of L;
Y1 in idFFDs by A45;
hence t in {inf YY where YY is Subset of L : YY in idFFDs} by A44
;
end;
assume t in {inf YY where YY is Subset of L : YY in idFFDs};
then consider YY being Subset of L such that
A48: t = inf YY and
A49: YY in idFFDs;
ex u1 being Element of Fs9 st YY = {f.(uparrow x) : ex z st x
= {z} & z in s.u1} & u1 in dom (FFD.s) by A49;
hence t in rFFDs(s) by A48;
end;
then
A50: rFFDs(s) = {inf YY where YY is Subset of L : YY in idFFDs} by
TARSKI:2;
A51: dom s = dom FD by A28,WAYBEL_5:8;
union rng s c= X
proof
let t be object;
assume t in union rng s;
then consider te being set such that
A52: t in te and
A53: te in rng s by TARSKI:def 4;
consider u being object such that
A54: u in dom s and
A55: te = s.u by A53,FUNCT_1:def 3;
reconsider u as set by TARSKI:1;
FD.u is Function of K.u, cL by A51,A54,WAYBEL_5:6;
then dom (FD.u) = K.u by FUNCT_2:def 1
.= u by A51,A54,FUNCT_1:17;
then
A56: te in u by A28,A51,A54,A55,WAYBEL_5:9;
u in cIP by A20,A51,A54;
then ex FF being Filter of BP st u = FF by A1;
hence thesis by A4,A52,A56;
end;
then reconsider Y = union rng s as Subset of X;
set Ys = {f.(uparrow x) : ex z st x = {z} & z in Y};
A57: dom FD = dom (FFD.s) by A28,WAYBEL_5:8;
now
let t be object;
hereby
assume t in union idFFDs;
then consider te being set such that
A58: t in te and
A59: te in idFFDs by TARSKI:def 4;
consider u being Element of Fs9 such that
A60: te = {f.(uparrow x) : ex z st x = {z} & z in s.u} and
A61: u in dom (FFD.s) by A59;
consider x such that
A62: t = f.(uparrow x) and
A63: ex z st x = {z} & z in s.u by A58,A60;
consider z such that
A64: x = {z} and
A65: z in s.u by A63;
s.u in rng s by A57,A51,A61,FUNCT_1:def 3;
then z in Y by A65,TARSKI:def 4;
hence t in Ys by A62,A64;
end;
assume t in Ys;
then consider x such that
A66: t = f.(uparrow x) and
A67: ex z st x = {z} & z in Y;
consider z such that
A68: x = {z} and
A69: z in Y by A67;
consider ze being set such that
A70: z in ze and
A71: ze in rng s by A69,TARSKI:def 4;
consider u being object such that
A72: u in dom s and
A73: ze = s.u by A71,FUNCT_1:def 3;
reconsider u as Element of Fs9 by A51,A72;
A74: {f.(uparrow x1) where x1 is Element of BP : ex z st x1 = {z}
& z in s.u} in idFFDs by A57,A51,A72;
t in {f.(uparrow x1) where x1 is Element of BP : ex z st x1
= {z} & z in s.u} by A66,A68,A70,A73;
hence t in union idFFDs by A74,TARSKI:def 4;
end;
then
A75: union idFFDs = Ys by TARSKI:2;
now
reconsider Y9 = Y as Element of BP by A3,YELLOW_1:4;
let Z be set;
assume
A76: Z in Fs9;
then FD.Z is Function of K.Z, cL by WAYBEL_5:6;
then
A77: dom (FD.Z) = K.Z by FUNCT_2:def 1
.= Z by A76,FUNCT_1:17;
s.Z in rng s by A20,A51,A76,FUNCT_1:def 3;
then
A78: s.Z c= Y by ZFMISC_1:74;
then reconsider sZ = s.Z as Element of BP by A2,A3,XBOOLE_1:1;
A79: sZ <= Y9 by A78,YELLOW_1:2;
Z in cIP by A76;
then
A80: ex FF being Filter of BP st Z = FF by A1;
s.Z in dom (FD.Z) by A20,A28,A76,WAYBEL_5:9;
hence Y in Z by A80,A77,A79,WAYBEL_0:def 20;
end;
then Y in mFs by SETFAM_1:def 1;
then
A81: "/\"(Ys, L) in smFs;
"/\"(rng (FFD.s), L) = "/\"(rFFDs(s), L) by A29
.= "/\"(union idFFDs, L) by A40,A50,Lm1;
hence r in smFs by A39,A81,A75,YELLOW_2:def 6;
end;
assume r in smFs;
then consider Y being Subset of X such that
A82: r = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A83: Y in mFs;
A84: "/\"({r}, L) = r by A82,YELLOW_0:39;
set s = Fs9 --> Y;
A85: dom doms FD = dom FD by FUNCT_6:59
.= dom s by A20;
A86: now
let w be object;
assume
A87: w in dom doms FD;
then FD.w is Function of K.w, (Fs9 --> cL).w by A85,PBOOLE:def 15;
then
A88: dom (FD.w) = K.w by A85,A87,FUNCT_2:def 1
.= w by A85,A87,FUNCT_1:18;
(doms FD).w = dom (FD.w) & s.w = Y by A20,A85,A87,FUNCOP_1:7
,FUNCT_6:22;
hence s.w in (doms FD).w by A83,A85,A87,A88,SETFAM_1:def 1;
end;
set s9 = s;
reconsider s as Element of pdFD by A85,A86,CARD_3:9;
now
set u = the Element of Fs9;
let t be object;
A89: dom s9 = Fs9 & s.u = Y;
hereby
assume t in rFFDs(s);
then consider u being Element of Fs9 such that
A90: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L ) and
u in dom (FFD.s);
thus t in {r} by A82,A90,TARSKI:def 1;
end;
assume t in {r};
then
A91: t = r by TARSKI:def 1;
dom FD = dom (FFD.s) & dom s = dom FD by A28,WAYBEL_5:8;
hence t in rFFDs(s) by A82,A91,A89;
end;
then
A92: {"/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L) where u
is Element of Fs9 : u in dom (FFD.s) } = {r} by TARSKI:2;
Inf (FFD.s) = "/\"(rng (FFD.s), L) & rng (FFD.s) = rFFDs(s) by A29,
YELLOW_2:def 6;
hence r in rng Infs Frege FD by A92,A84,WAYBEL_5:14;
end;
for j being Element of Fs9 holds rng(FD.j) is directed
proof
let j be Element of Fs9;
let k, m be Element of L;
assume that
A93: k in rng(FD.j) and
A94: m in rng(FD.j);
consider kd being object such that
A95: kd in dom (FD.j) and
A96: FD.j.kd = k by A93,FUNCT_1:def 3;
consider md being object such that
A97: md in dom (FD.j) and
A98: FD.j.md = m by A94,FUNCT_1:def 3;
j in cIP;
then consider FF being Filter of BP such that
A99: j = FF by A1;
A100: dom (FD.j) = K.j by FUNCT_2:def 1;
then reconsider kd as Element of BP by A95,A99;
reconsider md as Element of BP by A97,A100,A99;
consider nd being Element of BP such that
A101: nd in FF and
A102: nd <= kd and
A103: nd <= md by A95,A97,A99,WAYBEL_0:def 2;
set n = FD.j.nd;
A104: n in rng(FD.j) by A100,A99,A101,FUNCT_1:def 3;
consider g being Function of K.j, (Fs9 --> cL).j such that
A105: g = FD.j and
A106: for u being object st u in K.j holds P[g.u, u, j] by A7;
set nds = {f.(uparrow x) : ex z st x = {z} & z in nd};
P[g.nd, nd, j] by A99,A101,A106;
then
A107: g.nd = "/\"(nds, L);
reconsider n as Element of L by A104;
take n;
thus n in rng(FD.j) by A100,A99,A101,FUNCT_1:def 3;
A108: ex_inf_of nds, L by YELLOW_0:17;
set mds = {f.(uparrow x) : ex z st x = {z} & z in md};
A109: nd c= md by A103,YELLOW_1:2;
A110: nds c= mds
proof
let w be object;
assume w in nds;
then ex x st w = f.(uparrow x) & ex z st x = {z} & z in nd;
hence thesis by A109;
end;
A111: ex_inf_of mds, L by YELLOW_0:17;
set kds = {f.(uparrow x) : ex z st x = {z} & z in kd};
A112: ex_inf_of kds, L by YELLOW_0:17;
A113: nd c= kd by A102,YELLOW_1:2;
A114: nds c= kds
proof
let w be object;
assume w in nds;
then ex x st w = f.(uparrow x) & ex z st x = {z} & z in nd;
hence thesis by A113;
end;
P[g.kd, kd, j] by A95, A106;
then g.kd = "/\"(kds, L);
hence k <= n by A96,A105,A107,A112,A108,A114,YELLOW_0:35;
P[g.md, md, j] by A97, A106;
then g.md = "/\"(mds, L);
hence m <= n by A98,A105,A107,A108,A111,A110,YELLOW_0:35;
end;
then
A115: Inf Sups FD = Sup Infs Frege FD by WAYBEL_5:19
.= "\/"(rng Infs Frege FD, L) by YELLOW_2:def 5;
inf Fs9 = meet Fs9 & F.(meet Fs9) = "\/"(smFs, L) by Def3,WAYBEL16:10;
hence thesis by A26,A115,A27,TARSKI:2;
end;
end;
end;
theorem Th14:
for L being continuous complete non empty Poset, f being
Function of FixedUltraFilters X, the carrier of L holds f-extension_to_hom |
FixedUltraFilters X = f
proof
let L be continuous complete non empty Poset, f be Function of
FixedUltraFilters X, the carrier of L;
set FUF = FixedUltraFilters X;
set BP = BoolePoset X;
set IP = InclPoset Filt BP;
A1: InclPoset Filt BP = RelStr(#Filt BP, RelIncl Filt BP#) by YELLOW_1:def 1;
set F = f-extension_to_hom;
A2: the carrier of BP = the carrier of LattPOSet BooleLatt X by YELLOW_1:def 2
.= bool X by LATTICE3:def 1;
now
A3: dom F = the carrier of IP by FUNCT_2:def 1;
hence FUF = dom (F|FUF) by A1,Th9,RELAT_1:62;
thus FUF = dom f by FUNCT_2:def 1;
let xf be object;
assume
A4: xf in FUF;
then reconsider FUF9 = FUF as non empty Subset-Family of BoolePoset X;
A5: (F|FUF).xf = F.xf by A4,FUNCT_1:49;
FUF c= dom F by A1,A3,Th9;
then reconsider x9 = xf as Element of IP by A4,FUNCT_2:def 1;
reconsider xf9 = xf as Element of FUF9 by A4;
set Xs = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L) where Y is
Subset of X : Y in x9 };
reconsider f9 = f as Function of FUF9, the carrier of L;
f9.xf9 is Element of L;
then reconsider fxf = f.xf9 as Element of L;
consider xx being Element of BoolePoset X such that
A6: xf = uparrow xx and
A7: ex y being Element of X st xx = {y} by A4;
A8: Xs is_<=_than fxf
proof
let b be Element of L;
assume b in Xs;
then consider Y being Subset of X such that
A9: b = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A10: Y in x9;
set Xsi = {f.(uparrow x) : ex z st x = {z} & z in Y };
ex_inf_of Xsi, L by YELLOW_0:17;
then
A11: Xsi is_>=_than b by A9,YELLOW_0:def 10;
reconsider Y as Element of BoolePoset X by A6,A10;
consider y being Element of X such that
A12: xx = {y} by A7;
xx <= Y by A6,A10,WAYBEL_0:18;
then xx c= Y by YELLOW_1:2;
then y in Y by A12,ZFMISC_1:31;
then fxf in Xsi by A6,A12;
hence b <= fxf by A11;
end;
A13: for a being Element of L st Xs is_<=_than a holds fxf <= a
proof
xx <= xx;
then reconsider Y = xx as Element of x9 by A6,WAYBEL_0:18;
set Xsi = {f.(uparrow x) : ex z st x = {z} & z in Y };
consider y being Element of X such that
A14: xx = {y} by A7;
now
let p be object;
hereby
assume p in Xsi;
then consider r being Element of BoolePoset X such that
A15: p = f.(uparrow r) and
A16: ex z being Element of X st r = {z} & z in Y;
xx = r by A14,A16,TARSKI:def 1;
hence p in {fxf} by A6,A15,TARSKI:def 1;
end;
assume p in {fxf};
then
A17: p = fxf by TARSKI:def 1;
y in Y by A14,TARSKI:def 1;
hence p in Xsi by A6,A14,A17;
end;
then Xsi = {fxf} by TARSKI:2;
then fxf = "/\"(Xsi, L) by YELLOW_0:39;
then
A18: fxf in Xs by A2;
let a be Element of L;
assume Xs is_<=_than a;
hence thesis by A18;
end;
ex_sup_of Xs, L by YELLOW_0:17;
then f.xf = "\/"(Xs, L) by A8,A13,YELLOW_0:def 9;
hence (F|FUF).xf = f.xf by A5,Def3;
end;
hence thesis;
end;
theorem Th15:
for L being continuous complete non empty Poset, f being
Function of FixedUltraFilters X, the carrier of L, h being CLHomomorphism of
InclPoset Filt BoolePoset X, L st h | FixedUltraFilters X = f holds h = f
-extension_to_hom
proof
let L be continuous complete non empty Poset, f be Function of
FixedUltraFilters X, the carrier of L, h be CLHomomorphism of InclPoset Filt
BoolePoset X, L;
assume
A1: h | FixedUltraFilters X = f;
set F = f-extension_to_hom;
set cL = the carrier of L;
set BP = BoolePoset X;
set IP = InclPoset Filt BP;
set cIP = the carrier of IP;
A2: InclPoset Filt BP = RelStr(#Filt BP, RelIncl Filt BP#) by YELLOW_1:def 1;
reconsider F9 = F as Function of cIP, cL;
reconsider h9 = h as Function of cIP, cL;
A3: the carrier of BP = the carrier of LattPOSet BooleLatt X by YELLOW_1:def 2
.= bool X by LATTICE3:def 1;
now
set FUF = FixedUltraFilters X;
let Fi be Element of cIP;
Fi in Filt BP by A2;
then consider FF being Filter of BP such that
A4: Fi = FF;
set Xsf = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) where Y is
Subset of X : Y in FF };
set Xs = {"/\"({uparrow x : ex z st x = {z} & z in Y}, IP) where Y is
Subset of X : Y in FF };
A5: Xs c= cIP
proof
let p be object;
assume p in Xs;
then
ex YY being Subset of X st p = "/\"({uparrow x : ex z st x = {z} & z
in YY}, IP) & YY in FF;
hence thesis;
end;
now
consider YY being object such that
A6: YY in FF by XBOOLE_0:def 1;
reconsider YY as set by TARSKI:1;
"/\"({uparrow x : ex z st x = {z} & z in YY}, IP) in Xs by A3,A6;
hence Xs is non empty;
end;
then reconsider Xs as non empty Subset of IP by A5;
A7: ex_sup_of Xs, IP by YELLOW_0:17;
A8: Xs is directed
proof
let a, b be Element of IP;
assume that
A9: a in Xs and
A10: b in Xs;
consider Yb being Subset of X such that
A11: b = "/\"({uparrow x : ex z st x = {z} & z in Yb}, IP) and
A12: Yb in FF by A10;
reconsider Yb9 = Yb as Element of FF by A12;
set Xsb = {uparrow x : ex z st x = {z} & z in Yb};
consider Ya being Subset of X such that
A13: a = "/\"({uparrow x : ex z st x = {z} & z in Ya}, IP) and
A14: Ya in FF by A9;
reconsider Ya9 = Ya as Element of FF by A14;
set Xsa = {uparrow x : ex z st x = {z} & z in Ya};
per cases;
suppose
A15: Xsa is empty;
take a;
thus a in Xs by A9;
thus a <= a;
"/\"(Xsa, IP) = Top IP by A15;
hence b <= a by A13,YELLOW_0:45;
end;
suppose
A16: Xsb is empty;
take b;
thus b in Xs by A10;
"/\"(Xsb, IP) = Top IP by A16;
hence a <= b by A11,YELLOW_0:45;
thus b <= b;
end;
suppose
A17: Xsa is non empty & Xsb is non empty;
Xsb c= cIP
proof
let r be object;
assume r in Xsb;
then
ex xz being Element of BP st r = uparrow xz & ex z st xz = {z} &
z in Yb;
hence thesis by A2;
end;
then reconsider Xsb as non empty Subset of IP by A17;
Xsa c= cIP
proof
let r be object;
assume r in Xsa;
then
ex xz being Element of BP st r = uparrow xz & ex z st xz = {z} &
z in Ya;
hence thesis by A2;
end;
then reconsider Xsa as non empty Subset of IP by A17;
A18: "/\"(Xsb, IP) = meet Xsb by WAYBEL16:10;
consider Yab being Element of BP such that
A19: Yab in FF and
A20: Yab <= Ya9 and
A21: Yab <= Yb9 by WAYBEL_0:def 2;
reconsider Yab as Element of FF by A19;
set c = "/\"({uparrow x : ex z st x = {z} & z in Yab}, IP);
set Xsc = {uparrow x : ex z st x = {z} & z in Yab};
A22: "/\"(Xsa, IP) = meet Xsa by WAYBEL16:10;
thus thesis
proof
per cases;
suppose
A23: Xsc is empty;
take c;
thus c in Xs by A3;
A24: "/\"(Xsc, IP) = Top IP by A23;
hence a <= c by YELLOW_0:45;
thus b <= c by A24,YELLOW_0:45;
end;
suppose
A25: Xsc is non empty;
Xsc c= cIP
proof
let r be object;
assume r in Xsc;
then
ex xz being Element of BP st r = uparrow xz & ex z st xz = {
z} & z in Yab;
hence thesis by A2;
end;
then reconsider Xsc as non empty Subset of IP by A25;
take c;
thus c in Xs by A3;
A26: "/\"(Xsc, IP) = meet Xsc by WAYBEL16:10;
a c= c
proof
let d be object;
Xsc c= Xsa
proof
let r be object;
assume r in Xsc;
then
A27: ex xz being Element of BP st r = uparrow xz & ex z st xz =
{z} & z in Yab;
Yab c= Ya by A20,YELLOW_1:2;
hence thesis by A27;
end;
then
A28: meet Xsa c= meet Xsc by SETFAM_1:6;
assume d in a;
hence thesis by A13,A22,A26,A28;
end;
hence a <= c by YELLOW_1:3;
b c= c
proof
let d be object;
Xsc c= Xsb
proof
let r be object;
assume r in Xsc;
then
A29: ex xz being Element of BP st r = uparrow xz & ex z st xz =
{z} & z in Yab;
Yab c= Yb by A21,YELLOW_1:2;
hence thesis by A29;
end;
then
A30: meet Xsb c= meet Xsc by SETFAM_1:6;
assume d in b;
hence thesis by A11,A18,A26,A30;
end;
hence b <= c by YELLOW_1:3;
end;
end;
end;
end;
A31: h is infs-preserving by WAYBEL16:def 1;
now
let s be object;
hereby
assume s in h.:Xs;
then consider t being object such that
t in the carrier of IP and
A32: t in Xs and
A33: s = h.t by FUNCT_2:64;
consider Y being Subset of X such that
A34: t = "/\"({uparrow x : ex z st x = {z} & z in Y}, IP) & Y in FF by A32;
set Xsi = {uparrow x : ex z st x = {z} & z in Y};
Xsi c= cIP
proof
let r be object;
assume r in Xsi;
then
ex xz being Element of BP st r = uparrow xz & ex z being Element
of X st xz = {z} & z in Y;
hence thesis by A2;
end;
then reconsider Xsi as Subset of IP;
set Xsif = {f.(uparrow x) : ex z st x = {z} & z in Y};
now
let u be object;
hereby
assume u in h.:Xsi;
then consider v being object such that
v in the carrier of IP and
A35: v in Xsi and
A36: u = h.v by FUNCT_2:64;
A37: ex x st v = uparrow x & ex z st x = {z} & z in Y by A35;
then v in FUF;
then h.v = f.v by A1,FUNCT_1:49;
hence u in Xsif by A36,A37;
end;
assume u in Xsif;
then consider x such that
A38: u = f.(uparrow x) and
A39: ex z st x = {z} & z in Y;
uparrow x in FUF by A39;
then
A40: h.(uparrow x) = f.(uparrow x) by A1,FUNCT_1:49;
uparrow x in Xsi by A39;
hence u in h.:Xsi by A38,A40,FUNCT_2:35;
end;
then
A41: h.:Xsi = Xsif by TARSKI:2;
h preserves_inf_of Xsi & ex_inf_of Xsi, IP by A31,YELLOW_0:17;
then inf (h.:Xsi) = h.inf Xsi;
hence s in Xsf by A33,A34,A41;
end;
assume s in Xsf;
then consider Y being Subset of X such that
A42: s = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A43: Y in FF;
set Xsi = {uparrow x : ex z st x = {z} & z in Y};
Xsi c= cIP
proof
let r be object;
assume r in Xsi;
then ex xz being Element of BP st r = uparrow xz & ex z being Element
of X st xz = {z} & z in Y;
hence thesis by A2;
end;
then reconsider Xsi as Subset of IP;
set Xsif = {f.(uparrow x) : ex z st x = {z} & z in Y};
h preserves_inf_of Xsi & ex_inf_of Xsi, IP by A31,YELLOW_0:17;
then
A44: inf (h.:Xsi) = h.inf Xsi;
now
let u be object;
hereby
assume u in h.:Xsi;
then consider v being object such that
v in the carrier of IP and
A45: v in Xsi and
A46: u = h.v by FUNCT_2:64;
A47: ex x st v = uparrow x & ex z st x = {z} & z in Y by A45;
then v in FUF;
then h.v = f.v by A1,FUNCT_1:49;
hence u in Xsif by A46,A47;
end;
assume u in Xsif;
then consider x such that
A48: u = f.(uparrow x) and
A49: ex z st x = {z} & z in Y;
uparrow x in FUF by A49;
then
A50: h.(uparrow x) = f.(uparrow x) by A1,FUNCT_1:49;
uparrow x in Xsi by A49;
hence u in h.:Xsi by A48,A50,FUNCT_2:35;
end;
then
A51: h.:Xsi = Xsif by TARSKI:2;
inf Xsi in Xs by A43;
hence s in h.:Xs by A42,A44,A51,FUNCT_2:35;
end;
then
A52: h.:Xs = Xsf by TARSKI:2;
A53: FF = "\/"({"/\"({uparrow x : ex z st x = {z} & z in Y}, IP) where Y is
Subset of X : Y in FF }, IP) by Th11;
h is directed-sups-preserving by WAYBEL16:def 1;
then h preserves_sup_of Xs by A8;
hence h9.Fi = sup (h.:Xs) by A4,A53,A7
.= F9.Fi by A4,A52,Def3;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th16:
FixedUltraFilters X is_FreeGen_set_of InclPoset Filt BoolePoset X
proof
set FUF = FixedUltraFilters X;
set IP = InclPoset Filt BoolePoset X;
let L be continuous complete non empty Poset;
let f be Function of FUF, the carrier of L;
reconsider F = f-extension_to_hom as CLHomomorphism of IP, L by
WAYBEL16:def 1;
take F;
thus F|FUF = f by Th14;
let h9 be CLHomomorphism of IP, L;
assume h9|FUF = f;
hence thesis by Th15;
end;
theorem Th17:
for L, M being continuous complete LATTICE, F, G being set st F
is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds L, M
are_isomorphic
proof
let L, M be continuous complete LATTICE, Lg, Mg be set such that
A1: Lg is_FreeGen_set_of L and
A2: Mg is_FreeGen_set_of M and
A3: card Lg = card Mg;
Lg,Mg are_equipotent by A3,CARD_1:5;
then consider f being Function such that
A4: f is one-to-one and
A5: dom f = Lg and
A6: rng f = Mg;
set g = f";
A7: dom g = Mg by A4,A6,FUNCT_1:33;
reconsider Mg as Subset of M by A2,Th7;
A8: rng g = Lg by A4,A5,FUNCT_1:33;
reconsider Lg as Subset of L by A1,Th7;
Mg c= the carrier of M;
then reconsider f as Function of Lg, the carrier of M by A5,A6,FUNCT_2:def 1
,RELSET_1:4;
consider F being CLHomomorphism of L, M such that
A9: F|Lg = f and
for h9 being CLHomomorphism of L, M st h9|Lg = f holds h9 = F by A1;
Lg c= the carrier of L;
then reconsider g as Function of Mg, the carrier of L by A7,A8,FUNCT_2:def 1
,RELSET_1:4;
consider G being CLHomomorphism of M, L such that
A10: G|Mg = g and
for h9 being CLHomomorphism of M, L st h9|Mg = g holds h9 = G by A2;
reconsider GF = G*F as CLHomomorphism of L, L by Th2;
GF|Lg = G*f by A9,RELAT_1:83
.= g*f by A6,A10,FUNCT_4:2
.= id Lg by A4,A5,FUNCT_1:39;
then
A11: GF = id L by A1,Th8;
then
A12: F is one-to-one by FUNCT_2:23;
reconsider FG = F*G as CLHomomorphism of M, M by Th2;
F is directed-sups-preserving by WAYBEL16:def 1;
then
A13: F is monotone by WAYBEL17:3;
G is directed-sups-preserving by WAYBEL16:def 1;
then
A14: G is monotone by WAYBEL17:3;
FG|Mg = F*g by A10,RELAT_1:83
.= f*g by A8,A9,FUNCT_4:2
.= id Mg by A4,A6,FUNCT_1:39;
then FG = id M by A2,Th8;
then F is onto by FUNCT_2:23;
then rng F = the carrier of M by FUNCT_2:def 3;
then G = (F qua Function)" by A11,A12,FUNCT_2:30;
then F is isomorphic by A12,A13,A14,WAYBEL_0:def 38;
hence thesis by WAYBEL_1:def 8;
end;
::$N Representation Theorem for Free Continuous Lattices
theorem :: Theorem 4.17, p. 90-91
for L being continuous complete LATTICE, G being set st G
is_FreeGen_set_of L & card G = card X holds L, InclPoset Filt BoolePoset X
are_isomorphic
proof
A1: FixedUltraFilters X is_FreeGen_set_of InclPoset Filt BoolePoset X & card
X = card FixedUltraFilters X by Th10,Th16;
let L be continuous complete LATTICE, G be set;
assume G is_FreeGen_set_of L & card G = card X;
hence thesis by A1,Th17;
end;