:: Irreducible and Prime Elements
:: by Beata Madras
::
:: Received December 1, 1996
:: Copyright (c) 1996-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 WAYBEL_0, SUBSET_1, XBOOLE_0, ORDERS_2, FUNCT_1, RELAT_1, TARSKI,
NUMBERS, FUNCT_7, TREES_2, RELAT_2, XXREAL_0, STRUCT_0, ORDINAL2,
LATTICES, ORDERS_1, ZFMISC_1, YELLOW_0, EQREL_1, REWRITE1, FUNCOP_1,
LATTICE3, SEQM_3, WAYBEL_2, WAYBEL_3, CARD_FIL, SETFAM_1, ARYTM_3,
CARD_1, NAT_1, ORDINAL1, YELLOW_8, FINSET_1, INT_2, YELLOW_1, FUNCT_3,
LATTICE2, ARYTM_0, WAYBEL_5, PBOOLE, YELLOW_2, FUNCT_6, CARD_3, WAYBEL_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, FINSET_1, RELAT_1, RELAT_2, ORDERS_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, DOMAIN_1, FUNCOP_1, STRUCT_0, ORDERS_2, CARD_3, LATTICE3,
FUNCT_3, FUNCT_6, PBOOLE, YELLOW_0, YELLOW_1, WAYBEL_0, WAYBEL_1,
YELLOW_2, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, YELLOW_7,
FUNCT_7, ABIAN, XXREAL_0;
constructors SETFAM_1, XXREAL_0, NAT_1, FUNCT_7, BORSUK_1, PRALG_2, ORDERS_3,
WAYBEL_1, YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_4, WAYBEL_5, RELSET_1,
NUMBERS, ABIAN;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCOP_1, FINSET_1, PBOOLE,
STRUCT_0, ORDERS_2, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, WAYBEL_1,
YELLOW_4, WAYBEL_2, WAYBEL_3, WAYBEL_5, YELLOW_7, ORDINAL1, RELSET_1,
XXREAL_0, RELAT_1, XCMPLX_0, NAT_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, RELAT_2, LATTICE3, WAYBEL_0, WAYBEL_1, WAYBEL_2, WAYBEL_5,
FUNCT_1, ORDERS_3, XBOOLE_0;
equalities RELAT_1, LATTICE3, WAYBEL_0, SUBSET_1, STRUCT_0;
expansions TARSKI, RELAT_2, LATTICE3, WAYBEL_0, WAYBEL_1, XBOOLE_0, ORDINAL1;
theorems WAYBEL_3, TARSKI, YELLOW_0, ZFMISC_1, WAYBEL_0, ORDERS_2, WAYBEL_4,
FUNCT_2, FUNCT_1, LATTICE3, NAT_1, WAYBEL_1, YELLOW_1, YELLOW_5,
WAYBEL_2, YELLOW_2, WAYBEL_5, CARD_3, FUNCT_6, YELLOW_7, ORDERS_1,
FUNCT_3, YELLOW_4, YELLOW_3, FUNCOP_1, RELAT_1, RELSET_1, ORDINAL1,
XBOOLE_0, XBOOLE_1, FUNCT_7, CARD_1, PARTFUN1;
schemes FUNCT_1, FINSET_1, CLASSES1, NAT_1, FUNCT_2, YELLOW_3, SUBSET_1;
begin
reserve x,y,Y,Z for set,
L for LATTICE,
l for Element of L;
:: Preliminaries
scheme
NonUniqExD1 { Z() ->non empty RelStr, X() -> Subset of Z(), Y() -> non empty
Subset of Z(), P[object,object] }:
ex f being Function of X(),Y() st for e be Element
of Z() st e in X() ex u be Element of Z() st u in Y() & u = f.e & P[e,u]
provided
A1: for e be Element of Z() st e in X() ex u be Element of Z() st u in Y
() & P[e,u]
proof
A2: for e be object st e in X() ex u be object st u in Y() & P[e,u]
proof
let e be object;
assume
A3: e in X();
then reconsider e1 = e as Element of X();
reconsider e1 as Element of Z() by A3;
consider u be Element of Z() such that
A4: u in Y() & P[e1,u] by A1,A3;
reconsider u1 = u as set;
take u1;
thus thesis by A4;
end;
consider f being Function such that
A5: dom f = X() & rng f c= Y() and
A6: for e be object st e in X() holds P[e,f.e] from FUNCT_1:sch 6(A2);
reconsider f as Function of X(),Y() by A5,FUNCT_2:def 1,RELSET_1:4;
take f;
for e be Element of Z() st e in X() ex u be Element of Z() st u in Y() &
u = f.e & P[e,u]
proof
let e be Element of Z();
assume
A7: e in X();
then reconsider e1 = f.e as Element of Y() by FUNCT_2:5;
reconsider fe = e1 as Element of Z();
take fe;
thus thesis by A6,A7;
end;
hence thesis;
end;
definition
let L be non empty 1-sorted;
let C,D be non empty Subset of L;
let f be Function of C,D;
let c be Element of C;
redefine func f.c -> Element of L; :: redefines . (FUNCT_1, definition)
coherence
proof
f.c in D;
hence thesis;
end;
end;
registration
let L be non empty Poset;
cluster -> filtered directed for Chain of L;
coherence
proof
let C be Chain of L;
A1: the InternalRel of L is_strongly_connected_in C by ORDERS_2:def 7;
thus C is filtered
proof
let x,y be Element of L;
A2: x <= x & y <= y;
assume
A3: x in C & y in C;
then
[x,y] in the InternalRel of L or [y,x] in the InternalRel of L by A1;
then x <= y or y <= x by ORDERS_2:def 5;
hence thesis by A3,A2;
end;
let x,y be Element of L;
A4: x <= x & y <= y;
assume
A5: x in C & y in C;
then
[x,y] in the InternalRel of L or [y,x] in the InternalRel of L by A1;
then x <= y or y <= x by ORDERS_2:def 5;
hence thesis by A5,A4;
end;
end;
registration
cluster strict continuous distributive lower-bounded for LATTICE;
existence
proof
set x1 = the set,R = the Order of {x1};
take RelStr(#{x1},R#);
thus thesis;
end;
end;
theorem Th1:
for S,T being Semilattice, f being Function of S,T holds f is meet-preserving
iff for x,y being Element of S holds f.(x "/\" y) = f.x "/\" f.y
proof
let S,T be Semilattice, f be Function of S,T;
A1: dom f = the carrier of S by FUNCT_2:def 1;
thus f is meet-preserving implies for x,y being Element of S holds f.(x "/\"
y) = f. x "/\" f.y
proof
assume
A2: f is meet-preserving;
let z,y be Element of S;
A3: f preserves_inf_of {z,y} by A2;
A4: f.:{z,y} = {f.z,f.y} & ex_inf_of {z,y},S by A1,FUNCT_1:60,YELLOW_0:21;
thus f.(z "/\" y) = f.inf {z,y} by YELLOW_0:40
.= inf({f.z,f.y}) by A4,A3
.= f.z "/\" f.y by YELLOW_0:40;
end;
assume
A5: for x,y being Element of S holds f.(x "/\" y) = f. x "/\" f.y;
for z,y being Element of S holds f preserves_inf_of {z,y}
proof
let z,y be Element of S;
A6: f.:{z,y} = {f.z,f.y} by A1,FUNCT_1:60;
then
A7: ex_inf_of {z,y},S implies ex_inf_of f.:{z,y},T by YELLOW_0:21;
inf (f.:{z,y}) = f.z "/\" f.y by A6,YELLOW_0:40
.= f.(z "/\" y) by A5
.= f.inf {z,y} by YELLOW_0:40;
hence thesis by A7;
end;
hence thesis;
end;
theorem Th2:
for S,T being sup-Semilattice, f being Function of S,T holds f is
join-preserving iff for x,y being Element of S holds f.(x "\/" y) = f. x "\/" f
.y
proof
let S,T be sup-Semilattice, f be Function of S,T;
A1: dom f = the carrier of S by FUNCT_2:def 1;
thus f is join-preserving implies for x,y being Element of S holds f.(x "\/"
y) = f. x "\/" f.y
proof
assume
A2: f is join-preserving;
let z,y be Element of S;
A3: f preserves_sup_of {z,y} by A2;
A4: f.:{z,y} = {f.z,f.y} & ex_sup_of {z,y},S by A1,FUNCT_1:60,YELLOW_0:20;
thus f.(z "\/" y) = f.sup {z,y} by YELLOW_0:41
.= sup ({f.z,f.y}) by A4,A3
.= f.z "\/" f.y by YELLOW_0:41;
end;
assume
A5: for x,y being Element of S holds f.(x "\/" y) = f. x "\/" f.y;
for z,y being Element of S holds f preserves_sup_of {z,y}
proof
let z,y be Element of S;
A6: f.:{z,y} = {f.z,f.y} by A1,FUNCT_1:60;
then
A7: ex_sup_of {z,y},S implies ex_sup_of f.:{z,y},T by YELLOW_0:20;
sup (f.:{z,y}) = f.z "\/" f.y by A6,YELLOW_0:41
.= f.(z "\/" y) by A5
.= f.sup {z,y} by YELLOW_0:41;
hence thesis by A7;
end;
hence thesis;
end;
theorem Th3:
for S,T being LATTICE, f being Function of S,T st T is
distributive & f is meet-preserving join-preserving one-to-one holds S is
distributive
proof
let S,T be LATTICE, f be Function of S,T;
assume that
A1: T is distributive and
A2: f is meet-preserving join-preserving one-to-one;
let x,y,z be Element of S;
f.( x "/\" (y "\/" z)) = f. x "/\" f.(y "\/" z) by A2,Th1
.= f. x "/\" (f.y "\/" f.z) by A2,Th2
.= (f.x "/\" f.y) "\/" (f.x "/\" f.z) by A1
.= (f.x "/\" f.y) "\/" f.(x "/\" z) by A2,Th1
.= f.(x "/\" y) "\/" f.(x "/\" z) by A2,Th1
.= f.((x "/\" y) "\/" (x "/\" z))by A2,Th2;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A2;
end;
registration
let S,T be complete LATTICE;
cluster sups-preserving for Function of S,T;
existence
proof
set t = Bottom T;
set f = S --> t;
take f;
let X be Subset of S;
assume ex_sup_of X,S;
thus ex_sup_of f.:X,T by YELLOW_0:17;
(f.:X) c= rng f & rng f c= {t} by FUNCOP_1:13,RELAT_1:111;
then (f.:X) c= {t};
then
A1: (f.:X) = {t} or (f.:X) = {} by ZFMISC_1:33;
per cases;
suppose
X = {};
then (f.:X) = {};
then sup (f.:X) = t by YELLOW_0:def 11;
hence thesis;
end;
suppose
X <> {};
then reconsider X1 = X as non empty Subset of S;
set x = the Element of X1;
f.x in (f.:X) by FUNCT_2:35;
hence sup (f.:X) = t by A1,YELLOW_0:39
.= f.sup X;
end;
end;
end;
Lm1: for S,T being with_suprema non empty Poset for f being Function of S, T
holds f is directed-sups-preserving implies f is monotone
proof
let S,T be with_suprema non empty Poset;
let f be Function of S, T;
assume
A1: f is directed-sups-preserving;
let x, y be Element of S such that
A2: x <= y;
A3: y = y"\/"x by A2,YELLOW_0:24;
for a, b being Element of S st a in {x, y} & b in {x, y} ex z being
Element of S st z in {x, y} & a <= z & b <= z
proof
let a, b be Element of S such that
A4: a in {x, y} & b in {x, y};
take y;
thus y in {x, y} by TARSKI:def 2;
thus thesis by A2,A4,TARSKI:def 2;
end;
then {x, y} is directed non empty;
then
A5: f preserves_sup_of {x, y} by A1;
A6: dom f = the carrier of S by FUNCT_2:def 1;
y <= y;
then
A7: {x, y} is_<=_than y by A2,YELLOW_0:8;
for b being Element of S st {x, y} is_<=_than b holds y <= b by YELLOW_0:8;
then ex_sup_of {x, y},S by A7,YELLOW_0:30;
then sup(f.:{x, y}) = f.sup{x, y} by A5
.= f.y by A3,YELLOW_0:41;
then
A8: f.y = sup{f.x, f.y} by A6,FUNCT_1:60
.= f.y"\/"f.x by YELLOW_0:41;
let afx, bfy be Element of T;
assume afx = f.x & bfy = f.y;
hence afx <= bfy by A8,YELLOW_0:22;
end;
theorem Th4:
for S,T being complete LATTICE, f being sups-preserving Function
of S,T st T is meet-continuous & f is meet-preserving one-to-one holds S is
meet-continuous
proof
let S,T be complete LATTICE, f be sups-preserving Function of S,T;
assume that
A1: T is meet-continuous and
A2: f is meet-preserving one-to-one;
S is satisfying_MC
proof
let x be Element of S, D be non empty directed Subset of S;
A3: ex_sup_of D,S & f preserves_sup_of D by WAYBEL_0:75,def 33;
reconsider Y = {x} as directed non empty Subset of S by WAYBEL_0:5;
A4: ex_sup_of Y"/\"D,S & f preserves_sup_of {x}"/\"D by WAYBEL_0:75,def 33;
reconsider X = f.:D as directed Subset of T by Lm1,YELLOW_2:15;
A5: dom f = the carrier of S by FUNCT_2:def 1;
A6: {f.x} "/\" (f.:D) = {(f.x) "/\" y where y is Element of T: y in (f.:D)
} by YELLOW_4:42;
A7: {f.x} "/\" (f.:D) c= f.:({x}"/\"D)
proof
let p be object;
assume p in {f.x} "/\" (f.:D);
then consider y be Element of T such that
A8: p = (f.x) "/\" y and
A9: y in (f .:D) by A6;
consider k be object such that
A10: k in dom f and
A11: k in D and
A12: y = f.k by A9,FUNCT_1:def 6;
reconsider k as Element of S by A10;
(x "/\" k) in {x "/\" a where a is Element of S: a in D} by A11;
then
A13: (x "/\" k) in ({x} "/\" D) by YELLOW_4:42;
f preserves_inf_of {x,k} by A2;
then p = f.(x "/\" k) by A8,A12,YELLOW_3:8;
hence thesis by A5,A13,FUNCT_1:def 6;
end;
A14: {x} "/\" D = {x "/\" y where y is Element of S: y in D} by YELLOW_4:42;
A15: f.:({x}"/\"D) c= {f.x} "/\" (f.:D)
proof
let p be object;
assume p in f.:({x}"/\"D);
then consider m be object such that
A16: m in dom f and
A17: m in ({x} "/\" D) and
A18: p = f.m by FUNCT_1:def 6;
reconsider m as Element of S by A16;
consider a be Element of S such that
A19: m = x "/\" a and
A20: a in D by A14,A17;
reconsider fa = f.a as Element of T;
f preserves_inf_of {x,a} by A2;
then
A21: p = (f.x) "/\" fa by A18,A19,YELLOW_3:8;
fa in f.:D by A5,A20,FUNCT_1:def 6;
hence thesis by A6,A21;
end;
f.(x "/\" sup D) = (f.x) "/\" (f.sup D) by A2,Th1
.= (f.x) "/\" sup X by A3
.= sup ({f.x} "/\" X) by A1,WAYBEL_2:def 6
.= sup (f.:({x} "/\" D)) by A7,A15,XBOOLE_0:def 10
.= f.(sup ({x} "/\" D)) by A4;
hence x "/\" sup D = sup ({x} "/\" D) by A2;
end;
hence thesis;
end;
begin :: Open sets
definition
let L be non empty reflexive RelStr, X be Subset of L;
attr X is Open means
:Def1:
for x be Element of L st x in X ex y be Element of L st y in X & y << x;
end;
theorem
for L be up-complete LATTICE, X be upper Subset of L holds X is Open
iff for x be Element of L st x in X holds waybelow x meets X
proof
let L be up-complete LATTICE, X be upper Subset of L;
hereby
assume
A1: X is Open;
thus for x be Element of L st x in X holds waybelow x meets X
proof
let x be Element of L;
assume x in X;
then consider y be Element of L such that
A2: y in X and
A3: y << x by A1;
y in {y1 where y1 is Element of L: y1 << x} by A3;
then y in waybelow x by WAYBEL_3:def 3;
hence thesis by A2,XBOOLE_0:3;
end;
end;
assume
A4: for x be Element of L st x in X holds waybelow x meets X;
now
let x1 be Element of L;
assume x1 in X;
then (waybelow x1) meets X by A4;
then consider y being object such that
A5: y in (waybelow x1) and
A6: y in X by XBOOLE_0:3;
waybelow x1 = {y1 where y1 is Element of L: y1 << x1} by WAYBEL_3:def 3;
then ex z be Element of L st z = y & z << x1 by A5;
hence ex z be Element of L st z in X & z << x1 by A6;
end;
hence thesis;
end;
theorem ::3.2, p.68
for L be up-complete LATTICE, X be upper Subset of L holds X is Open
iff X = union {wayabove x where x is Element of L : x in X}
proof
let L be up-complete LATTICE, X be upper Subset of L;
hereby
assume
A1: X is Open;
A2: X c= union {wayabove x where x is Element of L : x in X}
proof
let z be object;
assume
A3: z in X;
then reconsider x1 = z as Element of X;
reconsider x1 as Element of L by A3;
consider y be Element of L such that
A4: y in X and
A5: y << x1 by A1,A3;
x1 in {y1 where y1 is Element of L: y1 >> y} by A5;
then
A6: x1 in wayabove y by WAYBEL_3:def 4;
wayabove y in {wayabove x where x is Element of L : x in X} by A4;
hence thesis by A6,TARSKI:def 4;
end;
union {wayabove x where x is Element of L : x in X} c= X
proof
let z be object;
assume z in union {wayabove x where x is Element of L : x in X};
then consider Y be set such that
A7: z in Y and
A8: Y in {wayabove x where x is Element of L : x in X} by TARSKI:def 4;
consider x be Element of L such that
A9: Y = wayabove x and
A10: x in X by A8;
z in {y where y is Element of L: y >> x} by A7,A9,WAYBEL_3:def 4;
then consider z1 be Element of L such that
A11: z1 = z and
A12: z1 >> x;
x <= z1 by A12,WAYBEL_3:1;
hence thesis by A10,A11,WAYBEL_0:def 20;
end;
hence X = union {wayabove x where x is Element of L : x in X} by A2;
end;
assume
A13: X = union {wayabove x where x is Element of L : x in X};
now
let x1 be Element of L;
assume x1 in X;
then consider Y be set such that
A14: x1 in Y and
A15: Y in {wayabove x where x is Element of L : x in X} by A13,TARSKI:def 4;
consider x be Element of L such that
A16: Y = wayabove x and
A17: x in X by A15;
x1 in {y where y is Element of L: y >> x} by A14,A16,WAYBEL_3:def 4;
then ex z1 be Element of L st z1 = x1 & z1 >> x;
hence ex x be Element of L st x in X & x << x1 by A17;
end;
hence thesis;
end;
registration
let L be up-complete lower-bounded LATTICE;
cluster Open for Filter of L;
existence
proof
take [#]L;
now
let x be Element of L;
assume x in [#]L;
Bottom L << x by WAYBEL_3:4;
hence ex y be Element of L st y in [#]L & y << x;
end;
hence thesis;
end;
end;
theorem
for L be lower-bounded continuous LATTICE, x be Element of L holds (
wayabove x) is Open
proof
let L be lower-bounded continuous LATTICE, x be Element of L;
for l be Element of L st l in (wayabove x) ex y be Element of L st y in
(wayabove x) & y << l
proof
let l be Element of L;
assume l in (wayabove x);
then x << l by WAYBEL_3:8;
then consider y be Element of L such that
A1: x << y & y << l by WAYBEL_4:52;
take y;
thus thesis by A1,WAYBEL_3:8;
end;
hence thesis;
end;
theorem Th8: ::3.3, p.68
for L be lower-bounded continuous LATTICE, x,y be Element of L st
x << y holds ex F be Open Filter of L st y in F & F c= wayabove x
proof
let L be lower-bounded continuous LATTICE, x,y be Element of L;
defpred P[Element of L, Element of L] means $2 << $1;
assume
A1: x << y;
then reconsider W = (wayabove x) as non empty Subset of L by WAYBEL_3:8;
A2: for z be Element of L st z in W ex z1 be Element of L st z1 in W & P[z, z1]
proof
let z be Element of L;
assume z in W;
then x << z by WAYBEL_3:8;
then consider x9 be Element of L such that
A3: x << x9 and
A4: x9 << z by WAYBEL_4:52;
x9 in W by A3,WAYBEL_3:8;
hence thesis by A4;
end;
consider f be Function of W,W such that
A5: for z be Element of L st z in W ex z1 be Element of L st z1 in W &
z1 = f.z & P[z,z1] from NonUniqExD1(A2);
set V = {uparrow z where z is Element of L : ex n being Element of NAT st z
= iter(f,n).y};
now
let u1 be object;
assume u1 in V;
then ex z be Element of L st u1 = uparrow z & ex n being Element of NAT st
z = iter(f,n).y;
hence u1 in bool the carrier of L;
end;
then reconsider V as Subset-Family of L by TARSKI:def 3;
A6: for X,Y being Subset of L st X in V & Y in V ex Z being Subset of L st
Z in V & X \/ Y c= Z
proof
reconsider y1 = y as Element of W by A1,WAYBEL_3:8;
let X,Y be Subset of L;
assume that
A7: X in V and
A8: Y in V;
consider z2 be Element of L such that
A9: Y = uparrow z2 and
A10: ex n being Element of NAT st z2 = iter(f,n).y by A8;
consider n2 be Element of NAT such that
A11: z2 = iter(f,n2).y by A10;
consider z1 be Element of L such that
A12: X = uparrow z1 and
A13: ex n being Element of NAT st z1 = iter(f,n).y by A7;
set z = z1 "/\" z2;
consider n1 be Element of NAT such that
A14: z1 = iter(f,n1).y by A13;
A15: for n,k being Element of NAT
holds iter(f,n+k).y1 <= iter(f,n).y1
proof
let n be Element of NAT;
defpred P[Nat] means iter(f,n+In($1,NAT)).y1 <= iter(f,n).y1;
A16: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A17: iter(f,n+In(k,NAT)).y1 <= iter(f,n).y1;
set nk = iter(f,n+In(k,NAT)).y1;
nk in W by FUNCT_2:5;
then consider znk be Element of L such that
znk in W and
A18: znk = f.nk and
A19: znk << nk by A5;
dom iter(f,n+In(k,NAT)) = W by FUNCT_2:def 1;
then
A20: znk = (f*(iter(f,n+k))).y1 by A18,FUNCT_1:13
.= iter(f,n+k+1).y1 by FUNCT_7:71
.= iter(f,n+(k+1)).y1;
znk <= nk by A19,WAYBEL_3:1;
hence thesis by A17,A20,ORDERS_2:3;
end;
A21: P[ 0 ];
let k be Element of NAT;
for k being Nat holds P[k] from NAT_1:sch 2(A21,A16);
then P[k];
hence thesis;
end;
A22: now
per cases;
suppose
n1 <= n2;
then consider k being Nat such that
A23: n1 + k = n2 by NAT_1:10;
k in NAT by ORDINAL1:def 12;
then z2 <= z1 by A14,A11,A15,A23;
hence uparrow z in V by A8,A9,YELLOW_0:25;
end;
suppose
n2 <= n1;
then consider k being Nat such that
A24: n2 + k = n1 by NAT_1:10;
k in NAT by ORDINAL1:def 12;
then z1 <= z2 by A14,A11,A15,A24;
hence uparrow z in V by A7,A12,YELLOW_0:25;
end;
end;
z <= z2 by YELLOW_0:23;
then
A25: uparrow z2 c= uparrow z by WAYBEL_0:22;
z <= z1 by YELLOW_0:23;
then uparrow z1 c= uparrow z by WAYBEL_0:22;
hence thesis by A12,A9,A22,A25,XBOOLE_1:8;
end;
A26: for X being Subset of L st X in V holds X is filtered
proof
let X be Subset of L;
assume X in V;
then
ex z be Element of L st X = uparrow z & ex n being Element of NAT st z
= iter(f,n).y;
hence thesis;
end;
y <= y;
then
A27: y in uparrow y by WAYBEL_0:18;
set F = union {uparrow z where z is Element of L : ex n being Element of NAT
st z = iter(f,n).y};
now
let u1 be object;
assume u1 in F;
then consider Y be set such that
A28: u1 in Y and
A29: Y in {uparrow z where z is Element of L : ex n being Element of
NAT st z = iter(f,n).y} by TARSKI:def 4;
consider z be Element of L such that
A30: Y = uparrow z and
ex n being Element of NAT st z = iter(f,n).y by A29;
reconsider z1 = {z} as Subset of L;
u1 in {a where a is Element of L: ex b being Element of L st a >= b &
b in z1} by A28,A30,WAYBEL_0:15;
then
ex a be Element of L st a = u1 & ex b being Element of L st a >= b & b
in z1;
hence u1 in the carrier of L;
end;
then reconsider F as Subset of L by TARSKI:def 3;
A31: y in (wayabove x) by A1,WAYBEL_3:8;
A32: now
let u1 be Element of L;
assume u1 in F;
then consider Y be set such that
A33: u1 in Y and
A34: Y in {uparrow z where z is Element of L : ex n being Element of
NAT st z = iter(f,n).y} by TARSKI:def 4;
consider z be Element of L such that
A35: Y = uparrow z and
A36: ex n being Element of NAT st z = iter(f,n).y by A34;
consider n being Element of NAT such that
A37: z = iter(f,n).y by A36;
z in W by A31,A37,FUNCT_2:5;
then consider z9 be Element of L such that
z9 in W and
A38: z9 = f.z and
A39: z9 << z by A5;
z9 <= z9;
then
A40: z9 in uparrow z9 by WAYBEL_0:18;
dom iter(f,n) = W by FUNCT_2:def 1;
then z9 = (f*(iter(f,n))).y by A31,A37,A38,FUNCT_1:13
.= iter(f,n+1).y by FUNCT_7:71;
then
uparrow z9 in {uparrow p where p is Element of L : ex n being Element
of NAT st p = iter(f,n).y};
then
A41: z9 in F by A40,TARSKI:def 4;
reconsider z1 = {z} as Subset of L;
u1 in {a where a is Element of L: ex b being Element of L st a >= b &
b in z1} by A33,A35,WAYBEL_0:15;
then consider a be Element of L such that
A42: a = u1 and
A43: ex b being Element of L st a >= b & b in z1;
consider b being Element of L such that
A44: a >= b and
A45: b in z1 by A43;
b = z by A45,TARSKI:def 1;
hence ex g be Element of L st g in F & g << u1 by A42,A44,A39,A41,
WAYBEL_3:2;
end;
dom f = W by FUNCT_2:def 1;
then
A46: y in field f by A31,XBOOLE_0:def 3;
iter(f,0).y = (id(field f)).y by FUNCT_7:68
.= y by A46,FUNCT_1:18;
then
A47: uparrow y in {uparrow z where z is Element of L : ex n being Element of
NAT st z = iter(f,n).y};
for X being Subset of L st X in V holds X is upper
proof
let X be Subset of L;
assume X in V;
then
ex z be Element of L st X = uparrow z & ex n being Element of NAT st z
= iter(f,n).y;
hence thesis;
end;
then reconsider F as Open Filter of L by A27,A47,A26,A6,A32,Def1,TARSKI:def 4
,WAYBEL_0:28,47;
take F;
now
let u1 be object;
assume
A48: u1 in F;
then consider Y be set such that
A49: u1 in Y and
A50: Y in {uparrow z where z is Element of L : ex n being Element of
NAT st z = iter(f,n).y} by TARSKI:def 4;
reconsider u = u1 as Element of L by A48;
consider z be Element of L such that
A51: Y = uparrow z and
A52: ex n being Element of NAT st z = iter(f,n).y by A50;
z in wayabove x by A31,A52,FUNCT_2:5;
then
A53: x << z by WAYBEL_3:8;
z <= u by A49,A51,WAYBEL_0:18;
then x << u by A53,WAYBEL_3:2;
hence u1 in wayabove x by WAYBEL_3:8;
end;
hence thesis by A27,A47,TARSKI:def 4;
end;
theorem Th9: ::3.4, p.69
for L being complete LATTICE, X being Open upper Subset of L
holds for x being Element of L st x in (X`) ex m being Element of L st x <= m &
m is_maximal_in (X`)
proof
let L be complete LATTICE, X be Open upper Subset of L;
let x be Element of L;
set A = {C where C is Chain of L : C c= (X`) & x in C};
reconsider x1 = {x} as Chain of L by ORDERS_2:8;
A1: for Z be set st Z <> {} & Z c= A & Z is c=-linear holds union Z in A
proof
let Z be set;
assume that
A2: Z <> {} and
A3: Z c= A and
A4: Z is c=-linear;
now
let Y;
assume Y in Z;
then Y in A by A3;
then ex C be Chain of L st Y = C & C c= (X`) & x in C;
hence Y c= the carrier of L;
end;
then reconsider UZ = union Z as Subset of L by ZFMISC_1:76;
the InternalRel of L is_strongly_connected_in UZ
proof
let a,b be object;
assume that
A5: a in UZ and
A6: b in UZ;
consider az be set such that
A7: a in az and
A8: az in Z by A5,TARSKI:def 4;
consider bz be set such that
A9: b in bz and
A10: bz in Z by A6,TARSKI:def 4;
az, bz are_c=-comparable by A4,A8,A10;
then
A11: az c= bz or bz c= az;
bz in A by A3,A10;
then
A12: ex C be Chain of L st bz = C & C c= (X`) & x in C;
az in A by A3,A8;
then
A13: ex C be Chain of L st az = C & C c= (X`) & x in C;
reconsider bz as Chain of L by A12;
reconsider az as Chain of L by A13;
the InternalRel of L is_strongly_connected_in az & the InternalRel
of L is_strongly_connected_in bz by ORDERS_2:def 7;
hence thesis by A7,A9,A11;
end;
then reconsider UZ as Chain of L by ORDERS_2:def 7;
A14: now
let Y;
assume Y in Z;
then Y in A by A3;
then ex C be Chain of L st Y = C & C c= (X`) & x in C;
hence Y c= (X`);
end;
set Y = the Element of Z;
Y in Z by A2;
then Y in A by A3;
then ex C be Chain of L st Y = C & C c= (X`) & x in C;
then
A15: x in UZ by A2,TARSKI:def 4;
UZ c= (X`) by A14,ZFMISC_1:76;
hence thesis by A15;
end;
assume x in (X`);
then
A16: x1 c= (X`) by ZFMISC_1:31;
x in x1 by ZFMISC_1:31;
then x1 in A by A16;
then consider Y1 be set such that
A17: Y1 in A and
A18: for Z st Z in A & Z <> Y1 holds not Y1 c= Z by A1,ORDERS_1:67;
consider Y be Chain of L such that
A19: Y = Y1 and
A20: Y c= (X`) and
A21: x in Y by A17;
set m = sup Y;
m is_>=_than Y by YELLOW_0:32;
then
A22: x <= m by A21;
A23: m is_>=_than Y by YELLOW_0:32;
A24: now
given y being Element of L such that
A25: y in (X`) and
A26: y > m;
A27: not y in Y by A26,ORDERS_2:6,A23;
set Y2 = Y \/ {y};
A28: m <= y by A26,ORDERS_2:def 6;
the InternalRel of L is_strongly_connected_in Y2
proof
let a,b be object;
assume
A29: a in Y2 & b in Y2;
per cases by A29,XBOOLE_0:def 3;
suppose
A30: a in Y & b in Y;
the InternalRel of L is_strongly_connected_in Y by ORDERS_2:def 7;
hence thesis by A30;
end;
suppose
A31: a in Y & b in {y};
then reconsider a1 = a as Element of L;
reconsider b1 = b as Element of L by A31;
b1 = y & a1 <= m by A23,A31,TARSKI:def 1;
then a1 <= b1 by A28,ORDERS_2:3;
hence thesis by ORDERS_2:def 5;
end;
suppose
A32: a in {y} & b in Y;
then reconsider a1 = b as Element of L;
reconsider b1 = a as Element of L by A32;
b1 = y & a1 <= m by A23,A32,TARSKI:def 1;
then a1 <= b1 by A28,ORDERS_2:3;
hence thesis by ORDERS_2:def 5;
end;
suppose
A33: a in {y} & b in {y};
then reconsider a1 = a as Element of L;
A34: a1 <= a1;
a = y & b = y by A33,TARSKI:def 1;
hence thesis by A34,ORDERS_2:def 5;
end;
end;
then reconsider Y2 as Chain of L by ORDERS_2:def 7;
{y} c= (X`) by A25,ZFMISC_1:31;
then
A35: Y2 c= (X`) by A20,XBOOLE_1:8;
y in {y} by TARSKI:def 1;
then
A36: y in Y2 by XBOOLE_0:def 3;
x in Y2 by A21,XBOOLE_0:def 3;
then Y2 in A by A35;
hence contradiction by A18,A19,A27,A36,XBOOLE_1:7;
end;
now
assume m in X;
then consider y be Element of L such that
A37: y in X and
A38: y << m by Def1;
consider d being Element of L such that
A39: d in Y and
A40: y <= d by A21,A38,WAYBEL_3:def 1;
d in X by A37,A40,WAYBEL_0:def 20;
hence contradiction by A20,A39,XBOOLE_0:def 5;
end;
then m in (X`) by XBOOLE_0:def 5;
then m is_maximal_in (X`) by A24,WAYBEL_4:55;
hence thesis by A22;
end;
begin :: Irreducible elements
definition ::def 3.5, p.69
let G be non empty RelStr, g be Element of G;
attr g is meet-irreducible means
for x,y being Element of G st g = x "/\" y holds x = g or y = g;
end;
notation ::def 3.5, p.69
let G be non empty RelStr, g be Element of G;
synonym g is irreducible for g is meet-irreducible;
end;
definition
let G be non empty RelStr, g be Element of G;
attr g is join-irreducible means
for x,y being Element of G st g = x "\/" y holds x = g or y = g;
end;
definition
let L be non empty RelStr;
func IRR L -> Subset of L means
:Def4:
for x be Element of L holds x in it iff x is irreducible;
existence
proof
defpred P[Element of L] means $1 is irreducible;
consider X being Subset of L such that
A1: for x being 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 X,Y be Subset of L such that
A2: for x be Element of L holds x in X iff x is irreducible and
A3: for x be Element of L holds x in Y iff x is irreducible;
for x being object st x in Y holds x in X by A2,A3;
then
A4: Y c= X;
for x being object st x in X holds x in Y by A3,A2;
then X c= Y;
hence thesis by A4;
end;
end;
theorem Th10:
for L being upper-bounded antisymmetric with_infima non empty
RelStr holds Top L is irreducible
proof
let L be upper-bounded with_infima antisymmetric non empty RelStr;
let x,y be Element of L;
assume x "/\" y = Top L;
then
A1: x >= Top L & y >= Top L by YELLOW_0:23;
x <= Top L or y <= Top L by YELLOW_0:45;
hence thesis by A1,ORDERS_2:2;
end;
registration
let L be upper-bounded antisymmetric with_infima non empty RelStr;
cluster irreducible for Element of L;
existence
proof
take Top L;
thus thesis by Th10;
end;
end;
theorem
for L being Semilattice, x being Element of L holds x is irreducible
iff for A being finite non empty Subset of L st x = inf A holds x in A
proof
let L be Semilattice, I be Element of L;
thus I is irreducible implies for A being finite non empty Subset of L st I
= inf A holds I in A
proof
defpred P[set] means $1 is non empty & I = "/\"($1,L) implies I in $1;
assume
A1: for x,y being Element of L st I = x"/\"y holds I = x or I = y;
let A be finite non empty Subset of L;
A2: now
let x,B be set such that
A3: x in A and
A4: B c= A and
A5: P[B];
thus P[B \/ {x}]
proof
reconsider a = x as Element of L by A3;
reconsider C = B as finite Subset of L by A4,XBOOLE_1:1;
assume that
B \/ {x} is non empty and
A6: I = "/\"(B \/ {x},L);
per cases;
suppose
A7: B = {};
then "/\"(B \/ {a},L) = a by YELLOW_0:39;
hence thesis by A6,A7,TARSKI:def 1;
end;
suppose
A8: B <> {};
A9: inf {a} = a by YELLOW_0:39;
A10: ex_inf_of {a}, L by YELLOW_0:55;
ex_inf_of C, L by A8,YELLOW_0:55;
then
A11: "/\"(B \/ {x},L) = (inf C)"/\"inf {a} by A10,YELLOW_2:4;
hereby
per cases by A1,A6,A11,A9;
suppose
inf C = I;
hence thesis by A5,A8,XBOOLE_0:def 3;
end;
suppose
A12: a = I;
a in {a} by TARSKI:def 1;
hence thesis by A12,XBOOLE_0:def 3;
end;
end;
end;
end;
end;
A13: P[{}];
A14: A is finite;
P[A] from FINSET_1:sch 2(A14,A13,A2);
hence thesis;
end;
assume
A15: for A being finite non empty Subset of L st I = inf A holds I in A;
let a,b be Element of L;
assume I = a"/\"b;
then I = inf {a,b} by YELLOW_0:40;
then I in {a,b} by A15;
hence thesis by TARSKI:def 2;
end;
theorem
for L be LATTICE,l be Element of L st (uparrow l \ {l}) is Filter of L
holds l is irreducible
proof
let L be LATTICE, l be Element of L;
set F = (uparrow l \ {l});
assume
A1: (uparrow l \ {l}) is Filter of L;
now
let x,y be Element of L;
assume that
A2: l = x "/\" y and
A3: x <> l and
A4: y <> l;
l <= y by A2,YELLOW_0:23;
then y in uparrow l by WAYBEL_0:18;
then
A5: y in F by A4,ZFMISC_1:56;
l <= x by A2,YELLOW_0:23;
then x in uparrow l by WAYBEL_0:18;
then x in F by A3,ZFMISC_1:56;
then consider z being Element of L such that
A6: z in F and
A7: z <= x & z <= y by A1,A5,WAYBEL_0:def 2;
l >= z by A2,A7,YELLOW_0:23;
then l in F by A1,A6,WAYBEL_0:def 20;
hence contradiction by ZFMISC_1:56;
end;
hence thesis;
end;
theorem Th13: ::3.6, p.69
for L be LATTICE, p be Element of L, F be Filter of L st p
is_maximal_in (F`) holds p is irreducible
proof
let L be LATTICE, p be Element of L, F be Filter of L such that
A1: p is_maximal_in (F`);
set X = (the carrier of L)\F;
A2: p in X by A1,WAYBEL_4:55;
now
let x,y be Element of L;
assume that
A3: p = x "/\" y and
A4: x <> p and
A5: y <> p;
p <= y by A3,YELLOW_0:23;
then
A6: p < y by A5,ORDERS_2:def 6;
now
assume x in F & y in F;
then consider z being Element of L such that
A7: z in F and
A8: z <= x & z <= y by WAYBEL_0:def 2;
p >= z by A3,A8,YELLOW_0:23;
then p in F by A7,WAYBEL_0:def 20;
hence contradiction by A2,XBOOLE_0:def 5;
end;
then
A9: x in X or y in X by XBOOLE_0:def 5;
p <= x by A3,YELLOW_0:23;
then p < x by A4,ORDERS_2:def 6;
hence contradiction by A1,A9,A6,WAYBEL_4:55;
end;
hence thesis;
end;
theorem Th14: ::3.7, p.69
for L be lower-bounded continuous LATTICE, x,y be Element of L
st not y <= x holds ex p be Element of L st p is irreducible & x <= p & not y
<= p
proof
let L be lower-bounded continuous LATTICE, x,y be Element of L such that
A1: not y <= x;
for x being Element of L holds waybelow x is non empty directed;
then consider u being Element of L such that
A2: u << y and
A3: not u <= x by A1,WAYBEL_3:24;
consider F be Open Filter of L such that
A4: y in F and
A5: F c= wayabove u by A2,Th8;
A6: wayabove u c= uparrow u by WAYBEL_3:11;
not x in F by A3,WAYBEL_0:18,A5,A6;
then x in (the carrier of L)\F by XBOOLE_0:def 5;
then consider m being Element of L such that
A7: x <= m and
A8: m is_maximal_in (F`) by Th9;
take m;
A9: m in (F`) by A8,WAYBEL_4:55;
now
assume y <= m;
then m in F by A4,WAYBEL_0:def 20;
hence contradiction by A9,XBOOLE_0:def 5;
end;
hence thesis by A7,A8,Th13;
end;
begin :: Order generating sets
definition
let L be non empty RelStr, X be Subset of L;
attr X is order-generating means
for x be Element of L holds
ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X);
end;
theorem Th15: ::3.9 (1-2), p.70
for L be up-complete lower-bounded LATTICE, X be Subset of L
holds X is order-generating iff for l being Element of L ex Y be Subset of X st
l = "/\" (Y,L)
proof
let L be up-complete lower-bounded LATTICE, X be Subset of L;
thus X is order-generating implies for l being Element of L ex Y be Subset
of X st l = "/\" (Y,L)
proof
assume
A1: X is order-generating;
let l be Element of L;
for x being object st x in ((uparrow l) /\ X)
holds x in X by XBOOLE_0:def 4;
then reconsider Y = ((uparrow l) /\ X) as Subset of X by TARSKI:def 3;
l = "/\" (Y,L) by A1;
hence thesis;
end;
thus (for l being Element of L ex Y be Subset of X st l = "/\" (Y,L))
implies X is order-generating
proof
assume
A2: for l being Element of L ex Y be Subset of X st l = "/\" (Y,L);
let l be Element of L;
consider Y be Subset of X such that
A3: l = "/\" (Y,L) by A2;
set S = ((uparrow l) /\ X);
thus ex_inf_of S,L by YELLOW_0:17;
A4: for b be Element of L st b is_<=_than S holds b <= l
proof
let b be Element of L;
assume
A5: b is_<=_than S;
now
let x be Element of L;
assume
A6: x in Y;
l is_<=_than Y by A3,YELLOW_0:33;
then l <= x by A6;
then x in uparrow l by WAYBEL_0:18;
then x in S by A6,XBOOLE_0:def 4;
hence b <= x by A5;
end;
then b is_<=_than Y;
hence thesis by A3,YELLOW_0:33;
end;
now
let x be Element of L;
assume x in S;
then x in (uparrow l) by XBOOLE_0:def 4;
hence l <= x by WAYBEL_0:18;
end;
then l is_<=_than S;
hence thesis by A4,YELLOW_0:33;
end;
end;
theorem ::3.9 (1-3), p.70
for L be up-complete lower-bounded LATTICE, X be Subset of L holds X
is order-generating iff for Y be Subset of L st X c= Y & for Z be Subset of Y
holds "/\" (Z,L) in Y holds the carrier of L = Y
proof
let L be up-complete lower-bounded LATTICE, X be Subset of L;
thus X is order-generating implies for Y be Subset of L st X c= Y & for Z be
Subset of Y holds "/\"(Z,L) in Y holds the carrier of L = Y
proof
assume
A1: X is order-generating;
let Y be Subset of L;
assume that
A2: X c= Y and
A3: for Z be Subset of Y holds "/\"(Z,L) in Y;
now
let l1 be object;
assume l1 in the carrier of L;
then reconsider l = l1 as Element of L;
(uparrow l) /\ Y c= Y & (uparrow l) /\ X c= (uparrow l) /\ Y by A2,
XBOOLE_1:17,26;
then
A4: (uparrow l) /\ X c= Y;
l = inf ((uparrow l) /\ X) by A1;
hence l1 in Y by A3,A4;
end;
hence the carrier of L c= Y;
thus thesis;
end;
thus (for Y be Subset of L st X c= Y & for Z be Subset of Y holds "/\"(Z,L)
in Y holds the carrier of L = Y) implies X is order-generating
proof
set Y = {"/\"(Z,L) where Z is Subset of L : Z c= X};
now
let x be object;
assume x in Y;
then ex Z be Subset of L st x = "/\"(Z,L) & Z c= X;
hence x in the carrier of L;
end;
then reconsider Y as Subset of L by TARSKI:def 3;
now
let x be object;
assume
A5: x in X;
then reconsider x1 = x as Element of L;
reconsider x2 = {x1} as Subset of L;
A6: x1 = "/\"(x2,L) by YELLOW_0:39;
{x1} c= X by A5,ZFMISC_1:31;
hence x in Y by A6;
end;
then
A7: X c= Y;
assume
A8: for Y be Subset of L st X c= Y & for Z be Subset of Y holds "/\"(Z
,L) in Y holds the carrier of L = Y;
for l being Element of L ex Z be Subset of X st l = "/\" (Z,L)
proof
let l be Element of L;
for Z be Subset of Y holds "/\"(Z,L) in Y
proof
let Z be Subset of Y;
set S = union {A where A is Subset of L : A c= X & "/\"(A,L) in Z};
now
let x be object;
assume x in S;
then consider Y be set such that
A9: x in Y and
A10: Y in {A where A is Subset of L : A c= X & "/\" (A,L) in Z}
by TARSKI:def 4;
ex A be Subset of L st Y = A & A c= X & "/\"(A,L) in Z by A10;
hence x in the carrier of L by A9;
end;
then reconsider S as Subset of L by TARSKI:def 3;
defpred P[Subset of L] means $1 c= X & "/\"($1,L) in Z;
set N = {"/\"(A,L) where A is Subset of L : P[A]};
now
let x be object;
assume
A11: x in Z;
then x in Y;
then ex Z be Subset of L st x = "/\"(Z,L) & Z c= X;
hence x in N by A11;
end;
then
A12: Z c= N;
now
let B be set;
assume B in {A where A is Subset of L : A c= X & "/\"(A,L) in Z};
then ex A be Subset of L st B = A & A c= X & "/\"(A, L) in Z;
hence B c= X;
end;
then
A13: S c= X by ZFMISC_1:76;
now
let x be object;
assume x in N;
then ex S be Subset of L st x = "/\"(S,L) & S c= X & "/\"(S, L) in Z;
hence x in Z;
end;
then N c= Z;
then "/\"(Z,L) = "/\"(N,L) by A12,XBOOLE_0:def 10
.= "/\" (union {A where A is Subset of L : P[A]}, L) from YELLOW_3
:sch 3;
hence thesis by A13;
end;
then the carrier of L = Y by A8,A7;
then l in Y;
then ex Z be Subset of L st l = "/\" (Z,L) & Z c= X;
hence thesis;
end;
hence thesis by Th15;
end;
end;
theorem Th17: ::3.9 (1-4), p.70
for L be up-complete lower-bounded LATTICE, X be Subset of L
holds X is order-generating iff for l1,l2 be Element of L st not l2 <= l1 ex p
be Element of L st p in X & l1 <= p & not l2 <= p
proof
let L be up-complete lower-bounded LATTICE, X be Subset of L;
thus X is order-generating implies for l1,l2 be Element of L st not l2 <= l1
ex p be Element of L st p in X & l1 <= p & not l2 <= p
proof
assume
A1: X is order-generating;
let l1,l2 be Element of L;
consider P be Subset of X such that
A2: l1 = "/\" (P,L) by A1,Th15;
assume
A3: not l2 <= l1;
now
assume for p be Element of L st p in P holds l2 <= p;
then l2 is_<=_than P;
hence contradiction by A3,A2,YELLOW_0:33;
end;
then consider p be Element of L such that
A4: p in P & not l2 <= p;
take p;
l1 is_<=_than P by A2,YELLOW_0:33;
hence thesis by A4;
end;
thus (for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st p in
X & l1 <= p & not l2 <= p) implies X is order-generating
proof
assume
A5: for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st
p in X & l1 <= p & not l2 <= p;
let l be Element of L;
set y = inf ((uparrow l) /\ X);
thus ex_inf_of (uparrow l) /\ X,L by YELLOW_0:17;
A6: y is_<=_than ((uparrow l) /\ X ) by YELLOW_0:33;
now
l is_<=_than ((uparrow l) /\ X )
proof
let b be Element of L;
assume b in ((uparrow l) /\ X );
then b in (uparrow l) by XBOOLE_0:def 4;
hence thesis by WAYBEL_0:18;
end;
then l <= y by YELLOW_0:33;
then
A7: not y < l by ORDERS_2:6;
assume
A8: y <> l;
now
per cases by A7,ORDERS_2:def 6;
suppose
not y <= l;
then consider p be Element of L such that
A9: p in X and
A10: l <= p and
A11: not y <= p by A5;
p in (uparrow l) by A10,WAYBEL_0:18;
then p in (uparrow l) /\ X by A9,XBOOLE_0:def 4;
hence contradiction by A6,A11;
end;
suppose
y = l;
hence contradiction by A8;
end;
end;
hence contradiction;
end;
hence thesis;
end;
end;
theorem Th18: ::3.10, p.70
for L be lower-bounded continuous LATTICE, X be Subset of L st X
= IRR L \ { Top L} holds X is order-generating
proof
let L be lower-bounded continuous LATTICE, X be Subset of L;
assume
A1: X = IRR L \ {Top L};
for l1,l2 be Element of L st not l2 <= l1 ex p be Element of L st p in X
& l1 <= p & not l2 <= p
proof
let x,y be Element of L;
assume not y <= x;
then consider p be Element of L such that
A2: p is irreducible and
A3: x <= p and
A4: not y <= p by Th14;
p <> Top L & p in IRR L by A2,A4,Def4,YELLOW_0:45;
then p in X by A1,ZFMISC_1:56;
hence thesis by A3,A4;
end;
hence thesis by Th17;
end;
theorem Th19:
for L being lower-bounded continuous LATTICE, X,Y being Subset
of L st X is order-generating & X c= Y holds Y is order-generating
proof
let L be lower-bounded continuous LATTICE, X,Y be Subset of L;
assume that
A1: X is order-generating and
A2: X c= Y;
let x be Element of L;
thus ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17;
A3: ex_inf_of ((uparrow x) /\ Y),L by YELLOW_0:17;
ex_inf_of (uparrow x),L by WAYBEL_0:39;
then inf ((uparrow x) /\ Y) >= inf (uparrow x) by A3,XBOOLE_1:17,YELLOW_0:35;
then
A4: inf ((uparrow x) /\ Y) >= x by WAYBEL_0:39;
ex_inf_of ((uparrow x) /\ X),L by YELLOW_0:17;
then inf ((uparrow x) /\ X) >= inf ((uparrow x) /\ Y) by A2,A3,XBOOLE_1:26
,YELLOW_0:35;
then x >= inf ((uparrow x) /\ Y) by A1;
hence thesis by A4,ORDERS_2:2;
end;
begin :: Prime elements
definition
let L be non empty RelStr;
let l be Element of L;
attr l is prime means
for x,y be Element of L st x "/\" y <= l holds x <= l or y <= l;
end;
definition
let L be non empty RelStr;
func PRIME L -> Subset of L means
:Def7:
for x be Element of L holds x in it iff x is prime;
existence
proof
defpred P[Element of L] means $1 is prime;
consider X being Subset of L such that
A1: for x being 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 X,Y be Subset of L;
assume that
A2: for x be Element of L holds x in X iff x is prime and
A3: for x be Element of L holds x in Y iff x is prime;
thus X c= Y
by A2,A3;
thus Y c= X
by A3,A2;
end;
end;
definition
let L be non empty RelStr;
let l be Element of L;
attr l is co-prime means
l~ is prime;
end;
theorem Th20:
for L being upper-bounded antisymmetric non empty RelStr holds Top L is prime
by YELLOW_0:45;
theorem
for L being lower-bounded antisymmetric non empty RelStr holds Bottom
L is co-prime
proof
let L be lower-bounded antisymmetric non empty RelStr;
Top (L~) is prime by Th20;
hence (Bottom L)~ is prime by YELLOW_7:33;
end;
registration
let L be upper-bounded antisymmetric non empty RelStr;
cluster prime for Element of L;
existence
proof
take Top L;
thus thesis by Th20;
end;
end;
theorem Th22:
for L being Semilattice, l being Element of L holds l is prime
iff for A being finite non empty Subset of L st l >= inf A ex a being Element
of L st a in A & l >= a
proof
let L be Semilattice, l be Element of L;
thus l is prime implies for A being finite non empty Subset of L st l >= inf
A ex a being Element of L st a in A & l >= a
proof
defpred P[set] means $1 is non empty & l >= "/\"($1,L) implies (ex k being
Element of L st k in $1 & l >= k);
assume
A1: for x,y being Element of L st l >= x"/\"y holds l >= x or l >= y;
let A be finite non empty Subset of L;
A2: now
let x,B be set such that
A3: x in A and
A4: B c= A and
A5: P[B];
thus P[B \/ {x}]
proof
reconsider a = x as Element of L by A3;
reconsider C = B as finite Subset of L by A4,XBOOLE_1:1;
assume that
B \/ {x} is non empty and
A6: l >= "/\"(B \/ {x},L);
per cases;
suppose
B = {};
then "/\"(B \/ {a},L) = a & a in B \/ {a} by TARSKI:def 1,YELLOW_0:39
;
hence thesis by A6;
end;
suppose
A7: B <> {};
A8: inf {a} = a by YELLOW_0:39;
A9: ex_inf_of {a}, L by YELLOW_0:55;
ex_inf_of C, L by A7,YELLOW_0:55;
then
A10: "/\"(B \/ {x},L) = (inf C)"/\"inf {a} by A9,YELLOW_2:4;
hereby
per cases by A1,A6,A10,A8;
suppose
inf C <= l;
then consider b being Element of L such that
A11: b in B and
A12: b <= l by A5,A7;
b in B \/ {x} by A11,XBOOLE_0:def 3;
hence thesis by A12;
end;
suppose
A13: a <= l;
a in {a} by TARSKI:def 1;
then a in B \/ {x} by XBOOLE_0:def 3;
hence thesis by A13;
end;
end;
end;
end;
end;
A14: P[{}];
A15: A is finite;
P[A] from FINSET_1:sch 2(A15,A14,A2);
hence thesis;
end;
assume
A16: for A being finite non empty Subset of L st l >= inf A ex a being
Element of L st a in A & l >= a;
let a,b be Element of L;
set A = {a,b};
A17: inf A = a"/\"b by YELLOW_0:40;
assume a "/\" b <= l;
then ex k being Element of L st k in A & l >= k by A16,A17;
hence thesis by TARSKI:def 2;
end;
theorem Th23:
for L being sup-Semilattice, x being Element of L holds x is
co-prime iff for A being finite non empty Subset of L st x <= sup A ex a being
Element of L st a in A & x <= a
proof
let L be sup-Semilattice, x be Element of L;
thus x is co-prime implies for A being finite non empty Subset of L st x <=
sup A ex a being Element of L st a in A & x <= a
proof
assume x is co-prime;
then
A1: x~ is prime;
let A be finite non empty Subset of L;
reconsider A1 = A as finite non empty Subset of L~;
assume x <= sup A;
then
A2: x~ >= (sup A)~ by LATTICE3:9;
A3: ex_sup_of A,L by YELLOW_0:54;
then "\/"(A,L) is_>=_than A by YELLOW_0:def 9;
then
A4: "\/"(A,L)~ is_<=_than A by YELLOW_7:8;
A5: now
let y be Element of L~;
assume y is_<=_than A;
then ~y is_>=_than A by YELLOW_7:9;
then ~y >= "\/"(A,L) by A3,YELLOW_0:def 9;
hence y <= "\/"(A,L)~ by YELLOW_7:2;
end;
ex_inf_of A,L~ by A3,YELLOW_7:10;
then (sup A)~ = (inf A1) by A4,A5,YELLOW_0:def 10;
then consider a being Element of L~ such that
A6: a in A1 & x~ >= a by A1,A2,Th22;
take ~a;
thus thesis by A6,YELLOW_7:2;
end;
thus (for A being finite non empty Subset of L st x <= sup A ex a being
Element of L st a in A & x <= a) implies x is co-prime
proof
assume
A7: for A being finite non empty Subset of L st x <= sup A ex a being
Element of L st a in A & x <= a;
now
let a,b be Element of L~;
set A = {~a,~b};
assume a "/\" b <= x~;
then x <= ~(a "/\" b) by YELLOW_7:2;
then sup A = (~a)"\/"(~b) & x <= (~a)"\/"(~b) by YELLOW_0:41,YELLOW_7:24;
then consider l being Element of L such that
A8: l in A and
A9: x <= l by A7;
l = ~a or l = ~b by A8,TARSKI:def 2;
hence a <= x~ or b <= x~ by A9,YELLOW_7:2;
end;
then x~ is prime;
hence thesis;
end;
end;
theorem Th24:
for L being LATTICE, l being Element of L st l is prime holds l
is irreducible
proof
let L be LATTICE, l be Element of L;
assume
A1: l is prime;
let x,y be Element of L;
assume
A2: l = x "/\" y;
then x "/\" y <= l;
then
A3: x <= l or y <= l by A1;
l <= x & l <= y by A2,YELLOW_0:23;
hence thesis by A3,ORDERS_2:2;
end;
theorem Th25: ::3.12 (1-2), p.70
for l holds l is prime iff for x being set, f being Function of
L,BoolePoset {x} st (for p be Element of L holds f.p = {} iff p <= l) holds f
is meet-preserving join-preserving
proof
let l;
thus l is prime implies for x being set, f being Function of L,BoolePoset {x
} st (for p be Element of L holds f.p = {} iff p <= l) holds f is
meet-preserving join-preserving
proof
assume
A1: l is prime;
let x be set, f be Function of L,BoolePoset {x};
assume
A2: for p be Element of L holds f.p = {} iff p <= l;
A3: the carrier of BoolePoset {x} = the carrier of InclPoset bool {x} by
YELLOW_1:4
.= bool {x} by YELLOW_1:1
.= { {} , {x}} by ZFMISC_1:24;
A4: dom f = the carrier of L by FUNCT_2:def 1;
for z,y being Element of L holds f preserves_inf_of {z,y}
proof
let z,y be Element of L;
A5: f.:{z,y} = {f.z,f.y} by A4,FUNCT_1:60;
then
A6: ex_inf_of {z,y},L implies ex_inf_of f.:{z,y},BoolePoset {x} by
YELLOW_0:21;
A7: now
per cases by A3,TARSKI:def 2;
suppose
A8: f.z = {} & f.y = {};
then z "/\" y <= z & z <= l by A2,YELLOW_0:23;
then
A9: z "/\" y <= l by ORDERS_2:3;
thus f.z "/\" f.y = {} /\ {} by A8,YELLOW_1:17
.= f.(z "/\" y) by A2,A9;
end;
suppose
A10: f.z = {x} & f.y = {x};
then ( not y <= l)& not z <= l by A2;
then not z "/\" y <= l by A1;
then
A11: not f.(z "/\" y) = {} by A2;
thus f.z "/\" f.y = {x} /\ {x} by A10,YELLOW_1:17
.= f.(z "/\" y) by A3,A11,TARSKI:def 2;
end;
suppose
A12: f.z = {} & f.y = {x};
then z "/\" y <= z & z <= l by A2,YELLOW_0:23;
then
A13: z "/\" y <= l by ORDERS_2:3;
thus f.z "/\" f.y = {} /\ {x} by A12,YELLOW_1:17
.= f.(z "/\" y) by A2,A13;
end;
suppose
A14: f.z = {x} & f.y = {};
then z "/\" y <= y & y <= l by A2,YELLOW_0:23;
then
A15: z "/\" y <= l by ORDERS_2:3;
thus f.z "/\" f.y = {x} /\ {} by A14,YELLOW_1:17
.= f.(z "/\" y) by A2,A15;
end;
end;
inf (f.:{z,y}) = f.z "/\" f.y by A5,YELLOW_0:40
.= f.inf {z,y} by A7,YELLOW_0:40;
hence thesis by A6;
end;
hence f is meet-preserving;
for z,y being Element of L holds f preserves_sup_of {z,y}
proof
let z,y be Element of L;
A16: f.:{z,y} = {f.z,f.y} by A4,FUNCT_1:60;
then
A17: ex_sup_of {z,y},L implies ex_sup_of f.:{z,y},BoolePoset {x} by
YELLOW_0:20;
A18: now
per cases by A3,TARSKI:def 2;
suppose
A19: f.z = {} & f.y = {};
then z <= l & y <= l by A2;
then
A20: z "\/" y <= l by YELLOW_0:22;
thus f.z "\/" f.y = {} \/ {} by A19,YELLOW_1:17
.= f.(z "\/" y) by A2,A20;
end;
suppose
A21: f.z = {x} & f.y = {x};
then z "\/" y >= z & not z <= l by A2,YELLOW_0:22;
then not z "\/" y <= l by ORDERS_2:3;
then
A22: not f.(z "\/" y) = {} by A2;
thus f.z "\/" f.y = {x} \/ {x} by A21,YELLOW_1:17
.= f.(z "\/" y) by A3,A22,TARSKI:def 2;
end;
suppose
A23: f.z = {} & f.y = {x};
then z "\/" y >= y & not y <= l by A2,YELLOW_0:22;
then not z "\/" y <= l by ORDERS_2:3;
then
A24: not f.(z "\/" y) = {} by A2;
thus f.z "\/" f.y = {} \/ {x} by A23,YELLOW_1:17
.= f.(z "\/" y) by A3,A24,TARSKI:def 2;
end;
suppose
A25: f.z = {x} & f.y = {};
then z "\/" y >= z & not z <= l by A2,YELLOW_0:22;
then not z "\/" y <= l by ORDERS_2:3;
then
A26: not f.(z "\/" y) = {} by A2;
thus f.z "\/" f.y = {x} \/ {} by A25,YELLOW_1:17
.= f.(z "\/" y) by A3,A26,TARSKI:def 2;
end;
end;
sup (f.:{z,y}) = f.z "\/" f.y by A16,YELLOW_0:41
.= f.sup {z,y} by A18,YELLOW_0:41;
hence thesis by A17;
end;
hence thesis;
end;
thus (for x being set, f being Function of L,BoolePoset {x} st (for p be
Element of L holds f.p = {} iff p <= l) holds f is meet-preserving
join-preserving) implies l is prime
proof
defpred P[Element of L, set] means $1 <= l iff $2 = {};
assume
A27: for x being set, f being Function of L,BoolePoset {x} st (for p
be Element of L holds f.p = {} iff p <= l) holds f is meet-preserving
join-preserving;
let z,y be Element of L;
A28: the carrier of BoolePoset {{}} = the carrier of InclPoset bool {{}}
by YELLOW_1:4
.= bool {{}} by YELLOW_1:1
.= { {} , {{}}} by ZFMISC_1:24;
A29: for a being Element of L ex b being Element of BoolePoset {{}} st P[a ,b]
proof
let a be Element of L;
now
per cases;
suppose
A30: a <= l;
set b = {};
reconsider b as Element of BoolePoset {{}} by A28,TARSKI:def 2;
a <= l iff b = {} by A30;
hence thesis;
end;
suppose
A31: not a <= l;
set b = {{}};
reconsider b as Element of BoolePoset {{}} by A28,TARSKI:def 2;
a <= l iff b = {} by A31;
hence thesis;
end;
end;
hence thesis;
end;
consider f being Function of L,BoolePoset {{}} such that
A32: for p be Element of L holds P[p, f.p] from FUNCT_2:sch 3(A29);
f is meet-preserving by A27,A32;
then
A33: ex_inf_of {z,y},L & f preserves_inf_of {z,y} by YELLOW_0:21;
dom f = the carrier of L by FUNCT_2:def 1;
then
A34: f.:{z,y} = {f.z,f.y} by FUNCT_1:60;
assume z "/\" y <= l;
then
A35: {} = f.(z "/\" y) by A32
.= f.inf {z,y} by YELLOW_0:40
.= inf({f.z,f.y}) by A34,A33
.= f.z "/\" f.y by YELLOW_0:40
.= f.z /\ f.y by YELLOW_1:17;
now
assume ( not f.z = {})& not f.y = {};
then f.z = {{}} & f.y = {{}} by A28,TARSKI:def 2;
hence contradiction by A35;
end;
hence z <= l or y <= l by A32;
end;
end;
theorem Th26: ::3.12 (1-3), p.70
for L being upper-bounded LATTICE, l being Element of L st l <>
Top L holds l is prime iff (downarrow l)` is Filter of L
proof
let L be upper-bounded LATTICE, l be Element of L;
set X1 = (the carrier of L)\(downarrow l);
reconsider X = X1 as Subset of L;
assume
A1: l <> Top L;
thus l is prime implies (downarrow l)` is Filter of L
proof
assume
A2: l is prime;
A3: now
let x,y be Element of L;
assume that
A4: x in X and
A5: y in X;
not y in (downarrow l) by A5,XBOOLE_0:def 5;
then
A6: not y <= l by WAYBEL_0:17;
not x in (downarrow l) by A4,XBOOLE_0:def 5;
then
A7: not x <= l by WAYBEL_0:17;
not x "/\" y in downarrow l by A2,A7,A6,WAYBEL_0:17;
then
A8: x "/\" y in X by XBOOLE_0:def 5;
x "/\" y <= x & x "/\" y <= y by YELLOW_0:23;
hence ex z being Element of L st z in X & z <= x & z <= y by A8;
end;
A9: now
let x,y be Element of L;
assume that
A10: x in X and
A11: x <= y;
not x in (downarrow l) by A10,XBOOLE_0:def 5;
then not x <= l by WAYBEL_0:17;
then not y <= l by A11,ORDERS_2:3;
then not y in (downarrow l) by WAYBEL_0:17;
hence y in X by XBOOLE_0:def 5;
end;
now
assume Top L in (downarrow l);
then Top L <= l by WAYBEL_0:17;
then Top L < l by A1,ORDERS_2:def 6;
hence contradiction by ORDERS_2:6,YELLOW_0:45;
end;
hence thesis by A3,A9,WAYBEL_0:def 2,def 20,XBOOLE_0:def 5;
end;
thus (downarrow l)` is Filter of L implies l is prime
proof
l <= l;
then
A12: l in (downarrow l) by WAYBEL_0:17;
assume
A13: (downarrow l)` is Filter of L;
let x,y be Element of L;
assume
A14: x "/\" y <= l;
now
assume that
A15: not x <= l and
A16: not y <= l;
not y in (downarrow l) by A16,WAYBEL_0:17;
then
A17: y in X by XBOOLE_0:def 5;
not x in (downarrow l) by A15,WAYBEL_0:17;
then x in X by XBOOLE_0:def 5;
then consider z being Element of L such that
A18: z in X and
A19: z <= x & z <= y by A13,A17,WAYBEL_0:def 2;
z <= x "/\" y by A19,YELLOW_0:23;
then z <= l by A14,ORDERS_2:3;
then l in X by A13,A18,WAYBEL_0:def 20;
hence contradiction by A12,XBOOLE_0:def 5;
end;
hence x <= l or y <= l;
end;
end;
theorem Th27: ::3.12 (1-4), p.70
for L being distributive LATTICE for l being Element of L holds
l is prime iff l is irreducible
proof
let L be distributive LATTICE,l be Element of L;
thus l is prime implies l is irreducible by Th24;
thus l is irreducible implies l is prime
proof
assume
A1: l is irreducible;
let x,y be Element of L;
assume x "/\" y <= l;
then l = l "\/" (x "/\" y) by YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5;
then l = l "\/" x or l = l "\/" y by A1;
hence x <= l or y <= l by YELLOW_0:24;
end;
end;
theorem Th28:
for L being distributive LATTICE holds PRIME L = IRR L
proof
let L be distributive LATTICE;
now
let l1 be object;
assume
A1: l1 in PRIME L;
then reconsider l = l1 as Element of PRIME L;
reconsider l as Element of L by A1;
l is prime by A1,Def7;
then l is irreducible by Th27;
hence l1 in IRR L by Def4;
end;
hence PRIME L c= IRR L;
now
let l1 be object;
assume
A2: l1 in IRR L;
then reconsider l = l1 as Element of IRR L;
reconsider l as Element of L by A2;
l is irreducible by A2,Def4;
then l is prime by Th27;
hence l1 in PRIME L by Def7;
end;
hence thesis;
end;
theorem ::3.12 (1-5), p.70
for L being Boolean LATTICE for l being Element of L st l <> Top L
holds l is prime iff for x be Element of L st x > l holds x = Top L
proof
let L be Boolean LATTICE, l be Element of L;
assume
A1: l <> Top L;
thus l is prime implies for x be Element of L st x > l holds x = Top L
proof
assume
A2: l is prime;
let x be Element of L;
consider y being Element of L such that
A3: y is_a_complement_of x by WAYBEL_1:def 24;
x "/\" y = Bottom L by A3;
then x "/\" y <= l by YELLOW_0:44;
then
A4: x <= l or y <= l by A2;
assume x > l;
then y < x by A4,ORDERS_2:7;
then
A5: y <= x by ORDERS_2:def 6;
x "\/" y = Top L by A3;
hence thesis by A5,YELLOW_0:24;
end;
thus (for x be Element of L st x > l holds x = Top L) implies l is prime
proof
assume
A6: for z be Element of L st z > l holds z = Top L;
let x,y be Element of L;
assume x "/\" y <= l;
then
A7: l = l "\/" (x "/\" y) by YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5;
assume that
A8: not x <= l and
A9: not y <= l;
A10: l <> (l "\/" y) by A9,YELLOW_0:24;
l <= (l "\/" y) by A7,YELLOW_0:23;
then l < (l "\/" y) by A10,ORDERS_2:def 6;
then
A11: (l "\/" y) = Top L by A6;
A12: l <> (l "\/" x) by A8,YELLOW_0:24;
l <= (l "\/" x) by A7,YELLOW_0:23;
then l < (l "\/" x) by A12,ORDERS_2:def 6;
then (l "\/" x) = Top L by A6;
hence contradiction by A1,A7,A11,YELLOW_5:2;
end;
end;
theorem ::3.12 (1-6), p.70
for L being continuous distributive lower-bounded LATTICE for l being
Element of L st l <> Top L holds l is prime iff ex F being Open Filter of L st
l is_maximal_in (F`)
proof
let L be continuous distributive lower-bounded LATTICE, l be Element of L;
set F = (downarrow l)`;
assume
A1: l <> Top L;
thus l is prime implies ex F being Open Filter of L st l is_maximal_in (F`)
proof
A2: for x being Element of L holds waybelow x is non empty directed;
A3: now
let x be Element of L;
assume x in F;
then not x in (downarrow l) by XBOOLE_0:def 5;
then not x <= l by WAYBEL_0:17;
then consider y be Element of L such that
A4: y << x and
A5: not y <= l by A2,WAYBEL_3:24;
not y in (downarrow l) by A5,WAYBEL_0:17;
then y in F by XBOOLE_0:def 5;
hence ex y be Element of L st y in F & y << x by A4;
end;
assume l is prime;
then reconsider F as Open Filter of L by A1,A3,Def1,Th26;
take F;
A6: not ex y being Element of L st y in F` & y > l by WAYBEL_0:17,ORDERS_2:6;
l <= l;
then l in (F`) by WAYBEL_0:17;
hence thesis by A6,WAYBEL_4:55;
end;
thus (ex F being Open Filter of L st l is_maximal_in (F`)) implies l is prime
proof
assume ex O being Open Filter of L st l is_maximal_in (O`);
then
A7: l is irreducible by Th13;
now
let x,y be Element of L;
assume x "/\" y <= l;
then l = l "\/" (x "/\" y) by YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5;
then
A8: l = (l "\/" x) or l = (l "\/" y) by A7;
assume ( not x <= l)& not y <= l;
hence contradiction by A8,YELLOW_0:24;
end;
hence thesis;
end;
end;
theorem Th31:
for L being RelStr, X being Subset of L holds chi(X, the carrier
of L) is Function of L, BoolePoset {{}}
proof
let L be RelStr, X be Subset of L;
the carrier of BoolePoset {{}} = the carrier of InclPoset bool {{}} by
YELLOW_1:4
.= bool {{}} by YELLOW_1:1
.= {0,1} by CARD_1:49,ZFMISC_1:24;
hence thesis;
end;
theorem Th32:
for L being non empty RelStr, p,x being Element of L holds chi((
downarrow p)`,the carrier of L).x = {} iff x <= p
proof
let L be non empty RelStr, p,x be Element of L;
not x in (downarrow p)` iff x in downarrow p by XBOOLE_0:def 5;
hence thesis by FUNCT_3:def 3,WAYBEL_0:17;
end;
theorem Th33:
for L being upper-bounded LATTICE, f being Function of L,
BoolePoset {{}}, p being prime Element of L st chi((downarrow p)`,the carrier
of L) = f holds f is meet-preserving join-preserving
proof
let L be upper-bounded LATTICE, f be Function of L,BoolePoset {{}}, p be
prime Element of L;
assume chi((downarrow p)`,the carrier of L) = f;
then for x being Element of L holds f.x = {} iff x <= p by Th32;
hence thesis by Th25;
end;
theorem Th34: ::3.13, p.71
for L being complete LATTICE st PRIME L is order-generating
holds L is distributive meet-continuous
proof
let L be complete LATTICE;
set H = {chi((downarrow p)`, the carrier of L) where p is Element of L: p is
prime};
set p9 = the prime Element of L;
A1: chi((downarrow p9)`, the carrier of L) in H;
now
let x be object;
assume x in H;
then
ex p being Element of L st x = chi((downarrow p)`, the carrier of L) &
p is prime;
hence x is Function;
end;
then reconsider H as functional non empty set by A1,FUNCT_1:def 13;
deffunc F(object) = {f where f is Element of H: f.$1 = 1};
consider F being Function such that
A2: dom F = the carrier of L and
A3: for x being object st x in the carrier of L holds F.x = F(x) from
FUNCT_1:sch 3;
A4: the carrier of BoolePoset H = the carrier of InclPoset bool H by YELLOW_1:4
.= bool H by YELLOW_1:1;
rng F c= the carrier of BoolePoset H
proof
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in rng F;
then consider x being object such that
A5: x in dom F & y = F.x by FUNCT_1:def 3;
A6: y = {f where f is Element of H: f.x = 1} by A2,A3,A5;
yy c= H
proof
let p be object;
assume p in yy;
then ex f be Element of H st p = f & f.x = 1 by A6;
hence thesis;
end;
hence thesis by A4;
end;
then reconsider F as Function of L, BoolePoset H by A2,FUNCT_2:def 1
,RELSET_1:4;
A7: F is meet-preserving
proof
let x,y be Element of L;
assume ex_inf_of {x,y},L;
thus ex_inf_of F.:{x,y},BoolePoset H by YELLOW_0:17;
A8: {f where f is Element of H: f.(x "/\" y) = 1} c= {f where f is
Element of H: f.x = 1} /\ {f where f is Element of H: f.y = 1}
proof
A9: ex_inf_of {x,y}, L & x"/\"y = inf {x,y} by YELLOW_0:17,40;
let p be object;
A10: 1 = Top BoolePoset {{}} by CARD_1:49,YELLOW_1:19;
assume p in {f where f is Element of H: f.(x "/\" y) = 1};
then consider g be Element of H such that
A11: g = p and
A12: g.(x "/\" y) = 1;
g in H;
then
A13: ex a be Element of L st chi((downarrow a)`, the carrier of L) = g &
a is prime;
then reconsider g as Function of L,BoolePoset {{}} by Th31;
g is meet-preserving by A13,Th33;
then
A14: g preserves_inf_of {x,y};
dom g = the carrier of L by FUNCT_2:def 1;
then
A15: {g.x,g.y} = g.:{x,y} by FUNCT_1:60;
(g.x)"/\"(g.y) = inf {g.x,g.y} by YELLOW_0:40;
then
A16: g.(x "/\" y) = (g.x)"/\"(g.y) by A15,A14,A9;
then
g.y <= Top BoolePoset {{}} & g.y >= Top BoolePoset {{}} by A12,A10,
YELLOW_0:23,45;
then g.y = 1 by A10,ORDERS_2:2;
then
A17: p in {f where f is Element of H: f.y = 1} by A11;
g.x <= Top BoolePoset {{}} & g.x >= Top BoolePoset {{}} by A12,A10,A16,
YELLOW_0:23,45;
then g.x = 1 by A10,ORDERS_2:2;
then p in {f where f is Element of H: f.x = 1} by A11;
hence thesis by A17,XBOOLE_0:def 4;
end;
A18: {f where f is Element of H: f.x = 1} /\ {f where f is Element of H: f
.y = 1} c= {f where f is Element of H: f.(x "/\" y) = 1}
proof
let p be object;
A19: ex_inf_of {x,y}, L & x"/\"y = inf {x,y} by YELLOW_0:17,40;
assume
A20: p in ({f where f is Element of H: f.x = 1} /\ {f where f is
Element of H: f.y = 1});
then p in {f where f is Element of H: f.x = 1} by XBOOLE_0:def 4;
then consider f1 be Element of H such that
A21: f1 = p and
A22: f1.x = 1;
p in {f where f is Element of H: f.y = 1} by A20,XBOOLE_0:def 4;
then
A23: ex f2 be Element of H st f2 = p & f2.y = 1;
f1 in H;
then consider a be Element of L such that
A24: chi((downarrow a)`, the carrier of L) = f1 and
A25: a is prime;
reconsider f1 as Function of L,BoolePoset {{}} by A24,Th31;
for x being Element of L holds f1.x = {} iff x <= a by A24,Th32;
then f1 is meet-preserving by A25,Th25;
then
A26: f1 preserves_inf_of {x,y};
dom f1 = the carrier of L by FUNCT_2:def 1;
then
A27: {f1.x,f1.y} = f1.:{x,y} by FUNCT_1:60;
(f1.x)"/\"(f1.y) = inf {f1.x,f1.y} by YELLOW_0:40;
then f1.(x "/\" y) = (f1.x)"/\"(f1.y) by A27,A26,A19
.= 1 by A21,A22,A23,YELLOW_5:2;
hence thesis by A21;
end;
F.:{x,y} = {F.x,F.y} by A2,FUNCT_1:60;
hence inf (F.:{x,y}) = F.x "/\" F.y by YELLOW_0:40
.= (F.x) /\ (F.y) by YELLOW_1:17
.= {f where f is Element of H: f.x = 1} /\ (F.y) by A3
.= {f where f is Element of H: f.x = 1} /\ {f where f is Element of H:
f.y = 1} by A3
.= {f where f is Element of H: f.(x "/\" y) = 1} by A18,A8
.= F.(x "/\" y) by A3
.= F.inf {x,y} by YELLOW_0:40;
end;
assume
A28: PRIME L is order-generating;
A29: F is one-to-one
proof
let x1,x2 be object;
assume that
A30: x1 in dom F and
A31: x2 in dom F and
A32: F.x1 = F.x2;
reconsider l2 = x2 as Element of L by A31;
reconsider l1 = x1 as Element of L by A30;
now
A33: F.l2 = {f where f is Element of H: f.l2 = 1} by A3;
A34: F.l1 = {f where f is Element of H: f.l1 = 1} by A3;
assume
A35: l1 <> l2;
per cases by A35,ORDERS_2:2;
suppose
not l1 <= l2;
then consider p be Element of L such that
A36: p in PRIME L and
A37: l2 <= p and
A38: not l1 <= p by A28,Th17;
set CH = chi((downarrow p)`,the carrier of L);
p is prime by A36,Def7;
then CH in H;
then reconsider CH as Element of H;
A39: now
assume CH in F.l2;
then ex f be Element of H st f = CH & f.l2 = 1 by A33;
hence contradiction by A37,Th32;
end;
dom CH = the carrier of L by FUNCT_2:def 1;
then rng CH c= {0,1} & CH.l1 in rng CH by FUNCT_1:def 3,RELAT_1:def 19;
then CH.l1 = 0 or CH.l1 = 1 by TARSKI:def 2;
hence contradiction by A32,A34,A38,A39,Th32;
end;
suppose
not l2 <= l1;
then consider p be Element of L such that
A40: p in PRIME L and
A41: l1 <= p and
A42: not l2 <= p by A28,Th17;
set CH = chi((downarrow p)`,the carrier of L);
p is prime by A40,Def7;
then CH in H;
then reconsider CH as Element of H;
A43: now
assume CH in F.l1;
then ex f be Element of H st f = CH & f.l1 = 1 by A34;
hence contradiction by A41,Th32;
end;
dom CH = the carrier of L by FUNCT_2:def 1;
then rng CH c= {0,1} & CH.l2 in rng CH by FUNCT_1:def 3,RELAT_1:def 19;
then CH.l2 = 0 or CH.l2 = 1 by TARSKI:def 2;
hence contradiction by A32,A33,A42,A43,Th32;
end;
end;
hence thesis;
end;
F is join-preserving
proof
let x,y be Element of L;
assume ex_sup_of {x,y},L;
thus ex_sup_of F.:{x,y},BoolePoset H by YELLOW_0:17;
A44: {f where f is Element of H: f.(x "\/" y) = 1} c= {f where f is
Element of H: f.x = 1} \/ {f where f is Element of H: f.y = 1}
proof
let p be object;
A45: 1 = Top BoolePoset {{}} by CARD_1:49,YELLOW_1:19;
assume p in {f where f is Element of H: f.(x "\/" y) = 1};
then consider g be Element of H such that
A46: g = p and
A47: g.(x "\/" y) = 1;
g in H;
then
A48: ex a be Element of L st chi((downarrow a)`, the carrier of L) = g &
a is prime;
then reconsider g as Function of L,BoolePoset {{}} by Th31;
g is join-preserving by A48,Th33;
then
A49: g preserves_sup_of {x,y};
dom g = the carrier of L by FUNCT_2:def 1;
then
A50: g.:{x,y} = {g.x,g.y} by FUNCT_1:60;
A51: ex_sup_of {x,y}, L & x"\/"y = sup {x,y} by YELLOW_0:17,41;
A52: (g.x)"\/"(g.y) = sup {g.x,g.y} by YELLOW_0:41;
A53: now
assume g.x = {} & g.y = {};
then (g.x)"\/"(g.y) = {} \/ {} by YELLOW_1:17
.= 0;
hence contradiction by A47,A50,A49,A51,A52;
end;
A54: the carrier of BoolePoset {{}} = the carrier of InclPoset bool {{}}
by YELLOW_1:4
.= bool {{}} by YELLOW_1:1
.= { {} , {{}}} by ZFMISC_1:24;
then
A55: g.y = {} or g.y = {{}} by TARSKI:def 2;
g.x = {} or g.x = {{}} by A54,TARSKI:def 2;
then g.x = Top BoolePoset {{}} or g.y = Top BoolePoset {{}} by A55,A53,
YELLOW_1:19;
then p in {f where f is Element of H: f.x = 1} or p in {f where f is
Element of H: f.y = 1} by A46,A45;
hence thesis by XBOOLE_0:def 3;
end;
A56: {f where f is Element of H: f.x = 1} \/ {f where f is Element of H: f
.y = 1} c= {f where f is Element of H: f.(x "\/" y) = 1}
proof
let p be object;
assume
A57: p in ({f where f is Element of H: f.x = 1} \/ {f where f is
Element of H: f.y = 1});
per cases by A57,XBOOLE_0:def 3;
suppose
p in {f where f is Element of H: f.x = 1};
then consider f1 be Element of H such that
A58: f1 = p and
A59: f1.x = 1;
f1 in H;
then consider a be Element of L such that
A60: chi((downarrow a)`, the carrier of L) = f1 and
A61: a is prime;
reconsider f1 as Function of L,BoolePoset {{}} by A60,Th31;
for x being Element of L holds f1.x = {} iff x <= a by A60,Th32;
then f1 is join-preserving by A61,Th25;
then
A62: f1 preserves_sup_of {x,y};
dom f1 = the carrier of L by FUNCT_2:def 1;
then
A63: {f1.x,f1.y} = f1.:{x,y} by FUNCT_1:60;
A64: 1 = Top BoolePoset {{}} & f1.y <= Top BoolePoset {{}} by CARD_1:49
,YELLOW_0:45,YELLOW_1:19;
A65: ex_sup_of {x,y}, L & x"\/"y = sup {x,y} by YELLOW_0:17,41;
(f1.x)"\/"(f1.y) = sup {f1.x,f1.y} by YELLOW_0:41;
then f1.(x "\/" y) = (f1.x)"\/"(f1.y) by A63,A62,A65
.= 1 by A59,A64,YELLOW_0:24;
hence thesis by A58;
end;
suppose
p in {f where f is Element of H: f.y = 1};
then consider f1 be Element of H such that
A66: f1 = p and
A67: f1.y = 1;
f1 in H;
then consider b be Element of L such that
A68: chi((downarrow b)`, the carrier of L) = f1 and
A69: b is prime;
reconsider f1 as Function of L,BoolePoset {{}} by A68,Th31;
for x being Element of L holds f1.x = {} iff x <= b by A68,Th32;
then f1 is join-preserving by A69,Th25;
then
A70: f1 preserves_sup_of {x,y};
dom f1 = the carrier of L by FUNCT_2:def 1;
then
A71: {f1.x,f1.y} = f1.:{x,y} by FUNCT_1:60;
A72: 1 = Top BoolePoset {{}} & f1.x <= Top BoolePoset {{}} by CARD_1:49
,YELLOW_0:45,YELLOW_1:19;
A73: ex_sup_of {x,y}, L & x"\/"y = sup {x,y} by YELLOW_0:17,41;
(f1.x)"\/"(f1.y) = sup {f1.x,f1.y} by YELLOW_0:41;
then f1.(x "\/" y) = (f1.y)"\/"(f1.x) by A71,A70,A73
.= 1 by A67,A72,YELLOW_0:24;
hence thesis by A66;
end;
end;
F.:{x,y} = {F.x,F.y} by A2,FUNCT_1:60;
hence sup (F.:{x,y}) = F.x "\/" F.y by YELLOW_0:41
.= (F.x) \/ (F.y) by YELLOW_1:17
.= {f where f is Element of H: f.x = 1} \/ (F.y) by A3
.= {f where f is Element of H: f.x = 1} \/ {f where f is Element of H:
f.y = 1} by A3
.= {f where f is Element of H: f.(x "\/" y) = 1} by A56,A44
.= F.(x "\/" y) by A3
.= F.sup {x,y} by YELLOW_0:41;
end;
hence L is distributive by A7,A29,Th3;
F is sups-preserving
proof
let X be Subset of L;
F preserves_sup_of X
proof
assume ex_sup_of X,L;
thus ex_sup_of (F.:X),BoolePoset H by YELLOW_0:17;
A74: F.(sup X) = {g where g is Element of H: g.(sup X) = 1} by A3;
A75: sup (F.:X) c= F.(sup X)
proof
let a be object;
assume a in sup (F.:X);
then a in union (F.:X) by YELLOW_1:21;
then consider Y be set such that
A76: a in Y and
A77: Y in (F.:X) by TARSKI:def 4;
consider z be object such that
A78: z in dom F and
A79: z in X and
A80: Y = F.z by A77,FUNCT_1:def 6;
reconsider z as Element of L by A78;
F.z = {f where f is Element of H: f.z = 1} by A3;
then consider f be Element of H such that
A81: a = f and
A82: f.z = 1 by A76,A80;
f in H;
then consider p be Element of L such that
A83: f = chi((downarrow p)`, the carrier of L) and
p is prime;
A84: now
sup X is_>=_than X by YELLOW_0:32;
then
A85: z <= sup X by A79;
assume f.(sup X) = 0;
then sup X <= p by A83,Th32;
then z <= p by A85,ORDERS_2:3;
hence contradiction by A82,A83,Th32;
end;
dom f = the carrier of L by A83,FUNCT_2:def 1;
then
A86: f.(sup X) in rng f by FUNCT_1:def 3;
rng f c= {0,1} by A83,RELAT_1:def 19;
then f.(sup X) = 0 or f.(sup X) = 1 by A86,TARSKI:def 2;
hence thesis by A74,A81,A84;
end;
F.(sup X) c= sup (F.:X)
proof
let a be object;
assume a in F.(sup X);
then consider f be Element of H such that
A87: a = f and
A88: f.(sup X) = 1 by A74;
f in H;
then consider p be Element of L such that
A89: f = chi((downarrow p)`, the carrier of L) and
p is prime;
A90: rng f c= {0,1} by A89,RELAT_1:def 19;
A91: not sup X <= p by A88,A89,Th32;
now
assume for l be Element of L st l in X holds l <= p;
then X is_<=_than p;
hence contradiction by A91,YELLOW_0:32;
end;
then consider l be Element of L such that
A92: l in X and
A93: not l <= p;
dom f = the carrier of L by A89,FUNCT_2:def 1;
then f.l in rng f by FUNCT_1:def 3;
then f.l = 0 or f.l = 1 by A90,TARSKI:def 2;
then f in {g where g is Element of H: g.l = 1} by A89,A93,Th32;
then
A94: f in F.l by A3;
(F.l) in (F.:X) by A2,A92,FUNCT_1:def 6;
then a in union (F.:X) by A87,A94,TARSKI:def 4;
hence thesis by YELLOW_1:21;
end;
hence thesis by A75;
end;
hence thesis;
end;
hence thesis by A7,A29,Th4;
end;
theorem Th35: ::3.14 (1-3), p.71
for L being lower-bounded continuous LATTICE holds L is
distributive iff PRIME L is order-generating
proof
let L be lower-bounded continuous LATTICE;
thus L is distributive implies PRIME L is order-generating
proof
assume L is distributive;
then
A1: PRIME L = IRR L by Th28;
IRR L \ {Top L} c= IRR L by XBOOLE_1:36;
hence thesis by A1,Th18,Th19;
end;
thus thesis by Th34;
end;
theorem ::3.14 (1-2), p.71
for L being lower-bounded continuous LATTICE holds L is distributive
iff L is Heyting
proof
let L be lower-bounded continuous LATTICE;
thus L is distributive implies L is Heyting
proof
assume L is distributive;
then PRIME L is order-generating by Th35;
then L is distributive meet-continuous by Th34;
hence thesis;
end;
thus thesis;
end;
theorem Th37:
for L being continuous complete LATTICE st for l being Element
of L ex X being Subset of L st l = sup X & for x being Element of L st x in X
holds x is co-prime for l being Element of L holds l = "\/"((waybelow l) /\
PRIME(L opp), L)
proof
let L be continuous complete LATTICE;
defpred P[object,object] means
ex A being set st A = $2 & A c= PRIME L~ & $1 = "\/"(A,L);
assume
A1: for l being Element of L ex X being Subset of L st l = sup X & for x
being Element of L st x in X holds x is co-prime;
A2: for e be object st e in the carrier of L ex u be object st P[e,u]
proof
let e be object;
assume e in the carrier of L;
then reconsider l = e as Element of L;
consider X being Subset of L such that
A3: l = sup X and
A4: for x being Element of L st x in X holds x is co-prime by A1;
now
let p1 be object;
assume
A5: p1 in X;
then reconsider p = p1 as Element of L;
p is co-prime by A4,A5;
then p~ is prime;
hence p1 in PRIME L~ by Def7;
end;
then X c= PRIME L~;
hence thesis by A3;
end;
consider f being Function such that
A6: dom f = the carrier of L and
A7: for e be object st e in the carrier of L holds P[e, f.e] from CLASSES1
:sch 1(A2);
let l be Element of L;
A8: ex_sup_of ((waybelow l) /\ PRIME(L~)),L by YELLOW_0:17;
A9: waybelow l c= {sup X where X is Subset of L : X in rng f & sup X in
waybelow l}
proof
let e be object;
assume
A10: e in waybelow l;
then
A11: P[e,f.e] by A7;
then f.e c= PRIME L~;
then
A12: f.e c= the carrier of L~ by XBOOLE_1:1;
e = "\/"((f.e),L) & f.e in rng f by A6,FUNCT_1:def 3,A11;
hence thesis by A10,A12;
end;
defpred P[Subset of L] means $1 in rng f & sup $1 in waybelow l;
A13: l = sup waybelow l by WAYBEL_3:def 5;
set Z = union {X where X is Subset of L : X in rng f & sup X in waybelow l};
A14: Z c= (waybelow l) /\ PRIME(L~)
proof
let e be object;
assume e in Z;
then consider Y be set such that
A15: e in Y and
A16: Y in {X where X is Subset of L : X in rng f & sup X in waybelow l
} by TARSKI:def 4;
consider X be Subset of L such that
A17: Y = X and
A18: X in rng f and
A19: sup X in waybelow l by A16;
reconsider e1 = e as Element of L by A15,A17;
e1 <= sup X by A15,A17,YELLOW_2:22;
then
A20: e in waybelow l by A19,WAYBEL_0:def 19;
consider r be object such that
A21: r in dom f & X = f.r by A18,FUNCT_1:def 3;
P[r,f.r] by A6,A7,A21;
then X c= PRIME(L~) by A21;
hence thesis by A15,A17,A20,XBOOLE_0:def 4;
end;
A22: ex_sup_of Z,L by YELLOW_0:17;
ex_sup_of (waybelow l),L by YELLOW_0:17;
then
A23: "\/"((waybelow l) /\ PRIME(L~),L) <= "\/"(waybelow l,L) by A8,XBOOLE_1:17
,YELLOW_0:34;
{sup X where X is Subset of L : P[X] } c= waybelow l
proof
let e be object;
assume
e in {sup X where X is Subset of L : X in rng f & sup X in waybelow l};
then
ex X be Subset of L st e = sup X & X in rng f & sup X in waybelow l;
hence thesis;
end;
then l = "\/"({sup X where X is Subset of L : P[X]}, L) by A13,A9,
XBOOLE_0:def 10
.= "\/"(union {X where X is Subset of L : P[X]}, L) from YELLOW_3:sch 5;
then l <= "\/"((waybelow l) /\ PRIME(L~),L) by A22,A8,A14,YELLOW_0:34;
hence thesis by A13,A23,ORDERS_2:2;
end;
Lm2: for L being continuous complete LATTICE st for l being Element of L ex X
being Subset of L st l = sup X & for x being Element of L st x in X holds x is
co-prime holds L is completely-distributive
proof
let L be continuous complete LATTICE such that
A1: for l being Element of L ex X being Subset of L st l = sup X & for x
being Element of L st x in X holds x is co-prime;
thus L is complete;
let J be non empty set, K be non-empty ManySortedSet of J;
let F be DoubleIndexedSet of K,L;
set l = Inf Sups F;
set X = (waybelow l) /\ PRIME(L~);
A2: X c= waybelow l by XBOOLE_1:17;
reconsider X as Subset of L;
A3: dom F = J by PARTFUN1:def 2;
A4: for x being Element of L st x in X holds x is co-prime
proof
let x be Element of L;
assume x in X;
then x in PRIME(L~) by XBOOLE_0:def 4;
then x~ is prime by Def7;
hence thesis;
end;
A5: inf rng Sups F = Inf Sups F by YELLOW_2:def 6;
X is_<=_than Sup Infs Frege F
proof
let p be Element of L;
defpred P[object,object] means
$2 in K.$1 & [p,(F.$1).$2] in the InternalRel of L;
assume
A6: p in X;
A7: for j being object st j in J ex k being object st P[j,k]
proof
let j1 be object;
assume j1 in J;
then reconsider j = j1 as Element of J;
set k = the Element of K.j;
dom (Sups F) = J by A3,FUNCT_2:def 1;
then
A8: (Sups F).j in rng Sups F by FUNCT_1:def 3;
A9: p << l & Sup (F.j) = sup rng (F.j) by A2,A6,WAYBEL_3:7,YELLOW_2:def 5;
Sup (F.j) = (Sups F).j by A3,WAYBEL_5:def 1;
then l <= Sup (F.j) by A5,A8,YELLOW_2:22;
then consider A being finite Subset of L such that
A10: A c= rng (F.j) and
A11: p <= sup A by A9,WAYBEL_3:18;
ex_sup_of A,L & ex_sup_of (A \/ {F.j.k}),L by YELLOW_0:17;
then sup A <= sup (A \/ {F.j.k}) by XBOOLE_1:7,YELLOW_0:34;
then
A12: p <= sup (A \/ {F.j.k}) by A11,ORDERS_2:3;
p is co-prime by A4,A6;
then consider a be Element of L such that
A13: a in (A \/ {F.j.k}) and
A14: p <= a by A12,Th23;
per cases by A13,XBOOLE_0:def 3;
suppose
a in A;
then consider k1 be object such that
A15: k1 in dom (F.j) and
A16: a = F.j.k1 by A10,FUNCT_1:def 3;
reconsider k1 as Element of K.j by A15;
[p,(F.j).k1] in the InternalRel of L by A14,A16,ORDERS_2:def 5;
hence thesis;
end;
suppose
a in {F.j.k};
then a = F.j.k by TARSKI:def 1;
then [p,(F.j).k] in the InternalRel of L by A14,ORDERS_2:def 5;
hence thesis;
end;
end;
consider f1 being Function such that
A17: dom f1 = J and
A18: for j being object st j in J holds P[j, f1.j]
from CLASSES1:sch 1(
A7);
now
let g be object;
assume g in dom doms F;
then g in dom F by FUNCT_6:def 2;
hence g in dom f1 by A17;
end;
then
A19: dom doms F c= dom f1;
for g being object st g in dom f1 holds g in dom doms F
by FUNCT_6:def 2,A3,A17;
then dom f1 c= dom doms F;
then
A20: dom f1 = dom doms F by A19;
A21: for b be object st b in dom doms F holds f1.b in (doms F).b
proof
let b be object;
assume
A22: b in dom doms F;
then
A23: F.b is Function of K.b, the carrier of L by A17,A19,WAYBEL_5:6;
(doms F).b = dom (F.b) by A3,A17,A19,A22,FUNCT_6:22
.= K.b by A23,FUNCT_2:def 1;
hence thesis by A17,A18,A19,A22;
end;
then reconsider D = product doms F as non empty set by A20,CARD_3:9;
reconsider f = f1 as Element of product doms F by A20,A21,CARD_3:9;
A24: f1 in product doms F by A20,A21,CARD_3:9;
p is_<=_than rng ((Frege F).f)
proof
let b be Element of L;
assume b in rng ((Frege F).f);
then consider a be object such that
A25: a in dom ((Frege F).f) and
A26: b = ((Frege F).f).a by FUNCT_1:def 3;
reconsider a as Element of J by A25;
f in dom Frege F by A24,PARTFUN1:def 2;
then ((Frege F).f).a = (F.a).(f1.a) by A3,WAYBEL_5:9;
then [p,((Frege F).f).a] in the InternalRel of L by A18;
hence p <= b by A26,ORDERS_2:def 5;
end;
then p <= inf rng ((Frege F).f) by YELLOW_0:33;
then
A27: p <= Inf((Frege F).f) by YELLOW_2:def 6;
reconsider P= D --> J as ManySortedSet of D;
reconsider R = Frege F as DoubleIndexedSet of P, L;
reconsider f2 = f as Element of D;
Inf(R.f2) in rng Infs (R) by WAYBEL_5:14;
then Inf((Frege F).f) <= sup rng Infs Frege F by YELLOW_2:22;
then Inf((Frege F).f) <= Sup Infs Frege F by YELLOW_2:def 5;
hence thesis by A27,ORDERS_2:3;
end;
then
A28: sup X <= Sup Infs Frege F by YELLOW_0:32;
Inf Sups F >= Sup Infs Frege F & Inf Sups F = sup X by A1,Th37,WAYBEL_5:16;
hence thesis by A28,ORDERS_2:2;
end;
Lm3: for L being completely-distributive complete LATTICE holds L is
distributive continuous & L~ is continuous
proof
let L be completely-distributive complete LATTICE;
L~ is completely-distributive by YELLOW_7:51;
hence thesis;
end;
Lm4: for L being complete LATTICE st L is distributive continuous & L~ is
continuous holds for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime
proof
let L be complete LATTICE;
assume that
A1: L is distributive continuous and
A2: L~ is continuous;
let l be Element of L;
reconsider L as distributive continuous complete LATTICE by A1;
reconsider l1 = l as Element of L~;
PRIME L~ is order-generating by A2,Th35;
then consider Y be Subset of (PRIME L~) such that
A3: l1 = "/\" (Y,L~) by Th15;
reconsider Y as Subset of L by XBOOLE_1:1;
A4: for x being Element of L st x in Y holds x is co-prime
by Def7;
ex_sup_of Y,L by YELLOW_0:17;
then "\/"(Y,L) = "/\"(Y,L~) by YELLOW_7:12;
hence thesis by A3,A4;
end;
theorem ::3.15 (2-1), p.72
for L being complete LATTICE holds L is completely-distributive iff L
is continuous & for l being Element of L ex X being Subset of L st l = sup X &
for x being Element of L st x in X holds x is co-prime
proof
let L be complete LATTICE;
thus L is completely-distributive implies L is continuous & for l being
Element of L ex X being Subset of L st l = sup X & for x being Element of L st
x in X holds x is co-prime
proof
assume L is completely-distributive;
then reconsider L as completely-distributive LATTICE;
L~ is continuous by Lm3;
hence thesis by Lm4;
end;
thus thesis by Lm2;
end;
theorem ::3.15 (2-3), p.72
for L being complete LATTICE holds L is completely-distributive iff L
is distributive continuous & L opp is continuous
proof
let L be complete LATTICE;
thus L is completely-distributive implies L is distributive continuous & L~
is continuous by Lm3;
assume that
A1: L is distributive continuous and
A2: L~ is continuous;
reconsider L as distributive continuous LATTICE by A1;
for l being Element of L ex X being Subset of L st l = sup X & for x
being Element of L st x in X holds x is co-prime by A2,Lm4;
hence thesis by Lm2;
end;