:: More on the Algebraic and Arithmetic Lattices
:: by Robert Milewski
::
:: Received October 29, 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 ORDERS_2, CAT_1, YELLOW_0, STRUCT_0, TARSKI, WELLORD1, XBOOLE_0,
FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, YELLOW_1, WAYBEL_0, XXREAL_0,
LATTICES, RELAT_2, WAYBEL_1, GROUP_6, SEQM_3, WAYBEL_8, RCOMP_1,
FINSET_1, LATTICE3, WAYBEL_3, ORDINAL2, YELLOW_2, CARD_FIL, BINOP_1,
EQREL_1, REWRITE1, WAYBEL_6, ARYTM_0, INT_2, ARYTM_3, XBOOLEAN, WAYBEL_5,
WAYBEL15;
notations TARSKI, XBOOLE_0, SUBSET_1, WELLORD1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FINSET_1, DOMAIN_1, STRUCT_0, ORDERS_2, QUANTAL1, LATTICE3,
YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_7, WAYBEL_0, WAYBEL_1, WAYBEL_3,
WAYBEL_5, WAYBEL_6, WAYBEL_8;
constructors DOMAIN_1, TOLER_1, QUANTAL1, ORDERS_3, WAYBEL_1, WAYBEL_3,
WAYBEL_5, WAYBEL_6, WAYBEL_8, RELSET_1;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0,
LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2,
WAYBEL_3, WAYBEL_5, WAYBEL_8, WAYBEL10;
requirements SUBSET, BOOLE;
definitions TARSKI;
equalities YELLOW_2, WAYBEL_1, STRUCT_0;
expansions WAYBEL_1;
theorems TARSKI, RELAT_1, WELLORD1, FUNCT_1, FUNCT_2, ORDERS_2, QUANTAL1,
LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_5, YELLOW_6, YELLOW_7,
WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_8, WAYBEL13,
XBOOLE_0, XBOOLE_1, WAYBEL14;
schemes FUNCT_2, SUBSET_1;
begin :: Preliminaries
theorem Th1:
for R be RelStr for S be full SubRelStr of R
for T be full SubRelStr of S holds T is full SubRelStr of R
proof
let R be RelStr;
let S be full SubRelStr of R;
let T be full SubRelStr of S;
reconsider T1 = T as SubRelStr of R by YELLOW_6:7;
A1: the carrier of T c= the carrier of S by YELLOW_0:def 13;
the InternalRel of S = (the InternalRel of R)|_2 the carrier of S by
YELLOW_0:def 14;
then the InternalRel of T = ((the InternalRel of R)|_2 the carrier of S)|_2
the carrier of T by YELLOW_0:def 14
.= (the InternalRel of R)|_2 the carrier of T by A1,WELLORD1:22;
then T1 is full by YELLOW_0:def 14;
hence thesis;
end;
Lm1:
for X be set, Y,Z be non empty set for f be Function of X,Y
for g be Function of Y,Z holds f is onto & g is onto implies g*f is onto
by FUNCT_2:27;
theorem
for X be set for a be Element of BoolePoset X holds uparrow a = {Y
where Y is Subset of X : a c= Y}
proof
let X be set;
let a be Element of BoolePoset X;
A1: {Y where Y is Subset of X : a c= Y} c= uparrow a
proof
let x be object;
assume x in {Y where Y is Subset of X : a c= Y};
then consider x9 be Subset of X such that
A2: x9 = x and
A3: a c= x9;
reconsider x9 as Element of BoolePoset X by WAYBEL_8:26;
a <= x9 by A3,YELLOW_1:2;
hence thesis by A2,WAYBEL_0:18;
end;
uparrow a c= {Y where Y is Subset of X : a c= Y}
proof
let x be object;
assume
A4: x in uparrow a;
then reconsider x9 = x as Element of BoolePoset X;
a <= x9 by A4,WAYBEL_0:18;
then x9 is Subset of X & a c= x9 by WAYBEL_8:26,YELLOW_1:2;
hence thesis;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
for L be upper-bounded non empty antisymmetric RelStr for a be Element
of L holds Top L <= a implies a = Top L
proof
let L be upper-bounded non empty antisymmetric RelStr;
let a be Element of L;
A1: a <= Top L by YELLOW_0:45;
assume Top L <= a;
hence thesis by A1,YELLOW_0:def 3;
end;
theorem Th4:
for S,T be non empty Poset for g be Function of S,T for d be
Function of T,S holds g is onto & [g,d] is Galois implies T,Image d
are_isomorphic
proof
let S,T be non empty Poset;
let g be Function of S,T;
let d be Function of T,S;
assume that
A1: g is onto and
A2: [g,d] is Galois;
d is one-to-one by A1,A2,WAYBEL_1:24;
then
A3: (the carrier of Image d)|`d is one-to-one by FUNCT_1:58;
A4: d is monotone by A2,WAYBEL_1:8;
A5: now
let x,y be Element of T;
thus x <= y implies (corestr(d)).x <= (corestr(d)).y by A4,WAYBEL_1:def 2;
thus (corestr(d)).x <= (corestr(d)).y implies x <= y
proof
for t be Element of T holds d.t is_minimum_of g"{t} by A1,A2,WAYBEL_1:22;
then
A6: g*d = id T by WAYBEL_1:23;
assume
A7: (corestr(d)).x <= (corestr(d)).y;
y in the carrier of T;
then
A8: y in dom d by FUNCT_2:def 1;
A9: g is monotone by A2,WAYBEL_1:8;
d.x = (corestr(d)).x & d.y = (corestr(d)).y by WAYBEL_1:30;
then d.x <= d.y by A7,YELLOW_0:59;
then
A10: g.(d.x) <= g.(d.y) by A9;
x in the carrier of T;
then x in dom d by FUNCT_2:def 1;
then (g*d).x <= g.(d.y) by A10,FUNCT_1:13;
then (g*d).x <= (g*d).y by A8,FUNCT_1:13;
then (id T).x <= y by A6;
hence thesis;
end;
end;
rng corestr(d) = the carrier of Image d by FUNCT_2:def 3;
then corestr(d) is isomorphic by A3,A5,WAYBEL_0:66;
hence thesis;
end;
theorem Th5:
for L1,L2,L3 be non empty Poset for g1 be Function of L1,L2 for
g2 be Function of L2,L3 for d1 be Function of L2,L1 for d2 be Function of L3,L2
st [g1,d1] is Galois & [g2,d2] is Galois holds [g2*g1,d1*d2] is Galois
proof
let L1,L2,L3 be non empty Poset;
let g1 be Function of L1,L2;
let g2 be Function of L2,L3;
let d1 be Function of L2,L1;
let d2 be Function of L3,L2;
assume that
A1: [g1,d1] is Galois and
A2: [g2,d2] is Galois;
A3: d1 is monotone by A1,WAYBEL_1:8;
A4: g2 is monotone by A2,WAYBEL_1:8;
A5: now
let s be Element of L3, t be Element of L1;
s in the carrier of L3;
then
A6: s in dom d2 by FUNCT_2:def 1;
t in the carrier of L1;
then
A7: t in dom g1 by FUNCT_2:def 1;
thus s <= (g2*g1).t implies (d1*d2).s <= t
proof
assume s <= (g2*g1).t;
then s <= g2.(g1.t) by A7,FUNCT_1:13;
then d2.s <= g1.t by A2,WAYBEL_1:8;
then d1.(d2.s) <= d1.(g1.t) by A3;
then
A8: d1.(d2.s) <= (d1*g1).t by A7,FUNCT_1:13;
d1*g1 <= id L1 by A1,WAYBEL_1:18;
then (d1*g1).t <= (id L1).t by YELLOW_2:9;
then d1.(d2.s) <= (id L1).t by A8,ORDERS_2:3;
then d1.(d2.s) <= t;
hence thesis by A6,FUNCT_1:13;
end;
thus (d1*d2).s <= t implies s <= (g2*g1).t
proof
assume (d1*d2).s <= t;
then d1.(d2.s) <= t by A6,FUNCT_1:13;
then d2.s <= g1.t by A1,WAYBEL_1:8;
then g2.(d2.s) <= g2.(g1.t) by A4;
then
A9: (g2*d2).s <= g2.(g1.t) by A6,FUNCT_1:13;
id L3 <= g2*d2 by A2,WAYBEL_1:18;
then (id L3).s <= (g2*d2).s by YELLOW_2:9;
then (id L3).s <= g2.(g1.t) by A9,ORDERS_2:3;
then s <= g2.(g1.t);
hence thesis by A7,FUNCT_1:13;
end;
end;
d2 is monotone by A2,WAYBEL_1:8;
then
A10: d1*d2 is monotone by A3,YELLOW_2:12;
g1 is monotone by A1,WAYBEL_1:8;
then g2*g1 is monotone by A4,YELLOW_2:12;
hence thesis by A10,A5;
end;
theorem Th6:
for L1,L2 be non empty Poset for f be Function of L1,L2 for f1 be
Function of L2,L1 st f1 = (f qua Function)" & f is isomorphic holds [f,f1] is
Galois & [f1,f] is Galois
proof
let L1,L2 be non empty Poset;
let f be Function of L1,L2;
let f1 be Function of L2,L1;
assume that
A1: f1 = (f qua Function)" and
A2: f is isomorphic;
A3: f1 is isomorphic by A1,A2,WAYBEL_0:68;
now
let t be Element of L2, s be Element of L1;
s in the carrier of L1;
then
A4: s in dom f by FUNCT_2:def 1;
A5: f1*f = id dom f by A1,A2,FUNCT_1:39
.= id L1 by FUNCT_2:def 1;
thus t <= f.s implies f1.t <= s
proof
assume t <= f.s;
then f1.t <= f1.(f.s) by A3,WAYBEL_1:def 2;
then f1.t <= (f1*f).s by A4,FUNCT_1:13;
hence thesis by A5;
end;
t in the carrier of L2;
then
A6: t in dom f1 by FUNCT_2:def 1;
A7: f*f1 = id rng f by A1,A2,FUNCT_1:39
.= id L2 by A2,WAYBEL_0:66;
thus f1.t <= s implies t <= f.s
proof
assume f1.t <= s;
then f.(f1.t) <= f.s by A2,WAYBEL_1:def 2;
then (f*f1).t <= f.s by A6,FUNCT_1:13;
hence thesis by A7;
end;
end;
hence [f,f1] is Galois by A2,A3;
now
let t be Element of L1, s be Element of L2;
s in the carrier of L2;
then
A8: s in dom f1 by FUNCT_2:def 1;
A9: f*f1 = id rng f by A1,A2,FUNCT_1:39
.= id L2 by A2,WAYBEL_0:66;
thus t <= f1.s implies f.t <= s
proof
assume t <= f1.s;
then f.t <= f.(f1.s) by A2,WAYBEL_1:def 2;
then f.t <= (f*f1).s by A8,FUNCT_1:13;
hence thesis by A9;
end;
t in the carrier of L1;
then
A10: t in dom f by FUNCT_2:def 1;
A11: f1*f = id dom f by A1,A2,FUNCT_1:39
.= id L1 by FUNCT_2:def 1;
thus f.t <= s implies t <= f1.s
proof
assume f.t <= s;
then f1.(f.t) <= f1.s by A3,WAYBEL_1:def 2;
then (f1*f).t <= f1.s by A10,FUNCT_1:13;
hence thesis by A11;
end;
end;
hence thesis by A2,A3;
end;
theorem Th7:
for X be set holds BoolePoset X is arithmetic
proof
let X be set;
now
let x,y be Element of CompactSublatt BoolePoset X;
reconsider x9 = x, y9 = y as Element of BoolePoset X by YELLOW_0:58;
x9 is compact by WAYBEL_8:def 1;
then x9 is finite by WAYBEL_8:28;
then x9 /\ y9 is finite;
then x9 "/\" y9 is finite by YELLOW_1:17;
then x9 "/\" y9 is compact by WAYBEL_8:28;
then reconsider
xy = x9 "/\" y9 as Element of CompactSublatt BoolePoset X by WAYBEL_8:def 1;
A1: now
let z be Element of CompactSublatt BoolePoset X;
reconsider z9 = z as Element of BoolePoset X by YELLOW_0:58;
assume that
A2: z <= x and
A3: z <= y;
z9 <= y9 by A3,YELLOW_0:59;
then
A4: z9 c= y9 by YELLOW_1:2;
z9 <= x9 by A2,YELLOW_0:59;
then z9 c= x9 by YELLOW_1:2;
then z9 c= x9 /\ y9 by A4,XBOOLE_1:19;
then z9 c= x9 "/\" y9 by YELLOW_1:17;
then z9 <= x9 "/\" y9 by YELLOW_1:2;
hence xy >= z by YELLOW_0:60;
end;
x9 /\ y9 c= y9 by XBOOLE_1:17;
then x9 "/\" y9 c= y9 by YELLOW_1:17;
then x9 "/\" y9 <= y9 by YELLOW_1:2;
then
A5: xy <= y by YELLOW_0:60;
x9 /\ y9 c= x9 by XBOOLE_1:17;
then x9 "/\" y9 c= x9 by YELLOW_1:17;
then x9 "/\" y9 <= x9 by YELLOW_1:2;
then xy <= x by YELLOW_0:60;
hence ex_inf_of {x,y},CompactSublatt BoolePoset X by A5,A1,YELLOW_0:19;
end;
then CompactSublatt BoolePoset X is with_infima by YELLOW_0:21;
hence thesis by WAYBEL_8:19;
end;
registration
let X be set;
cluster BoolePoset X -> arithmetic;
coherence by Th7;
end;
theorem Th8:
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.:(waybelow x) =
waybelow 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 qua Function)" as Function of L2,L1 by WAYBEL_0:67;
let x be Element of L1;
A2: waybelow f.x c= f.:(waybelow x)
proof
let z be object;
assume z in waybelow f.x;
then z in { y where y is Element of L2 : y << f.x } by WAYBEL_3:def 3;
then consider z1 be Element of L2 such that
A3: z1 = z and
A4: z1 << f.x;
g.z1 in the carrier of L1;
then
A5: g.z1 in dom f by FUNCT_2:def 1;
z1 in the carrier of L2;
then z1 in dom g by FUNCT_2:def 1;
then z1 in rng f by A1,FUNCT_1:33;
then
A6: z1 = f.(g.z1) by A1,FUNCT_1:35;
then g.z1 << x by A1,A4,WAYBEL13:27;
then g.z1 in waybelow x by WAYBEL_3:7;
hence thesis by A3,A5,A6,FUNCT_1:def 6;
end;
f.:(waybelow x) c= waybelow f.x
proof
let z be object;
assume z in f.:(waybelow x);
then consider v be object such that
v in dom f and
A7: v in waybelow x and
A8: z = f.v by FUNCT_1:def 6;
v in { y where y is Element of L1 : y << x } by A7,WAYBEL_3:def 3;
then consider v1 be Element of L1 such that
A9: v1 = v and
A10: v1 << x;
f.v1 << f.x by A1,A10,WAYBEL13:27;
hence thesis by A8,A9,WAYBEL_3:7;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
theorem Th9:
for L1,L2 be non empty Poset st L1,L2 are_isomorphic & L1 is
continuous holds L2 is continuous
proof
let L1,L2 be non empty Poset;
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is continuous;
consider f be Function of L1,L2 such that
A3: f is isomorphic by A1;
reconsider g = (f qua Function)" as Function of L2,L1 by A3,WAYBEL_0:67;
A4: L1 is up-complete non empty Poset & L2 is up-complete non empty Poset
by A1,A2,WAYBEL13:30;
now
let y be Element of L2;
A5: ex_sup_of waybelow (g.y),L1 by A2,WAYBEL_0:75;
f is sups-preserving by A3,WAYBEL13:20;
then
A6: f preserves_sup_of waybelow (g.y) by WAYBEL_0:def 33;
y in the carrier of L2;
then
A7: y in rng f by A3,WAYBEL_0:66;
hence y = f.(g.y) by A3,FUNCT_1:35
.= f.(sup waybelow (g.y)) by A2,WAYBEL_3:def 5
.= sup (f.:(waybelow (g.y))) by A6,A5,WAYBEL_0:def 31
.= sup waybelow f.(g.y) by A3,A4,Th8
.= sup waybelow y by A3,A7,FUNCT_1:35;
end;
then
A8: L2 is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
A9: g is isomorphic by A3,WAYBEL_0:68;
A10: now
let y be Element of L2;
for Y be finite Subset of waybelow y ex z be Element of L2 st z in
waybelow y & z is_>=_than Y
proof
let Y be finite Subset of waybelow y;
Y c= the carrier of L2 by XBOOLE_1:1;
then
A11: Y c= rng f by A3,WAYBEL_0:66;
now
let u be object;
assume u in g.:Y;
then consider v be object such that
v in dom g and
A12: v in Y and
A13: u = g.v by FUNCT_1:def 6;
v in waybelow y by A12;
then v in { k where k is Element of L2 : k << y } by WAYBEL_3:def 3;
then consider v1 be Element of L2 such that
A14: v1 = v and
A15: v1 << y;
g.v1 << g.y by A9,A4,A15,WAYBEL13:27;
hence u in waybelow g.y by A13,A14,WAYBEL_3:7;
end;
then reconsider X = g.:Y as finite Subset of waybelow g.y by TARSKI:def 3
;
consider x be Element of L1 such that
A16: x in waybelow g.y and
A17: x is_>=_than X by A2,WAYBEL_0:1;
y in the carrier of L2;
then y in rng f by A3,WAYBEL_0:66;
then
A18: f.(g.y) = y by A3,FUNCT_1:35;
take z = f.x;
x << g.y by A16,WAYBEL_3:7;
then z << y by A3,A4,A18,WAYBEL13:27;
hence z in waybelow y by WAYBEL_3:7;
f.:X = f.:(f"Y) by A3,FUNCT_1:85
.= Y by A11,FUNCT_1:77;
hence thesis by A3,A17,WAYBEL13:19;
end;
hence waybelow y is non empty directed by WAYBEL_0:1;
end;
L2 is up-complete by A1,A2,WAYBEL13:30;
hence thesis by A8,A10,WAYBEL_3:def 6;
end;
theorem Th10:
for L1,L2 be LATTICE st L1,L2 are_isomorphic & L1 is
lower-bounded arithmetic holds L2 is arithmetic
proof
let L1,L2 be LATTICE;
assume that
A1: L1,L2 are_isomorphic and
A2: L1 is lower-bounded arithmetic;
consider f be Function of L1,L2 such that
A3: f is isomorphic by A1;
reconsider g = (f qua Function)" as Function of L2,L1 by A3,WAYBEL_0:67;
A4: g is isomorphic by A3,WAYBEL_0:68;
A5: L2 is up-complete LATTICE by A1,A2,WAYBEL13:30;
now
let x2,y2 be Element of L2;
assume that
A6: x2 in the carrier of CompactSublatt L2 and
A7: y2 in the carrier of CompactSublatt L2 and
A8: ex_inf_of {x2,y2},L2;
x2 is compact by A6,WAYBEL_8:def 1;
then g.x2 is compact by A2,A4,A5,WAYBEL13:28;
then
A9: g.x2 in the carrier of CompactSublatt L1 by WAYBEL_8:def 1;
y2 is compact by A7,WAYBEL_8:def 1;
then g.y2 is compact by A2,A4,A5,WAYBEL13:28;
then
A10: g.y2 in the carrier of CompactSublatt L1 by WAYBEL_8:def 1;
x2 in the carrier of L2;
then
A11: x2 in dom g by FUNCT_2:def 1;
A12: CompactSublatt L1 is meet-inheriting by A2,WAYBEL_8:def 5;
y2 in the carrier of L2;
then
A13: y2 in dom g by FUNCT_2:def 1;
g is infs-preserving by A4,WAYBEL13:20;
then
A14: g preserves_inf_of {x2,y2} by WAYBEL_0:def 32;
then ex_inf_of g.:{x2,y2},L1 by A8,WAYBEL_0:def 30;
then ex_inf_of {g.x2,g.y2},L1 by A11,A13,FUNCT_1:60;
then inf {g.x2,g.y2} in the carrier of CompactSublatt L1 by A9,A10,A12,
YELLOW_0:def 16;
then
A15: inf {g.x2,g.y2} is compact by WAYBEL_8:def 1;
g.(inf {x2,y2}) = inf (g.:{x2,y2}) by A8,A14,WAYBEL_0:def 30
.= inf {g.x2,g.y2} by A11,A13,FUNCT_1:60;
then inf {x2,y2} is compact by A2,A4,A5,A15,WAYBEL13:28;
hence inf {x2,y2} in the carrier of CompactSublatt L2 by WAYBEL_8:def 1;
end;
then
A16: CompactSublatt L2 is meet-inheriting by YELLOW_0:def 16;
L2 is algebraic by A1,A2,WAYBEL13:32;
hence thesis by A16,WAYBEL_8:def 5;
end;
Lm2: for L be lower-bounded LATTICE holds L is continuous implies ex A be
arithmetic lower-bounded LATTICE, g be Function of A,L st g is onto & g is
infs-preserving & g is directed-sups-preserving
proof
let L be lower-bounded LATTICE;
assume
A1: L is continuous;
reconsider A = InclPoset Ids L as arithmetic lower-bounded LATTICE by
WAYBEL13:14;
take A;
reconsider g = SupMap L as Function of A,L;
take g;
the carrier of L c= rng g
proof
let y be object;
assume y in the carrier of L;
then reconsider y9 = y as Element of L;
downarrow y9 is Element of A by YELLOW_2:41;
then downarrow y9 in the carrier of A;
then
A2: downarrow y9 in dom g by FUNCT_2:def 1;
g.(downarrow y9) = sup (downarrow y9) by YELLOW_2:def 3
.= y9 by WAYBEL_0:34;
hence thesis by A2,FUNCT_1:def 3;
end;
then rng g = the carrier of L by XBOOLE_0:def 10;
hence g is onto by FUNCT_2:def 3;
thus g is infs-preserving by A1,WAYBEL13:33;
g is sups-preserving by A1,WAYBEL13:33;
hence thesis;
end;
theorem Th11:
for L1,L2,L3 be non empty Poset for f be Function of L1,L2 for g
be Function of L2,L3 st f is directed-sups-preserving & g is
directed-sups-preserving holds g*f is directed-sups-preserving
proof
let L1,L2,L3 be non empty Poset;
let f be Function of L1,L2;
let g be Function of L2,L3;
assume that
A1: f is directed-sups-preserving and
A2: g is directed-sups-preserving;
now
let X be Subset of L1;
assume
A3: X is non empty directed;
for X1 be Ideal of L1 holds f preserves_sup_of X1 by A1,WAYBEL_0:def 37;
then
A4: f.:X is non empty directed by A3,WAYBEL_0:72,YELLOW_2:15;
now
sup X in the carrier of L1;
then
A5: sup X in dom f by FUNCT_2:def 1;
assume
A6: ex_sup_of X,L1;
A7: f preserves_sup_of X by A1,A3,WAYBEL_0:def 37;
then
A8: ex_sup_of f.:X,L2 by A6,WAYBEL_0:def 31;
A9: g preserves_sup_of f.:X by A2,A4,WAYBEL_0:def 37;
then
A10: sup (g.:(f.:X)) = g.sup (f.:X) by A8,WAYBEL_0:def 31;
ex_sup_of g.:(f.:X),L3 by A8,A9,WAYBEL_0:def 31;
hence ex_sup_of (g*f).:X,L3 by RELAT_1:126;
sup (f.: X) = f.sup X by A6,A7,WAYBEL_0:def 31;
hence sup ((g*f).:X) = g.(f.sup X) by A10,RELAT_1:126
.= (g*f).sup X by A5,FUNCT_1:13;
end;
hence g*f preserves_sup_of X by WAYBEL_0:def 31;
end;
hence thesis by WAYBEL_0:def 37;
end;
begin :: Maps Preserving Sup's and Inf's
theorem
for L1,L2 be non empty RelStr for f be Function of L1,L2 for X be
Subset of Image f holds (inclusion f).:X = X by FUNCT_1:92;
theorem Th13:
for X be set for c be Function of BoolePoset X,BoolePoset X st c
is idempotent directed-sups-preserving holds inclusion c is
directed-sups-preserving
proof
let X be set;
let c be Function of BoolePoset X,BoolePoset X;
assume
A1: c is idempotent directed-sups-preserving;
now
let Y be Ideal of Image c;
now
"\/"(Y,BoolePoset X) in the carrier of BoolePoset X;
then "\/"(Y,BoolePoset X) in dom c by FUNCT_2:def 1;
then
A2: c.("\/"(Y,BoolePoset X)) in rng c by FUNCT_1:def 3;
Y c= the carrier of Image c;
then
A3: Y c= rng c by YELLOW_0:def 15;
reconsider Y9 = Y as non empty directed Subset of BoolePoset X by
YELLOW_2:7;
assume ex_sup_of Y,Image c;
A4: ex_sup_of Y,BoolePoset X by YELLOW_0:17;
c preserves_sup_of Y9 by A1,WAYBEL_0:def 37;
then "\/"(c.:Y,BoolePoset X) in rng c by A4,A2,WAYBEL_0:def 31;
then "\/"(Y,BoolePoset X) in rng c by A1,A3,YELLOW_2:20;
then
A5: "\/"(Y,BoolePoset X) in the carrier of Image c by YELLOW_0:def 15;
thus ex_sup_of (inclusion c).:Y,BoolePoset X by YELLOW_0:17;
thus sup ((inclusion c).:Y) = "\/"(Y,BoolePoset X) by FUNCT_1:92
.= sup Y by A4,A5,YELLOW_0:64
.= (inclusion c).sup Y;
end;
hence inclusion c preserves_sup_of Y by WAYBEL_0:def 31;
end;
hence thesis by WAYBEL_0:73;
end;
Lm3: for L be lower-bounded LATTICE holds (ex A be algebraic lower-bounded
LATTICE, g be Function of A,L st g is onto & g is infs-preserving & g is
directed-sups-preserving) implies ex X be non empty set, p be projection
Function of BoolePoset X,BoolePoset X st p is directed-sups-preserving & L,
Image p are_isomorphic
proof
let L be lower-bounded LATTICE;
given A be algebraic lower-bounded LATTICE, g be Function of A,L such that
A1: g is onto and
A2: g is infs-preserving and
A3: g is directed-sups-preserving;
g is upper_adjoint by A2,WAYBEL_1:16;
then consider d be Function of L,A such that
A4: [g,d] is Galois;
g is monotone & d is monotone by A4,WAYBEL_1:8;
then d*g is monotone by YELLOW_2:12;
then reconsider k = d*g as kernel Function of A,A by A4,WAYBEL_1:41;
d is lower_adjoint by A4;
then
A5: k is directed-sups-preserving by A3,Th11;
consider X be non empty set, c be closure Function of BoolePoset X,
BoolePoset X such that
A6: c is directed-sups-preserving and
A7: A,Image c are_isomorphic by WAYBEL13:35;
consider f be Function of A,Image c such that
A8: f is isomorphic by A7;
reconsider f1 = (f qua Function)" as Function of Image c,A by A8,WAYBEL_0:67;
reconsider p = (inclusion c)*f*k*f1*(corestr c) as Function of BoolePoset X,
BoolePoset X;
A9: f1*f = id dom f by A8,FUNCT_1:39
.= id A by FUNCT_2:def 1;
A10: f1 is isomorphic by A8,WAYBEL_0:68;
then rng f1 = the carrier of A by WAYBEL_0:66;
then f1 is onto by FUNCT_2:def 3;
then
A11: g*f1 is onto by A1,Lm1;
then g*f1*(corestr c) is onto by Lm1;
then
A12: rng(g*f1*(corestr c)) = the carrier of L by FUNCT_2:def 3
.= dom(inclusion(c)*f*d) by FUNCT_2:def 1;
A13: f is sups-preserving by A8,WAYBEL13:20;
inclusion c is directed-sups-preserving by A6,Th13;
then (inclusion c)*f is directed-sups-preserving by A13,Th11;
then
A14: (inclusion c)*f*k is directed-sups-preserving by A5,Th11;
take X;
A15: dom (f*d) = the carrier of L by FUNCT_2:def 1;
A16: now
let x be object;
assume
A17: x in the carrier of L;
then (f*d).x in the carrier of Image c by FUNCT_2:5;
hence (f*d).x = (inclusion(c)).((f*d).x) by FUNCT_1:18
.= (inclusion(c)*(f*d)).x by A15,A17,FUNCT_1:13
.= (inclusion(c)*f*d).x by RELAT_1:36;
end;
A18: (inclusion c)*f*k*(f1*(id(Image c)))*(f*(k*(f1*(corestr c)))) = (
inclusion c)*f*k*f1*(f*(k*(f1*(corestr c)))) by FUNCT_2:17
.= (inclusion c)*f*k*f1*f*(k*(f1*(corestr c))) by RELAT_1:36
.= (inclusion c)*f*k*(id A)*(k*(f1*(corestr c))) by A9,RELAT_1:36
.= (inclusion c)*f*k*(k*(f1*(corestr c))) by FUNCT_2:17
.= (inclusion c)*f*k*k*(f1*(corestr c)) by RELAT_1:36
.= (inclusion c)*f*(k*k)*(f1*(corestr c)) by RELAT_1:36
.= (inclusion c)*f*k*(f1*(corestr c)) by QUANTAL1:def 9
.= p by RELAT_1:36;
p * p = (inclusion c)*f*k*f1*(corestr c)*((inclusion c)*f*k*(f1*(
corestr c))) by RELAT_1:36
.= (inclusion c)*f*k*f1*(corestr c)* ((inclusion c)*f*(k*(f1*(corestr c)
))) by RELAT_1:36
.= (inclusion c)*f*k*f1*(corestr c)*((inclusion c)* (f*(k*(f1*(corestr c
))))) by RELAT_1:36
.= (inclusion c)*f*k*f1*(corestr c)*(inclusion c)* (f*(k*(f1*(corestr c)
))) by RELAT_1:36
.= (inclusion c)*f*k*f1*((corestr c)*(inclusion c))* (f*(k*(f1*(corestr
c)))) by RELAT_1:36
.= (inclusion c)*f*k*f1*(id(Image c))*(f*(k*(f1*(corestr c)))) by
WAYBEL_1:33
.= p by A18,RELAT_1:36;
then
A19: p is idempotent by QUANTAL1:def 9;
(inclusion c)*f is monotone by A8,YELLOW_2:12;
then (inclusion c)*f*k is monotone by YELLOW_2:12;
then (inclusion c)*f*k*f1 is monotone by A10,YELLOW_2:12;
then p is monotone by YELLOW_2:12;
then reconsider
p as projection Function of BoolePoset X,BoolePoset X by A19,WAYBEL_1:def 13;
take p;
p = inclusion(c)*f*d*g*f1*(corestr c) by RELAT_1:36
.= inclusion(c)*f*d*g*(f1*(corestr c)) by RELAT_1:36
.= inclusion(c)*f*d*(g*(f1*(corestr c))) by RELAT_1:36
.= inclusion(c)*f*d*(g*f1*(corestr c)) by RELAT_1:36;
then
A20: rng(inclusion(c)*f*d) = rng p by A12,RELAT_1:28;
dom (inclusion(c)*f*d) = the carrier of L by FUNCT_2:def 1;
then rng (f*d) = rng (inclusion(c)*f*d) by A15,A16,FUNCT_1:2;
then
A21: the carrier of (subrelstr rng (f*d)) = rng (inclusion(c)*f*d) by
YELLOW_0:def 15;
[f1,f] is Galois by A8,Th6;
then [g*f1,f*d] is Galois by A4,Th5;
then
A22: L,Image(f*d) are_isomorphic by A11,Th4;
f1 is sups-preserving by A10,WAYBEL13:20;
then corestr c is sups-preserving & (inclusion c)*f*k*f1 is
directed-sups-preserving by A14,Th11,WAYBEL_1:55;
hence p is directed-sups-preserving by Th11;
subrelstr rng (f*d) is full strict SubRelStr of BoolePoset X by Th1;
hence thesis by A22,A21,A20,YELLOW_0:def 15;
end;
theorem Th14: :: THEOREM 2.10.
for L be continuous complete LATTICE for p be kernel Function of
L,L st p is directed-sups-preserving holds Image p is continuous LATTICE
proof
let L be continuous complete LATTICE;
let p be kernel Function of L,L such that
A1: p is directed-sups-preserving;
now
let X be Subset of L;
assume X is non empty directed;
then
A2: p preserves_sup_of X by A1,WAYBEL_0:def 37;
A3: Image p is sups-inheriting by WAYBEL_1:53;
now
assume
A4: ex_sup_of X,L;
Image p is complete by WAYBEL_1:54;
hence ex_sup_of (corestr(p)).:X,Image p by YELLOW_0:17;
A5: (corestr(p)).:X = p.:X by WAYBEL_1:30;
ex_sup_of (p).:X,L by YELLOW_0:17;
then "\/"((corestr p).:X,L) in the carrier of Image p by A3,A5,
YELLOW_0:def 19;
hence sup ((corestr(p)).:X) = sup (p.:X) by A5,YELLOW_0:68
.= p.sup X by A2,A4,WAYBEL_0:def 31
.= (corestr(p)).sup X by WAYBEL_1:30;
end;
hence corestr(p) preserves_sup_of X by WAYBEL_0:def 31;
end;
then corestr(p) is directed-sups-preserving by WAYBEL_0:def 37;
hence thesis by WAYBEL_1:56,WAYBEL_5:33;
end;
theorem Th15: :: THEOREM 2.14.
for L be continuous complete LATTICE for p be projection
Function of L,L st p is directed-sups-preserving holds Image p is continuous
LATTICE
proof
let L be continuous complete LATTICE;
let p be projection Function of L,L such that
A1: p is directed-sups-preserving;
reconsider Lk = {k where k is Element of L: p.k <= k} as non empty Subset of
L by WAYBEL_1:43;
A2: subrelstr Lk is infs-inheriting by WAYBEL_1:50;
reconsider pk = p|Lk as Function of subrelstr Lk, subrelstr Lk by WAYBEL_1:46
;
A3: pk is kernel by WAYBEL_1:48;
now
let X be Subset of subrelstr Lk;
reconsider X9 = X as Subset of L by WAYBEL13:3;
assume
A4: X is non empty directed;
then reconsider X9 as non empty directed Subset of L by YELLOW_2:7;
A5: p preserves_sup_of X9 by A1,WAYBEL_0:def 37;
now
X c= the carrier of subrelstr Lk;
then X c= Lk by YELLOW_0:def 15;
then
A6: pk.:X = p.:X by RELAT_1:129;
assume ex_sup_of X,subrelstr Lk;
subrelstr Lk is infs-inheriting by WAYBEL_1:50;
then subrelstr Lk is complete LATTICE by YELLOW_2:30;
hence ex_sup_of pk.:X,subrelstr Lk by YELLOW_0:17;
A7: ex_sup_of X,L by YELLOW_0:17;
A8: subrelstr Lk is directed-sups-inheriting by A1,WAYBEL_1:52;
then
A9: dom pk = the carrier of subrelstr Lk & sup X9 = sup X by A4,A7,
FUNCT_2:def 1,WAYBEL_0:7;
ex_sup_of p.:X,L & pk.:X is directed Subset of subrelstr Lk by A3,A4,
YELLOW_0:17,YELLOW_2:15;
hence sup (pk.:X) = sup (p.:X) by A4,A8,A6,WAYBEL_0:7
.= p.sup X9 by A5,A7,WAYBEL_0:def 31
.= pk.sup X by A9,FUNCT_1:47;
end;
hence pk preserves_sup_of X by WAYBEL_0:def 31;
end;
then
A10: pk is directed-sups-preserving by WAYBEL_0:def 37;
subrelstr Lk is directed-sups-inheriting by A1,WAYBEL_1:52;
then
A11: subrelstr Lk is continuous LATTICE by A2,WAYBEL_5:28;
A12: the carrier of subrelstr rng p = rng p by YELLOW_0:def 15
.= rng pk by WAYBEL_1:44
.= the carrier of subrelstr rng pk by YELLOW_0:def 15;
subrelstr rng pk is full SubRelStr of L by Th1;
then
A13: Image p = Image pk by A12,YELLOW_0:57;
subrelstr Lk is complete by A2,YELLOW_2:30;
hence thesis by A11,A3,A13,A10,Th14;
end;
Lm4: for L be LATTICE holds (ex X be set, p be projection Function of
BoolePoset X,BoolePoset X st p is directed-sups-preserving & L,Image p
are_isomorphic) implies L is continuous
proof
let L be LATTICE;
given X be set, p be projection Function of BoolePoset X,BoolePoset X such
that
A1: p is directed-sups-preserving and
A2: L,Image p are_isomorphic;
Image p is continuous by A1,Th15;
hence thesis by A2,Th9,WAYBEL_1:6;
end;
theorem :: THEOREM 4.16. (1) iff (2)
for L be lower-bounded LATTICE holds L is continuous iff ex A be
arithmetic lower-bounded LATTICE, g be Function of A,L st g is onto & g is
infs-preserving & g is directed-sups-preserving
proof
let L be lower-bounded LATTICE;
thus L is continuous implies ex A be arithmetic lower-bounded LATTICE, g be
Function of A,L st g is onto & g is infs-preserving & g is
directed-sups-preserving by Lm2;
thus (ex A be arithmetic lower-bounded LATTICE, g be Function of A,L st g is
onto & g is infs-preserving & g is directed-sups-preserving) implies L is
continuous
proof
assume ex A be arithmetic lower-bounded LATTICE, g be Function of A,L st
g is onto & g is infs-preserving & g is directed-sups-preserving;
then ex X be non empty set, p be projection Function of BoolePoset X,
BoolePoset X st p is directed-sups-preserving & L,Image p are_isomorphic
by Lm3;
hence thesis by Lm4;
end;
end;
theorem :: THEOREM 4.16. (1) iff (3)
for L be lower-bounded LATTICE holds L is continuous iff ex A be
algebraic lower-bounded LATTICE, g be Function of A,L st g is onto & g is
infs-preserving & g is directed-sups-preserving
proof
let L be lower-bounded LATTICE;
thus L is continuous implies ex A be algebraic lower-bounded LATTICE, g be
Function of A,L st g is onto & g is infs-preserving & g is
directed-sups-preserving
proof
assume L is continuous;
then
ex A be arithmetic lower-bounded LATTICE, g be Function of A,L st g is
onto & g is infs-preserving & g is directed-sups-preserving by Lm2;
hence thesis;
end;
thus (ex A be algebraic lower-bounded LATTICE, g be Function of A,L st g is
onto & g is infs-preserving & g is directed-sups-preserving) implies L is
continuous
proof
assume ex A be algebraic lower-bounded LATTICE, g be Function of A,L st g
is onto & g is infs-preserving & g is directed-sups-preserving;
then ex X be non empty set, p be projection Function of BoolePoset X,
BoolePoset X st p is directed-sups-preserving & L,Image p are_isomorphic
by Lm3;
hence thesis by Lm4;
end;
end;
theorem :: THEOREM 4.16. (1) iff (4)
for L be lower-bounded LATTICE holds ( L is continuous implies ex X be
non empty set, p be projection Function of BoolePoset X,BoolePoset X st p is
directed-sups-preserving & L,Image p are_isomorphic ) & (( ex X be set, p be
projection Function of BoolePoset X,BoolePoset X st p is
directed-sups-preserving & L,Image p are_isomorphic ) implies L is continuous )
proof
let L be lower-bounded LATTICE;
thus L is continuous implies ex X be non empty set, p be projection Function
of BoolePoset X,BoolePoset X st p is directed-sups-preserving & L,Image p
are_isomorphic
proof
assume L is continuous;
then
ex A be arithmetic lower-bounded LATTICE, g be Function of A,L st g is
onto & g is infs-preserving & g is directed-sups-preserving by Lm2;
hence thesis by Lm3;
end;
thus thesis by Lm4;
end;
begin :: Atoms Elements
theorem
for L be non empty RelStr for x be Element of L holds x in PRIME (L
opp) iff x is co-prime
proof
let L be non empty RelStr;
let x be Element of L;
hereby
assume x in PRIME (L opp);
then x~ in PRIME (L opp) by LATTICE3:def 6;
then x~ is prime by WAYBEL_6:def 7;
hence x is co-prime by WAYBEL_6:def 8;
end;
assume x is co-prime;
then x~ is prime by WAYBEL_6:def 8;
then x~ in PRIME (L opp) by WAYBEL_6:def 7;
hence thesis by LATTICE3:def 6;
end;
definition
let L be non empty RelStr;
let a be Element of L;
attr a is atom means
Bottom L < a & for b be Element of L st Bottom L < b & b <= a holds b = a;
end;
definition
let L be non empty RelStr;
func ATOM L -> Subset of L means
:Def2:
for x be Element of L holds x in it iff x is atom;
existence
proof
defpred P[Element of L] means $1 is atom;
consider X be Subset of L such that
A1: for x be Element of L holds x in X iff P[x] from SUBSET_1:sch 3;
take X;
thus thesis by A1;
end;
uniqueness
proof
let A1,A2 be Subset of L such that
A2: for x be Element of L holds x in A1 iff x is atom and
A3: for x be Element of L holds x in A2 iff x is atom;
for x being object holds x in A1 iff x in A2 by A2,A3;
hence thesis by TARSKI:2;
end;
end;
theorem Th20:
for L be Boolean LATTICE for a be Element of L holds a is atom
iff a is co-prime & a <> Bottom L
proof
let L be Boolean LATTICE;
let a be Element of L;
thus a is atom implies a is co-prime & a <> Bottom L
proof
assume
A1: a is atom;
now
let x,y be Element of L;
assume that
A2: a <= x "\/" y and
A3: not a <= x;
A4: a "/\" x <= a by YELLOW_0:23;
a "/\" x <> a by A3,YELLOW_0:25;
then not Bottom L < a "/\" x by A1,A4;
then
A5: (not Bottom L <= a "/\" x) or not Bottom L <> a "/\" x by ORDERS_2:def 6;
a = a "/\" (x "\/" y) by A2,YELLOW_0:25
.= (a "/\" x) "\/" (a "/\" y) by WAYBEL_1:def 3
.= a "/\" y by A5,WAYBEL_1:3,YELLOW_0:44;
hence a <= y by YELLOW_0:25;
end;
hence a is co-prime by WAYBEL14:14;
thus thesis by A1;
end;
assume that
A6: a is co-prime and
A7: a <> Bottom L;
A8: now
let b be Element of L;
assume that
A9: Bottom L < b and
A10: b <= a;
consider c be Element of L such that
A11: c is_a_complement_of b by WAYBEL_1:def 24;
A12: b "/\" c = Bottom L by A11;
A13: not a <= c
by A10,ORDERS_2:3,A9,A12,YELLOW_0:25;
b "\/" c = Top L by A11;
then a <= b "\/" c by YELLOW_0:45;
then a <= b by A6,A13,WAYBEL14:14;
hence b = a by A10,ORDERS_2:2;
end;
Bottom L <= a by YELLOW_0:44;
then Bottom L < a by A7,ORDERS_2:def 6;
hence thesis by A8;
end;
registration
let L be Boolean LATTICE;
cluster atom -> co-prime for Element of L;
coherence by Th20;
end;
theorem
for L be Boolean LATTICE holds ATOM L = (PRIME (L opp)) \ {Bottom L}
proof
let L be Boolean LATTICE;
A1: (PRIME (L opp)) \ {Bottom L} c= ATOM L
proof
let x be object;
assume
A2: x in (PRIME (L opp)) \ {Bottom L};
then reconsider x9 = x as Element of (L opp);
x in PRIME (L opp) by A2,XBOOLE_0:def 5;
then
A3: x9 is prime by WAYBEL_6:def 7;
not x in {Bottom L} by A2,XBOOLE_0:def 5;
then x9 <> Bottom L by TARSKI:def 1;
then
A4: ~x9 <> Bottom L by LATTICE3:def 7;
(~x9)~ = ~x9 by LATTICE3:def 6
.= x9 by LATTICE3:def 7;
then ~x9 is co-prime by A3,WAYBEL_6:def 8;
then ~x9 is atom by A4,Th20;
then ~x9 in ATOM L by Def2;
hence thesis by LATTICE3:def 7;
end;
ATOM L c= (PRIME (L opp)) \ {Bottom L}
proof
let x be object;
assume
A5: x in ATOM L;
then reconsider x9 = x as Element of L;
A6: x9 is atom by A5,Def2;
then x9~ is prime by WAYBEL_6:def 8;
then x9~ in PRIME (L opp) by WAYBEL_6:def 7;
then
A7: x in PRIME (L opp) by LATTICE3:def 6;
x <> Bottom L by A6;
then not x in {Bottom L} by TARSKI:def 1;
hence thesis by A7,XBOOLE_0:def 5;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
for L be Boolean LATTICE for x,a be Element of L st a is atom holds a
<= x iff not a <= 'not' x
proof
let L be Boolean LATTICE;
let x,a be Element of L;
assume
A1: a is atom;
thus a <= x implies not a <= 'not' x
proof
assume that
A2: a <= x and
A3: a <= 'not' x;
a = a "\/" Bottom L by WAYBEL_1:3
.= a "\/" (x "/\" 'not' x) by YELLOW_5:34
.= (a "\/" x) "/\" ('not' x "\/" a) by WAYBEL_1:5
.= x "/\" ('not' x "\/" a) by A2,YELLOW_0:24
.= x "/\" 'not' x by A3,YELLOW_0:24
.= Bottom L by YELLOW_5:34;
hence contradiction by A1;
end;
thus not a <= 'not' x implies a <= x
proof
a <= Top L by YELLOW_0:45;
then
A4: a <= (x "\/" 'not' x) by YELLOW_5:34;
assume ( not a <= 'not' x)& not a <= x;
hence contradiction by A1,A4,WAYBEL14:14;
end;
end;
theorem Th23:
for L be complete Boolean LATTICE for X be Subset of L for x be
Element of L holds x "/\" sup X = "\/"({x"/\"y where y is Element of L: y in X}
,L)
proof
let L be complete Boolean LATTICE;
let X be Subset of L;
let x be Element of L;
for y be Element of L holds y "/\" is lower_adjoint by WAYBEL_1:def 19;
hence thesis by WAYBEL_1:64;
end;
theorem Th24:
for L be lower-bounded with_infima antisymmetric non empty
RelStr for x,y be Element of L st x is atom & y is atom & x <> y holds x "/\" y
= Bottom L
proof
let L be lower-bounded with_infima antisymmetric non empty RelStr;
let x,y be Element of L;
assume that
A1: x is atom and
A2: y is atom and
A3: x <> y and
A4: x "/\" y <> Bottom L;
Bottom L <= x "/\" y by YELLOW_0:44;
then
A5: Bottom L < x "/\" y by A4,ORDERS_2:def 6;
A6: x "/\" y <= y by YELLOW_0:23;
x "/\" y <= x by YELLOW_0:23;
then x = x "/\" y by A1,A5
.= y by A2,A5,A6;
hence contradiction by A3;
end;
theorem Th25:
for L be complete Boolean LATTICE for x be Element of L for A be
Subset of L st A c= ATOM L holds x in A iff x is atom & x <= sup A
proof
let L be complete Boolean LATTICE;
let x be Element of L;
let A be Subset of L;
assume
A1: A c= ATOM L;
thus x in A implies x is atom & x <= sup A
proof
assume
A2: x in A;
hence x is atom by A1,Def2;
sup A is_>=_than A by YELLOW_0:32;
hence thesis by A2,LATTICE3:def 9;
end;
thus x is atom & x <= sup A implies x in A
proof
assume that
A3: x is atom and
A4: x <= sup A and
A5: not x in A;
now
let b be Element of L;
assume b in { x "/\" y where y is Element of L: y in A };
then consider y be Element of L such that
A6: b = x "/\" y and
A7: y in A;
y is atom by A1,A7,Def2;
hence b <= Bottom L by A3,A5,A6,A7,Th24;
end;
then
A8: Bottom L is_>=_than { x "/\" y where y is Element of L: y in A } by
LATTICE3:def 9;
x = x "/\" sup A by A4,YELLOW_0:25
.= "\/"({ x "/\" y where y is Element of L: y in A },L) by Th23;
then x <= Bottom L by A8,YELLOW_0:32;
then x = Bottom L by YELLOW_5:19;
hence contradiction by A3;
end;
end;
theorem Th26:
for L be complete Boolean LATTICE for X,Y be Subset of L st X c=
ATOM L & Y c= ATOM L holds X c= Y iff sup X <= sup Y
proof
let L be complete Boolean LATTICE;
let X,Y be Subset of L;
assume that
A1: X c= ATOM L and
A2: Y c= ATOM L;
thus X c= Y implies sup X <= sup Y
proof
A3: ex_sup_of X,L & ex_sup_of Y,L by YELLOW_0:17;
assume X c= Y;
hence thesis by A3,YELLOW_0:34;
end;
thus sup X <= sup Y implies X c= Y
proof
assume
A4: sup X <= sup Y;
thus X c= Y
proof
let z be object;
assume
A5: z in X;
then reconsider z1 = z as Element of L;
sup X is_>=_than X by YELLOW_0:32;
then z1 <= sup X by A5,LATTICE3:def 9;
then
A6: z1 <= sup Y by A4,ORDERS_2:3;
z1 is atom by A1,A5,Def2;
hence thesis by A2,A6,Th25;
end;
end;
end;
Lm5: for L be Boolean LATTICE holds L is completely-distributive implies ( L
is complete & for x be Element of L ex X be Subset of L st X c= ATOM L & x =
sup X )
proof
let L be Boolean LATTICE;
assume
A1: L is completely-distributive;
hence L is complete;
let x be Element of L;
consider X1 be Subset of L such that
A2: x = sup X1 and
A3: for y be Element of L st y in X1 holds y is co-prime by A1,WAYBEL_6:38;
reconsider X = X1 \ {Bottom L} as Subset of L;
A4: now
let b be Element of L;
assume
A5: b is_>=_than X;
now
let c be Element of L;
assume
A6: c in X1;
now
per cases;
suppose
c <> Bottom L;
then not c in {Bottom L} by TARSKI:def 1;
then c in X by A6,XBOOLE_0:def 5;
hence c <= b by A5,LATTICE3:def 9;
end;
suppose
c = Bottom L;
hence c <= b by YELLOW_0:44;
end;
end;
hence c <= b;
end;
then b is_>=_than X1 by LATTICE3:def 9;
hence x <= b by A1,A2,YELLOW_0:32;
end;
take X;
thus X c= ATOM L
proof
let z be object;
assume
A7: z in X;
then reconsider z9 = z as Element of L;
not z in {Bottom L} by A7,XBOOLE_0:def 5;
then
A8: z9 <> Bottom L by TARSKI:def 1;
z in X1 by A7,XBOOLE_0:def 5;
then z9 is co-prime by A3;
then z9 is atom by A8,Th20;
hence thesis by Def2;
end;
A9: x is_>=_than X1 by A1,A2,YELLOW_0:32;
now
let c be Element of L;
assume c in X;
then c in X1 by XBOOLE_0:def 5;
hence c <= x by A9,LATTICE3:def 9;
end;
then x is_>=_than X by LATTICE3:def 9;
hence thesis by A1,A4,YELLOW_0:32;
end;
Lm6: for L be Boolean LATTICE holds ( L is complete & for x be Element of L ex
X be Subset of L st X c= ATOM L & x = sup X ) implies ex Y be set st L,
BoolePoset Y are_isomorphic
proof
let L be Boolean LATTICE;
assume that
A1: L is complete and
A2: for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X;
defpred P[set,set] means ex x9 be Subset of L st x9 = $1 & $2 = sup x9;
take Y = ATOM L;
A3: for x be Element of BoolePoset Y ex y be Element of L st P[x, y]
proof
let x be Element of BoolePoset Y;
x c= Y by WAYBEL_8:26;
then reconsider x9 = x as Subset of L by XBOOLE_1:1;
take sup x9;
take x9;
thus thesis;
end;
consider f be Function of BoolePoset Y,L such that
A4: for x be Element of BoolePoset Y holds P[x, f.x] from FUNCT_2:sch 3
(A3 );
A5: now
let z,v be Element of BoolePoset Y;
consider z9 be Subset of L such that
A6: z9 = z and
A7: f.z = sup z9 by A4;
consider v9 be Subset of L such that
A8: v9 = v and
A9: f.v = sup v9 by A4;
A10: ex_sup_of z9,L & ex_sup_of v9,L by A1,YELLOW_0:17;
thus z <= v implies f.z <= f.v
by YELLOW_1:2,A6,A7,A8,A9,A10,YELLOW_0:34;
A11: v9 c= ATOM L by A8,WAYBEL_8:26;
A12: z9 c= ATOM L by A6,WAYBEL_8:26;
thus f.z <= f.v implies z <= v
proof
assume f.z <= f.v;
then z c= v by A1,A6,A7,A8,A9,A12,A11,Th26;
hence thesis by YELLOW_1:2;
end;
end;
the carrier of L c= rng f
proof
let k be object;
assume k in the carrier of L;
then consider K be Subset of L such that
A13: K c= ATOM L and
A14: k = sup K by A2;
A15: K is Element of BoolePoset Y by A13,WAYBEL_8:26;
then K in the carrier of BoolePoset Y;
then
A16: K in dom f by FUNCT_2:def 1;
ex K9 be Subset of L st K9 = K & f.K = sup K9 by A4,A15;
hence thesis by A14,A16,FUNCT_1:def 3;
end;
then
A17: rng f = the carrier of L by XBOOLE_0:def 10;
now
let z,v be Element of BoolePoset Y;
assume
A18: f.z = f.v;
consider z9 be Subset of L such that
A19: z9 = z and
A20: f.z = sup z9 by A4;
consider v9 be Subset of L such that
A21: v9 = v and
A22: f.v = sup v9 by A4;
A23: v9 c= ATOM L by A21,WAYBEL_8:26;
z9 c= ATOM L by A19,WAYBEL_8:26;
then z c= v & v c= z by A1,A19,A20,A21,A22,A23,A18,Th26;
hence z = v by XBOOLE_0:def 10;
end;
then f is one-to-one;
then f is isomorphic by A17,A5,WAYBEL_0:66;
then BoolePoset Y,L are_isomorphic;
hence thesis by WAYBEL_1:6;
end;
begin :: More on the Boolean Lattice
theorem
for L be Boolean LATTICE holds L is arithmetic iff ex X be set st L,
BoolePoset X are_isomorphic
proof
let L be Boolean LATTICE;
hereby
assume
A1: L is arithmetic;
then L opp is continuous by Th9,YELLOW_7:38;
then L is completely-distributive by A1,WAYBEL_6:39;
then for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X
by Lm5;
hence ex X be set st L,BoolePoset X are_isomorphic by A1,Lm6;
end;
thus thesis by Th10,WAYBEL_1:6;
end;
theorem :: THEOREM 4.18. (2) iff (3)
for L be Boolean LATTICE holds L is arithmetic iff L is algebraic
proof
let L be Boolean LATTICE;
thus L is arithmetic implies L is algebraic;
assume
A1: L is algebraic;
then L opp is continuous by Th9,YELLOW_7:38;
then L is completely-distributive by A1,WAYBEL_6:39;
then
for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X by Lm5;
then ex X be set st L,BoolePoset X are_isomorphic by A1,Lm6;
hence thesis by Th10,WAYBEL_1:6;
end;
theorem :: THEOREM 4.18. (2) iff (4)
for L be Boolean LATTICE holds L is arithmetic iff L is continuous
proof
let L be Boolean LATTICE;
thus L is arithmetic implies L is continuous;
assume
A1: L is continuous;
then L opp is continuous by Th9,YELLOW_7:38;
then L is completely-distributive by A1,WAYBEL_6:39;
then
for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X by Lm5;
then ex X be set st L,BoolePoset X are_isomorphic by A1,Lm6;
hence thesis by Th10,WAYBEL_1:6;
end;
theorem :: THEOREM 4.18. (2) iff (5)
for L be Boolean LATTICE holds L is arithmetic iff L is continuous & L
opp is continuous
proof
let L be Boolean LATTICE;
thus L is arithmetic implies L is continuous & L opp is continuous by Th9,
YELLOW_7:38;
assume that
A1: L is continuous and
A2: L opp is continuous;
L is completely-distributive by A1,A2,WAYBEL_6:39;
then
for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X by Lm5;
then ex X be set st L,BoolePoset X are_isomorphic by A1,Lm6;
hence thesis by Th10,WAYBEL_1:6;
end;
theorem :: THEOREM 4.18. (2) iff (6)
for L be Boolean LATTICE holds L is arithmetic iff L is
completely-distributive
proof
let L be Boolean LATTICE;
thus L is arithmetic implies L is completely-distributive
proof
assume
A1: L is arithmetic;
then L opp is continuous by Th9,YELLOW_7:38;
hence thesis by A1,WAYBEL_6:39;
end;
assume
A2: L is completely-distributive;
then
for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X by Lm5;
then ex X be set st L,BoolePoset X are_isomorphic by A2,Lm6;
hence thesis by Th10,WAYBEL_1:6;
end;
theorem :: THEOREM 4.18. (2) iff (7)
for L be Boolean LATTICE holds L is arithmetic iff ( L is complete &
for x be Element of L ex X be Subset of L st X c= ATOM L & x = sup X )
proof
let L be Boolean LATTICE;
hereby
assume
A1: L is arithmetic;
then L opp is continuous by Th9,YELLOW_7:38;
then L is completely-distributive by A1,WAYBEL_6:39;
hence L is complete & for x be Element of L ex X be Subset of L st X c=
ATOM L & x = sup X by Lm5;
end;
assume L is complete & for x be Element of L ex X be Subset of L st X c=
ATOM L & x = sup X;
then ex X be set st L,BoolePoset X are_isomorphic by Lm6;
hence thesis by Th10,WAYBEL_1:6;
end;