Copyright (c) 1998 Association of Mizar Users
environ
vocabulary BHSP_3, WAYBEL_0, LATTICES, TARSKI, ORDINAL2, QUANTAL1, YELLOW_1,
OPPCAT_1, ORDERS_1, PRE_TOPC, WAYBEL16, FUNCT_1, YELLOW_0, RELAT_1,
LATTICE3, WAYBEL_5, WELLORD2, FILTER_0, WELLORD1, BOOLE, CAT_1, SUBSET_1,
SETFAM_1, CARD_1, FILTER_1, SEQM_3, AMI_1, ZF_REFLE, PBOOLE, FUNCOP_1,
PRALG_1, YELLOW_2, FUNCT_6, CARD_3, FRAENKEL, WAYBEL22;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
STRUCT_0, FUNCT_2, FUNCT_6, PRALG_3, GRCAT_1, WELLORD1, CARD_1, CARD_3,
PRE_TOPC, ORDERS_1, LATTICE3, PBOOLE, MSUALG_1, AMI_1, FRAENKEL,
YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3,
WAYBEL_5, WAYBEL16;
constructors ORDERS_3, TOPS_2, GRCAT_1, TOLER_1, PRALG_3, WAYBEL_1, WAYBEL_5,
WAYBEL_8, WAYBEL16;
clusters STRUCT_0, FUNCT_1, LATTICE3, PBOOLE, PRALG_1, PRVECT_1, AMI_1,
YELLOW_0, YELLOW_7, WAYBEL_0, WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL16,
RELSET_1, SUBSET_1, FRAENKEL, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, ORDERS_3, LATTICE3, WELLORD2, YELLOW_0, 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,
PRE_TOPC, GRCAT_1, BORSUK_1, LATTICE3, AMI_1, MSUALG_1, PBOOLE, EXTENS_1,
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;
schemes FUNCT_1, 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 set;
hereby assume x in XX; then consider Z being Subset of L such that
A3: x = Z & Z in X;
thus x in X by A3;
end;
assume A4: x in X;
then reconsider x' = x as Subset of L by A1;
x' in XX by A4;
hence x in XX;
end;
"/\"({"/\"(Y, L) where Y is Subset of L: P[Y]}, L) = "/\"(union XX, L)
from Inf_of_Infs;
hence "/\"(union X, L) = "/\"({inf Y where Y is Subset of L: Y in X}, L)
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 set;
hereby assume x in XX; then consider Z being Subset of L such that
A3: x = Z & Z in X;
thus x in X by A3;
end;
assume A4: x in X;
then reconsider x' = x as Subset of L by A1;
x' in XX by A4;
hence x in XX;
end;
"\/"({"\/"(Y, L) where Y is Subset of L: P[Y]}, L) = "\/"(union XX, L)
from Sup_of_Sups;
hence "\/"(union X, L) = "\/"
({sup Y where Y is Subset of L: Y in X}, L) 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 sup F = union F 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;
A1: f is infs-preserving & g is infs-preserving &
f is directed-sups-preserving & g is directed-sups-preserving
by WAYBEL16:def 1;
then A2: g*f is infs-preserving by WAYBEL20:26;
g*f is directed-sups-preserving by A1,WAYBEL20:29;
hence g*f is CLHomomorphism of L, T by A2,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;
assume
A1: ex_inf_of X, L; set f = id L;
A2: f = id the carrier of L by GRCAT_1:def 11;
then A3: f.:X = X by BORSUK_1:3;
thus ex_inf_of f.:X, L by A1,A2,BORSUK_1:3;
thus inf (f.:X) = f.inf X by A3,GRCAT_1:11;
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; assume
A1: ex_sup_of X, L; set f = id L;
A2: f = id the carrier of L by GRCAT_1:def 11;
then A3: f.:X = X by BORSUK_1:3;
thus ex_sup_of f.:X, L by A1,A2,BORSUK_1:3;
thus sup (f.:X) = f.sup X by A3,GRCAT_1:11;
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);
A1: id L is directed-sups-preserving by Th4;
id L is infs-preserving by Th3;
hence id L is CLHomomorphism of L, L by A1,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: BoolePoset cL = InclPoset bool cL by YELLOW_1:4;
A2: InclPoset bool cL = RelStr(#bool cL, RelIncl bool cL#)
by YELLOW_1:def 1;
then A3: cBP = bool cL & rBP = RelIncl bool cL by YELLOW_1:4;
A4: InclPoset Filt L = RelStr(#Filt L, RelIncl Filt L#)
by YELLOW_1:def 1;
then A5: field rIP = Filt L by WELLORD2:def 1;
A6: Filt L = {X where X is Filter of L: not contradiction}by WAYBEL_0:def 24;
A7: Filt L c= bool cL proof let x be set; assume x in Filt L;
then consider X being Filter of L such that
A8: x = X by A6;
thus x in bool cL by A8;
end;
A9: cIP c= cBP proof let x be set; assume x in cIP;
then consider X being Filter of L such that
A10: x = X by A4,A6;
thus x in cBP by A1,A2,A10;
end;
rIP c= rBP proof let p be set; assume
A11: p in rIP;
then consider x, y being set such that
A12: p = [x, y] by RELAT_1:def 1;
A13: x in field rIP & y in field rIP by A11,A12,RELAT_1:30;
then consider X being Filter of L such that
A14: x = X by A5,A6;
consider Y being Filter of L such that
A15: y = Y by A5,A6,A13;
X c= Y by A4,A5,A11,A12,A13,A14,A15,WELLORD2:def 1;
hence p in rBP by A1,A2,A12,A14,A15,WELLORD2:def 1;
end;
then reconsider IP as SubRelStr of BP by A9,YELLOW_0:def 13;
now let p be set;
A16: rBP|_2 cIP = rBP /\ [:cIP, cIP:] by WELLORD1:def 6;
hereby assume
A17: p in rIP;
then consider x, y being set such that
A18: p = [x, y] by RELAT_1:def 1;
A19: x in field rIP & y in field rIP by A17,A18,RELAT_1:30;
then consider X being Filter of L such that
A20: x = X by A5,A6;
consider Y being Filter of L such that
A21: y = Y by A5,A6,A19;
X c= Y by A4,A5,A17,A18,A19,A20,A21,WELLORD2:def 1;
then p in rBP by A1,A2,A18,A20,A21,WELLORD2:def 1;
hence p in rBP|_2 cIP by A16,A17,XBOOLE_0:def 3;
end;
assume p in rBP|_2 cIP;
then A22: p in rBP & p in [:cIP, cIP:] by A16,XBOOLE_0:def 3;
then consider x, y being set such that
A23: x in cIP & y in cIP & p = [x, y] by ZFMISC_1:def 2;
consider X being Filter of L such that
A24: x = X by A4,A6,A23;
consider Y being Filter of L such that
A25: y = Y by A4,A6,A23;
x c= y by A1,A2,A22,A23,A24,A25,WELLORD2:def 1;
hence p in rIP by A4,A23,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;
A26: 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 X is empty;
then A27: "/\"(X, BP) = Top BP by YELLOW_0:def 12
.= cL by YELLOW_1:19;
[#]L = cL by PRE_TOPC:12;
hence "/\"(X, BP) in the carrier of IP by A4,A6,A27;
suppose A28: X is non empty;
X c= bool cL by A4,A7,XBOOLE_1:1;
then reconsider X' = X as Subset of BP by A1,A2;
reconsider F = X as Subset of bool cL by A4,A7,XBOOLE_1:1;
A29: inf X' = meet X by A28,YELLOW_1:20;
reconsider sX as Subset of L by A3;
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 A4;
then consider Z being Filter of L such that
A30: Y = Z by A6;
thus Top L in Y by A30,WAYBEL_4:22;
end;
then A31: sX is non empty by A28,A29,SETFAM_1:def 1;
A32: for X being Subset of L st X in F holds X is upper filtered proof
let X be Subset of L such that
A33: X in F; X in Filt L by A4,A33;
then consider Y being Filter of L such that
A34: X = Y by A6;
thus X is upper filtered by A34;
end;
then for X being Subset of L st X in F holds X is upper;
then A35: sX is upper by A29,YELLOW_2:39;
sX is filtered by A29,A32,YELLOW_2:41;
hence "/\"(X, BP) in the carrier of IP by A4,A6,A31,A35;
end;
IP is directed-sups-inheriting proof
let X be directed Subset of IP such that
A36: X <> {} & ex_sup_of X, BP;
set sX = "\/"(X, BP);
X c= bool cL by A4,A7,XBOOLE_1:1;
then reconsider X' = X as Subset of BP by A1,A2;
reconsider F = X as Subset of bool cL by A4,A7,XBOOLE_1:1;
A37: sup X' = union X by YELLOW_1:21;
reconsider sX as Subset of L by A3;
consider Y being set such that
A38: Y in X by A36,XBOOLE_0:def 1;
Y in Filt L by A4,A38;
then consider Z being Filter of L such that
A39: Y = Z by A6;
Top L in Y by A39,WAYBEL_4:22;
then A40: sX is non empty by A37,A38,TARSKI:def 4;
A41: 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 A4;
then consider Y being Filter of L such that
A42: X = Y by A6;
thus X is upper filtered by A42;
end;
then for X being Subset of L st X in F holds X is upper;
then A43: sX is upper by A37,WAYBEL_0:28;
A44: for X being Subset of L st X in F holds X is filtered by A41;
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
A45: P in F & R in F;
then reconsider P' = P, R' = R as Element of IP;
consider Z being Element of IP such that
A46: Z in X & P' <= Z & R' <= Z by A45,WAYBEL_0:def 1;
Z in the carrier of IP by A46;
then consider Z' being Filter of L such that
A47: Z' = Z by A4,A6;
take Z';
thus Z' in F by A46,A47;
P' c= Z & R' c= Z by A46,YELLOW_1:3;
hence P \/ R c= Z' by A47,XBOOLE_1:8;
end;
then sX is filtered by A37,A44,WAYBEL_0:47;
hence "\/"(X,BP) in the carrier of IP by A4,A6,A40,A43;
end;
hence InclPoset Filt L is CLSubFrame of BP by A26;
end;
definition
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 InclPoset Filt L is continuous by WAYBEL_5:28;
end;
end;
definition
let L be upper-bounded non empty Poset;
cluster -> non empty 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 x in {X where X is Filter of L: not contradiction} by WAYBEL_0:def 24;
then consider X being Filter of L such that
A1: x = X;
thus x is non empty by A1;
end;
end;
begin :: Free generators of continuous lattices
definition :: replaces :: WAYBEL16:def 2
let S be continuous complete (non empty Poset);
let A be set;
pred A is_FreeGen_set_of S means :Def1:
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 h' being CLHomomorphism of S,T st h'|A = f holds h' = 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 let S be continuous complete (non empty Poset), A be set such that
A1: A is_FreeGen_set_of S;
consider T being continuous complete (non empty Poset);
consider f being Function of A, the carrier of T;
consider h being CLHomomorphism of S, T such that
A2: h|A = f and
for h' being CLHomomorphism of S, T st h'|A = f holds h' = h by A1,Def1;
A3: dom f = A by FUNCT_2:def 1;
A4: dom h = the carrier of S by FUNCT_2:def 1;
dom (h|A) = dom h /\ A by RELAT_1:90;
then A c= the carrier of S by A2,A3,A4,XBOOLE_1:17;
hence A is Subset of S;
end;
theorem Th8:
for S being continuous complete (non empty Poset), A being set
st A is_FreeGen_set_of S
for h' being CLHomomorphism of S, S st h'|A = id A holds h' = 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;
dom id A = A & rng id A = A by RELAT_1:71;
then reconsider f = id A as Function of A,the carrier of L
by A2,FUNCT_2:def 1,RELSET_1:11;
consider h being CLHomomorphism of L, L such that
h|A = f and
A3: for h' being CLHomomorphism of L,L st h'|A = f holds h' = h by A1,Def1;
let h' be CLHomomorphism of S, S such that
A4: h'|A = id A;
A5: id L is CLHomomorphism of L, L by Th5;
id L = id the carrier of L by GRCAT_1:def 11;
then A6: (id L)|A = id A by A2,FUNCT_3:1;
thus h' = h by A3,A4
.= id L by A3,A5,A6;
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 :Def2:
{ 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 set; assume
z in FUF; then consider x being Element of BoolePoset X such that
A1: z = uparrow x & ex y being Element of X st x = {y};
thus z in bool the carrier of BoolePoset X by A1;
end;
then FUF is Subset-Family of BoolePoset X by SETFAM_1:def 7;
hence FUF is Subset-Family of BoolePoset X;
end;
end;
theorem Th9:
FixedUltraFilters X c= Filt BoolePoset X
proof
A1: FixedUltraFilters X = { uparrow x : ex z st x = {z} } by Def2;
let F be set; assume F in FixedUltraFilters X;
then consider x being Element of BoolePoset X such that
A2: F = uparrow x and
ex y being Element of X st x = {y} by A1;
F in {Z where Z is Filter of BoolePoset X : not contradiction} by A2;
hence F in Filt BoolePoset X by WAYBEL_0:def 24;
end;
theorem Th10:
Card FixedUltraFilters X = Card X
proof set FUF = { uparrow x : ex z st x = {z} };
A1: FUF = FixedUltraFilters X by Def2;
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;
X,FUF are_equipotent proof
defpred P[set, set] means
ex y being Element of X, x being Element of BoolePoset X
st x = {y} & $1 = y & $2 = uparrow x;
A5: for x,y1,y2 being set st x in X & P[x,y1] & P[x,y2] holds y1 = y2;
A6: for x being set st x in X ex y being set st P[x,y] proof
let x be set; assume
A7: x in X;
then reconsider x' = x as Element of X;
{x} c= X by A7,ZFMISC_1:37;
then reconsider bx = {x} as Element of BoolePoset X by A2,A3;
take uparrow bx; take x'; take bx; thus thesis;
end;
consider f being Function such that
A8: dom f = X & for x being set st x in X holds P[x, f.x] from FuncEx(A5,A6);
take f;
thus f is one-to-one proof
let x1, x2 be set such that
A9: x1 in dom f & x2 in dom f and
A10: f.x1 = f.x2;
consider x1' being Element of X, bx1 being Element of BoolePoset X
such that
A11: bx1 = {x1'} & x1 = x1' & f.x1 = uparrow bx1 by A8,A9;
consider x2' being Element of X, bx2 being Element of BoolePoset X
such that
A12: bx2 = {x2'} & x2 = x2' & f.x2 = uparrow bx2 by A8,A9;
bx1 = bx2 by A10,A11,A12,WAYBEL_0:20;
hence x1 = x2 by A11,A12,ZFMISC_1:6;
end;
thus dom f = X by A8;
now let z be set;
hereby assume z in rng f; then consider x1 being set such that
A13: x1 in dom f & z = f.x1 by FUNCT_1:def 5;
consider x1' being Element of X, bx1 being Element of BoolePoset X
such that
A14: bx1 = {x1'} & x1 = x1' & f.x1 = uparrow bx1 by A8,A13;
thus z in FUF by A13,A14;
end;
assume z in FUF;
then consider bx being Element of BoolePoset X such that
A15: z = uparrow bx & ex y being Element of X st bx = {y};
consider y being Element of X such that
A16: bx = {y} by A15;
A17: y in X by A4,A16,ZFMISC_1:37;
then consider x1' being Element of X, bx1 being Element of BoolePoset
X
such that
A18: bx1 = {x1'} & y = x1' & f.y = uparrow bx1 by A8;
thus z in rng f by A8,A15,A16,A17,A18,FUNCT_1:def 5;
end;
hence rng f = FUF by TARSKI:2;
end;
hence Card FixedUltraFilters X = Card X by A1,CARD_1:21;
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;
A2: the carrier of BP = the carrier of LattPOSet BooleLatt X
by YELLOW_1:def 2
.= the carrier of RelStr(#the carrier of BooleLatt X,
LattRel BooleLatt X#) by LATTICE3:def 2
.= bool X by LATTICE3:def 1;
A3: Xs c= cIP proof let p be set; assume p in Xs;
then consider YY being Subset of X such that
A4: p = "/\"({uparrow x : ex z st x = {z} & z in YY}, IP) and YY in F;
thus p in cIP by A4;
end;
now consider YY being set such that
A5: YY in F by XBOOLE_0:def 1;
"/\"({uparrow x : ex z st x = {z} & z in YY}, IP) in Xs by A2,A5;
hence Xs is non empty;
end;
then reconsider Xs' = Xs as non empty Subset of IP by A3;
A6: ex_sup_of Xs', IP by YELLOW_0:17;
A7: Filt BP = { FF where FF is Filter of BP : not contradiction }
by WAYBEL_0:def 24;
then F in Filt BP;
then reconsider F' = F as Element of IP by A1;
F c= RS proof let p be set; assume
A8: 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};
A9: "/\"(Xsi, IP) in Xs by A2;
per cases;
suppose Xsi is empty;
then A10: "/\"(Xsi, IP) = Top IP by YELLOW_0:def 12 .= bool X by WAYBEL16:
15;
Xs' is_<=_than RS by A6,YELLOW_0:def 9;
then "/\"(Xsi, IP) <= RS by A9,LATTICE3:def 9;
then A11: bool X c= RS by A10,YELLOW_1:3;
p in the carrier of BP by A8;
hence p in RS by A2,A11;
suppose A12: Xsi is non empty;
Xsi c= cIP proof let r be set; assume r in Xsi;
then consider xz being Element of BP such that
A13: r = uparrow xz and
ex z being Element of X st xz = {z} & z in Y;
thus r in cIP by A1,A7,A13;
end;
then reconsider Xsi as non empty Subset of IP by A12;
A14: "/\"(Xsi, IP) = meet Xsi by WAYBEL16:10;
for yy being set st yy in Xsi holds Y in yy proof
let yy be set; assume yy in Xsi;
then consider r being Element of BP such that
A15: yy = uparrow r and
A16: ex z being Element of X st r = {z} & z in Y;
reconsider Y' = Y as Element of BP;
r c= Y by A16,ZFMISC_1:37; then r <= Y' by YELLOW_1:2;
hence Y in yy by A15,WAYBEL_0:18;
end; then Y in meet Xsi by SETFAM_1:def 1;
then A17: p in union Xs by A9,A14,TARSKI:def 4;
union Xs' c= RS by A6,WAYBEL16:17;
hence p in RS by A17;
end;
then A18: F' <= RS by YELLOW_1:3;
Xs is_<=_than F' proof let b be Element of IP; assume b in Xs;
then consider Y being Subset of X such that
A19: b = "/\"({uparrow x : ex z st x = {z} & z in Y}, IP) and
A20: Y in F;
reconsider Y' = Y as Element of F by A20;
set Xsi = {uparrow x : ex z st x = {z} & z in Y};
per cases;
suppose A21: Y is empty;
now assume Xsi is non empty; then consider p being set such that
A22: p in Xsi by XBOOLE_0:def 1;
consider x being Element of BP such that
p = uparrow x and
A23: ex z being Element of X st x = {z} & z in Y by A22;
consider z being Element of X such that
A24: x = {z} & z in Y by A23;
thus contradiction by A21,A24;
end;
then A25: "/\"(Xsi, IP) = Top IP by YELLOW_0:def 12 .= bool X by WAYBEL16:
15;
Bottom BP = {} by YELLOW_1:18;
then uparrow Bottom BP c= F by A20,A21,WAYBEL11:42;
then bool X c= F by A2,WAYBEL14:10;
hence b <= F' by A2,A19,A25,XBOOLE_0:def 10;
suppose A26: Y is non empty;
A27: now consider z being set such that
A28: z in Y by A26,XBOOLE_0:def 1;
reconsider z as Element of X by A28; {z} c= X by A28,ZFMISC_1:37;
then reconsider x = {z} as Element of BP by A2;
uparrow x in Xsi by A28;
hence Xsi is non empty;
end;
Xsi c= cIP proof let r be set; assume r in Xsi;
then consider xz being Element of BP such that
A29: r = uparrow xz and
ex z being Element of X st xz = {z} & z in Y;
thus r in cIP by A1,A7,A29;
end;
then reconsider Xsi as non empty Subset of IP by A27;
A30: "/\"(Xsi, IP) = meet Xsi by WAYBEL16:10;
b c= F' proof let yy be set; assume
A31: yy in b;
b in Filt BP by A1;
then consider bf being Filter of BP such that
A32: b = bf by A7;
reconsider yy' = yy as Element of bf by A31,A32;
reconsider yy' as Element of BP;
A33: uparrow Y' c= F' by WAYBEL11:42;
Y c= yy' proof let zz be set; assume
A34: zz in Y;
then reconsider z = zz as Element of X;
{z} c= X by A34,ZFMISC_1:37;
then reconsider xz = {z} as Element of BP by A2;
uparrow xz in Xsi by A34;
then yy in uparrow xz by A19,A30,A31,SETFAM_1:def 1; then xz <=
yy' by WAYBEL_0:18;
then {z} c= yy by YELLOW_1:2;
hence zz in yy' by ZFMISC_1:37;
end; then Y' <= yy' by YELLOW_1:2;
then yy in uparrow Y' by WAYBEL_0:18;
hence yy in F' by A33;
end;
hence b <= F' by YELLOW_1:3;
end; then RS <= F' by A6,YELLOW_0:def 9;
hence F = RS by A18,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 -> map 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 LambdaD;
reconsider F as map of IP, L;
take F;
thus thesis by A1;
end;
uniqueness proof
set IP = InclPoset Filt BoolePoset X;
let it1, it2 be map 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 it1' = it1 as Function of the carrier of IP, the carrier of L;
reconsider it2' = it2 as Function of the carrier of IP, the carrier of L;
now let Fi be Element of IP;
thus it1'.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
.= it2'.Fi by A3;
end;
hence it1 = it2 by FUNCT_2:113;
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; assume
F1 <= F2;
then A1: F1 c= F2 by YELLOW_1:3;
set F = f-extension_to_hom;
let FF1, FF2 be Element of L such that
A2: FF1 = F.F1 & FF2 = F.F2;
A3: 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;
A4: 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;
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 };
A5: ex_sup_of F1s, L by YELLOW_0:17;
A6: ex_sup_of F2s, L by YELLOW_0:17;
F1s c= F2s proof let s be set; assume s in F1s;
then consider Y being Subset of X such that
A7: s = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A8: Y in F1;
thus s in F2s by A1,A7,A8;
end;
hence FF1 <= FF2 by A2,A3,A4,A5,A6,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;
A1: 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;
A2: T = bool X by WAYBEL16:15;
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};
A3: "/\"({f.(uparrow x) : ex z st x = {z} & z in E}, L) in Z by A2;
A4: {f.(uparrow x) : ex z st x = {z} & z in E} = {} proof
assume not thesis; then consider r being set such that
A5: r in {f.(uparrow x) : ex z st x = {z} & z in E} by XBOOLE_0:def 1;
consider x such that r = f.(uparrow x) and
A6: ex z st x = {z} & z in E by A5;
thus contradiction by A6;
end;
A7: "/\"({}, L) = Top L by YELLOW_0:def 12;
Z is_<=_than "\/"(Z, L) by YELLOW_0:32;
then Top L <= "\/"(Z, L) by A3,A4,A7,LATTICE3:def 9;
hence F.Top IP = Top L by A1,WAYBEL15:5;
end;
definition :: 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 IP = InclPoset Filt BoolePoset X;
set F = f-extension_to_hom;
let Fs be Subset of IP such that
A1: Fs is non empty directed; assume ex_sup_of Fs, IP;
thus ex_sup_of F.:Fs, L by YELLOW_0:17;
A2: sup Fs = union Fs by A1,Th1;
reconsider Fs' = Fs as non empty Subset of IP by A1;
reconsider sFs = sup Fs as Element of IP;
A3: 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;
set FFs = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y
}, L) where Y is Subset of X : Y in sFs };
set FFsU = {{"/\"({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 Fs' : not contradiction
};
set Zs = {sup Z where Z is Subset of L : Z in FFsU};
FFsU c= bool the carrier of L proof let r be set; assume r in FFsU;
then consider YY being Element of Fs' such that
A4: r = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L)
where Y is Subset of X : Y in YY};
r c= the carrier of L proof let s be set; assume s in r;
then consider Y being Subset of X such that
A5: s = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
Y in YY by A4;
thus thesis by A5;
end;
hence r in bool the carrier of L;
end;
then A6: "\/"(union FFsU, L) = "\/"(Zs, L) by Lm2;
now let p be set;
hereby assume p in FFs; then consider Y being Subset of X such that
A7: p = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A8: Y in sFs;
consider YY being set such that
A9: Y in YY and
A10: YY in Fs by A2,A8,TARSKI:def 4;
A11: p in {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y1}, L)
where Y1 is Subset of X : Y1 in YY} by A7,A9;
{"/\"({f.(uparrow x) : ex z st x = {z} & z in Y1}, L)
where Y1 is Subset of X : Y1 in YY} in FFsU by A10;
hence p in union FFsU by A11,TARSKI:def 4;
end;
assume p in union FFsU; then consider r being set such that
A12: p in r and
A13: r in FFsU by TARSKI:def 4;
consider YY being Element of Fs' 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} by A13;
consider Y being Subset of X such that
A15: p = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A16: Y in YY by A12,A14;
Y in sFs by A2,A16,TARSKI:def 4;
hence p in FFs by A15;
end;
then A17: FFs = union FFsU by TARSKI:2;
now let r be set;
hereby assume r in F.:Fs; then consider YY being set such that
A18: YY in the carrier of IP and
A19: YY in Fs and
A20: F.YY = r by FUNCT_2:115;
reconsider YY as Element of Fs by A19;
reconsider YY' = YY as Element of IP by A18;
A21: F.YY' = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y
}, L) where Y is Subset of X : Y in YY'}, L) by Def3;
set Zi = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L)
where Y is Subset of X : Y in YY' };
Zi c= the carrier of L proof let t be set; assume t in Zi;
then consider Y being Subset of X such that
A22: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
Y in YY';
thus t in the carrier of L by A22;
end;
then reconsider Zi as Subset of L;
Zi in FFsU;
hence r in Zs by A20,A21;
end;
assume r in Zs; then consider Z being Subset of L such that
A23: r = sup Z and
A24: Z in FFsU;
consider YY being Element of Fs such that
A25: Z = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L)
where Y is Subset of X : Y in YY} by A24;
reconsider YY as Element of Fs';
reconsider YY' = YY as Element of IP;
F.YY' = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y
}, L) where Y is Subset of X : Y in YY'}, L) by Def3;
hence r in F.:Fs by A23,A25,FUNCT_2:43;
end;
hence sup (F.:Fs) = F.sup Fs by A3,A6,A17,TARSKI:2;
end;
end;
Lm3:
for X be with_non-empty_elements set holds
id X is non-empty ManySortedSet of X;
definition :: 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 BP = BoolePoset X; set IP = InclPoset Filt BP;
set F = f-extension_to_hom;
set cIP = the carrier of IP; set cL = the carrier of L;
set FUF = FixedUltraFilters X;
A1: FUF = { uparrow x where x is Element of BoolePoset X :
ex y being Element of X st x = {y} } by Def2;
A2: InclPoset Filt BP = RelStr(#Filt BP, RelIncl Filt BP#)
by YELLOW_1:def 1;
A3: Filt BP = { FF where FF is Filter of BP : not contradiction }
by WAYBEL_0:def 24;
A4: BoolePoset X = InclPoset bool X by YELLOW_1:4;
A5: InclPoset bool X = RelStr(#bool X, RelIncl bool X#)
by YELLOW_1:def 1;
then A6: the carrier of BoolePoset X = bool X by YELLOW_1:4;
let Fs be Subset of IP;
assume ex_inf_of Fs, IP;
thus ex_inf_of F.:Fs, L by YELLOW_0:17;
per cases;
suppose A7: Fs is empty;
then A8: "/\"(F.:Fs, L) = "/\"({}, L) by RELAT_1:149
.= Top L by YELLOW_0:def 12;
"/\"(Fs, IP) = Top IP by A7,YELLOW_0:def 12;
hence inf (F.:Fs) = F.inf Fs by A8,Th13;
suppose Fs is non empty;
then reconsider Fs' = Fs as non empty Subset of IP;
now assume {} in Fs'; then {} is Element of Fs';
then {} is Element of IP;
hence contradiction;
end;
then Fs' is with_non-empty_elements by AMI_1:def 1;
then reconsider K = id Fs' as non-empty ManySortedSet of Fs' by Lm3;
defpred P[set, set, set] means
$1 = "/\"({f.(uparrow x) : ex z st x = {z} & z in $2}, L);
A9: for i be set st i in Fs' holds
for s be set st s in K.i ex y be set st y in (Fs' --> cL).i &
P[y, s, i] proof
let i be set such that
A10: i in Fs';
let s be set such that s in K.i;
take y = "/\"({f.(uparrow x) : ex z st x = {z} & z in s}, L);
y in cL;
hence y in (Fs' --> cL).i by A10,FUNCOP_1:13;
thus P[y, s, i];
end;
consider FD being ManySortedFunction of K, (Fs' --> cL) such that
A11: for i being set st i in Fs' holds
ex g being Function of K.i, (Fs' --> cL).i st g = FD.i &
for s being set st s in K.i holds P[g.s, s, i] from MSFExFunc(A9);
A12: dom FD = Fs' by PBOOLE:def 3;
deffunc FDi(Element of Fs')
= {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y
}, L) where Y is Subset of X : Y in $1};
defpred rFD[Element of Fs'] means rng (FD.$1) = FDi($1);
A13: for s being Element of Fs' holds rFD[s] proof
let s be Element of Fs';
now let t be set;
hereby assume t in rng (FD.s);
then consider u being set such that
A14: u in dom (FD.s) and
A15: t = (FD.s).u by FUNCT_1:def 5;
A16: dom (FD.s) = K.s by FUNCT_2:def 1;
consider g being Function of K.s, (Fs' --> cL).s such that
A17: g = FD.s and
A18: for u being set st u in K.s holds P[g.u, u, s] by A11;
A19: g.u = "/\"({f.(uparrow x) : ex z st x = {z} & z in u}, L)
by A14,A16,A18;
A20: K.s = s by FUNCT_1:35;
s in cIP; then consider FF being Filter of BP such that
A21: s = FF by A2,A3;
reconsider u as Subset of X by A5,A14,A16,A20,A21,YELLOW_1:4;
u in s by A14,A16,FUNCT_1:35;
hence t in FDi(s) by A15,A17,A19;
end;
assume t in FDi(s); then consider Y being Subset of X such that
A22: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A23: Y in s;
A24: dom (FD.s) = K.s by FUNCT_2:def 1;
A25: K.s = s by FUNCT_1:35;
A26: Y in dom (FD.s) by A23,A24,FUNCT_1:35;
consider g being Function of K.s, (Fs' --> cL).s such that
A27: g = FD.s and
A28: for u being set st u in K.s holds P[g.u, u, s] by A11;
g.Y = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L)
by A23,A25,A28;
hence t in rng (FD.s) by A22,A26,A27,FUNCT_1:def 5;
end;
hence rFD[s] by TARSKI:2;
end;
reconsider FD as DoubleIndexedSet of K, L;
now let r be set;
hereby assume r in F.:Fs; then consider s being set such that
A29: s in cIP and
A30: s in Fs and
A31: F.s = r by FUNCT_2:115;
reconsider s' = s as Element of cIP by A29;
A32: F.s' = "\/"({"/\"({f.(uparrow x) : ex z st x = {z} & z in Y
}, L) where Y is Subset of X : Y in s'
}, L) by Def3;
reconsider s as Element of Fs' by A30;
rFD[s] by A13;
then r = Sup (FD.s) by A31,A32,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 Fs' such that
A33: r = Sup (FD.s) by WAYBEL_5:14;
rFD[s] by A13;
then F.s = "\/"(rng (FD.s), L) by Def3
.= Sup (FD.s) by YELLOW_2:def 5;
hence r in F.:Fs by A33,FUNCT_2:43;
end;
then F.:Fs = rng Sups FD by TARSKI:2;
then A34: inf (F.:Fs) = Inf Sups FD by YELLOW_2:def 6;
for j being Element of Fs' holds rng(FD.j) is directed proof
let j be Element of Fs';
let k, m be Element of L; assume
A35: k in rng(FD.j) & m in rng(FD.j);
then consider kd being set such that
A36: kd in dom (FD.j) and
A37: FD.j.kd = k by FUNCT_1:def 5;
consider md being set such that
A38: md in dom (FD.j) and
A39: FD.j.md = m by A35,FUNCT_1:def 5;
A40: dom (FD.j) = K.j by FUNCT_2:def 1;
A41: K.j = j by FUNCT_1:35;
j in cIP; then consider FF being Filter of BP such that
A42: j = FF by A2,A3;
reconsider kd as Element of BP by A36,A40,A41,A42;
reconsider md as Element of BP by A38,A40,A41,A42;
consider nd being Element of BP such that
A43: nd in FF & nd <= kd & nd <= md by A36,A38,A40,A41,A42,WAYBEL_0:def 2;
A44: rng(FD.j) = FDi(j) by A13;
set n = FD.j.nd;
n in rng(FD.j) by A40,A41,A42,A43,FUNCT_1:def 5;
then consider Y being Subset of X such that
A45: n = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
Y in j by A44;
reconsider n as Element of L by A45;
take n;
thus n in rng(FD.j) by A40,A41,A42,A43,FUNCT_1:def 5;
consider g being Function of K.j, (Fs' --> cL).j such that
A46: g = FD.j and
A47: for u being set st u in K.j holds P[g.u, u, j] by A11;
set kds = {f.(uparrow x) : ex z st x = {z} & z in kd};
A48: g.kd = "/\"(kds, L) by A36,A40,A47;
set nds = {f.(uparrow x) : ex z st x = {z} & z in nd};
A49: g.nd = "/\"(nds, L) by A41,A42,A43,A47;
A50: nd c= kd by A43,YELLOW_1:2;
A51: ex_inf_of kds, L by YELLOW_0:17;
A52: ex_inf_of nds, L by YELLOW_0:17;
nds c= kds proof let w be set; assume w in nds;
then consider x such that
A53: w = f.(uparrow x) and
A54: ex z st x = {z} & z in nd;
consider z such that
A55: x = {z} & z in nd by A54;
thus w in kds by A50,A53,A55;
end;
hence k <= n by A37,A46,A48,A49,A51,A52,YELLOW_0:35;
set mds = {f.(uparrow x) : ex z st x = {z} & z in md};
A56: g.md = "/\"(mds, L) by A38,A40,A47;
A57: nd c= md by A43,YELLOW_1:2;
A58: ex_inf_of mds, L by YELLOW_0:17;
nds c= mds proof let w be set; assume w in nds;
then consider x such that
A59: w = f.(uparrow x) and
A60: ex z st x = {z} & z in nd;
consider z such that
A61: x = {z} & z in nd by A60;
thus w in mds by A57,A59,A61;
end;
hence m <= n by A39,A46,A49,A52,A56,A58,YELLOW_0:35;
end;
then A62: Inf Sups FD = Sup Infs Frege FD by WAYBEL_5:19
.= "\/"(rng Infs Frege FD, L) by YELLOW_2:def 5;
meet Fs' is Filter of BoolePoset X by WAYBEL16:9;
then meet Fs' in Filt BP by A3;
then reconsider mFs = meet Fs' as Element of cIP by A2;
A63: inf Fs' = meet Fs' by WAYBEL16:10;
set smFs = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y
}, L) where Y is Subset of X : Y in mFs};
A64: F.(meet Fs') = "\/"(smFs, L) by Def3;
now let r be set;
reconsider pdFD = product doms FD as non empty functional set;
reconsider dFFD = product doms FD --> Fs' as ManySortedSet of pdFD;
reconsider FFD = Frege FD as DoubleIndexedSet of dFFD, L;
A65: dom FFD = pdFD by PBOOLE:def 3;
deffunc rFFDs(Element of pdFD) =
{"/\"({f.(uparrow x) : ex z st x = {z} & z in $1.u}, L)
where u is Element of Fs' : u in dom (FFD.$1) };
A66: now let s be Element of pdFD;
A67: dom FD = dom (FFD.s) by A65,WAYBEL_5:8;
now let t be set;
hereby assume t in rng (FFD.s);
then consider u being set such that
A68: u in dom (FFD.s) and
A69: t = FFD.s.u by FUNCT_1:def 5;
A70: FFD.s.u = (FD.u).(s.u) by A65,A67,A68,WAYBEL_5:9;
reconsider u as Element of Fs' by A67,A68,PBOOLE:def 3;
consider g being Function of K.u, (Fs' --> cL).u such that
A71: g = FD.u and
A72: for v being set st v in K.u holds P[g.v, v, u] by A11;
dom (FD.u) = K.u by FUNCT_2:def 1;
then s.u in K.u by A12,A65,WAYBEL_5:9;
then g.(s.u) = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L)
by A72;
hence t in rFFDs(s) by A68,A69,A70,A71;
end;
assume t in rFFDs(s);
then consider u being Element of Fs' such that
A73: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L) and
A74: u in dom (FFD.s);
reconsider u as Element of Fs';
consider g being Function of K.u, (Fs' --> cL).u such that
A75: g = FD.u and
A76: for v being set st v in K.u holds P[g.v, v, u] by A11;
dom (FD.u) = K.u by FUNCT_2:def 1;
then s.u in K.u by A12,A65,WAYBEL_5:9;
then g.(s.u) = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L)
by A76;
hence t in rng(FFD.s) by A65,A67,A73,A74,A75,WAYBEL_5:9;
end;
hence rng (FFD.s) = rFFDs(s) by TARSKI:2;
end; :: rFFDs
hereby assume r in rng Infs Frege FD;
then consider s being Element of pdFD such that
A77: r = Inf (FFD.s) by WAYBEL_5:14;
A78: dom FD = dom (FFD.s) by A65,WAYBEL_5:8;
A79: dom s = dom FD by A65,WAYBEL_5:8;
union rng s c= X proof let t be set; assume t in union rng s;
then consider te being set such that
A80: t in te & te in rng s by TARSKI:def 4;
consider u being set such that
A81: u in dom s & te = s.u by A80,FUNCT_1:def 5;
FD.u is Function of K.u, cL by A12,A79,A81,WAYBEL_5:6;
then dom (FD.u) = K.u by FUNCT_2:def 1
.= u by A12,A79,A81,FUNCT_1:34;
then A82: te in u by A65,A79,A81,WAYBEL_5:9;
u in cIP by A12,A79,A81; then consider FF being Filter of BP such
that
A83: u = FF by A2,A3;
thus t in X by A6,A80,A82,A83;
end;
then reconsider Y = union rng s as Subset of X;
set Ys = {f.(uparrow x) : ex z st x = {z} & z in Y};
now let Z be set; assume
A84: Z in Fs';
then Z in cIP; then consider FF being Filter of BP such that
A85: Z = FF by A2,A3;
s.Z in rng s by A12,A79,A84,FUNCT_1:def 5;
then A86: s.Z c= Y by ZFMISC_1:92;
A87: s.Z in dom (FD.Z) by A12,A65,A84,WAYBEL_5:9;
FD.Z is Function of K.Z, cL by A84,WAYBEL_5:6;
then A88: dom (FD.Z) = K.Z by FUNCT_2:def 1
.= Z by A84,FUNCT_1:34;
s.Z c= X by A86,XBOOLE_1:1;
then reconsider sZ = s.Z as Element of BP by A4,A5;
reconsider Y' = Y as Element of BP by A4,A5;
sZ <= Y' by A86,YELLOW_1:2;
hence Y in Z by A85,A87,A88,WAYBEL_0:def 20;
end;
then Y in mFs by SETFAM_1:def 1;
then A89: "/\"(Ys, L) in smFs;
set idFFDs = {{f.(uparrow x) : ex z st x = {z} & z in s.u}
where u is Element of Fs' : u in dom (FFD.s)};
A90: idFFDs c= bool the carrier of L proof let t be set; assume
t in idFFDs; then consider u being Element of Fs' such that
A91: t = {f.(uparrow x) : ex z st x = {z} & z in s.u} and
u in dom (FFD.s);
t c= cL proof let v be set; assume v in t;
then consider x such that
A92: v = f.(uparrow x) and
A93: ex z st x = {z} & z in s.u by A91;
consider z such that
A94: x = {z} and z in s.u by A93;
uparrow x in FUF by A1,A94;
hence v in cL by A92,FUNCT_2:7;
end;
hence t in bool cL;
end;
now let t be set;
hereby assume t in rFFDs(s);
then consider u being Element of Fs' such that
A95: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L) and
A96: u in dom (FFD.s);
{f.(uparrow x) : ex z st x = {z} & z in s.u} c= cL proof
let v be set; assume
v in {f.(uparrow x) : ex z st x = {z} & z in s.u};
then consider x such that
A97: v = f.(uparrow x) and
A98: ex z st x = {z} & z in s.u;
consider z such that
A99: x = {z} and
z in s.u by A98;
uparrow x in FUF by A1,A99;
hence v in cL by A97,FUNCT_2:7;
end;
then reconsider Y1 ={f.(uparrow x) : ex z st x = {z} & z in s.u}
as Subset of L;
Y1 in idFFDs by A96;
hence t in {inf YY where YY is Subset of L : YY in idFFDs} by A95;
end;
assume t in {inf YY where YY is Subset of L : YY in idFFDs};
then consider YY being Subset of L such that
A100: t = inf YY and
A101: YY in idFFDs;
consider u1 being Element of Fs' such that
A102: YY = {f.(uparrow x) : ex z st x = {z} & z in s.u1} and
A103: u1 in dom (FFD.s) by A101;
thus t in rFFDs(s) by A100,A102,A103;
end;
then A104: rFFDs(s) = {inf YY where YY is Subset of L : YY in idFFDs}
by TARSKI:2;
A105: "/\"(rng (FFD.s), L) = "/\"(rFFDs(s), L) by A66
.= "/\"(union idFFDs, L) by A90,A104,Lm1;
now let t be set;
hereby assume t in union idFFDs;
then consider te being set such that
A106: t in te and
A107: te in idFFDs by TARSKI:def 4;
consider u being Element of Fs' such that
A108: te = {f.(uparrow x) : ex z st x = {z} & z in s.u} and
A109: u in dom (FFD.s) by A107;
consider x such that
A110: t = f.(uparrow x) and
A111: ex z st x = {z} & z in s.u by A106,A108;
consider z such that
A112: x = {z} & z in s.u by A111;
s.u in rng s by A78,A79,A109,FUNCT_1:def 5;
then z in Y by A112,TARSKI:def 4;
hence t in Ys by A110,A112;
end;
assume t in Ys; then consider x such that
A113: t = f.(uparrow x) and
A114: ex z st x = {z} & z in Y;
consider z such that
A115: x = {z} & z in Y by A114;
consider ze being set such that
A116: z in ze & ze in rng s by A115,TARSKI:def 4;
consider u being set such that
A117: u in dom s & ze = s.u by A116,FUNCT_1:def 5;
reconsider u as Element of Fs' by A79,A117,PBOOLE:def 3;
A118: t in {f.(uparrow x1) where x1 is Element of BP :
ex z st x1 = {z} & z in s.u} by A113,A115,A116,A117;
{f.(uparrow x1) where x1 is Element of BP :
ex z st x1 = {z} & z in s.u} in idFFDs by A78,A79,A117;
hence t in union idFFDs by A118,TARSKI:def 4;
end;
then union idFFDs = Ys by TARSKI:2;
hence r in smFs by A77,A89,A105,YELLOW_2:def 6;
end;
assume r in smFs; then consider Y being Subset of X such that
A119: r = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A120: Y in mFs;
set s = Fs' --> Y;
set s' = s;
A121: dom doms FD = dom FD by EXTENS_1:3 .= dom s by A12,FUNCOP_1:19;
now let w be set; assume
w in dom doms FD;
then A122: w in Fs' by A121,FUNCOP_1:19;
then A123: (doms FD).w = dom (FD.w) by A12,FUNCT_6:31;
A124: FD.w is Function of K.w, (Fs' --> cL).w by A122,MSUALG_1:def 2;
(Fs' --> cL).w = cL by A122,FUNCOP_1:13;
then A125: dom (FD.w) = K.w by A124,FUNCT_2:def 1 .= w by A122,FUNCT_1:
35;
s.w = Y by A122,FUNCOP_1:13;
hence s.w in (doms FD).w by A120,A122,A123,A125,SETFAM_1:def 1;
end;
then reconsider s as Element of pdFD by A121,CARD_3:18;
A126: Inf (FFD.s) = "/\"(rng (FFD.s), L) by YELLOW_2:def 6;
A127: rng (FFD.s) = rFFDs(s) by A66;
now let t be set;
hereby assume t in rFFDs(s);
then consider u being Element of Fs' such that
A128: t = "/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L) and
u in dom (FFD.s);
s.u = Y by FUNCOP_1:13;
hence t in {r} by A119,A128,TARSKI:def 1;
end;
assume t in {r};
then A129: t = r by TARSKI:def 1;
consider u being Element of Fs';
A130: dom FD = dom (FFD.s) by A65,WAYBEL_5:8;
A131: dom s = dom FD by A65,WAYBEL_5:8;
A132: s' = s & dom s' = Fs' by FUNCOP_1:19;
s.u = Y by FUNCOP_1:13;
hence t in rFFDs(s) by A119,A129,A130,A131,A132;
end;
then A133: {"/\"({f.(uparrow x) : ex z st x = {z} & z in s.u}, L)
where u is Element of Fs' : u in dom (FFD.s) }
= {r} by TARSKI:2;
"/\"({r}, L) = r by A119,YELLOW_0:39;
hence r in rng Infs Frege FD by A126,A127,A133,WAYBEL_5:14;
end;
hence inf (F.:Fs) = F.inf Fs by A34,A62,A63,A64,TARSKI:2;
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;
A1: FUF = { uparrow x : ex z st x = {z} } by Def2;
set BP = BoolePoset X;
set IP = InclPoset Filt BP;
A2: InclPoset Filt BP = RelStr(#Filt BP, RelIncl Filt BP#)
by YELLOW_1:def 1;
A3: the carrier of BP = the carrier of LattPOSet BooleLatt X
by YELLOW_1:def 2
.= the carrier of RelStr(#the carrier of BooleLatt X,
LattRel BooleLatt X#) by LATTICE3:def 2
.= bool X by LATTICE3:def 1;
set F = f-extension_to_hom;
now
dom F = the carrier of IP by FUNCT_2:def 1;
then A4: FUF c= dom F by A2,Th9;
hence FUF = dom (F|FUF) by RELAT_1:91;
thus FUF = dom f by FUNCT_2:def 1;
let xf be set; assume
A5: xf in FUF;
then 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 A1;
A8: (F|FUF).xf = F.xf by A5,FUNCT_1:72;
reconsider x' = xf as Element of IP by A4,A5,FUNCT_2:def 1
;
set Xs = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y }, L)
where Y is Subset of X : Y in x' };
A9: ex_sup_of Xs, L by YELLOW_0:17;
reconsider FUF' = FUF as non empty Subset-Family of BoolePoset X by A5;
reconsider xf' = xf as Element of FUF' by A5;
reconsider f' = f as Function of FUF', the carrier of L;
f'.xf' is Element of L;
then reconsider fxf = f.xf' as Element of L;
A10: Xs is_<=_than fxf proof
let b be Element of L; assume
b in Xs;
then consider Y being Subset of X such that
A11: b = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A12: Y in x';
set Xsi = {f.(uparrow x) : ex z st x = {z} & z in Y };
consider y being Element of X such that
A13: xx = {y} by A7;
reconsider Y as Element of BoolePoset X by A6,A12;
xx <= Y by A6,A12,WAYBEL_0:18;
then xx c= Y by YELLOW_1:2;
then y in Y by A13,ZFMISC_1:37;
then A14: fxf in Xsi by A6,A13;
ex_inf_of Xsi, L by YELLOW_0:17;
then Xsi is_>=_than b by A11,YELLOW_0:def 10;
hence b <= fxf by A14,LATTICE3:def 8;
end;
for a being Element of L st Xs is_<=_than a holds fxf <= a proof
let a be Element of L such that
A15: Xs is_<=_than a;
xx <= xx;
then reconsider Y = xx as Element of x' 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
A16: xx = {y} by A7;
now let p be set;
hereby assume p in Xsi;
then consider r being Element of BoolePoset X such that
A17: p = f.(uparrow r) and
A18: ex z being Element of X st r = {z} & z in Y;
consider z being Element of X such that
A19: r = {z} & z in Y by A18;
xx = r by A16,A19,TARSKI:def 1;
hence p in {fxf} by A6,A17,TARSKI:def 1;
end;
assume p in {fxf};
then A20: p = fxf by TARSKI:def 1;
y in Y by A16,TARSKI:def 1;
hence p in Xsi by A6,A16,A20;
end;
then Xsi = {fxf} by TARSKI:2;
then fxf = "/\"(Xsi, L) & Y in x' by YELLOW_0:39;
then fxf in Xs by A3;
hence fxf <= a by A15,LATTICE3:def 9;
end;
then f.xf = "\/"(Xs, L) by A9,A10,YELLOW_0:def 9;
hence (F|FUF).xf = f.xf by A8,Def3;
end;
hence F|FUF = f by FUNCT_1:9;
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 BP = BoolePoset X; set IP = InclPoset Filt BP;
set cIP = the carrier of IP; set cL = the carrier of L;
set F = f-extension_to_hom;
A2: InclPoset Filt BP = RelStr(#Filt BP, RelIncl Filt BP#)
by YELLOW_1:def 1;
A3: Filt BP = { FF where FF is Filter of BP : not contradiction }
by WAYBEL_0:def 24;
A4: the carrier of BP = the carrier of LattPOSet BooleLatt X
by YELLOW_1:def 2
.= the carrier of RelStr(#the carrier of BooleLatt X,
LattRel BooleLatt X#) by LATTICE3:def 2
.= bool X by LATTICE3:def 1;
reconsider h' = h as Function of cIP, cL;
reconsider F' = F as Function of cIP, cL;
now let Fi be Element of cIP;
Fi in Filt BP by A2;
then consider FF being Filter of BP such that
A5: Fi = FF by A3;
A6: FF = "\/"({"/\"({uparrow x : ex z st x = {z} & z in Y}, IP)
where Y is Subset of X : Y in FF }, IP) by Th11;
set Xs = {"/\"({uparrow x : ex z st x = {z} & z in Y}, IP)
where Y is Subset of X : Y in FF };
A7: h is infs-preserving & h is directed-sups-preserving by WAYBEL16:def 1;
A8: Xs c= cIP proof let p be set; assume p in Xs;
then consider YY being Subset of X such that
A9: p = "/\"({uparrow x : ex z st x = {z} & z in YY}, IP) and
YY in FF;
thus p in cIP by A9;
end;
now consider YY being set such that
A10: YY in FF by XBOOLE_0:def 1;
"/\"({uparrow x : ex z st x = {z} & z in YY}, IP) in Xs by A4,A10;
hence Xs is non empty;
end;
then reconsider Xs as non empty Subset of IP by A8;
Xs is directed proof let a, b be Element of IP; assume
A11: a in Xs & b in Xs;
then consider Ya being Subset of X such that
A12: a = "/\"({uparrow x : ex z st x = {z} & z in Ya}, IP) and
A13: Ya in FF;
reconsider Ya' = Ya as Element of FF by A13;
consider Yb being Subset of X such that
A14: b = "/\"({uparrow x : ex z st x = {z} & z in Yb}, IP) and
A15: Yb in FF by A11;
reconsider Yb' = Yb as Element of FF by A15;
set Xsa = {uparrow x : ex z st x = {z} & z in Ya};
set Xsb = {uparrow x : ex z st x = {z} & z in Yb};
per cases;
suppose Xsa is empty;
then A16: "/\"(Xsa, IP) = Top IP by YELLOW_0:def 12;
take a;
thus a in Xs by A11;
thus a <= a;
thus b <= a by A12,A16,YELLOW_0:45;
suppose Xsb is empty;
then A17: "/\"(Xsb, IP) = Top IP by YELLOW_0:def 12;
take b;
thus b in Xs by A11;
thus a <= b by A14,A17,YELLOW_0:45;
thus b <= b;
suppose A18: Xsa is non empty & Xsb is non empty;
Xsa c= cIP proof let r be set; assume r in Xsa;
then consider xz being Element of BP such that
A19: r = uparrow xz and
ex z st xz = {z} & z in Ya;
thus r in cIP by A2,A3,A19;
end;
then reconsider Xsa as non empty Subset of IP by A18;
A20: "/\"(Xsa, IP) = meet Xsa by WAYBEL16:10;
Xsb c= cIP proof let r be set; assume r in Xsb;
then consider xz being Element of BP such that
A21: r = uparrow xz and
ex z st xz = {z} & z in Yb;
thus r in cIP by A2,A3,A21;
end;
then reconsider Xsb as non empty Subset of IP by A18;
A22: "/\"(Xsb, IP) = meet Xsb by WAYBEL16:10;
consider Yab being Element of BP such that
A23: Yab in FF and
A24: Yab <= Ya' and
A25: Yab <= Yb' by WAYBEL_0:def 2;
reconsider Yab as Element of FF by A23;
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};
thus thesis proof
per cases;
suppose Xsc is empty;
then A26: "/\"(Xsc, IP) = Top IP by YELLOW_0:def 12;
take c;
thus c in Xs by A4;
thus a <= c by A26,YELLOW_0:45;
thus b <= c by A26,YELLOW_0:45;
suppose A27: Xsc is non empty;
Xsc c= cIP proof let r be set; assume r in Xsc;
then consider xz being Element of BP such that
A28: r = uparrow xz and
ex z st xz = {z} & z in Yab;
thus r in cIP by A2,A3,A28;
end;
then reconsider Xsc as non empty Subset of IP by A27;
A29: "/\"(Xsc, IP) = meet Xsc by WAYBEL16:10;
take c;
thus c in Xs by A4;
a c= c proof let d be set; assume
A30: d in a;
Xsc c= Xsa proof let r be set; assume r in Xsc;
then consider xz being Element of BP such that
A31: r = uparrow xz and
A32: ex z st xz = {z} & z in Yab;
consider zz being Element of X such that
A33: xz = {zz} and
A34: zz in Yab by A32;
Yab c= Ya by A24,YELLOW_1:2;
hence r in Xsa by A31,A33,A34;
end;
then meet Xsa c= meet Xsc by SETFAM_1:7;
hence d in c by A12,A20,A29,A30;
end;
hence a <= c by YELLOW_1:3;
b c= c proof let d be set; assume
A35: d in b;
Xsc c= Xsb proof let r be set; assume r in Xsc;
then consider xz being Element of BP such that
A36: r = uparrow xz and
A37: ex z st xz = {z} & z in Yab;
consider zz being Element of X such that
A38: xz = {zz} and
A39: zz in Yab by A37;
Yab c= Yb by A25,YELLOW_1:2;
hence r in Xsb by A36,A38,A39;
end;
then meet Xsb c= meet Xsc by SETFAM_1:7;
hence d in c by A14,A22,A29,A35;
end;
hence b <= c by YELLOW_1:3;
end;
end;
then A40: h preserves_sup_of Xs by A7,WAYBEL_0:def 37;
A41: ex_sup_of Xs, IP by YELLOW_0:17;
set Xsf = {"/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L)
where Y is Subset of X : Y in FF };
set FUF = FixedUltraFilters X;
A42: FUF = { uparrow x : ex z st x = {z} } by Def2;
now let s be set;
hereby assume s in h.:Xs;
then consider t being set such that
t in the carrier of IP and
A43: t in Xs and
A44: s = h.t by FUNCT_2:115;
consider Y being Subset of X such that
A45: t = "/\"({uparrow x : ex z st x = {z} & z in Y}, IP) and
A46: Y in FF by A43;
set Xsi = {uparrow x : ex z st x = {z} & z in Y};
Xsi c= cIP proof let r be set; assume r in Xsi;
then consider xz being Element of BP such that
A47: r = uparrow xz and
ex z being Element of X st xz = {z} & z in Y;
thus r in cIP by A2,A3,A47;
end;
then reconsider Xsi as Subset of IP;
A48: h preserves_inf_of Xsi by A7,WAYBEL_0:def 32;
ex_inf_of Xsi, IP by YELLOW_0:17;
then A49: inf (h.:Xsi) = h.inf Xsi by A48,WAYBEL_0:def 30;
set Xsif = {f.(uparrow x) : ex z st x = {z} & z in Y};
now let u be set;
hereby assume u in h.:Xsi;
then consider v being set such that
v in the carrier of IP and
A50: v in Xsi and
A51: u = h.v by FUNCT_2:115;
consider x such that
A52: v = uparrow x and
A53: ex z st x = {z} & z in Y by A50;
consider z such that
A54: x = {z} & z in Y by A53;
v in FUF by A42,A52,A54;
then h.v = f.v by A1,FUNCT_1:72;
hence u in Xsif by A51,A52,A53;
end;
assume u in Xsif; then consider x such that
A55: u = f.(uparrow x) and
A56: ex z st x = {z} & z in Y;
consider z such that
A57: x = {z} & z in Y by A56;
A58: uparrow x in Xsi by A56;
uparrow x in FUF by A42,A57;
then h.(uparrow x) = f.(uparrow x) by A1,FUNCT_1:72;
hence u in h.:Xsi by A55,A58,FUNCT_2:43;
end;
then h.:Xsi = Xsif by TARSKI:2;
hence s in Xsf by A44,A45,A46,A49;
end;
assume s in Xsf; then consider Y being Subset of X such that
A59: s = "/\"({f.(uparrow x) : ex z st x = {z} & z in Y}, L) and
A60: Y in FF;
set Xsi = {uparrow x : ex z st x = {z} & z in Y};
Xsi c= cIP proof let r be set; assume r in Xsi;
then consider xz being Element of BP such that
A61: r = uparrow xz and
ex z being Element of X st xz = {z} & z in Y;
thus r in cIP by A2,A3,A61;
end;
then reconsider Xsi as Subset of IP;
A62: h preserves_inf_of Xsi by A7,WAYBEL_0:def 32;
ex_inf_of Xsi, IP by YELLOW_0:17;
then A63: inf (h.:Xsi) = h.inf Xsi by A62,WAYBEL_0:def 30;
set Xsif = {f.(uparrow x) : ex z st x = {z} & z in Y};
A64: inf Xsi in Xs by A60;
now let u be set;
hereby assume u in h.:Xsi;
then consider v being set such that
v in the carrier of IP and
A65: v in Xsi and
A66: u = h.v by FUNCT_2:115;
consider x such that
A67: v = uparrow x and
A68: ex z st x = {z} & z in Y by A65;
consider z such that
A69: x = {z} & z in Y by A68;
v in FUF by A42,A67,A69;
then h.v = f.v by A1,FUNCT_1:72;
hence u in Xsif by A66,A67,A68;
end;
assume u in Xsif; then consider x such that
A70: u = f.(uparrow x) and
A71: ex z st x = {z} & z in Y;
consider z such that
A72: x = {z} & z in Y by A71;
A73: uparrow x in Xsi by A71;
uparrow x in FUF by A42,A72;
then h.(uparrow x) = f.(uparrow x) by A1,FUNCT_1:72;
hence u in h.:Xsi by A70,A73,FUNCT_2:43;
end;
then h.:Xsi = Xsif by TARSKI:2;
hence s in h.:Xs by A59,A63,A64,FUNCT_2:43;
end;
then A74: h.:Xs = Xsf by TARSKI:2;
thus h'.Fi
= sup (h.:Xs) by A5,A6,A40,A41,WAYBEL_0:def 31
.= F'.Fi by A5,A74,Def3;
end;
hence h = f-extension_to_hom by FUNCT_2:113;
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 h' be CLHomomorphism of IP, L;
assume h'|FUF = f;
hence h' = F 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:21; then consider f being Function
such that
A4: f is one-to-one and
A5: dom f = Lg and
A6: rng f = Mg by WELLORD2:def 4;
set g = f";
A7: dom g = Mg by A4,A6,FUNCT_1:55;
A8: rng g = Lg by A4,A5,FUNCT_1:55;
reconsider Lg as Subset of L by A1,Th7;
reconsider Mg as Subset of M by A2,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:11;
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:11;
consider F being CLHomomorphism of L, M such that
A9: F|Lg = f and
for h' being CLHomomorphism of L, M st h'|Lg = f holds h' = F by A1,Def1;
consider G being CLHomomorphism of M, L such that
A10: G|Mg = g and
for h' being CLHomomorphism of M, L st h'|Mg = g holds h' = G by A2,Def1;
reconsider GF = G*F as CLHomomorphism of L, L by Th2;
GF|Lg = G*f by A9,RELAT_1:112
.= g*f by A6,A10,FUNCT_4:2
.= id Lg by A4,A5,FUNCT_1:61;
then GF = id L by A1,Th8;
then A11: G*F = id the carrier of L by GRCAT_1:def 11;
then A12: F is one-to-one by FUNCT_2:29;
F is directed-sups-preserving by WAYBEL16:def 1;
then A13: F is monotone by WAYBEL17:3;
reconsider FG = F*G as CLHomomorphism of M, M by Th2;
FG|Mg = F*g by A10,RELAT_1:112
.= f*g by A8,A9,FUNCT_4:2
.= id Mg by A4,A6,FUNCT_1:61;
then FG = id M by A2,Th8;
then F*G = id the carrier of M by GRCAT_1:def 11;
then rng F = the carrier of M by FUNCT_2:29;
then A14: G = (F qua Function)" by A11,A12,FUNCT_2:36;
G is directed-sups-preserving by WAYBEL16:def 1;
then G is monotone by WAYBEL17:3;
then F is isomorphic by A12,A13,A14,WAYBEL_0:def 38;
hence L, M are_isomorphic by WAYBEL_1:def 8;
end;
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 let L be continuous complete LATTICE, G be set such that
A1: G is_FreeGen_set_of L and
A2: Card G = Card X;
A3: FixedUltraFilters X is_FreeGen_set_of InclPoset Filt BoolePoset X by Th16;
Card X = Card FixedUltraFilters X by Th10;
hence L, InclPoset Filt BoolePoset X are_isomorphic by A1,A2,A3,Th17;
end;