:: Algebraic and Arithmetic Lattices
:: by Robert Milewski
::
:: Received March 4, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, RELAT_2, ORDERS_2, SUBSET_1, XXREAL_0, WAYBEL_8,
TARSKI, RCOMP_1, STRUCT_0, YELLOW_0, LATTICE3, CARD_FIL, LATTICES,
WAYBEL_0, WAYBEL_5, GROUP_6, WAYBEL10, YELLOW_1, FINSET_1, SETFAM_1,
REWRITE1, RELAT_1, FUNCT_1, ZFMISC_1, CAT_1, EQREL_1, WELLORD2, ORDINAL2,
WAYBEL_3, SEQM_3, PBOOLE, CARD_3, WELLORD1, WAYBEL_1, YELLOW_2;
notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, FINSET_1, RELAT_1,
ORDERS_1, ORDERS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, STRUCT_0,
PBOOLE, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, WAYBEL_1,
WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10;
constructors DOMAIN_1, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_3, WAYBEL_8,
WAYBEL10, RELSET_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1,
STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1,
WAYBEL_3, WAYBEL_8, WAYBEL10;
requirements SUBSET, BOOLE;
definitions TARSKI;
equalities YELLOW_2, STRUCT_0;
expansions TARSKI;
theorems TARSKI, ZFMISC_1, SETFAM_1, ORDERS_2, FUNCT_1, FUNCT_2, LATTICE3,
YELLOW_0, YELLOW_1, YELLOW_2, WAYBEL_0, CARD_3, WAYBEL_1, WAYBEL_3,
WAYBEL_4, WAYBEL_5, WAYBEL_8, WAYBEL10, XBOOLE_0, XBOOLE_1;
schemes FUNCT_2, PARTFUN1;
begin :: Preliminaries
theorem Th1:
for L be non empty reflexive transitive RelStr for x,y be Element
of L holds x <= y implies compactbelow x c= compactbelow y
proof
let L be non empty reflexive transitive RelStr;
let x,y be Element of L;
assume
A1: x <= y;
now
let z be object;
assume z in compactbelow x;
then z in {v where v is Element of L: x >= v & v is compact} by
WAYBEL_8:def 2;
then consider z9 be Element of L such that
A2: z9 = z and
A3: x >= z9 and
A4: z9 is compact;
z9 <= y by A1,A3,ORDERS_2:3;
hence z in compactbelow y by A2,A4,WAYBEL_8:4;
end;
hence thesis;
end;
theorem Th2:
for L be non empty reflexive RelStr for x be Element of L holds
compactbelow x is Subset of CompactSublatt L
proof
let L be non empty reflexive RelStr;
let x be Element of L;
now
let v be object;
assume v in compactbelow x;
then v in {z where z is Element of L: x >= z & z is compact} by
WAYBEL_8:def 2;
then ex v1 be Element of L st v1 = v & x >= v1 & v1 is compact;
hence v in the carrier of CompactSublatt L by WAYBEL_8:def 1;
end;
hence thesis by TARSKI:def 3;
end;
theorem Th3:
for L be RelStr for S be SubRelStr of L for X be Subset of S
holds X is Subset of L
proof
let L be RelStr;
let S be SubRelStr of L;
let X be Subset of S;
the carrier of S c= the carrier of L by YELLOW_0:def 13;
hence thesis by XBOOLE_1:1;
end;
theorem Th4:
for L be with_suprema non empty reflexive transitive RelStr holds
the carrier of L is Ideal of L
proof
let L be with_suprema non empty reflexive transitive RelStr;
[#]L is Ideal of L;
hence thesis;
end;
theorem Th5:
for L1 be lower-bounded non empty reflexive antisymmetric RelStr
for L2 be non empty reflexive antisymmetric RelStr st the RelStr of L1 = the
RelStr of L2 & L1 is up-complete holds the carrier of CompactSublatt L1 = the
carrier of CompactSublatt L2
proof
let L1 be lower-bounded non empty reflexive antisymmetric RelStr;
let L2 be non empty reflexive antisymmetric RelStr;
assume that
A1: the RelStr of L1 = the RelStr of L2 and
A2: L1 is up-complete;
now
reconsider L29 = L2 as lower-bounded non empty reflexive antisymmetric
RelStr by A1,YELLOW_0:13;
let x be object;
assume
A3: x in the carrier of CompactSublatt L2;
then x is Element of CompactSublatt L29;
then reconsider x2 = x as Element of L2 by YELLOW_0:58;
reconsider x1 = x2 as Element of L1 by A1;
A4: x2 is compact by A3,WAYBEL_8:def 1;
L2 is up-complete by A1,A2,WAYBEL_8:15;
then x1 is compact by A1,A4,WAYBEL_8:9;
hence x in the carrier of CompactSublatt L1 by WAYBEL_8:def 1;
end;
then
A5: the carrier of CompactSublatt L2 c= the carrier of CompactSublatt L1;
now
let x be object;
assume
A6: x in the carrier of CompactSublatt L1;
then reconsider x1 = x as Element of L1 by YELLOW_0:58;
reconsider x2 = x1 as Element of L2 by A1;
x1 is compact by A6,WAYBEL_8:def 1;
then x2 is compact by A1,A2,WAYBEL_8:9;
hence x in the carrier of CompactSublatt L2 by WAYBEL_8:def 1;
end;
then
the carrier of CompactSublatt L1 c= the carrier of CompactSublatt L2;
hence thesis by A5,XBOOLE_0:def 10;
end;
begin :: Algebraic and Arithmetic Lattices
theorem Th6: :: COROLLARY 4.10.
for L be algebraic lower-bounded LATTICE for S be CLSubFrame of L
holds S is algebraic
proof
let L be algebraic lower-bounded LATTICE;
let S be CLSubFrame of L;
the RelStr of S = Image closure_op S by WAYBEL10:18;
then (the RelStr of S) is algebraic by WAYBEL_8:24;
hence thesis by WAYBEL_8:17;
end;
theorem Th7: :: EXAMPLES 4.11.(2)
for X,E be set for L be CLSubFrame of BoolePoset X holds E in the
carrier of CompactSublatt L iff ex F be Element of BoolePoset X st F is finite
& E = meet { Y where Y is Element of L : F c= Y } & F c= E
proof
let X,E be set;
let L be CLSubFrame of BoolePoset X;
A1: the carrier of L c= the carrier of BoolePoset X by YELLOW_0:def 13;
A2: L is complete LATTICE by YELLOW_2:30;
thus E in the carrier of CompactSublatt L implies ex F be Element of
BoolePoset X st F is finite & E = meet { Y where Y is Element of L : F c= Y } &
F c= E
proof
A3: (closure_op L).:([#]CompactSublatt (BoolePoset X)) = [#]CompactSublatt
Image (closure_op L) by WAYBEL_8:25
.= [#]CompactSublatt (the RelStr of L) by WAYBEL10:18
.= the carrier of CompactSublatt (the RelStr of L);
assume E in the carrier of CompactSublatt L;
then E in (closure_op L).:([#]CompactSublatt (BoolePoset X)) by A2,A3,Th5;
then consider x be object such that
A4: x in dom (closure_op L) and
A5: x in [#]CompactSublatt (BoolePoset X) and
A6: E = (closure_op L).x by FUNCT_1:def 6;
reconsider F = x as Element of BoolePoset X by A4;
id(BoolePoset X) <= closure_op L by WAYBEL_1:def 14;
then id(BoolePoset X).F <= (closure_op L).F by YELLOW_2:9;
then F <= (closure_op L).F;
then
A7: F c= (closure_op L).F by YELLOW_1:2;
(closure_op L).x in rng (closure_op L) by A4,FUNCT_1:def 3;
then (closure_op L).x in the carrier of Image (closure_op L) by
YELLOW_0:def 15;
then (closure_op L).x in the carrier of the RelStr of L by WAYBEL10:18;
then
A8: (closure_op L).x in { Y where Y is Element of L : F c= Y } by A7;
take F;
F is compact by A5,WAYBEL_8:def 1;
hence F is finite by WAYBEL_8:28;
A9: (uparrow F) /\ the carrier of L c= { Y where Y is Element of L : F c= Y }
proof
let z be object;
assume
A10: z in (uparrow F) /\ the carrier of L;
then reconsider z9 = z as Element of BoolePoset X;
z in uparrow F by A10,XBOOLE_0:def 4;
then F <= z9 by WAYBEL_0:18;
then
A11: F c= z9 by YELLOW_1:2;
z in the carrier of L by A10,XBOOLE_0:def 4;
hence thesis by A11;
end;
{ Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the carrier of L
proof
let z be object;
assume z in { Y where Y is Element of L : F c= Y };
then consider z9 be Element of L such that
A12: z = z9 and
A13: F c= z9;
reconsider z1 = z9 as Element of BoolePoset X by A1;
F <= z1 by A13,YELLOW_1:2;
then z in uparrow F by A12,WAYBEL_0:18;
hence thesis by A12,XBOOLE_0:def 4;
end;
then
A14: (uparrow F) /\ the carrier of L = { Y where Y is Element of L : F c=
Y } by A9,XBOOLE_0:def 10;
thus
A15: E = "/\"((uparrow F) /\ the carrier of L,BoolePoset X) by A6,
WAYBEL10:def 5
.= meet { Y where Y is Element of L : F c= Y } by A8,A14,YELLOW_1:20;
now
let v be object;
assume
A16: v in F;
now
let V be set;
assume V in { Y where Y is Element of L : F c= Y };
then ex V9 be Element of L st V = V9 & F c= V9;
hence v in V by A16;
end;
hence v in E by A8,A15,SETFAM_1:def 1;
end;
hence thesis;
end;
thus ( ex F be Element of BoolePoset X st F is finite & E = meet { Y where Y
is Element of L : F c= Y } & F c= E ) implies E in the carrier of
CompactSublatt L
proof
given F be Element of BoolePoset X such that
A17: F is finite and
A18: E = meet { Y where Y is Element of L : F c= Y } and
F c= E;
F is compact by A17,WAYBEL_8:28;
then
A19: F in [#]CompactSublatt (BoolePoset X) by WAYBEL_8:def 1;
A20: (uparrow F) /\ the carrier of L c= { Y where Y is Element of L : F c= Y }
proof
let z be object;
assume
A21: z in (uparrow F) /\ the carrier of L;
then reconsider z9 = z as Element of BoolePoset X;
z in uparrow F by A21,XBOOLE_0:def 4;
then F <= z9 by WAYBEL_0:18;
then
A22: F c= z9 by YELLOW_1:2;
z in the carrier of L by A21,XBOOLE_0:def 4;
hence thesis by A22;
end;
{ Y where Y is Element of L : F c= Y } c= (uparrow F) /\ the carrier of L
proof
let z be object;
assume z in { Y where Y is Element of L : F c= Y };
then consider z9 be Element of L such that
A23: z = z9 and
A24: F c= z9;
reconsider z1 = z9 as Element of BoolePoset X by A1;
F <= z1 by A24,YELLOW_1:2;
then z in uparrow F by A23,WAYBEL_0:18;
hence thesis by A23,XBOOLE_0:def 4;
end;
then
A25: (uparrow F) /\ the carrier of L = { Y where Y is Element of L : F c=
Y } by A20,XBOOLE_0:def 10;
id(BoolePoset X) <= closure_op L by WAYBEL_1:def 14;
then id(BoolePoset X).F <= (closure_op L).F by YELLOW_2:9;
then F <= (closure_op L).F;
then
A26: F c= (closure_op L).F by YELLOW_1:2;
F in the carrier of BoolePoset X;
then
A27: F in dom (closure_op L) by FUNCT_2:def 1;
then (closure_op L).F in rng (closure_op L) by FUNCT_1:def 3;
then (closure_op L).F in the carrier of Image (closure_op L) by
YELLOW_0:def 15;
then (closure_op L).F in the carrier of the RelStr of L by WAYBEL10:18;
then (closure_op L).F in { Y where Y is Element of L : F c= Y } by A26;
then E = "/\"((uparrow F) /\ the carrier of L,BoolePoset X) by A18,A25,
YELLOW_1:20
.= (closure_op L).F by WAYBEL10:def 5;
then
A28: E in (closure_op L).:([#]CompactSublatt (BoolePoset X)) by A27,A19,
FUNCT_1:def 6;
(closure_op L).:([#]CompactSublatt (BoolePoset X)) = [#]
CompactSublatt Image (closure_op L) by WAYBEL_8:25
.= [#]CompactSublatt (the RelStr of L) by WAYBEL10:18
.= the carrier of CompactSublatt (the RelStr of L);
hence thesis by A2,A28,Th5;
end;
end;
theorem Th8:
for L be lower-bounded sup-Semilattice holds InclPoset Ids L is
CLSubFrame of BoolePoset the carrier of L
proof
let L be lower-bounded sup-Semilattice;
now
let x be object;
assume x in Ids L;
then x in the set of all X where X is Ideal of L by WAYBEL_0:def 23;
then ex x9 be Ideal of L st x9 = x;
hence x in bool the carrier of L;
end;
then Ids L is Subset-Family of L by TARSKI:def 3;
then reconsider
InIdL = InclPoset Ids L as non empty full SubRelStr of BoolePoset
the carrier of L by YELLOW_1:5;
A1: for X be directed Subset of InIdL st X <> {} & ex_sup_of X,BoolePoset
the carrier of L holds "\/"(X,BoolePoset the carrier of L) in the carrier of
InIdL
proof
let X be directed Subset of InIdL;
assume that
A2: X <> {} and
ex_sup_of X,BoolePoset the carrier of L;
consider Y be object such that
A3: Y in X by A2,XBOOLE_0:def 1;
X is Subset of BoolePoset the carrier of L by Th3;
then
A4: "\/"(X,BoolePoset the carrier of L) = union X by YELLOW_1:21;
then reconsider uX = union X as Subset of L by WAYBEL_8:26;
reconsider Y as set by TARSKI:1;
Y is Ideal of L by A3,YELLOW_2:41;
then Bottom L in Y by WAYBEL_4:21;
then reconsider uX as non empty Subset of L by A3,TARSKI:def 4;
now
let z be object;
assume z in X;
then z is Ideal of L by YELLOW_2:41;
hence z in bool the carrier of L;
end;
then
A5: X c= bool the carrier of L;
A6: now
let Y,Z be Subset of L;
assume
A7: Y in X & Z in X;
then reconsider Y9 = Y, Z9 = Z as Element of InIdL;
consider V9 be Element of InIdL such that
A8: V9 in X and
A9: Y9 <= V9 & Z9 <= V9 by A7,WAYBEL_0:def 1;
reconsider V = V9 as Subset of L by YELLOW_2:41;
take V;
thus V in X by A8;
Y9 "\/" Z9 <= V9 by A9,YELLOW_0:22;
then
A10: Y9 "\/" Z9 c= V9 by YELLOW_1:3;
Y \/ Z c= Y9 "\/" Z9 by YELLOW_1:6;
hence Y \/ Z c= V by A10;
end;
( for Y be Subset of L st Y in X holds Y is lower)& for Y be Subset
of L st Y in X holds Y is directed by YELLOW_2:41;
then uX is Ideal of L by A5,A6,WAYBEL_0:26,46;
then "\/"(X,BoolePoset the carrier of L) is Element of InIdL by A4,
YELLOW_2:41;
hence thesis;
end;
for X be Subset of InIdL st ex_inf_of X,BoolePoset the carrier of L
holds "/\"(X,BoolePoset the carrier of L) in the carrier of InIdL
proof
let X be Subset of InIdL;
assume ex_inf_of X,BoolePoset the carrier of L;
now
per cases;
suppose
A11: X is non empty;
X is Subset of BoolePoset the carrier of L by Th3;
then
A12: "/\"(X,BoolePoset the carrier of L) = meet X by A11,YELLOW_1:20;
InclPoset Ids L = RelStr (# Ids L, RelIncl Ids L #) by YELLOW_1:def 1;
then "/\"(X,BoolePoset the carrier of L) is Ideal of L by A11,A12,
YELLOW_2:45;
then "/\"(X,BoolePoset the carrier of L) is Element of InIdL by
YELLOW_2:41;
hence thesis;
end;
suppose
A13: X is empty;
"/\"({},BoolePoset the carrier of L) = Top (BoolePoset the
carrier of L ) by YELLOW_0:def 12
.= the carrier of L by YELLOW_1:19;
then "/\"({},BoolePoset the carrier of L) is Ideal of L by Th4;
then "/\"(X,BoolePoset the carrier of L) is Element of InIdL by A13,
YELLOW_2:41;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by A1,WAYBEL_0:def 4,YELLOW_0:def 18;
end;
registration
let L be non empty reflexive transitive RelStr;
cluster principal for Ideal of L;
existence
proof
set x = the Element of L;
take downarrow x;
thus thesis by WAYBEL_0:48;
end;
end;
theorem Th9:
for L be lower-bounded sup-Semilattice for X be non empty
directed Subset of InclPoset Ids L holds sup X = union X
proof
let L be lower-bounded sup-Semilattice;
let X be non empty directed Subset of InclPoset Ids L;
consider z be object such that
A1: z in X by XBOOLE_0:def 1;
X c= the carrier of InclPoset Ids L;
then
A2: X c= Ids L by YELLOW_1:1;
now
let x be object;
assume x in X;
then x in Ids L by A2;
then x in the set of all Y where Y is Ideal of L by WAYBEL_0:def 23;
then ex x1 be Ideal of L st x = x1;
hence x in bool the carrier of L;
end;
then
A3: X c= bool the carrier of L;
now
let Z be Subset of L;
assume Z in X;
then Z in Ids L by A2;
then Z in the set of all Y where Y is Ideal of L by WAYBEL_0:def 23;
then ex Z1 be Ideal of L st Z = Z1;
hence Z is lower;
end;
then reconsider unX = union X as lower Subset of L by A3,WAYBEL_0:26;
reconsider z as set by TARSKI:1;
z in Ids L by A2,A1;
then z in the set of all Y where Y is Ideal of L by WAYBEL_0:def 23;
then ex z1 be Ideal of L st z = z1;
then ex v be object st v in z by XBOOLE_0:def 1;
then reconsider unX as lower non empty Subset of L by A1,TARSKI:def 4;
A4: now
let V,Y be Subset of L;
assume
A5: V in X & Y in X;
then reconsider V1 = V, Y1 = Y as Element of InclPoset Ids L;
consider Z1 be Element of InclPoset Ids L such that
A6: Z1 in X and
A7: V1 <= Z1 & Y1 <= Z1 by A5,WAYBEL_0:def 1;
Z1 in Ids L by A2,A6;
then Z1 in the set of all Y9 where Y9 is Ideal of L by
WAYBEL_0:def 23;
then ex Z2 be Ideal of L st Z1 = Z2;
then reconsider Z = Z1 as Subset of L;
take Z;
thus Z in X by A6;
V c= Z & Y c= Z by A7,YELLOW_1:3;
hence V \/ Y c= Z by XBOOLE_1:8;
end;
now
let Z be Subset of L;
assume Z in X;
then Z in Ids L by A2;
then Z in the set of all Y where Y is Ideal of L by WAYBEL_0:def 23;
then ex Z1 be Ideal of L st Z = Z1;
hence Z is directed;
end;
then reconsider unX as directed lower non empty Subset of L by A3,A4,
WAYBEL_0:46;
reconsider unX as Element of InclPoset Ids L by YELLOW_2:41;
now
let Y be set;
assume
A8: Y in X;
then reconsider Y9 = Y as Element of InclPoset Ids L;
sup X is_>=_than X by YELLOW_0:32;
then Y9 <= sup X by A8,LATTICE3:def 9;
hence Y c= sup X by YELLOW_1:3;
end;
then union X c= sup X by ZFMISC_1:76;
then
A9: unX <= sup X by YELLOW_1:3;
for b be Element of InclPoset Ids L st b in X holds b <= unX
by YELLOW_1:3,ZFMISC_1:74;
then unX is_>=_than X by LATTICE3:def 9;
then sup X <= unX by YELLOW_0:32;
hence thesis by A9,ORDERS_2:2;
end;
theorem Th10: :: PROPOSITION 4.12.(i)
for S be lower-bounded sup-Semilattice holds InclPoset Ids S is algebraic
proof
let S be lower-bounded sup-Semilattice;
set BS = BoolePoset (the carrier of S);
Ids S c= bool the carrier of S
proof
let x be object;
assume x in Ids S;
then x in the set of all X where X is Ideal of S by
WAYBEL_0:def 23;
then ex x1 be Ideal of S st x = x1;
hence thesis;
end;
then reconsider InIdsS = InclPoset Ids S as non empty full SubRelStr of
BoolePoset (the carrier of S) by YELLOW_1:5;
A1: the carrier of InIdsS c= the carrier of BS by YELLOW_0:def 13;
now
let X be Subset of InIdsS;
assume ex_inf_of X,BS;
now
per cases;
suppose
A2: X <> {};
for x being object st x in X holds x in the carrier of BS by A1;
then X c= the carrier of BS;
then "/\"(X,BS) = meet X by A2,YELLOW_1:20
.= "/\"(X,InIdsS) by A2,YELLOW_2:46;
hence "/\"(X,BS) in the carrier of InIdsS;
end;
suppose
A3: X = {};
"/\"({},BS) = Top BS by YELLOW_0:def 12
.= the carrier of S by YELLOW_1:19
.= [#]S
.= "/\"({},InIdsS) by YELLOW_2:47;
hence "/\"(X,BS) in the carrier of InIdsS by A3;
end;
end;
hence "/\"(X,BS) in the carrier of InIdsS;
end;
then
A4: InIdsS is infs-inheriting by YELLOW_0:def 18;
now
let Y be directed Subset of InIdsS;
assume that
A5: Y <> {} and
ex_sup_of Y,BS;
for x being object st x in Y holds x in the carrier of BS by A1;
then Y c= the carrier of BS;
then "\/"(Y,BS) = union Y by YELLOW_1:21
.= "\/"(Y,InIdsS) by A5,Th9;
hence "\/"(Y,BS) in the carrier of InIdsS;
end;
then InIdsS is directed-sups-inheriting by WAYBEL_0:def 4;
hence thesis by A4,Th6;
end;
theorem Th11: :: PROPOSITION 4.12.(i)
for S be lower-bounded sup-Semilattice for x be Element of
InclPoset Ids S holds x is compact iff x is principal Ideal of S
proof
let S be lower-bounded sup-Semilattice;
reconsider InIdS = InclPoset Ids S as CLSubFrame of BoolePoset the carrier
of S by Th8;
let x be Element of InclPoset Ids S;
reconsider x9 = x as Ideal of S by YELLOW_2:41;
thus x is compact implies x is principal Ideal of S
proof
assume x is compact;
then x in the carrier of CompactSublatt InIdS by WAYBEL_8:def 1;
then consider F be Element of BoolePoset the carrier of S such that
A1: F is finite and
A2: x = meet { Y where Y is Element of InIdS : F c= Y } and
A3: F c= x by Th7;
A4: F c= the carrier of S by WAYBEL_8:26;
ex y be Element of S st y in x9 & y is_>=_than x9
proof
reconsider F9 = F as Subset of S by WAYBEL_8:26;
reconsider F9 as Subset of S;
reconsider y = sup F9 as Element of S;
take y;
now
per cases;
suppose
F9 <> {};
hence y in x9 by A1,A3,WAYBEL_0:42;
end;
suppose
F9 = {};
then y = Bottom S by YELLOW_0:def 11;
hence y in x9 by WAYBEL_4:21;
end;
end;
hence y in x9;
now
now
let u be object;
assume
A5: u in F;
then reconsider u9 = u as Element of S by A4;
ex_sup_of F9,S by A1,A5,YELLOW_0:54;
then y is_>=_than F by YELLOW_0:30;
then u9 <= y by A5,LATTICE3:def 9;
hence u in downarrow y by WAYBEL_0:17;
end;
then
A6: F c= downarrow y;
let b be Element of S;
assume
A7: b in x9;
downarrow y is Element of InIdS by YELLOW_2:41;
then downarrow y in { Y where Y is Element of InIdS : F c= Y } by A6;
then b in downarrow y by A2,A7,SETFAM_1:def 1;
hence b <= y by WAYBEL_0:17;
end;
hence thesis by LATTICE3:def 9;
end;
hence thesis by WAYBEL_0:def 21;
end;
thus x is principal Ideal of S implies x is compact
proof
assume x is principal Ideal of S;
then consider y be Element of S such that
A8: y in x9 and
A9: y is_>=_than x9 by WAYBEL_0:def 21;
ex F be Element of BoolePoset the carrier of S st F is finite & F c=
x & x = meet { Y where Y is Element of InIdS : F c= Y }
proof
reconsider F = {y} as Element of BoolePoset the carrier of S by
WAYBEL_8:26;
take F;
thus F is finite;
for v be object st v in F holds v in x by A8,TARSKI:def 1;
hence
A10: F c= x;
A11: now
let z be object;
thus z in x implies for Z be set holds Z in { Y where Y is Element of
InIdS: F c= Y } implies z in Z
proof
assume
A12: z in x;
then reconsider z9 = z as Element of S by YELLOW_2:42;
A13: z9 <= y by A9,A12,LATTICE3:def 9;
let Z be set;
assume Z in { Y where Y is Element of InIdS : F c= Y };
then consider Z1 be Element of InIdS such that
A14: Z1 = Z & F c= Z1;
Z1 is Ideal of S & y in F by TARSKI:def 1,YELLOW_2:41;
hence thesis by A14,A13,WAYBEL_0:def 19;
end;
thus ( for Z be set holds Z in { Y where Y is Element of InIdS : F c=
Y } implies z in Z ) implies z in x
proof
assume
A15: for Z be set holds Z in { Y where Y is Element of InIdS : F
c= Y } implies z in Z;
x in { Y where Y is Element of InIdS : F c= Y } by A10;
hence thesis by A15;
end;
end;
[#]S is Element of InIdS by YELLOW_2:41;
then [#]S in { Y where Y is Element of InIdS : F c= Y };
hence thesis by A11,SETFAM_1:def 1;
end;
then x in the carrier of CompactSublatt InIdS by Th7;
hence thesis by WAYBEL_8:def 1;
end;
end;
theorem Th12:
for S be lower-bounded sup-Semilattice for x be Element of
InclPoset Ids S holds x is compact iff ex a be Element of S st x = downarrow a
proof
let S be lower-bounded sup-Semilattice;
let x be Element of InclPoset Ids S;
thus x is compact implies ex a be Element of S st x = downarrow a
proof
assume x is compact;
then x is principal Ideal of S by Th11;
hence thesis by WAYBEL_0:48;
end;
thus (ex a be Element of S st x = downarrow a) implies x is compact
by WAYBEL_0:48,Th11;
end;
theorem :: PROPOSITION 4.12.(ii)
for L be lower-bounded sup-Semilattice for f be Function of L,
CompactSublatt InclPoset Ids L st for x be Element of L holds f.x = downarrow x
holds f is isomorphic
proof
let L be lower-bounded sup-Semilattice;
let f be Function of L, CompactSublatt InclPoset Ids L;
assume
A1: for x be Element of L holds f.x = downarrow x;
A2: for x,y be Element of L holds x <= y iff f.x <= f.y
proof
let x,y be Element of L;
reconsider fx = f.x as Element of InclPoset Ids L by YELLOW_0:58;
reconsider fy = f.y as Element of InclPoset Ids L by YELLOW_0:58;
thus x <= y implies f.x <= f.y
proof
assume x <= y;
then downarrow x c= downarrow y by WAYBEL_0:21;
then f.x c= downarrow y by A1;
then fx c= fy by A1;
then fx <= fy by YELLOW_1:3;
hence thesis by YELLOW_0:60;
end;
x <= x;
then
A3: x in downarrow x by WAYBEL_0:17;
thus f.x <= f.y implies x <= y
proof
assume f.x <= f.y;
then fx <= fy by YELLOW_0:59;
then fx c= fy by YELLOW_1:3;
then f.x c= downarrow y by A1;
then downarrow x c= downarrow y by A1;
hence thesis by A3,WAYBEL_0:17;
end;
end;
now
let y be object;
assume
A4: y in the carrier of CompactSublatt InclPoset Ids L;
the carrier of CompactSublatt InclPoset Ids L c= the carrier of
InclPoset Ids L by YELLOW_0:def 13;
then reconsider y9 = y as Element of InclPoset Ids L by A4;
y9 is compact by A4,WAYBEL_8:def 1;
then consider x be Element of L such that
A5: y9 = downarrow x by Th12;
reconsider x9 = x as object;
take x9;
thus x9 in the carrier of L;
thus y = f.x9 by A1,A5;
end;
then
A6: rng f = the carrier of CompactSublatt InclPoset Ids L by FUNCT_2:10;
now
let x,y be Element of L;
assume f.x = f.y;
then f.x = downarrow y by A1;
then downarrow x = downarrow y by A1;
hence x = y by WAYBEL_0:19;
end;
then f is one-to-one by WAYBEL_1:def 1;
hence thesis by A6,A2,WAYBEL_0:66;
end;
theorem :: PROPOSITION 4.12.(iii)
for S be lower-bounded LATTICE holds InclPoset Ids S is arithmetic
proof
let S be lower-bounded LATTICE;
now
let x,y be Element of CompactSublatt InclPoset Ids S;
reconsider x1 = x, y1 = y as Element of InclPoset Ids S by YELLOW_0:58;
x1 is compact by WAYBEL_8:def 1;
then consider a be Element of S such that
A1: x1 = downarrow a by Th12;
y1 is compact by WAYBEL_8:def 1;
then consider b be Element of S such that
A2: y1 = downarrow b by Th12;
Bottom S <= b by YELLOW_0:44;
then
A3: Bottom S in downarrow b by WAYBEL_0:17;
Bottom S <= a by YELLOW_0:44;
then Bottom S in downarrow a by WAYBEL_0:17;
then reconsider
xy = downarrow a /\ downarrow b as non empty Subset of S by A3,
XBOOLE_0:def 4;
reconsider xy as lower non empty Subset of S by WAYBEL_0:27;
reconsider xy as lower directed non empty Subset of S by WAYBEL_0:44;
xy is Ideal of S;
then downarrow a /\ downarrow b in the set of all X where X is Ideal of S;
then downarrow a /\ downarrow b in Ids S by WAYBEL_0:def 23;
then x1 "/\" y1 = downarrow a /\ downarrow b by A1,A2,YELLOW_1:9;
then reconsider
z1 = downarrow a /\ downarrow b as Element of InclPoset Ids S;
z1 c= y1 by A2,XBOOLE_1:17;
then
A4: z1 <= y1 by YELLOW_1:3;
A5: downarrow (a "/\" b) c= downarrow a /\ downarrow b
proof
let v be object;
assume
A6: v in downarrow (a "/\" b);
then reconsider v1 = v as Element of S;
A7: v1 <= a "/\" b by A6,WAYBEL_0:17;
a "/\" b <= b by YELLOW_0:23;
then v1 <= b by A7,ORDERS_2:3;
then
A8: v in downarrow b by WAYBEL_0:17;
a "/\" b <= a by YELLOW_0:23;
then v1 <= a by A7,ORDERS_2:3;
then v in downarrow a by WAYBEL_0:17;
hence thesis by A8,XBOOLE_0:def 4;
end;
downarrow a /\ downarrow b c= downarrow (a "/\" b)
proof
let v be object;
assume
A9: v in downarrow a /\ downarrow b;
then reconsider v1 = v as Element of S;
v in downarrow b by A9,XBOOLE_0:def 4;
then
A10: v1 <= b by WAYBEL_0:17;
v in downarrow a by A9,XBOOLE_0:def 4;
then v1 <= a by WAYBEL_0:17;
then v1 <= a "/\" b by A10,YELLOW_0:23;
hence thesis by WAYBEL_0:17;
end;
then z1 = downarrow (a "/\" b) by A5,XBOOLE_0:def 10;
then z1 is compact by Th12;
then reconsider z = z1 as Element of CompactSublatt InclPoset Ids S by
WAYBEL_8:def 1;
take z;
z1 c= x1 by A1,XBOOLE_1:17;
then z1 <= x1 by YELLOW_1:3;
hence z <= x & z <= y by A4,YELLOW_0:60;
let v be Element of CompactSublatt InclPoset Ids S;
reconsider v1 = v as Element of InclPoset Ids S by YELLOW_0:58;
assume that
A11: v <= x and
A12: v <= y;
v1 <= y1 by A12,YELLOW_0:59;
then
A13: v1 c= y1 by YELLOW_1:3;
v1 <= x1 by A11,YELLOW_0:59;
then v1 c= x1 by YELLOW_1:3;
then v1 c= z1 by A1,A2,A13,XBOOLE_1:19;
then v1 <= z1 by YELLOW_1:3;
hence v <= z by YELLOW_0:60;
end;
then
A14: CompactSublatt InclPoset Ids S is with_infima by LATTICE3:def 11;
InclPoset Ids S is algebraic by Th10;
hence thesis by A14,WAYBEL_8:19;
end;
theorem Th15: :: PROPOSITION 4.12.(iv)
for L be lower-bounded sup-Semilattice holds CompactSublatt L is
lower-bounded sup-Semilattice
proof
let L be lower-bounded sup-Semilattice;
ex x being Element of CompactSublatt L st x is_<=_than the carrier of
CompactSublatt L
proof
reconsider x = Bottom L as Element of CompactSublatt L by WAYBEL_8:3;
take x;
now
let a be Element of CompactSublatt L;
A1: the carrier of CompactSublatt L c= the carrier of L by YELLOW_0:def 13;
assume a in the carrier of CompactSublatt L;
reconsider a9 = a as Element of L by A1;
Bottom L <= a9 by YELLOW_0:44;
hence x <= a by YELLOW_0:60;
end;
hence thesis by LATTICE3:def 8;
end;
hence thesis by YELLOW_0:def 4;
end;
theorem Th16: :: PROPOSITION 4.12.(v)
for L be algebraic lower-bounded sup-Semilattice for f be
Function of L,InclPoset Ids CompactSublatt L st for x be Element of L holds f.x
= compactbelow x holds f is isomorphic
proof
let L be algebraic lower-bounded sup-Semilattice;
let f be Function of L,InclPoset Ids CompactSublatt L;
assume
A1: for x be Element of L holds f.x = compactbelow x;
A2: now
let x,y be Element of L;
thus x <= y implies f.x <= f.y
proof
assume x <= y;
then compactbelow x c= compactbelow y by Th1;
then f.x c= compactbelow y by A1;
then f.x c= f.y by A1;
hence thesis by YELLOW_1:3;
end;
thus f.x <= f.y implies x <= y
proof
assume f.x <= f.y;
then f.x c= f.y by YELLOW_1:3;
then f.x c= compactbelow y by A1;
then
A3: compactbelow x c= compactbelow y by A1;
ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L by YELLOW_0:17;
then sup compactbelow x <= sup compactbelow y by A3,YELLOW_0:34;
then sup compactbelow x <= y by WAYBEL_8:def 3;
hence thesis by WAYBEL_8:def 3;
end;
end;
now
let y be object;
assume y in the carrier of InclPoset Ids CompactSublatt L;
then reconsider y9 = y as Ideal of CompactSublatt L by YELLOW_2:41;
reconsider y1 = y9 as non empty Subset of L by Th3;
reconsider y1 as non empty directed Subset of L by YELLOW_2:7;
set x = sup y1;
reconsider x9 = x as object;
take x9;
thus x9 in the carrier of L;
A4: compactbelow x c= y9
proof
let d be object;
assume d in compactbelow x;
then d in {v where v is Element of L: x >= v & v is compact} by
WAYBEL_8:def 2;
then consider d1 be Element of L such that
A5: d1 = d and
A6: d1 <= x and
A7: d1 is compact;
reconsider d9 = d1 as Element of CompactSublatt L by A7,WAYBEL_8:def 1;
d1 << d1 by A7,WAYBEL_3:def 2;
then consider z be Element of L such that
A8: z in y1 and
A9: d1 <= z by A6,WAYBEL_3:def 1;
reconsider z9 = z as Element of CompactSublatt L by A8;
d9 <= z9 by A9,YELLOW_0:60;
hence thesis by A5,A8,WAYBEL_0:def 19;
end;
y9 c= compactbelow x
proof
let d be object;
assume
A10: d in y9;
then reconsider d1 = d as Element of CompactSublatt L;
reconsider d9 = d1 as Element of L by YELLOW_0:58;
y9 is_<=_than sup y1 by YELLOW_0:32;
then d9 is compact & d9 <= x by A10,LATTICE3:def 9,WAYBEL_8:def 1;
hence thesis by WAYBEL_8:4;
end;
hence y = compactbelow x by A4,XBOOLE_0:def 10
.= f.x9 by A1;
end;
then
A11: rng f = the carrier of InclPoset Ids CompactSublatt L by FUNCT_2:10;
now
let x,y be Element of L;
assume f.x = f.y;
then f.x = compactbelow y by A1;
then compactbelow x = compactbelow y by A1;
then sup compactbelow x = y by WAYBEL_8:def 3;
hence x = y by WAYBEL_8:def 3;
end;
then f is one-to-one by WAYBEL_1:def 1;
hence thesis by A11,A2,WAYBEL_0:66;
end;
theorem :: PROPOSITION 4.12.(vi)
for L be algebraic lower-bounded sup-Semilattice for x be Element of L
holds compactbelow x is principal Ideal of CompactSublatt L iff x is compact
proof
let L be algebraic lower-bounded sup-Semilattice;
let x be Element of L;
thus compactbelow x is principal Ideal of CompactSublatt L implies x is
compact
proof
assume compactbelow x is principal Ideal of CompactSublatt L;
then consider y be Element of CompactSublatt L such that
A1: y in compactbelow x and
A2: y is_>=_than compactbelow x by WAYBEL_0:def 21;
reconsider y9 = y as Element of L by YELLOW_0:58;
compactbelow x is Subset of CompactSublatt L by Th2;
then y9 is_>=_than compactbelow x by A2,YELLOW_0:62;
then y9 >= sup compactbelow x by YELLOW_0:32;
then
A3: x <= y9 by WAYBEL_8:def 3;
y9 <= x & y9 is compact by A1,WAYBEL_8:4;
hence thesis by A3,ORDERS_2:2;
end;
thus x is compact implies compactbelow x is principal Ideal of
CompactSublatt L
proof
reconsider I = compactbelow x as non empty Subset of CompactSublatt L by
Th2;
assume
A4: x is compact;
then reconsider x9 = x as Element of CompactSublatt L by WAYBEL_8:def 1;
compactbelow x is non empty directed Subset of L by WAYBEL_8:def 4;
then reconsider I as non empty directed Subset of CompactSublatt L by
WAYBEL10:23;
now
let y,z be Element of CompactSublatt L;
reconsider y9 = y, z9 = z as Element of L by YELLOW_0:58;
assume y in I & z <= y;
then y9 <= x & z9 <= y9 by WAYBEL_8:4,YELLOW_0:59;
then
A5: z9 <= x by ORDERS_2:3;
z9 is compact by WAYBEL_8:def 1;
hence z in I by A5,WAYBEL_8:4;
end;
then reconsider I as Ideal of CompactSublatt L by WAYBEL_0:def 19;
sup compactbelow x is_>=_than compactbelow x by YELLOW_0:32;
then x is_>=_than I by WAYBEL_8:def 3;
then
A6: x9 is_>=_than I by YELLOW_0:61;
x <= x;
then x9 in I by A4,WAYBEL_8:4;
hence thesis by A6,WAYBEL_0:def 21;
end;
end;
begin :: Maps
theorem Th18:
for L1,L2 be non empty RelStr for X be Subset of L1, x be
Element of L1 for f be Function of L1,L2 st f is isomorphic holds x is_<=_than
X iff f.x is_<=_than f.:X
proof
let L1,L2 be non empty RelStr;
let X be Subset of L1;
let x be Element of L1;
let f be Function of L1,L2;
assume
A1: f is isomorphic;
hence x is_<=_than X implies f.x is_<=_than f.:X by YELLOW_2:13;
thus f.x is_<=_than f.:X implies x is_<=_than X
proof
reconsider g = f" as Function of L2,L1 by A1,WAYBEL_0:67;
assume
A2: f.x is_<=_than f.:X;
g is isomorphic by A1,WAYBEL_0:68;
then
A3: g.(f.x) is_<=_than g.:(f.:X) by A2,YELLOW_2:13;
A4: f"(f.:X) c= X by A1,FUNCT_1:82;
X c= the carrier of L1;
then X c= dom f by FUNCT_2:def 1;
then
A5: X c= f"(f.:X) by FUNCT_1:76;
x in the carrier of L1;
then
A6: x in dom f by FUNCT_2:def 1;
g.:(f.:X) = f"(f.:X) by A1,FUNCT_1:85
.= X by A4,A5,XBOOLE_0:def 10;
hence thesis by A1,A6,A3,FUNCT_1:34;
end;
end;
theorem Th19:
for L1,L2 be non empty RelStr for X be Subset of L1, x be
Element of L1 for f be Function of L1,L2 st f is isomorphic holds x is_>=_than
X iff f.x is_>=_than f.:X
proof
let L1,L2 be non empty RelStr;
let X be Subset of L1;
let x be Element of L1;
let f be Function of L1,L2;
assume
A1: f is isomorphic;
hence x is_>=_than X implies f.x is_>=_than f.:X by YELLOW_2:14;
thus f.x is_>=_than f.:X implies x is_>=_than X
proof
reconsider g = f" as Function of L2,L1 by A1,WAYBEL_0:67;
assume
A2: f.x is_>=_than f.:X;
g is isomorphic by A1,WAYBEL_0:68;
then
A3: g.(f.x) is_>=_than g.:(f.:X) by A2,YELLOW_2:14;
A4: f"(f.:X) c= X by A1,FUNCT_1:82;
X c= the carrier of L1;
then X c= dom f by FUNCT_2:def 1;
then
A5: X c= f"(f.:X) by FUNCT_1:76;
x in the carrier of L1;
then
A6: x in dom f by FUNCT_2:def 1;
g.:(f.:X) = f"(f.:X) by A1,FUNCT_1:85
.= X by A4,A5,XBOOLE_0:def 10;
hence thesis by A1,A6,A3,FUNCT_1:34;
end;
end;
theorem Th20:
for L1,L2 be non empty antisymmetric RelStr for f be Function of
L1,L2 holds f is isomorphic implies f is infs-preserving sups-preserving
proof
let L1,L2 be non empty antisymmetric RelStr;
let f be Function of L1,L2;
assume
A1: f is isomorphic;
then
A2: rng f = the carrier of L2 by WAYBEL_0:66;
now
let X be Subset of L1;
now
assume
A3: ex_inf_of X,L1;
then consider a be Element of L1 such that
A4: X is_>=_than a and
A5: for b be Element of L1 st X is_>=_than b holds a >= b by YELLOW_0:16;
A6: now
let c be Element of L2;
consider e be object such that
A7: e in dom f and
A8: c = f.e by A2,FUNCT_1:def 3;
reconsider e as Element of L1 by A7;
assume f.:X is_>=_than c;
then X is_>=_than e by A1,A8,Th18;
then a >= e by A5;
hence f.a >= c by A1,A8,WAYBEL_0:66;
end;
f.:X is_>=_than f.a by A1,A4,Th18;
hence ex_inf_of f.:X,L2 by A6,YELLOW_0:16;
A9: now
let b be Element of L2;
consider v be object such that
A10: v in dom f and
A11: b = f.v by A2,FUNCT_1:def 3;
reconsider v as Element of L1 by A10;
assume b is_<=_than f.:X;
then v is_<=_than X by A1,A11,Th18;
then inf X >= v by A3,YELLOW_0:31;
hence f.inf X >= b by A1,A11,WAYBEL_0:66;
end;
inf X is_<=_than X by A3,YELLOW_0:31;
then f.inf X is_<=_than f.:X by A1,Th18;
hence inf (f.:X) = f.inf X by A9,YELLOW_0:31;
end;
hence f preserves_inf_of X by WAYBEL_0:def 30;
end;
hence f is infs-preserving by WAYBEL_0:def 32;
now
let X be Subset of L1;
now
assume
A12: ex_sup_of X,L1;
then consider a be Element of L1 such that
A13: X is_<=_than a and
A14: for b be Element of L1 st X is_<=_than b holds a <= b by YELLOW_0:15;
A15: now
let c be Element of L2;
consider e be object such that
A16: e in dom f and
A17: c = f.e by A2,FUNCT_1:def 3;
reconsider e as Element of L1 by A16;
assume f.:X is_<=_than c;
then X is_<=_than e by A1,A17,Th19;
then a <= e by A14;
hence f.a <= c by A1,A17,WAYBEL_0:66;
end;
f.:X is_<=_than f.a by A1,A13,Th19;
hence ex_sup_of f.:X,L2 by A15,YELLOW_0:15;
A18: now
let b be Element of L2;
consider v be object such that
A19: v in dom f and
A20: b = f.v by A2,FUNCT_1:def 3;
reconsider v as Element of L1 by A19;
assume b is_>=_than f.:X;
then v is_>=_than X by A1,A20,Th19;
then sup X <= v by A12,YELLOW_0:30;
hence f.sup X <= b by A1,A20,WAYBEL_0:66;
end;
sup X is_>=_than X by A12,YELLOW_0:30;
then f.sup X is_>=_than f.:X by A1,Th19;
hence sup (f.:X) = f.sup X by A18,YELLOW_0:30;
end;
hence f preserves_sup_of X by WAYBEL_0:def 31;
end;
hence thesis by WAYBEL_0:def 33;
end;
registration
let L1,L2 be non empty antisymmetric RelStr;
cluster isomorphic -> infs-preserving sups-preserving for Function of L1,L2;
coherence by Th20;
end;
theorem Th21:
for L1,L2,L3 be non empty transitive antisymmetric RelStr for f
be Function of L1,L2 st f is infs-preserving holds L2 is full infs-inheriting
SubRelStr of L3 & L3 is complete implies ex g be Function of L1,L3 st f = g & g
is infs-preserving
proof
let L1,L2,L3 be non empty transitive antisymmetric RelStr;
let f be Function of L1,L2;
assume that
A1: f is infs-preserving and
A2: L2 is full infs-inheriting SubRelStr of L3 and
A3: L3 is complete;
the carrier of L2 c= the carrier of L3 by A2,YELLOW_0:def 13;
then reconsider g = f as Function of L1,L3 by FUNCT_2:7;
take g;
thus f = g;
now
let X be Subset of L1;
now
A4: f preserves_inf_of X by A1,WAYBEL_0:def 32;
assume
A5: ex_inf_of X,L1;
thus
A6: ex_inf_of g.:X,L3 by A3,YELLOW_0:17;
then "/\"(f.:X,L3) in the carrier of L2 by A2,YELLOW_0:def 18;
hence inf (g.:X) = inf (f.:X) by A2,A6,YELLOW_0:63
.= g.inf X by A5,A4,WAYBEL_0:def 30;
end;
hence g preserves_inf_of X by WAYBEL_0:def 30;
end;
hence thesis by WAYBEL_0:def 32;
end;
theorem Th22:
for L1,L2,L3 be non empty transitive antisymmetric RelStr for f
be Function of L1,L2 st f is monotone directed-sups-preserving holds L2 is full
directed-sups-inheriting SubRelStr of L3 & L3 is complete implies ex g be
Function of L1,L3 st f = g & g is directed-sups-preserving
proof
let L1,L2,L3 be non empty transitive antisymmetric RelStr;
let f be Function of L1,L2;
assume that
A1: f is monotone directed-sups-preserving and
A2: L2 is full directed-sups-inheriting SubRelStr of L3 and
A3: L3 is complete;
the carrier of L2 c= the carrier of L3 by A2,YELLOW_0:def 13;
then reconsider g = f as Function of L1,L3 by FUNCT_2:7;
take g;
thus f = g;
now
let X be Subset of L1;
assume
A4: X is non empty directed;
then consider d be object such that
A5: d in X by XBOOLE_0:def 1;
d in the carrier of L1 by A5;
then d in dom f by FUNCT_2:def 1;
then f.d in f.:X by A5,FUNCT_1:def 6;
then
A6: f.:X is non empty directed by A1,A4,YELLOW_2:15;
now
A7: f preserves_sup_of X by A1,A4,WAYBEL_0:def 37;
assume
A8: ex_sup_of X,L1;
thus ex_sup_of g.:X,L3 by A3,YELLOW_0:17;
hence sup (g.:X) = sup (f.:X) by A2,A6,WAYBEL_0:7
.= g.sup X by A8,A7,WAYBEL_0:def 31;
end;
hence g preserves_sup_of X by WAYBEL_0:def 31;
end;
hence thesis by WAYBEL_0:def 37;
end;
theorem Th23:
for L be lower-bounded sup-Semilattice holds InclPoset Ids
CompactSublatt L is CLSubFrame of BoolePoset the carrier of CompactSublatt L
proof
let L be lower-bounded sup-Semilattice;
CompactSublatt L is lower-bounded sup-Semilattice by Th15;
hence thesis by Th8;
end;
theorem Th24: :: COROLLARY 4.13.
for L be algebraic lower-bounded LATTICE ex g be Function of L,
BoolePoset the carrier of CompactSublatt L st g is infs-preserving & g is
directed-sups-preserving & g is one-to-one & for x be Element of L holds g.x =
compactbelow x
proof
let L be algebraic lower-bounded LATTICE;
deffunc F(Element of L) = compactbelow $1;
A1: for y be Element of L holds F(y) is Element of InclPoset Ids
CompactSublatt L
proof
let y be Element of L;
reconsider comy = compactbelow y as non empty directed Subset of L by
WAYBEL_8:def 4;
reconsider comy as non empty Subset of CompactSublatt L by Th2;
reconsider comy as non empty directed Subset of CompactSublatt L by
WAYBEL10:23;
now
let x1,z1 be Element of CompactSublatt L;
reconsider x2 = x1, z2 = z1 as Element of L by YELLOW_0:58;
assume x1 in comy & z1 <= x1;
then x2 <= y & z2 <= x2 by WAYBEL_8:4,YELLOW_0:59;
then
A2: z2 <= y by ORDERS_2:3;
z2 is compact by WAYBEL_8:def 1;
hence z1 in comy by A2,WAYBEL_8:4;
end;
then comy is lower by WAYBEL_0:def 19;
hence thesis by YELLOW_2:41;
end;
consider g1 be Function of L, InclPoset Ids CompactSublatt L such that
A3: for y be Element of L holds g1.y = F(y) from FUNCT_2:sch 9(A1);
now
let k be object;
assume k in the carrier of InclPoset Ids CompactSublatt L;
then k is Ideal of CompactSublatt L by YELLOW_2:41;
then k is Element of BoolePoset the carrier of CompactSublatt L by
WAYBEL_8:26;
hence k in the carrier of BoolePoset the carrier of CompactSublatt L;
end;
then the carrier of InclPoset Ids CompactSublatt L c= the carrier of
BoolePoset the carrier of CompactSublatt L;
then reconsider
g = g1 as Function of L,BoolePoset the carrier of CompactSublatt
L by FUNCT_2:7;
take g;
A4: g1 is isomorphic by A3,Th16;
A5: InclPoset Ids CompactSublatt L is full infs-inheriting
directed-sups-inheriting SubRelStr of BoolePoset the carrier of CompactSublatt
L by Th23;
then ex g2 be Function of L,BoolePoset the carrier of CompactSublatt L st g1
= g2 & g2 is infs-preserving by A4,Th21;
hence g is infs-preserving;
ex g3 be Function of L,BoolePoset the carrier of CompactSublatt L st g1
= g3 & g3 is directed-sups-preserving by A4,A5,Th22;
hence g is directed-sups-preserving;
thus g is one-to-one by A4;
let x be Element of L;
thus thesis by A3;
end;
theorem :: PROPOSITION 4.14.
for I be non empty set for J be RelStr-yielding non-Empty
reflexive-yielding ManySortedSet of I st for i be Element of I holds J.i is
algebraic lower-bounded LATTICE holds product J is algebraic lower-bounded
LATTICE
proof
let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
assume
A1: for i be Element of I holds J.i is algebraic lower-bounded LATTICE;
then
A2: for i be Element of I holds J.i is complete LATTICE;
then reconsider L = product J as non empty lower-bounded LATTICE by
WAYBEL_3:31;
for i be Element of I holds J.i is antisymmetric by A1;
then
A3: product J is antisymmetric by WAYBEL_3:30;
now
let x be Element of product J;
A4: for i be Element of I holds sup compactbelow (x.i) = (sup compactbelow x).i
proof
let i be Element of I;
A5: compactbelow (x.i) c= pi(compactbelow x,i)
proof
deffunc G(Element of I) = Bottom (J.$1);
defpred C[set] means $1 = i;
let v be object;
assume v in compactbelow (x.i);
then v in {y where y is Element of J.i: x.i >= y & y is compact} by
WAYBEL_8:def 2;
then consider v1 be Element of J.i such that
A6: v1 = v and
A7: x.i >= v1 and
A8: v1 is compact;
deffunc F(set) = v1;
consider f be Function such that
A9: dom f = I and
A10: for j be Element of I holds ( C[j] implies f.j = F(j) ) & (
not C[j] implies f.j = G(j)) from PARTFUN1:sch 4;
A11: f.i = v1 by A10;
now
let k be Element of I;
now
per cases;
suppose
k = i;
hence f.k is Element of J.k by A10;
end;
suppose
k <> i;
then f.k = Bottom (J.k) by A10;
hence f.k is Element of J.k;
end;
end;
hence f.k is Element of J.k;
end;
then reconsider f as Element of product J by A9,WAYBEL_3:27;
now
let k be Element of I;
A12: J.k is algebraic lower-bounded LATTICE by A1;
now
per cases;
suppose
k = i;
hence f.k <= x.k by A7,A10;
end;
suppose
k <> i;
then f.k = Bottom (J.k) by A10;
hence f.k <= x.k by A12,YELLOW_0:44;
end;
end;
hence f.k <= x.k;
end;
then
A13: f <= x by WAYBEL_3:28;
A14: now
let k be Element of I;
A15: J.k is algebraic lower-bounded LATTICE by A1;
now
per cases;
suppose
A16: k = i;
then f.k = v1 by A10;
hence f.k << f.k by A8,A16,WAYBEL_3:def 2;
end;
suppose
k <> i;
then f.k = Bottom (J.k) by A10;
then f.k is compact by A15,WAYBEL_3:15;
hence f.k << f.k by WAYBEL_3:def 2;
end;
end;
hence f.k << f.k;
end;
ex K be finite Subset of I st for k be Element of I st not k in K
holds f.k = Bottom (J.k)
proof
take K = {i};
let k be Element of I;
assume not k in K;
then k <> i by TARSKI:def 1;
hence thesis by A10;
end;
then f << f by A2,A14,WAYBEL_3:33;
then f is compact by WAYBEL_3:def 2;
then f in compactbelow x by A13,WAYBEL_8:4;
hence thesis by A6,A11,CARD_3:def 6;
end;
pi(compactbelow x,i) c= compactbelow (x.i)
proof
let v be object;
assume v in pi(compactbelow x,i);
then consider f be Function such that
A17: f in compactbelow x and
A18: v = f.i by CARD_3:def 6;
f in {y where y is Element of product J: x >= y & y is compact}
by A17,WAYBEL_8:def 2;
then consider f1 be Element of product J such that
A19: f1 = f and
A20: x >= f1 and
A21: f1 is compact;
f1 << f1 by A21,WAYBEL_3:def 2;
then f1.i << f1.i by A2,WAYBEL_3:33;
then
A22: f1.i is compact by WAYBEL_3:def 2;
f1.i <= x.i by A20,WAYBEL_3:28;
hence thesis by A18,A19,A22,WAYBEL_8:4;
end;
hence sup compactbelow (x.i) = sup pi(compactbelow x,i) by A5,
XBOOLE_0:def 10
.= (sup compactbelow x).i by A2,WAYBEL_3:32;
end;
now
let i be Element of I;
J.i is satisfying_axiom_K by A1;
then x.i = sup compactbelow (x.i) by WAYBEL_8:def 3;
hence (sup compactbelow x).i <= x.i by A4;
end;
then
A23: sup compactbelow x <= x by WAYBEL_3:28;
now
let i be Element of I;
J.i is satisfying_axiom_K by A1;
then x.i = sup compactbelow (x.i) by WAYBEL_8:def 3;
hence x.i <= (sup compactbelow x).i by A4;
end;
then x <= sup compactbelow x by WAYBEL_3:28;
hence x = sup compactbelow x by A3,A23,YELLOW_0:def 3;
end;
then
A24: product J is satisfying_axiom_K by WAYBEL_8:def 3;
A25: for x be Element of L holds compactbelow x is non empty directed
proof
let x be Element of L;
now
let c,d be Element of L;
assume that
A26: c in compactbelow x and
A27: d in compactbelow x;
d is compact by A27,WAYBEL_8:4;
then d <= c "\/" d & d << d by WAYBEL_3:def 2,YELLOW_0:22;
then
A28: d << c "\/" d by WAYBEL_3:2;
c is compact by A26,WAYBEL_8:4;
then c <= c "\/" d & c << c by WAYBEL_3:def 2,YELLOW_0:22;
then c << c "\/" d by WAYBEL_3:2;
then c "\/" d << c "\/" d by A28,WAYBEL_3:3;
then
A29: c "\/" d is compact by WAYBEL_3:def 2;
take e = c "\/" d;
c <= x & d <= x by A26,A27,WAYBEL_8:4;
then c "\/" d <= x by YELLOW_0:22;
hence e in compactbelow x by A29,WAYBEL_8:4;
thus c <= e & d <= e by YELLOW_0:22;
end;
hence thesis by WAYBEL_0:def 1;
end;
L is up-complete by A2,WAYBEL_3:31;
hence thesis by A25,A24,WAYBEL_8:def 4;
end;
Lm1: for L be lower-bounded LATTICE holds L is algebraic implies ex X be non
empty set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S is
directed-sups-inheriting & L,S are_isomorphic
proof
let L be lower-bounded LATTICE;
assume
A1: L is algebraic;
then reconsider L9 = L as algebraic lower-bounded LATTICE;
take X = the carrier of CompactSublatt L;
consider g be Function of L,BoolePoset the carrier of CompactSublatt L such
that
A2: g is infs-preserving and
A3: g is directed-sups-preserving and
A4: g is one-to-one and
A5: for x be Element of L holds g.x = compactbelow x by A1,Th24;
reconsider S = Image g as non empty full SubRelStr of BoolePoset X;
take S;
A6: L9 is complete;
hence S is infs-inheriting by A2,YELLOW_2:33;
A7: rng g = the carrier of S by YELLOW_0:def 15;
dom g = the carrier of L by FUNCT_2:def 1;
then reconsider g1 = g as Function of L,S by A7,FUNCT_2:1;
now
let x,y be Element of L;
thus x <= y implies g1.x <= g1.y
proof
assume x <= y;
then compactbelow x c= compactbelow y by Th1;
then g.x c= compactbelow y by A5;
then g.x c= g.y by A5;
then g.x <= g.y by YELLOW_1:2;
hence thesis by YELLOW_0:60;
end;
thus g1.x <= g1.y implies x <= y
proof
assume g1.x <= g1.y;
then g.x <= g.y by YELLOW_0:59;
then g.x c= g.y by YELLOW_1:2;
then g.x c= compactbelow y by A5;
then
A8: compactbelow x c= compactbelow y by A5;
ex_sup_of compactbelow x,L & ex_sup_of compactbelow y,L by A6,YELLOW_0:17
;
then sup compactbelow x <= sup compactbelow y by A8,YELLOW_0:34;
then x <= sup compactbelow y by A1,WAYBEL_8:def 3;
hence thesis by A1,WAYBEL_8:def 3;
end;
end;
then
A9: g1 is isomorphic by A4,A7,WAYBEL_0:66;
then reconsider f1 = g1" as Function of S,L by WAYBEL_0:67;
A10: f1 is isomorphic by A9,WAYBEL_0:68;
now
let Y be directed Subset of S;
assume that
A11: Y <> {} and
ex_sup_of Y,BoolePoset X;
now
let X2 be finite Subset of f1.:Y;
A12: g1"(g1.:X2) c= X2 by A4,FUNCT_1:82;
now
let v be object;
assume v in g1.:X2;
then ex u be object st u in dom g1 & u in X2 & v = g1.u
by FUNCT_1:def 6;
then v in g1.:(f1.:Y) by FUNCT_1:def 6;
then v in g1.:(g1"Y) by A4,FUNCT_1:85;
hence v in Y by A7,FUNCT_1:77;
end;
then reconsider Y1 = g1.:X2 as finite Subset of Y by TARSKI:def 3;
consider y1 be Element of S such that
A13: y1 in Y and
A14: y1 is_>=_than Y1 by A11,WAYBEL_0:1;
take f1y1 = f1.y1;
y1 in the carrier of S;
then y1 in dom f1 by FUNCT_2:def 1;
hence f1y1 in f1.:Y by A13,FUNCT_1:def 6;
X2 c= the carrier of L by XBOOLE_1:1;
then X2 c= dom g1 by FUNCT_2:def 1;
then
A15: X2 c= g1"(g1.:X2) by FUNCT_1:76;
f1.:Y1 = g1"(g1.:X2) by A4,FUNCT_1:85
.= X2 by A15,A12,XBOOLE_0:def 10;
hence f1y1 is_>=_than X2 by A10,A14,Th19;
end;
then reconsider X1 = f1.:Y as non empty directed Subset of L by WAYBEL_0:1;
sup X1 in the carrier of L;
then sup X1 in dom g by FUNCT_2:def 1;
then
A16: g.sup X1 in rng g by FUNCT_1:def 3;
ex_sup_of X1,L & g preserves_sup_of X1 by A6,A3,WAYBEL_0:def 37,YELLOW_0:17
;
then
A17: sup (g.:X1) in rng g by A16,WAYBEL_0:def 31;
g.:X1 = g.:(g1"Y) by A4,FUNCT_1:85
.= Y by A7,FUNCT_1:77;
hence "\/"(Y,BoolePoset X) in the carrier of S by A17,YELLOW_0:def 15;
end;
hence S is directed-sups-inheriting by WAYBEL_0:def 4;
thus thesis by A9,WAYBEL_1:def 8;
end;
theorem Th26:
for L1,L2 be non empty RelStr st the RelStr of L1 = the RelStr
of L2 holds L1,L2 are_isomorphic
proof
let L1,L2 be non empty RelStr;
assume
A1: the RelStr of L1 = the RelStr of L2;
ex f be Function of L1,L2 st f is isomorphic
proof
reconsider f = id the carrier of L1 as Function of L1,L2 by A1;
take f;
now
let z be object;
assume
A2: z in the carrier of L2;
take v = z;
thus v in the carrier of L1 by A1,A2;
thus z = f.v by A1,A2,FUNCT_1:18;
end;
then
A3: rng f = the carrier of L2 by FUNCT_2:10;
for x,y be Element of L1 holds x <= y iff f.x <= f.y
by A1,YELLOW_0:1;
hence thesis by A3,WAYBEL_0:66;
end;
hence thesis by WAYBEL_1:def 8;
end;
Lm2: for L be LATTICE holds (ex X be non empty set, S be full SubRelStr of
BoolePoset X st ( S is infs-inheriting & S is directed-sups-inheriting & L,S
are_isomorphic )) implies ex X be non empty set, c be closure Function of
BoolePoset X,BoolePoset X st c is directed-sups-preserving & L,Image c
are_isomorphic
proof
let L be LATTICE;
given X be non empty set, S be full SubRelStr of BoolePoset X such that
A1: S is infs-inheriting and
A2: S is directed-sups-inheriting and
A3: L,S are_isomorphic;
reconsider S9 = S as closure System of BoolePoset X by A1;
take X;
reconsider c = closure_op S9 as closure Function of BoolePoset X,BoolePoset
X;
take c;
thus c is directed-sups-preserving by A2;
Image c = the RelStr of S by WAYBEL10:18;
then S,Image c are_isomorphic by Th26;
hence thesis by A3,WAYBEL_1:7;
end;
Lm3: for L be LATTICE holds (ex X be set, S be full SubRelStr of BoolePoset X
st ( S is infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic
)) implies ex X be set, c be closure Function of BoolePoset X,BoolePoset X st c
is directed-sups-preserving & L,Image c are_isomorphic
proof
let L be LATTICE;
given X be set, S be full SubRelStr of BoolePoset X such that
A1: S is infs-inheriting and
A2: S is directed-sups-inheriting and
A3: L,S are_isomorphic;
reconsider S9 = S as closure System of BoolePoset X by A1;
take X;
reconsider c = closure_op S9 as closure Function of BoolePoset X,BoolePoset
X;
take c;
thus c is directed-sups-preserving by A2;
Image c = the RelStr of S by WAYBEL10:18;
then S,Image c are_isomorphic by Th26;
hence thesis by A3,WAYBEL_1:7;
end;
Lm4: for L1,L2 be up-complete non empty Poset for f be Function of L1,L2 st
f is isomorphic for x,y be Element of L1 holds x << y implies f.x << f.y
proof
let L1,L2 be up-complete non empty Poset;
let f be Function of L1,L2;
assume
A1: f is isomorphic;
then reconsider g = f" as Function of L2,L1 by WAYBEL_0:67;
let x,y be Element of L1;
A2: g is isomorphic by A1,WAYBEL_0:68;
assume
A3: x << y;
now
let X be non empty directed Subset of L2;
y in the carrier of L1;
then
A4: y in dom f by FUNCT_2:def 1;
X c= the carrier of L2;
then
A5: X c= rng f by A1,WAYBEL_0:66;
now
let Y1 be finite Subset of g.:X;
A6: f"(f.:Y1) c= Y1 by A1,FUNCT_1:82;
now
let v be object;
assume v in f.:Y1;
then ex u be object st u in dom f & u in Y1 & v = f.u
by FUNCT_1:def 6;
then v in f.:(g.:X) by FUNCT_1:def 6;
then v in f.:(f"X) by A1,FUNCT_1:85;
hence v in X by A5,FUNCT_1:77;
end;
then reconsider X1 = f.:Y1 as finite Subset of X by TARSKI:def 3;
consider y1 be Element of L2 such that
A7: y1 in X and
A8: y1 is_>=_than X1 by WAYBEL_0:1;
take gy1 = g.y1;
y1 in the carrier of L2;
then y1 in dom g by FUNCT_2:def 1;
hence gy1 in g.:X by A7,FUNCT_1:def 6;
Y1 c= the carrier of L1 by XBOOLE_1:1;
then Y1 c= dom f by FUNCT_2:def 1;
then
A9: Y1 c= f"(f.:Y1) by FUNCT_1:76;
g.:X1 = f"(f.:Y1) by A1,FUNCT_1:85
.= Y1 by A9,A6,XBOOLE_0:def 10;
hence gy1 is_>=_than Y1 by A2,A8,Th19;
end;
then reconsider Y = g.:X as non empty directed Subset of L1 by WAYBEL_0:1;
A10: ex_sup_of X,L2 & g preserves_sup_of X by A2,WAYBEL_0:75,def 33;
assume f.y <= sup X;
then g.(f.y) <= g.(sup X) by A2,WAYBEL_0:66;
then y <= g.(sup X) by A1,A4,FUNCT_1:34;
then y <= sup Y by A10,WAYBEL_0:def 31;
then consider c be Element of L1 such that
A11: c in Y and
A12: x <= c by A3,WAYBEL_3:def 1;
take fc = f.c;
c in the carrier of L1;
then c in dom f by FUNCT_2:def 1;
then f.c in f.:Y by A11,FUNCT_1:def 6;
then f.c in f.:(f"X) by A1,FUNCT_1:85;
hence fc in X by A5,FUNCT_1:77;
thus f.x <= fc by A1,A12,WAYBEL_0:66;
end;
hence thesis by WAYBEL_3:def 1;
end;
theorem Th27:
for L1,L2 be up-complete non empty Poset for f be Function of
L1,L2 st f is isomorphic for x,y be Element of L1 holds x << y iff f.x << f.y
proof
let L1,L2 be up-complete non empty Poset;
let f be Function of L1,L2;
assume
A1: f is isomorphic;
then reconsider g = f" as Function of L2,L1 by WAYBEL_0:67;
let x,y be Element of L1;
thus x << y implies f.x << f.y by A1,Lm4;
thus f.x << f.y implies x << y
proof
y in the carrier of L1;
then
A2: y in dom f by FUNCT_2:def 1;
x in the carrier of L1;
then
A3: x in dom f by FUNCT_2:def 1;
assume f.x << f.y;
then g.(f.x) << g.(f.y) by A1,Lm4,WAYBEL_0:68;
then x << g.(f.y) by A1,A3,FUNCT_1:34;
hence thesis by A1,A2,FUNCT_1:34;
end;
end;
theorem Th28:
for L1,L2 be up-complete non empty Poset for f be Function of
L1,L2 st f is isomorphic for x be Element of L1 holds x is compact iff f.x is
compact
proof
let L1,L2 be up-complete non empty Poset;
let f be Function of L1,L2;
assume
A1: f is isomorphic;
let x be Element of L1;
thus x is compact implies f.x is compact
proof
assume x is compact;
then x << x by WAYBEL_3:def 2;
then f.x << f.x by A1,Th27;
hence thesis by WAYBEL_3:def 2;
end;
thus f.x is compact implies x is compact
proof
assume f.x is compact;
then f.x << f.x by WAYBEL_3:def 2;
then x << x by A1,Th27;
hence thesis by WAYBEL_3:def 2;
end;
end;
theorem Th29:
for L1,L2 be up-complete non empty Poset for f be Function of
L1,L2 st f is isomorphic for x be Element of L1 holds f.:(compactbelow x) =
compactbelow f.x
proof
let L1,L2 be up-complete non empty Poset;
let f be Function of L1,L2;
assume
A1: f is isomorphic;
then reconsider g = f" as Function of L2,L1 by WAYBEL_0:67;
let x be Element of L1;
A2: g is isomorphic by A1,WAYBEL_0:68;
A3: compactbelow f.x c= f.:(compactbelow x)
proof
let z be object;
x in the carrier of L1;
then
A4: x in dom f by FUNCT_2:def 1;
assume z in compactbelow f.x;
then z in { y where y is Element of L2: f.x >= y & y is compact } by
WAYBEL_8:def 2;
then consider z1 be Element of L2 such that
A5: z1 = z and
A6: f.x >= z1 and
A7: z1 is compact;
A8: g.z1 is compact by A2,A7,Th28;
g.z1 <= g.(f.x) by A2,A6,WAYBEL_0:66;
then g.z1 <= x by A1,A4,FUNCT_1:34;
then
A9: g.z1 in compactbelow x by A8,WAYBEL_8:4;
z1 in the carrier of L2;
then
A10: z1 in rng f by A1,WAYBEL_0:66;
g.z1 in the carrier of L1;
then g.z1 in dom f by FUNCT_2:def 1;
then f.(g.z1) in f.:(compactbelow x) by A9,FUNCT_1:def 6;
hence thesis by A1,A5,A10,FUNCT_1:35;
end;
f.:(compactbelow x) c= compactbelow f.x
proof
let z be object;
assume z in f.:(compactbelow x);
then consider u be object such that
u in dom f and
A11: u in compactbelow x and
A12: z = f.u by FUNCT_1:def 6;
u in { y where y is Element of L1: x >= y & y is compact } by A11,
WAYBEL_8:def 2;
then consider u1 be Element of L1 such that
A13: u1 = u and
A14: x >= u1 & u1 is compact;
f.u1 <= f.x & f.u1 is compact by A1,A14,Th28,WAYBEL_0:66;
hence thesis by A12,A13,WAYBEL_8:4;
end;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem Th30:
for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is
up-complete holds L2 is up-complete
proof
let L1,L2 be non empty Poset;
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is up-complete;
consider f be Function of L1,L2 such that
A3: f is isomorphic by A1,WAYBEL_1:def 8;
reconsider g = f" as Function of L2,L1 by A3,WAYBEL_0:67;
A4: g is isomorphic by A3,WAYBEL_0:68;
now
let Y be non empty directed Subset of L2;
Y c= the carrier of L2;
then
A5: Y c= rng f by A3,WAYBEL_0:66;
now
let X1 be finite Subset of g.:Y;
A6: f"(f.:X1) c= X1 by A3,FUNCT_1:82;
now
let v be object;
assume v in f.:X1;
then ex u be object st u in dom f & u in X1 & v = f.u
by FUNCT_1:def 6;
then v in f.:(g.:Y) by FUNCT_1:def 6;
then v in f.:(f"Y) by A3,FUNCT_1:85;
hence v in Y by A5,FUNCT_1:77;
end;
then reconsider Y1 = f.:X1 as finite Subset of Y by TARSKI:def 3;
consider y1 be Element of L2 such that
A7: y1 in Y and
A8: y1 is_>=_than Y1 by WAYBEL_0:1;
take gy1 = g.y1;
y1 in the carrier of L2;
then y1 in dom g by FUNCT_2:def 1;
hence gy1 in g.:Y by A7,FUNCT_1:def 6;
X1 c= the carrier of L1 by XBOOLE_1:1;
then X1 c= dom f by FUNCT_2:def 1;
then
A9: X1 c= f"(f.:X1) by FUNCT_1:76;
g.:Y1 = f"(f.:X1) by A3,FUNCT_1:85
.= X1 by A9,A6,XBOOLE_0:def 10;
hence gy1 is_>=_than X1 by A4,A8,Th19;
end;
then reconsider X = g.:Y as non empty directed Subset of L1 by WAYBEL_0:1;
ex_sup_of X,L1 by A2,WAYBEL_0:75;
then consider x be Element of L1 such that
A10: X is_<=_than x and
A11: for b be Element of L1 st X is_<=_than b holds x <= b by YELLOW_0:15;
A12: now
let y be Element of L2;
assume Y is_<=_than y;
then X is_<=_than g.y by A4,Th19;
then x <= g.y by A11;
then
A13: f.x <= f.(g.y) by A3,WAYBEL_0:66;
y in the carrier of L2;
then y in dom g by FUNCT_2:def 1;
then y in rng f by A3,FUNCT_1:33;
hence f.x <= y by A3,A13,FUNCT_1:35;
end;
f.:X = f.:(f"Y) by A3,FUNCT_1:85
.= Y by A5,FUNCT_1:77;
then Y is_<=_than f.x by A3,A10,Th19;
hence ex_sup_of Y,L2 by A12,YELLOW_0:15;
end;
hence thesis by WAYBEL_0:75;
end;
theorem Th31:
for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is
complete satisfying_axiom_K holds L2 is satisfying_axiom_K
proof
let L1,L2 be non empty Poset;
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is complete satisfying_axiom_K;
consider f be Function of L1,L2 such that
A3: f is isomorphic by A1,WAYBEL_1:def 8;
reconsider g = f" as Function of L2,L1 by A3,WAYBEL_0:67;
now
let x be Element of L2;
A4: f preserves_sup_of compactbelow g.x & ex_sup_of compactbelow g.x,L1 by A2
,A3,WAYBEL_0:def 33,YELLOW_0:17;
A5: L2 is up-complete non empty Poset by A1,A2,Th30;
x in the carrier of L2;
then x in dom g by FUNCT_2:def 1;
then
A6: x in rng f by A3,FUNCT_1:33;
hence x = f.(g.x) by A3,FUNCT_1:35
.= f.(sup compactbelow g.x) by A2,WAYBEL_8:def 3
.= sup (f.:(compactbelow g.x)) by A4,WAYBEL_0:def 31
.= sup compactbelow f.(g.x) by A2,A3,A5,Th29
.= sup compactbelow x by A3,A6,FUNCT_1:35;
end;
hence thesis by WAYBEL_8:def 3;
end;
theorem Th32:
for L1,L2 be sup-Semilattice st L1,L2 are_isomorphic & L1 is
lower-bounded algebraic holds L2 is algebraic
proof
let L1,L2 be sup-Semilattice;
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is lower-bounded algebraic;
consider f be Function of L1,L2 such that
A3: f is isomorphic by A1,WAYBEL_1:def 8;
reconsider g = f" as Function of L2,L1 by A3,WAYBEL_0:67;
A4: g is isomorphic by A3,WAYBEL_0:68;
A5: now
let y be Element of L2;
y in the carrier of L2;
then y in dom g by FUNCT_2:def 1;
then
A6: y in rng f by A3,FUNCT_1:33;
A7: L2 is up-complete non empty Poset by A1,A2,Th30;
A8: compactbelow (g.y) is non empty directed by A2,WAYBEL_8:def 4;
now
let Y be finite Subset of compactbelow f.(g.y);
Y c= the carrier of L2 by XBOOLE_1:1;
then
A9: Y c= rng f by A3,WAYBEL_0:66;
now
let z be object;
assume z in g.:Y;
then consider v be object such that
A10: v in dom g and
A11: v in Y and
A12: z = g.v by FUNCT_1:def 6;
reconsider v as Element of L2 by A10;
v in compactbelow f.(g.y) by A11;
then v in compactbelow y by A3,A6,FUNCT_1:35;
then v <= y by WAYBEL_8:4;
then
A13: g.v <= g.y by A4,WAYBEL_0:66;
v is compact by A11,WAYBEL_8:4;
then g.v is compact by A2,A4,A7,Th28;
hence z in compactbelow (g.y) by A12,A13,WAYBEL_8:4;
end;
then reconsider X = g.:Y as finite Subset of compactbelow (g.y) by
TARSKI:def 3;
consider x be Element of L1 such that
A14: x in compactbelow (g.y) and
A15: x is_>=_than X by A8,WAYBEL_0:1;
take fx = f.x;
x <= g.y by A14,WAYBEL_8:4;
then
A16: f.x <= f.(g.y) by A3,WAYBEL_0:66;
x is compact by A14,WAYBEL_8:4;
then f.x is compact by A2,A3,A7,Th28;
hence fx in compactbelow f.(g.y) by A16,WAYBEL_8:4;
f.:X = f.:(f"Y) by A3,FUNCT_1:85
.= Y by A9,FUNCT_1:77;
hence fx is_>=_than Y by A3,A15,Th19;
end;
then compactbelow f.(g.y) is non empty directed by WAYBEL_0:1;
hence compactbelow y is non empty directed by A3,A6,FUNCT_1:35;
end;
L2 is up-complete & L2 is satisfying_axiom_K by A1,A2,Th30,Th31;
hence thesis by A5,WAYBEL_8:def 4;
end;
Lm5: for L be LATTICE holds (ex X be set, c be closure Function of BoolePoset
X,BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic)
implies L is algebraic
proof
let L be LATTICE;
given X be set, c be closure Function of BoolePoset X,BoolePoset X such that
A1: c is directed-sups-preserving and
A2: L,Image c are_isomorphic;
Image c is complete LATTICE & Image c is algebraic LATTICE by A1,WAYBEL_8:24
,YELLOW_2:35;
hence thesis by A2,Th32,WAYBEL_1:6;
end;
theorem
for L be continuous lower-bounded sup-Semilattice holds SupMap L is
infs-preserving sups-preserving by WAYBEL_1:12,57,WAYBEL_5:3;
:: THEOREM 4.15. (1) iff (2)
theorem
for L be lower-bounded LATTICE holds ( L is algebraic implies ex X be
non empty set, S be full SubRelStr of BoolePoset X st S is infs-inheriting & S
is directed-sups-inheriting & L,S are_isomorphic ) & (( ex X be set, S be full
SubRelStr of BoolePoset X st S is infs-inheriting & S is
directed-sups-inheriting & L,S are_isomorphic ) implies L is algebraic )
proof
let L be lower-bounded LATTICE;
thus L is algebraic implies ex X be non empty set, S be full SubRelStr of
BoolePoset X st S is infs-inheriting & S is directed-sups-inheriting & L,S
are_isomorphic by Lm1;
thus (ex X be set, S be full SubRelStr of BoolePoset X st ( S is
infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic )) implies
L is algebraic
proof
assume ex X be set, S be full SubRelStr of BoolePoset X st S is
infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic;
then ex X be set, c be closure Function of BoolePoset X,BoolePoset X st c
is directed-sups-preserving & L,Image c are_isomorphic by Lm3;
hence thesis by Lm5;
end;
end;
:: THEOREM 4.15. (1) iff (3)
theorem
for L be lower-bounded LATTICE holds ( L is algebraic implies ex X be
non empty set, c be closure Function of BoolePoset X,BoolePoset X st c is
directed-sups-preserving & L,Image c are_isomorphic ) & (( ex X be set, c be
closure Function of BoolePoset X,BoolePoset X st c is directed-sups-preserving
& L,Image c are_isomorphic ) implies L is algebraic )
proof
let L be lower-bounded LATTICE;
hereby
assume L is algebraic;
then ex X be non empty set, S be full SubRelStr of BoolePoset X st S is
infs-inheriting & S is directed-sups-inheriting & L,S are_isomorphic by Lm1;
hence ex X be non empty set, c be closure Function of BoolePoset X,
BoolePoset X st c is directed-sups-preserving & L,Image c are_isomorphic
by Lm2;
end;
thus thesis by Lm5;
end;