:: WAYBEL_6 semantic presentation
begin
scheme :: WAYBEL_6:sch 1
NonUniqExD1{ F1() -> non empty RelStr , F2() -> Subset of F1(), F3() -> non empty Subset of F1(), P1[ set , set ] } :
ex f being Function of F2(),F3() st
for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
provided
A1: for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & P1[e,u] )
proof
A2: for e being set st e in F2() holds
ex u being set st
( u in F3() & P1[e,u] )
proof
let e be set ; ::_thesis: ( e in F2() implies ex u being set st
( u in F3() & P1[e,u] ) )
assume A3: e in F2() ; ::_thesis: ex u being set st
( u in F3() & P1[e,u] )
then reconsider e1 = e as Element of F2() ;
reconsider e1 = e1 as Element of F1() by A3;
consider u being Element of F1() such that
A4: ( u in F3() & P1[e1,u] ) by A1, A3;
reconsider u1 = u as set ;
take u1 ; ::_thesis: ( u1 in F3() & P1[e,u1] )
thus ( u1 in F3() & P1[e,u1] ) by A4; ::_thesis: verum
end;
consider f being Function such that
A5: ( dom f = F2() & rng f c= F3() ) and
A6: for e being set st e in F2() holds
P1[e,f . e] from FUNCT_1:sch_5(A2);
reconsider f = f as Function of F2(),F3() by A5, FUNCT_2:def_1, RELSET_1:4;
take f ; ::_thesis: for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
proof
let e be Element of F1(); ::_thesis: ( e in F2() implies ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] ) )
assume A7: e in F2() ; ::_thesis: ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] )
then reconsider e1 = f . e as Element of F3() by FUNCT_2:5;
reconsider fe = e1 as Element of F1() ;
take fe ; ::_thesis: ( fe in F3() & fe = f . e & P1[e,fe] )
thus ( fe in F3() & fe = f . e & P1[e,fe] ) by A6, A7; ::_thesis: verum
end;
hence for e being Element of F1() st e in F2() holds
ex u being Element of F1() st
( u in F3() & u = f . e & P1[e,u] ) ; ::_thesis: verum
end;
definition
let L be LATTICE;
let A be non empty Subset of L;
let f be Function of A,A;
let n be Element of NAT ;
:: original: iter
redefine func iter (f,n) -> Function of A,A;
coherence
iter (f,n) is Function of A,A by FUNCT_7:83;
end;
definition
let L be LATTICE;
let C, D be non empty Subset of L;
let f be Function of C,D;
let c be Element of C;
:: original: .
redefine funcf . c -> Element of L;
coherence
f . c is Element of L
proof
f . c in D ;
hence f . c is Element of L ; ::_thesis: verum
end;
end;
registration
let L be non empty Poset;
cluster strongly_connected -> directed filtered for Element of bool the carrier of L;
coherence
for b1 being Chain of L holds
( b1 is filtered & b1 is directed )
proof
let C be Chain of L; ::_thesis: ( C is filtered & C is directed )
A1: the InternalRel of L is_strongly_connected_in C by ORDERS_2:def_7;
thus C is filtered ::_thesis: C is directed
proof
let x, y be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in C or not y in C or ex b1 being Element of the carrier of L st
( b1 in C & b1 <= x & b1 <= y ) )
A2: ( x <= x & y <= y ) ;
assume A3: ( x in C & y in C ) ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in C & b1 <= x & b1 <= y )
then ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A1, RELAT_2:def_7;
then ( x <= y or y <= x ) by ORDERS_2:def_5;
hence ex b1 being Element of the carrier of L st
( b1 in C & b1 <= x & b1 <= y ) by A3, A2; ::_thesis: verum
end;
let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in C or not y in C or ex b1 being Element of the carrier of L st
( b1 in C & x <= b1 & y <= b1 ) )
A4: ( x <= x & y <= y ) ;
assume A5: ( x in C & y in C ) ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in C & x <= b1 & y <= b1 )
then ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A1, RELAT_2:def_7;
then ( x <= y or y <= x ) by ORDERS_2:def_5;
hence ex b1 being Element of the carrier of L st
( b1 in C & x <= b1 & y <= b1 ) by A5, A4; ::_thesis: verum
end;
end;
registration
cluster non empty strict V110() reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima continuous for RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & b1 is continuous & b1 is distributive & b1 is lower-bounded )
proof
set x1 = the set ;
set R = the Order of { the set };
reconsider RS = RelStr(# { the set }, the Order of { the set } #) as 1 -element reflexive RelStr ;
take RS ; ::_thesis: ( RS is strict & RS is continuous & RS is distributive & RS is lower-bounded )
thus ( RS is strict & RS is continuous & RS is distributive & RS is lower-bounded ) ; ::_thesis: verum
end;
end;
theorem Th1: :: WAYBEL_6:1
for S, T being Semilattice
for 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; ::_thesis: for 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) )
let f be Function of S,T; ::_thesis: ( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )
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) ) ::_thesis: ( ( for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) implies f is meet-preserving )
proof
assume A2: f is meet-preserving ; ::_thesis: for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y)
let z, y be Element of S; ::_thesis: f . (z "/\" y) = (f . z) "/\" (f . y)
A3: f preserves_inf_of {z,y} by A2, WAYBEL_0:def_34;
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, WAYBEL_0:def_30
.= (f . z) "/\" (f . y) by YELLOW_0:40 ; ::_thesis: verum
end;
assume A5: for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ; ::_thesis: f is meet-preserving
for z, y being Element of S holds f preserves_inf_of {z,y}
proof
let z, y be Element of S; ::_thesis: f preserves_inf_of {z,y}
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 f preserves_inf_of {z,y} by A7, WAYBEL_0:def_30; ::_thesis: verum
end;
hence f is meet-preserving by WAYBEL_0:def_34; ::_thesis: verum
end;
theorem Th2: :: WAYBEL_6:2
for S, T being sup-Semilattice
for 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; ::_thesis: for 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) )
let f be Function of S,T; ::_thesis: ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )
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) ) ::_thesis: ( ( for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) implies f is join-preserving )
proof
assume A2: f is join-preserving ; ::_thesis: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y)
let z, y be Element of S; ::_thesis: f . (z "\/" y) = (f . z) "\/" (f . y)
A3: f preserves_sup_of {z,y} by A2, WAYBEL_0:def_35;
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, WAYBEL_0:def_31
.= (f . z) "\/" (f . y) by YELLOW_0:41 ; ::_thesis: verum
end;
assume A5: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ; ::_thesis: f is join-preserving
for z, y being Element of S holds f preserves_sup_of {z,y}
proof
let z, y be Element of S; ::_thesis: f preserves_sup_of {z,y}
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 f preserves_sup_of {z,y} by A7, WAYBEL_0:def_31; ::_thesis: verum
end;
hence f is join-preserving by WAYBEL_0:def_35; ::_thesis: verum
end;
theorem Th3: :: WAYBEL_6:3
for S, T being LATTICE
for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V24() holds
S is distributive
proof
let S, T be LATTICE; ::_thesis: for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V24() holds
S is distributive
let f be Function of S,T; ::_thesis: ( T is distributive & f is meet-preserving & f is join-preserving & f is V24() implies S is distributive )
assume that
A1: T is distributive and
A2: ( f is meet-preserving & f is join-preserving & f is V24() ) ; ::_thesis: S is distributive
let x, y, z be Element of S; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
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, WAYBEL_1:def_3
.= ((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, FUNCT_2:19; ::_thesis: verum
end;
registration
let S, T be complete LATTICE;
cluster Relation-like the carrier of S -defined the carrier of T -valued Function-like V32( the carrier of S, the carrier of T) sups-preserving for Element of bool [: the carrier of S, the carrier of T:];
existence
ex b1 being Function of S,T st b1 is sups-preserving
proof
set t = Bottom T;
set f = S --> (Bottom T);
take S --> (Bottom T) ; ::_thesis: S --> (Bottom T) is sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: S --> (Bottom T) preserves_sup_of X
assume ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (S --> (Bottom T)) .: X,T & "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) )
thus ex_sup_of (S --> (Bottom T)) .: X,T by YELLOW_0:17; ::_thesis: "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S))
( (S --> (Bottom T)) .: X c= rng (S --> (Bottom T)) & rng (S --> (Bottom T)) c= {(Bottom T)} ) by FUNCOP_1:13, RELAT_1:111;
then (S --> (Bottom T)) .: X c= {(Bottom T)} by XBOOLE_1:1;
then A1: ( (S --> (Bottom T)) .: X = {(Bottom T)} or (S --> (Bottom T)) .: X = {} ) by ZFMISC_1:33;
percases ( X = {} or X <> {} ) ;
suppose X = {} ; ::_thesis: "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S))
then (S --> (Bottom T)) .: X = {} ;
then sup ((S --> (Bottom T)) .: X) = Bottom T by YELLOW_0:def_11;
hence "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S)) by FUNCOP_1:7; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: "\/" (((S --> (Bottom T)) .: X),T) = (S --> (Bottom T)) . ("\/" (X,S))
then reconsider X1 = X as non empty Subset of S ;
set x = the Element of X1;
(S --> (Bottom T)) . the Element of X1 in (S --> (Bottom T)) .: X by FUNCT_2:35;
hence sup ((S --> (Bottom T)) .: X) = Bottom T by A1, YELLOW_0:39
.= (S --> (Bottom T)) . (sup X) by FUNCOP_1:7 ;
::_thesis: verum
end;
end;
end;
end;
Lm1: for S, T being non empty with_suprema Poset
for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
proof
let S, T be non empty with_suprema Poset; ::_thesis: for f being Function of S,T st f is directed-sups-preserving holds
f is monotone
let f be Function of S,T; ::_thesis: ( f is directed-sups-preserving implies f is monotone )
assume A1: f is directed-sups-preserving ; ::_thesis: f is monotone
let x, y be Element of S; :: according to ORDERS_3:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
assume A2: x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )
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} holds
ex z being Element of S st
( z in {x,y} & a <= z & b <= z )
proof
let a, b be Element of S; ::_thesis: ( a in {x,y} & b in {x,y} implies ex z being Element of S st
( z in {x,y} & a <= z & b <= z ) )
assume A4: ( a in {x,y} & b in {x,y} ) ; ::_thesis: ex z being Element of S st
( z in {x,y} & a <= z & b <= z )
take y ; ::_thesis: ( y in {x,y} & a <= y & b <= y )
thus y in {x,y} by TARSKI:def_2; ::_thesis: ( a <= y & b <= y )
thus ( a <= y & b <= y ) by A2, A4, TARSKI:def_2; ::_thesis: verum
end;
then ( {x,y} is directed & not {x,y} is empty ) by WAYBEL_0:def_1;
then A5: f preserves_sup_of {x,y} by A1, WAYBEL_0:def_37;
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, WAYBEL_0:def_31
.= 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; ::_thesis: ( not afx = f . x or not bfy = f . y or afx <= bfy )
assume ( afx = f . x & bfy = f . y ) ; ::_thesis: afx <= bfy
hence afx <= bfy by A8, YELLOW_0:22; ::_thesis: verum
end;
theorem Th4: :: WAYBEL_6:4
for S, T being complete LATTICE
for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V24() holds
S is meet-continuous
proof
let S, T be complete LATTICE; ::_thesis: for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V24() holds
S is meet-continuous
let f be sups-preserving Function of S,T; ::_thesis: ( T is meet-continuous & f is meet-preserving & f is V24() implies S is meet-continuous )
assume that
A1: T is meet-continuous and
A2: ( f is meet-preserving & f is V24() ) ; ::_thesis: S is meet-continuous
S is satisfying_MC
proof
let x be Element of S; :: according to WAYBEL_2:def_6 ::_thesis: for b1 being Element of bool the carrier of S holds x "/\" ("\/" (b1,S)) = "\/" (({x} "/\" b1),S)
let D be non empty directed Subset of S; ::_thesis: x "/\" ("\/" (D,S)) = "\/" (({x} "/\" D),S)
A3: ( ex_sup_of D,S & f preserves_sup_of D ) by WAYBEL_0:75, WAYBEL_0:def_33;
reconsider Y = {x} as non empty directed Subset of S by WAYBEL_0:5;
A4: ( ex_sup_of Y "/\" D,S & f preserves_sup_of {x} "/\" D ) by WAYBEL_0:75, WAYBEL_0: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 set ; :: according to TARSKI:def_3 ::_thesis: ( not p in {(f . x)} "/\" (f .: D) or p in f .: ({x} "/\" D) )
assume p in {(f . x)} "/\" (f .: D) ; ::_thesis: p in f .: ({x} "/\" D)
then consider y being Element of T such that
A8: p = (f . x) "/\" y and
A9: y in f .: D by A6;
consider k being set 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 = 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, WAYBEL_0:def_34;
then p = f . (x "/\" k) by A8, A12, YELLOW_3:8;
hence p in f .: ({x} "/\" D) by A5, A13, FUNCT_1:def_6; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not p in f .: ({x} "/\" D) or p in {(f . x)} "/\" (f .: D) )
assume p in f .: ({x} "/\" D) ; ::_thesis: p in {(f . x)} "/\" (f .: D)
then consider m being set 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 = m as Element of S by A16;
consider a being 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, WAYBEL_0:def_34;
then A21: p = (f . x) "/\" fa by A18, A19, YELLOW_3:8;
fa in f .: D by A5, A20, FUNCT_1:def_6;
hence p in {(f . x)} "/\" (f .: D) by A6, A21; ::_thesis: verum
end;
f . (x "/\" (sup D)) = (f . x) "/\" (f . (sup D)) by A2, Th1
.= (f . x) "/\" (sup X) by A3, WAYBEL_0:def_31
.= 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, WAYBEL_0:def_31 ;
hence x "/\" (sup D) = sup ({x} "/\" D) by A2, A5, FUNCT_1:def_4; ::_thesis: verum
end;
hence S is meet-continuous ; ::_thesis: verum
end;
begin
definition
let L be non empty reflexive RelStr ;
let X be Subset of L;
attrX is Open means :Def1: :: WAYBEL_6:def 1
for x being Element of L st x in X holds
ex y being Element of L st
( y in X & y << x );
end;
:: deftheorem Def1 defines Open WAYBEL_6:def_1_:_
for L being non empty reflexive RelStr
for X being Subset of L holds
( X is Open iff for x being Element of L st x in X holds
ex y being Element of L st
( y in X & y << x ) );
theorem :: WAYBEL_6:5
for L being up-complete LATTICE
for X being upper Subset of L holds
( X is Open iff for x being Element of L st x in X holds
waybelow x meets X )
proof
let L be up-complete LATTICE; ::_thesis: for X being upper Subset of L holds
( X is Open iff for x being Element of L st x in X holds
waybelow x meets X )
let X be upper Subset of L; ::_thesis: ( X is Open iff for x being Element of L st x in X holds
waybelow x meets X )
hereby ::_thesis: ( ( for x being Element of L st x in X holds
waybelow x meets X ) implies X is Open )
assume A1: X is Open ; ::_thesis: for x being Element of L st x in X holds
waybelow x meets X
thus for x being Element of L st x in X holds
waybelow x meets X ::_thesis: verum
proof
let x be Element of L; ::_thesis: ( x in X implies waybelow x meets X )
assume x in X ; ::_thesis: waybelow x meets X
then consider y being Element of L such that
A2: y in X and
A3: y << x by A1, Def1;
y in { y1 where y1 is Element of L : y1 << x } by A3;
then y in waybelow x by WAYBEL_3:def_3;
hence waybelow x meets X by A2, XBOOLE_0:3; ::_thesis: verum
end;
end;
assume A4: for x being Element of L st x in X holds
waybelow x meets X ; ::_thesis: X is Open
now__::_thesis:_for_x1_being_Element_of_L_st_x1_in_X_holds_
ex_z_being_Element_of_L_st_
(_z_in_X_&_z_<<_x1_)
let x1 be Element of L; ::_thesis: ( x1 in X implies ex z being Element of L st
( z in X & z << x1 ) )
assume x1 in X ; ::_thesis: ex z being Element of L st
( z in X & z << x1 )
then waybelow x1 meets X by A4;
then consider y being set 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 being Element of L st
( z = y & z << x1 ) by A5;
hence ex z being Element of L st
( z in X & z << x1 ) by A6; ::_thesis: verum
end;
hence X is Open by Def1; ::_thesis: verum
end;
theorem :: WAYBEL_6:6
for L being up-complete LATTICE
for X being 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; ::_thesis: for X being upper Subset of L holds
( X is Open iff X = union { (wayabove x) where x is Element of L : x in X } )
let X be upper Subset of L; ::_thesis: ( X is Open iff X = union { (wayabove x) where x is Element of L : x in X } )
hereby ::_thesis: ( X = union { (wayabove x) where x is Element of L : x in X } implies X is Open )
assume A1: X is Open ; ::_thesis: X = union { (wayabove x) where x is Element of L : x in X }
A2: X c= union { (wayabove x) where x is Element of L : x in X }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in union { (wayabove x) where x is Element of L : x in X } )
assume A3: z in X ; ::_thesis: z in union { (wayabove x) where x is Element of L : x in X }
then reconsider x1 = z as Element of X ;
reconsider x1 = x1 as Element of L by A3;
consider y being Element of L such that
A4: y in X and
A5: y << x1 by A1, A3, Def1;
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 z in union { (wayabove x) where x is Element of L : x in X } by A6, TARSKI:def_4; ::_thesis: verum
end;
union { (wayabove x) where x is Element of L : x in X } c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union { (wayabove x) where x is Element of L : x in X } or z in X )
assume z in union { (wayabove x) where x is Element of L : x in X } ; ::_thesis: z in X
then consider Y being 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 being 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 being Element of L such that
A11: z1 = z and
A12: z1 >> x ;
x <= z1 by A12, WAYBEL_3:1;
hence z in X by A10, A11, WAYBEL_0:def_20; ::_thesis: verum
end;
hence X = union { (wayabove x) where x is Element of L : x in X } by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
assume A13: X = union { (wayabove x) where x is Element of L : x in X } ; ::_thesis: X is Open
now__::_thesis:_for_x1_being_Element_of_L_st_x1_in_X_holds_
ex_x_being_Element_of_L_st_
(_x_in_X_&_x_<<_x1_)
let x1 be Element of L; ::_thesis: ( x1 in X implies ex x being Element of L st
( x in X & x << x1 ) )
assume x1 in X ; ::_thesis: ex x being Element of L st
( x in X & x << x1 )
then consider Y being 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 being 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 being Element of L st
( z1 = x1 & z1 >> x ) ;
hence ex x being Element of L st
( x in X & x << x1 ) by A17; ::_thesis: verum
end;
hence X is Open by Def1; ::_thesis: verum
end;
registration
let L be lower-bounded up-complete LATTICE;
cluster non empty filtered upper Open for Element of bool the carrier of L;
existence
ex b1 being Filter of L st b1 is Open
proof
take [#] L ; ::_thesis: [#] L is Open
now__::_thesis:_for_x_being_Element_of_L_st_x_in_[#]_L_holds_
ex_y_being_Element_of_L_st_
(_y_in_[#]_L_&_y_<<_x_)
let x be Element of L; ::_thesis: ( x in [#] L implies ex y being Element of L st
( y in [#] L & y << x ) )
assume x in [#] L ; ::_thesis: ex y being Element of L st
( y in [#] L & y << x )
Bottom L << x by WAYBEL_3:4;
hence ex y being Element of L st
( y in [#] L & y << x ) ; ::_thesis: verum
end;
hence [#] L is Open by Def1; ::_thesis: verum
end;
end;
theorem :: WAYBEL_6:7
for L being lower-bounded continuous LATTICE
for x being Element of L holds wayabove x is Open
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for x being Element of L holds wayabove x is Open
let x be Element of L; ::_thesis: wayabove x is Open
for l being Element of L st l in wayabove x holds
ex y being Element of L st
( y in wayabove x & y << l )
proof
let l be Element of L; ::_thesis: ( l in wayabove x implies ex y being Element of L st
( y in wayabove x & y << l ) )
assume l in wayabove x ; ::_thesis: ex y being Element of L st
( y in wayabove x & y << l )
then x << l by WAYBEL_3:8;
then consider y being Element of L such that
A1: ( x << y & y << l ) by WAYBEL_4:52;
take y ; ::_thesis: ( y in wayabove x & y << l )
thus ( y in wayabove x & y << l ) by A1, WAYBEL_3:8; ::_thesis: verum
end;
hence wayabove x is Open by Def1; ::_thesis: verum
end;
theorem Th8: :: WAYBEL_6:8
for L being lower-bounded continuous LATTICE
for x, y being Element of L st x << y holds
ex F being Open Filter of L st
( y in F & F c= wayabove x )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for x, y being Element of L st x << y holds
ex F being Open Filter of L st
( y in F & F c= wayabove x )
let x, y be Element of L; ::_thesis: ( x << y implies ex F being Open Filter of L st
( y in F & F c= wayabove x ) )
defpred S1[ Element of L, Element of L] means $2 << $1;
assume A1: x << y ; ::_thesis: ex F being Open Filter of L st
( y in F & F c= wayabove x )
then reconsider W = wayabove x as non empty Subset of L by WAYBEL_3:8;
A2: for z being Element of L st z in W holds
ex z1 being Element of L st
( z1 in W & S1[z,z1] )
proof
let z be Element of L; ::_thesis: ( z in W implies ex z1 being Element of L st
( z1 in W & S1[z,z1] ) )
assume z in W ; ::_thesis: ex z1 being Element of L st
( z1 in W & S1[z,z1] )
then x << z by WAYBEL_3:8;
then consider x9 being 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 ex z1 being Element of L st
( z1 in W & S1[z,z1] ) by A4; ::_thesis: verum
end;
consider f being Function of W,W such that
A5: for z being Element of L st z in W holds
ex z1 being Element of L st
( z1 in W & z1 = f . z & S1[z,z1] ) from WAYBEL_6:sch_1(A2);
set V = { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ;
now__::_thesis:_for_u1_being_set_st_u1_in__{__(uparrow_z)_where_z_is_Element_of_L_:_ex_n_being_Element_of_NAT_st_z_=_(iter_(f,n))_._y__}__holds_
u1_in_bool_the_carrier_of_L
let u1 be set ; ::_thesis: ( u1 in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } implies u1 in bool the carrier of L )
assume u1 in { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; ::_thesis: u1 in bool the carrier of L
then ex z being 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 ; ::_thesis: verum
end;
then reconsider V = { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } as Subset-Family of L by TARSKI:def_3;
A6: for X, Y being Subset of L st X in V & Y in V holds
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; ::_thesis: ( X in V & Y in V implies ex Z being Subset of L st
( Z in V & X \/ Y c= Z ) )
assume that
A7: X in V and
A8: Y in V ; ::_thesis: ex Z being Subset of L st
( Z in V & X \/ Y c= Z )
consider z2 being 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 being Element of NAT such that
A11: z2 = (iter (f,n2)) . y by A10;
consider z1 being 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 being 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 ; ::_thesis: for k being Element of NAT holds (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1
defpred S2[ Element of NAT ] means (iter (f,(n + $1))) . y1 <= (iter (f,n)) . y1;
A16: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A17: (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 ; ::_thesis: S2[k + 1]
set nk = (iter (f,(n + k))) . y1;
(iter (f,(n + k))) . y1 in W by FUNCT_2:5;
then consider znk being Element of L such that
znk in W and
A18: znk = f . ((iter (f,(n + k))) . y1) and
A19: znk << (iter (f,(n + k))) . y1 by A5;
dom (iter (f,(n + k))) = 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 <= (iter (f,(n + k))) . y1 by A19, WAYBEL_3:1;
hence S2[k + 1] by A17, A20, ORDERS_2:3; ::_thesis: verum
end;
A21: S2[ 0 ] ;
for k being Element of NAT holds S2[k] from NAT_1:sch_1(A21, A16);
hence for k being Element of NAT holds (iter (f,(n + k))) . y1 <= (iter (f,n)) . y1 ; ::_thesis: verum
end;
A22: now__::_thesis:_uparrow_(z1_"/\"_z2)_in_V
percases ( n1 <= n2 or n2 <= n1 ) ;
suppose n1 <= n2 ; ::_thesis: uparrow (z1 "/\" z2) in V
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 (z1 "/\" z2) in V by A8, A9, YELLOW_0:25; ::_thesis: verum
end;
suppose n2 <= n1 ; ::_thesis: uparrow (z1 "/\" z2) in V
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 (z1 "/\" z2) in V by A7, A12, YELLOW_0:25; ::_thesis: verum
end;
end;
end;
z1 "/\" z2 <= z2 by YELLOW_0:23;
then A25: uparrow z2 c= uparrow (z1 "/\" z2) by WAYBEL_0:22;
z1 "/\" z2 <= z1 by YELLOW_0:23;
then uparrow z1 c= uparrow (z1 "/\" z2) by WAYBEL_0:22;
hence ex Z being Subset of L st
( Z in V & X \/ Y c= Z ) by A12, A9, A22, A25, XBOOLE_1:8; ::_thesis: verum
end;
A26: for X being Subset of L st X in V holds
X is filtered
proof
let X be Subset of L; ::_thesis: ( X in V implies X is filtered )
assume X in V ; ::_thesis: X is filtered
then ex z being Element of L st
( X = uparrow z & ex n being Element of NAT st z = (iter (f,n)) . y ) ;
hence X is filtered ; ::_thesis: verum
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__::_thesis:_for_u1_being_set_st_u1_in_union__{__(uparrow_z)_where_z_is_Element_of_L_:_ex_n_being_Element_of_NAT_st_z_=_(iter_(f,n))_._y__}__holds_
u1_in_the_carrier_of_L
let u1 be set ; ::_thesis: ( u1 in union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } implies u1 in the carrier of L )
assume u1 in union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } ; ::_thesis: u1 in the carrier of L
then consider Y being 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 being 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 being 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 ; ::_thesis: verum
end;
then reconsider F = union { (uparrow z) where z is Element of L : ex n being Element of NAT st z = (iter (f,n)) . y } as Subset of L by TARSKI:def_3;
A31: y in wayabove x by A1, WAYBEL_3:8;
A32: now__::_thesis:_for_u1_being_Element_of_L_st_u1_in_F_holds_
ex_g_being_Element_of_L_st_
(_g_in_F_&_g_<<_u1_)
let u1 be Element of L; ::_thesis: ( u1 in F implies ex g being Element of L st
( g in F & g << u1 ) )
assume u1 in F ; ::_thesis: ex g being Element of L st
( g in F & g << u1 )
then consider Y being 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 being 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 being 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 being 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 being Element of L st
( g in F & g << u1 ) by A42, A44, A39, A41, WAYBEL_3:2; ::_thesis: verum
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; ::_thesis: ( X in V implies X is upper )
assume X in V ; ::_thesis: X is upper
then ex z being Element of L st
( X = uparrow z & ex n being Element of NAT st z = (iter (f,n)) . y ) ;
hence X is upper ; ::_thesis: verum
end;
then reconsider F = F as Open Filter of L by A27, A47, A26, A6, A32, Def1, TARSKI:def_4, WAYBEL_0:28, WAYBEL_0:47;
take F ; ::_thesis: ( y in F & F c= wayabove x )
now__::_thesis:_for_u1_being_set_st_u1_in_F_holds_
u1_in_wayabove_x
let u1 be set ; ::_thesis: ( u1 in F implies u1 in wayabove x )
assume A48: u1 in F ; ::_thesis: u1 in wayabove x
then consider Y being 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 being 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; ::_thesis: verum
end;
hence ( y in F & F c= wayabove x ) by A27, A47, TARSKI:def_3, TARSKI:def_4; ::_thesis: verum
end;
theorem Th9: :: WAYBEL_6:9
for L being complete LATTICE
for X being upper Open Subset of L
for x being Element of L st x in X ` holds
ex m being Element of L st
( x <= m & m is_maximal_in X ` )
proof
let L be complete LATTICE; ::_thesis: for X being upper Open Subset of L
for x being Element of L st x in X ` holds
ex m being Element of L st
( x <= m & m is_maximal_in X ` )
let X be upper Open Subset of L; ::_thesis: for x being Element of L st x in X ` holds
ex m being Element of L st
( x <= m & m is_maximal_in X ` )
let x be Element of L; ::_thesis: ( x in X ` implies ex m being Element of L st
( x <= m & m is_maximal_in X ` ) )
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 being set st Z <> {} & Z c= { C where C is Chain of L : ( C c= X ` & x in C ) } & Z is c=-linear holds
union Z in { C where C is Chain of L : ( C c= X ` & x in C ) }
proof
let Z be set ; ::_thesis: ( Z <> {} & Z c= { C where C is Chain of L : ( C c= X ` & x in C ) } & Z is c=-linear implies union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } )
assume that
A2: Z <> {} and
A3: Z c= { C where C is Chain of L : ( C c= X ` & x in C ) } and
A4: Z is c=-linear ; ::_thesis: union Z in { C where C is Chain of L : ( C c= X ` & x in C ) }
now__::_thesis:_for_Y_being_set_st_Y_in_Z_holds_
Y_c=_the_carrier_of_L
let Y be set ; ::_thesis: ( Y in Z implies Y c= the carrier of L )
assume Y in Z ; ::_thesis: Y c= the carrier of L
then Y in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3;
then ex C being Chain of L st
( Y = C & C c= X ` & x in C ) ;
hence Y c= the carrier of L ; ::_thesis: verum
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 set ; :: according to RELAT_2:def_7 ::_thesis: ( not a in UZ or not b in UZ or [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
assume that
A5: a in UZ and
A6: b in UZ ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
consider az being set such that
A7: a in az and
A8: az in Z by A5, TARSKI:def_4;
consider bz being 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, ORDINAL1:def_8;
then A11: ( az c= bz or bz c= az ) by XBOOLE_0:def_9;
bz in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3, A10;
then A12: ex C being Chain of L st
( bz = C & C c= X ` & x in C ) ;
az in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3, A8;
then A13: ex C being Chain of L st
( az = C & C c= X ` & x in C ) ;
reconsider bz = bz as Chain of L by A12;
reconsider az = 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 ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A7, A9, A11, RELAT_2:def_7; ::_thesis: verum
end;
then reconsider UZ = UZ as Chain of L by ORDERS_2:def_7;
A14: now__::_thesis:_for_Y_being_set_st_Y_in_Z_holds_
Y_c=_X_`
let Y be set ; ::_thesis: ( Y in Z implies Y c= X ` )
assume Y in Z ; ::_thesis: Y c= X `
then Y in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3;
then ex C being Chain of L st
( Y = C & C c= X ` & x in C ) ;
hence Y c= X ` ; ::_thesis: verum
end;
set Y = the Element of Z;
the Element of Z in Z by A2;
then the Element of Z in { C where C is Chain of L : ( C c= X ` & x in C ) } by A3;
then ex C being Chain of L st
( the Element of Z = 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 union Z in { C where C is Chain of L : ( C c= X ` & x in C ) } by A15; ::_thesis: verum
end;
assume x in X ` ; ::_thesis: ex m being Element of L st
( x <= m & m is_maximal_in X ` )
then A16: x1 c= X ` by ZFMISC_1:31;
x in x1 by ZFMISC_1:31;
then x1 in { C where C is Chain of L : ( C c= X ` & x in C ) } by A16;
then consider Y1 being set such that
A17: Y1 in { C where C is Chain of L : ( C c= X ` & x in C ) } and
A18: for Z being set st Z in { C where C is Chain of L : ( C c= X ` & x in C ) } & Z <> Y1 holds
not Y1 c= Z by A1, ORDERS_1:67;
consider Y being Chain of L such that
A19: Y = Y1 and
A20: Y c= X ` and
A21: x in Y by A17;
set m = sup Y;
sup Y is_>=_than Y by YELLOW_0:32;
then A22: x <= sup Y by A21, LATTICE3:def_9;
A23: sup Y is_>=_than Y by YELLOW_0:32;
A24: now__::_thesis:_for_y_being_Element_of_L_holds_
(_not_y_in_X_`_or_not_y_>_sup_Y_)
given y being Element of L such that A25: y in X ` and
A26: y > sup Y ; ::_thesis: contradiction
A27: now__::_thesis:_not_y_in_Y
assume y in Y ; ::_thesis: contradiction
then y <= sup Y by A23, LATTICE3:def_9;
hence contradiction by A26, ORDERS_2:6; ::_thesis: verum
end;
set Y2 = Y \/ {y};
A28: sup Y <= y by A26, ORDERS_2:def_6;
the InternalRel of L is_strongly_connected_in Y \/ {y}
proof
let a, b be set ; :: according to RELAT_2:def_7 ::_thesis: ( not a in Y \/ {y} or not b in Y \/ {y} or [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
assume A29: ( a in Y \/ {y} & b in Y \/ {y} ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
percases ( ( a in Y & b in Y ) or ( a in Y & b in {y} ) or ( a in {y} & b in Y ) or ( a in {y} & b in {y} ) ) by A29, XBOOLE_0:def_3;
supposeA30: ( a in Y & b in Y ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
the InternalRel of L is_strongly_connected_in Y by ORDERS_2:def_7;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A30, RELAT_2:def_7; ::_thesis: verum
end;
supposeA31: ( a in Y & b in {y} ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
then reconsider a1 = a as Element of L ;
reconsider b1 = b as Element of L by A31;
( b1 = y & a1 <= sup Y ) by A23, A31, LATTICE3:def_9, TARSKI:def_1;
then a1 <= b1 by A28, ORDERS_2:3;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
supposeA32: ( a in {y} & b in Y ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
then reconsider a1 = b as Element of L ;
reconsider b1 = a as Element of L by A32;
( b1 = y & a1 <= sup Y ) by A23, A32, LATTICE3:def_9, TARSKI:def_1;
then a1 <= b1 by A28, ORDERS_2:3;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by ORDERS_2:def_5; ::_thesis: verum
end;
supposeA33: ( a in {y} & b in {y} ) ; ::_thesis: ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L )
then reconsider a1 = a as Element of L ;
A34: a1 <= a1 ;
( a = y & b = y ) by A33, TARSKI:def_1;
hence ( [a,b] in the InternalRel of L or [b,a] in the InternalRel of L ) by A34, ORDERS_2:def_5; ::_thesis: verum
end;
end;
end;
then reconsider Y2 = Y \/ {y} 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 { C where C is Chain of L : ( C c= X ` & x in C ) } by A35;
hence contradiction by A18, A19, A27, A36, XBOOLE_1:7; ::_thesis: verum
end;
now__::_thesis:_not_sup_Y_in_X
assume sup Y in X ; ::_thesis: contradiction
then consider y being Element of L such that
A37: y in X and
A38: y << sup Y 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; ::_thesis: verum
end;
then sup Y in X ` by XBOOLE_0:def_5;
then sup Y is_maximal_in X ` by A24, WAYBEL_4:55;
hence ex m being Element of L st
( x <= m & m is_maximal_in X ` ) by A22; ::_thesis: verum
end;
begin
definition
let G be non empty RelStr ;
let g be Element of G;
attrg is meet-irreducible means :Def2: :: WAYBEL_6:def 2
for x, y being Element of G holds
( not g = x "/\" y or x = g or y = g );
end;
:: deftheorem Def2 defines meet-irreducible WAYBEL_6:def_2_:_
for G being non empty RelStr
for g being Element of G holds
( g is meet-irreducible iff for x, y being Element of G holds
( not g = x "/\" y or x = g or y = g ) );
notation
let G be non empty RelStr ;
let g be Element of G;
synonym irreducible g for meet-irreducible ;
end;
definition
let G be non empty RelStr ;
let g be Element of G;
attrg is join-irreducible means :: WAYBEL_6:def 3
for x, y being Element of G holds
( not g = x "\/" y or x = g or y = g );
end;
:: deftheorem defines join-irreducible WAYBEL_6:def_3_:_
for G being non empty RelStr
for g being Element of G holds
( g is join-irreducible iff for x, y being Element of G holds
( not g = x "\/" y or x = g or y = g ) );
definition
let L be non empty RelStr ;
func IRR L -> Subset of L means :Def4: :: WAYBEL_6:def 4
for x being Element of L holds
( x in it iff x is irreducible );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is irreducible )
proof
defpred S1[ 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 S1[x] ) from SUBSET_1:sch_3();
take X ; ::_thesis: for x being Element of L holds
( x in X iff x is irreducible )
thus for x being Element of L holds
( x in X iff x is irreducible ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is irreducible ) ) & ( for x being Element of L holds
( x in b2 iff x is irreducible ) ) holds
b1 = b2
proof
let X, Y be Subset of L; ::_thesis: ( ( for x being Element of L holds
( x in X iff x is irreducible ) ) & ( for x being Element of L holds
( x in Y iff x is irreducible ) ) implies X = Y )
assume that
A2: for x being Element of L holds
( x in X iff x is irreducible ) and
A3: for x being Element of L holds
( x in Y iff x is irreducible ) ; ::_thesis: X = Y
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
x_in_X
let x be set ; ::_thesis: ( x in Y implies x in X )
assume A4: x in Y ; ::_thesis: x in X
then reconsider x1 = x as Element of L ;
x1 is irreducible by A3, A4;
hence x in X by A2; ::_thesis: verum
end;
then A5: Y c= X by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_in_Y
let x be set ; ::_thesis: ( x in X implies x in Y )
assume A6: x in X ; ::_thesis: x in Y
then reconsider x1 = x as Element of L ;
x1 is irreducible by A2, A6;
hence x in Y by A3; ::_thesis: verum
end;
then X c= Y by TARSKI:def_3;
hence X = Y by A5, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines IRR WAYBEL_6:def_4_:_
for L being non empty RelStr
for b2 being Subset of L holds
( b2 = IRR L iff for x being Element of L holds
( x in b2 iff x is irreducible ) );
theorem Th10: :: WAYBEL_6:10
for L being non empty antisymmetric upper-bounded with_infima RelStr holds Top L is irreducible
proof
let L be non empty antisymmetric upper-bounded with_infima RelStr ; ::_thesis: Top L is irreducible
let x, y be Element of L; :: according to WAYBEL_6:def_2 ::_thesis: ( not Top L = x "/\" y or x = Top L or y = Top L )
assume x "/\" y = Top L ; ::_thesis: ( x = Top L or 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 ( x = Top L or y = Top L ) by A1, ORDERS_2:2; ::_thesis: verum
end;
registration
let L be non empty antisymmetric upper-bounded with_infima RelStr ;
cluster irreducible for Element of the carrier of L;
existence
ex b1 being Element of L st b1 is irreducible
proof
take Top L ; ::_thesis: Top L is irreducible
thus Top L is irreducible by Th10; ::_thesis: verum
end;
end;
theorem :: WAYBEL_6:11
for L being Semilattice
for x being Element of L holds
( x is irreducible iff for A being non empty finite Subset of L st x = inf A holds
x in A )
proof
let L be Semilattice; ::_thesis: for x being Element of L holds
( x is irreducible iff for A being non empty finite Subset of L st x = inf A holds
x in A )
let I be Element of L; ::_thesis: ( I is irreducible iff for A being non empty finite Subset of L st I = inf A holds
I in A )
thus ( I is irreducible implies for A being non empty finite Subset of L st I = inf A holds
I in A ) ::_thesis: ( ( for A being non empty finite Subset of L st I = inf A holds
I in A ) implies I is irreducible )
proof
defpred S1[ set ] means ( not $1 is empty & I = "/\" ($1,L) implies I in $1 );
assume A1: for x, y being Element of L holds
( not I = x "/\" y or I = x or I = y ) ; :: according to WAYBEL_6:def_2 ::_thesis: for A being non empty finite Subset of L st I = inf A holds
I in A
let A be non empty finite Subset of L; ::_thesis: ( I = inf A implies I in A )
A2: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in A and
A4: B c= A and
A5: S1[B] ; ::_thesis: S1[B \/ {x}]
thus S1[B \/ {x}] ::_thesis: verum
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
not B \/ {x} is empty and
A6: I = "/\" ((B \/ {x}),L) ; ::_thesis: I in B \/ {x}
percases ( B = {} or B <> {} ) ;
supposeA7: B = {} ; ::_thesis: I in B \/ {x}
then "/\" ((B \/ {a}),L) = a by YELLOW_0:39;
hence I in B \/ {x} by A6, A7, TARSKI:def_1; ::_thesis: verum
end;
supposeA8: B <> {} ; ::_thesis: I in B \/ {x}
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 ::_thesis: verum
percases ( inf C = I or a = I ) by A1, A6, A11, A9;
suppose inf C = I ; ::_thesis: I in B \/ {x}
hence I in B \/ {x} by A5, A8, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA12: a = I ; ::_thesis: I in B \/ {x}
a in {a} by TARSKI:def_1;
hence I in B \/ {x} by A12, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
A13: S1[ {} ] ;
A14: A is finite ;
S1[A] from FINSET_1:sch_2(A14, A13, A2);
hence ( I = inf A implies I in A ) ; ::_thesis: verum
end;
assume A15: for A being non empty finite Subset of L st I = inf A holds
I in A ; ::_thesis: I is irreducible
let a, b be Element of L; :: according to WAYBEL_6:def_2 ::_thesis: ( not I = a "/\" b or a = I or b = I )
assume I = a "/\" b ; ::_thesis: ( a = I or b = I )
then I = inf {a,b} by YELLOW_0:40;
then I in {a,b} by A15;
hence ( a = I or b = I ) by TARSKI:def_2; ::_thesis: verum
end;
theorem :: WAYBEL_6:12
for L being LATTICE
for l being Element of L st (uparrow l) \ {l} is Filter of L holds
l is irreducible
proof
let L be LATTICE; ::_thesis: for l being Element of L st (uparrow l) \ {l} is Filter of L holds
l is irreducible
let l be Element of L; ::_thesis: ( (uparrow l) \ {l} is Filter of L implies l is irreducible )
set F = (uparrow l) \ {l};
assume A1: (uparrow l) \ {l} is Filter of L ; ::_thesis: l is irreducible
now__::_thesis:_for_x,_y_being_Element_of_L_st_l_=_x_"/\"_y_&_x_<>_l_holds_
not_y_<>_l
let x, y be Element of L; ::_thesis: ( l = x "/\" y & x <> l implies not y <> l )
assume that
A2: l = x "/\" y and
A3: x <> l and
A4: y <> l ; ::_thesis: contradiction
l <= y by A2, YELLOW_0:23;
then y in uparrow l by WAYBEL_0:18;
then A5: y in (uparrow l) \ {l} by A4, ZFMISC_1:56;
l <= x by A2, YELLOW_0:23;
then x in uparrow l by WAYBEL_0:18;
then x in (uparrow l) \ {l} by A3, ZFMISC_1:56;
then consider z being Element of L such that
A6: z in (uparrow l) \ {l} and
A7: ( z <= x & z <= y ) by A1, A5, WAYBEL_0:def_2;
l >= z by A2, A7, YELLOW_0:23;
then l in (uparrow l) \ {l} by A1, A6, WAYBEL_0:def_20;
hence contradiction by ZFMISC_1:56; ::_thesis: verum
end;
hence l is irreducible by Def2; ::_thesis: verum
end;
theorem Th13: :: WAYBEL_6:13
for L being LATTICE
for p being Element of L
for F being Filter of L st p is_maximal_in F ` holds
p is irreducible
proof
let L be LATTICE; ::_thesis: for p being Element of L
for F being Filter of L st p is_maximal_in F ` holds
p is irreducible
let p be Element of L; ::_thesis: for F being Filter of L st p is_maximal_in F ` holds
p is irreducible
let F be Filter of L; ::_thesis: ( p is_maximal_in F ` implies p is irreducible )
assume A1: p is_maximal_in F ` ; ::_thesis: p is irreducible
set X = the carrier of L \ F;
A2: p in the carrier of L \ F by A1, WAYBEL_4:55;
now__::_thesis:_for_x,_y_being_Element_of_L_st_p_=_x_"/\"_y_&_x_<>_p_holds_
not_y_<>_p
let x, y be Element of L; ::_thesis: ( p = x "/\" y & x <> p implies not y <> p )
assume that
A3: p = x "/\" y and
A4: x <> p and
A5: y <> p ; ::_thesis: contradiction
p <= y by A3, YELLOW_0:23;
then A6: p < y by A5, ORDERS_2:def_6;
now__::_thesis:_(_x_in_F_implies_not_y_in_F_)
assume ( x in F & y in F ) ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then A9: ( x in the carrier of L \ F or y in the carrier of L \ F ) 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; ::_thesis: verum
end;
hence p is irreducible by Def2; ::_thesis: verum
end;
theorem Th14: :: WAYBEL_6:14
for L being lower-bounded continuous LATTICE
for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is irreducible & x <= p & not y <= p )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for x, y being Element of L st not y <= x holds
ex p being Element of L st
( p is irreducible & x <= p & not y <= p )
let x, y be Element of L; ::_thesis: ( not y <= x implies ex p being Element of L st
( p is irreducible & x <= p & not y <= p ) )
assume A1: not y <= x ; ::_thesis: ex p being Element of L st
( p is irreducible & x <= p & not y <= p )
for x being Element of L holds
( not waybelow x is empty & waybelow x is 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 being 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;
now__::_thesis:_not_x_in_F
assume x in F ; ::_thesis: contradiction
then x in uparrow u by A5, A6, TARSKI:def_3;
hence contradiction by A3, WAYBEL_0:18; ::_thesis: verum
end;
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 ; ::_thesis: ( m is irreducible & x <= m & not y <= m )
A9: m in F ` by A8, WAYBEL_4:55;
now__::_thesis:_not_y_<=_m
assume y <= m ; ::_thesis: contradiction
then m in F by A4, WAYBEL_0:def_20;
hence contradiction by A9, XBOOLE_0:def_5; ::_thesis: verum
end;
hence ( m is irreducible & x <= m & not y <= m ) by A7, A8, Th13; ::_thesis: verum
end;
begin
definition
let L be non empty RelStr ;
let X be Subset of L;
attrX is order-generating means :Def5: :: WAYBEL_6:def 5
for x being Element of L holds
( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) );
end;
:: deftheorem Def5 defines order-generating WAYBEL_6:def_5_:_
for L being non empty RelStr
for X being Subset of L holds
( X is order-generating iff for x being Element of L holds
( ex_inf_of (uparrow x) /\ X,L & x = inf ((uparrow x) /\ X) ) );
theorem Th15: :: WAYBEL_6:15
for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) )
proof
let L be lower-bounded up-complete LATTICE; ::_thesis: for X being Subset of L holds
( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) )
let X be Subset of L; ::_thesis: ( X is order-generating iff for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) )
thus ( X is order-generating implies for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) ::_thesis: ( ( for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) implies X is order-generating )
proof
assume A1: X is order-generating ; ::_thesis: for l being Element of L ex Y being Subset of X st l = "/\" (Y,L)
let l be Element of L; ::_thesis: ex Y being Subset of X st l = "/\" (Y,L)
for x being set 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, Def5;
hence ex Y being Subset of X st l = "/\" (Y,L) ; ::_thesis: verum
end;
thus ( ( for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ) implies X is order-generating ) ::_thesis: verum
proof
assume A2: for l being Element of L ex Y being Subset of X st l = "/\" (Y,L) ; ::_thesis: X is order-generating
let l be Element of L; :: according to WAYBEL_6:def_5 ::_thesis: ( ex_inf_of (uparrow l) /\ X,L & l = inf ((uparrow l) /\ X) )
consider Y being Subset of X such that
A3: l = "/\" (Y,L) by A2;
set S = (uparrow l) /\ X;
thus ex_inf_of (uparrow l) /\ X,L by YELLOW_0:17; ::_thesis: l = inf ((uparrow l) /\ X)
A4: for b being Element of L st b is_<=_than (uparrow l) /\ X holds
b <= l
proof
let b be Element of L; ::_thesis: ( b is_<=_than (uparrow l) /\ X implies b <= l )
assume A5: b is_<=_than (uparrow l) /\ X ; ::_thesis: b <= l
now__::_thesis:_for_x_being_Element_of_L_st_x_in_Y_holds_
b_<=_x
let x be Element of L; ::_thesis: ( x in Y implies b <= x )
assume A6: x in Y ; ::_thesis: b <= x
l is_<=_than Y by A3, YELLOW_0:33;
then l <= x by A6, LATTICE3:def_8;
then x in uparrow l by WAYBEL_0:18;
then x in (uparrow l) /\ X by A6, XBOOLE_0:def_4;
hence b <= x by A5, LATTICE3:def_8; ::_thesis: verum
end;
then b is_<=_than Y by LATTICE3:def_8;
hence b <= l by A3, YELLOW_0:33; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Element_of_L_st_x_in_(uparrow_l)_/\_X_holds_
l_<=_x
let x be Element of L; ::_thesis: ( x in (uparrow l) /\ X implies l <= x )
assume x in (uparrow l) /\ X ; ::_thesis: l <= x
then x in uparrow l by XBOOLE_0:def_4;
hence l <= x by WAYBEL_0:18; ::_thesis: verum
end;
then l is_<=_than (uparrow l) /\ X by LATTICE3:def_8;
hence l = inf ((uparrow l) /\ X) by A4, YELLOW_0:33; ::_thesis: verum
end;
end;
theorem :: WAYBEL_6:16
for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y )
proof
let L be lower-bounded up-complete LATTICE; ::_thesis: for X being Subset of L holds
( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y )
let X be Subset of L; ::_thesis: ( X is order-generating iff for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y )
thus ( X is order-generating implies for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y ) ::_thesis: ( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y ) implies X is order-generating )
proof
assume A1: X is order-generating ; ::_thesis: for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y
let Y be Subset of L; ::_thesis: ( X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) implies the carrier of L = Y )
assume that
A2: X c= Y and
A3: for Z being Subset of Y holds "/\" (Z,L) in Y ; ::_thesis: the carrier of L = Y
now__::_thesis:_for_l1_being_set_st_l1_in_the_carrier_of_L_holds_
l1_in_Y
let l1 be set ; ::_thesis: ( l1 in the carrier of L implies l1 in Y )
assume l1 in the carrier of L ; ::_thesis: l1 in Y
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, XBOOLE_1:26;
then A4: (uparrow l) /\ X c= Y by XBOOLE_1:1;
l = inf ((uparrow l) /\ X) by A1, Def5;
hence l1 in Y by A3, A4; ::_thesis: verum
end;
hence the carrier of L c= Y by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: Y c= the carrier of L
thus Y c= the carrier of L ; ::_thesis: verum
end;
thus ( ( for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y ) implies X is order-generating ) ::_thesis: verum
proof
set Y = { ("/\" (Z,L)) where Z is Subset of L : Z c= X } ;
now__::_thesis:_for_x_being_set_st_x_in__{__("/\"_(Z,L))_where_Z_is_Subset_of_L_:_Z_c=_X__}__holds_
x_in_the_carrier_of_L
let x be set ; ::_thesis: ( x in { ("/\" (Z,L)) where Z is Subset of L : Z c= X } implies x in the carrier of L )
assume x in { ("/\" (Z,L)) where Z is Subset of L : Z c= X } ; ::_thesis: x in the carrier of L
then ex Z being Subset of L st
( x = "/\" (Z,L) & Z c= X ) ;
hence x in the carrier of L ; ::_thesis: verum
end;
then reconsider Y = { ("/\" (Z,L)) where Z is Subset of L : Z c= X } as Subset of L by TARSKI:def_3;
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_in_Y
let x be set ; ::_thesis: ( x in X implies x in Y )
assume A5: x in X ; ::_thesis: x in Y
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; ::_thesis: verum
end;
then A7: X c= Y by TARSKI:def_3;
assume A8: for Y being Subset of L st X c= Y & ( for Z being Subset of Y holds "/\" (Z,L) in Y ) holds
the carrier of L = Y ; ::_thesis: X is order-generating
for l being Element of L ex Z being Subset of X st l = "/\" (Z,L)
proof
let l be Element of L; ::_thesis: ex Z being Subset of X st l = "/\" (Z,L)
for Z being Subset of Y holds "/\" (Z,L) in Y
proof
let Z be Subset of Y; ::_thesis: "/\" (Z,L) in Y
set S = union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ;
now__::_thesis:_for_x_being_set_st_x_in_union__{__A_where_A_is_Subset_of_L_:_(_A_c=_X_&_"/\"_(A,L)_in_Z_)__}__holds_
x_in_the_carrier_of_L
let x be set ; ::_thesis: ( x in union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } implies x in the carrier of L )
assume x in union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ; ::_thesis: x in the carrier of L
then consider Y being 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 being Subset of L st
( Y = A & A c= X & "/\" (A,L) in Z ) by A10;
hence x in the carrier of L by A9; ::_thesis: verum
end;
then reconsider S = union { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } as Subset of L by TARSKI:def_3;
defpred S1[ Subset of L] means ( $1 c= X & "/\" ($1,L) in Z );
set N = { ("/\" (A,L)) where A is Subset of L : S1[A] } ;
now__::_thesis:_for_x_being_set_st_x_in_Z_holds_
x_in__{__("/\"_(A,L))_where_A_is_Subset_of_L_:_S1[A]__}_
let x be set ; ::_thesis: ( x in Z implies x in { ("/\" (A,L)) where A is Subset of L : S1[A] } )
assume A11: x in Z ; ::_thesis: x in { ("/\" (A,L)) where A is Subset of L : S1[A] }
then x in Y ;
then ex Z being Subset of L st
( x = "/\" (Z,L) & Z c= X ) ;
hence x in { ("/\" (A,L)) where A is Subset of L : S1[A] } by A11; ::_thesis: verum
end;
then A12: Z c= { ("/\" (A,L)) where A is Subset of L : S1[A] } by TARSKI:def_3;
now__::_thesis:_for_B_being_set_st_B_in__{__A_where_A_is_Subset_of_L_:_(_A_c=_X_&_"/\"_(A,L)_in_Z_)__}__holds_
B_c=_X
let B be set ; ::_thesis: ( B in { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } implies B c= X )
assume B in { A where A is Subset of L : ( A c= X & "/\" (A,L) in Z ) } ; ::_thesis: B c= X
then ex A being Subset of L st
( B = A & A c= X & "/\" (A,L) in Z ) ;
hence B c= X ; ::_thesis: verum
end;
then A13: S c= X by ZFMISC_1:76;
now__::_thesis:_for_x_being_set_st_x_in__{__("/\"_(A,L))_where_A_is_Subset_of_L_:_S1[A]__}__holds_
x_in_Z
let x be set ; ::_thesis: ( x in { ("/\" (A,L)) where A is Subset of L : S1[A] } implies x in Z )
assume x in { ("/\" (A,L)) where A is Subset of L : S1[A] } ; ::_thesis: x in Z
then ex S being Subset of L st
( x = "/\" (S,L) & S c= X & "/\" (S,L) in Z ) ;
hence x in Z ; ::_thesis: verum
end;
then { ("/\" (A,L)) where A is Subset of L : S1[A] } c= Z by TARSKI:def_3;
then "/\" (Z,L) = "/\" ( { ("/\" (A,L)) where A is Subset of L : S1[A] } ,L) by A12, XBOOLE_0:def_10
.= "/\" ((union { A where A is Subset of L : S1[A] } ),L) from YELLOW_3:sch_3() ;
hence "/\" (Z,L) in Y by A13; ::_thesis: verum
end;
then the carrier of L = Y by A8, A7;
then l in Y ;
then ex Z being Subset of L st
( l = "/\" (Z,L) & Z c= X ) ;
hence ex Z being Subset of X st l = "/\" (Z,L) ; ::_thesis: verum
end;
hence X is order-generating by Th15; ::_thesis: verum
end;
end;
theorem Th17: :: WAYBEL_6:17
for L being lower-bounded up-complete LATTICE
for X being Subset of L holds
( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )
proof
let L be lower-bounded up-complete LATTICE; ::_thesis: for X being Subset of L holds
( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )
let X be Subset of L; ::_thesis: ( X is order-generating iff for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )
thus ( X is order-generating implies for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) ) ::_thesis: ( ( for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) ) implies X is order-generating )
proof
assume A1: X is order-generating ; ::_thesis: for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p )
let l1, l2 be Element of L; ::_thesis: ( not l2 <= l1 implies ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) )
consider P being Subset of X such that
A2: l1 = "/\" (P,L) by A1, Th15;
assume A3: not l2 <= l1 ; ::_thesis: ex p being Element of L st
( p in X & l1 <= p & not l2 <= p )
now__::_thesis:_ex_p_being_Element_of_L_st_
(_p_in_P_&_not_l2_<=_p_)
assume for p being Element of L st p in P holds
l2 <= p ; ::_thesis: contradiction
then l2 is_<=_than P by LATTICE3:def_8;
hence contradiction by A3, A2, YELLOW_0:33; ::_thesis: verum
end;
then consider p being Element of L such that
A4: ( p in P & not l2 <= p ) ;
take p ; ::_thesis: ( p in X & l1 <= p & not l2 <= p )
l1 is_<=_than P by A2, YELLOW_0:33;
hence ( p in X & l1 <= p & not l2 <= p ) by A4, LATTICE3:def_8; ::_thesis: verum
end;
thus ( ( for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) ) implies X is order-generating ) ::_thesis: verum
proof
assume A5: for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p ) ; ::_thesis: X is order-generating
let l be Element of L; :: according to WAYBEL_6:def_5 ::_thesis: ( ex_inf_of (uparrow l) /\ X,L & l = inf ((uparrow l) /\ X) )
set y = inf ((uparrow l) /\ X);
thus ex_inf_of (uparrow l) /\ X,L by YELLOW_0:17; ::_thesis: l = inf ((uparrow l) /\ X)
A6: inf ((uparrow l) /\ X) is_<=_than (uparrow l) /\ X by YELLOW_0:33;
now__::_thesis:_not_inf_((uparrow_l)_/\_X)_<>_l
l is_<=_than (uparrow l) /\ X
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in (uparrow l) /\ X or l <= b )
assume b in (uparrow l) /\ X ; ::_thesis: l <= b
then b in uparrow l by XBOOLE_0:def_4;
hence l <= b by WAYBEL_0:18; ::_thesis: verum
end;
then l <= inf ((uparrow l) /\ X) by YELLOW_0:33;
then A7: not inf ((uparrow l) /\ X) < l by ORDERS_2:6;
assume A8: inf ((uparrow l) /\ X) <> l ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( not inf ((uparrow l) /\ X) <= l or inf ((uparrow l) /\ X) = l ) by A7, ORDERS_2:def_6;
suppose not inf ((uparrow l) /\ X) <= l ; ::_thesis: contradiction
then consider p being Element of L such that
A9: p in X and
A10: l <= p and
A11: not inf ((uparrow l) /\ X) <= 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, LATTICE3:def_8; ::_thesis: verum
end;
suppose inf ((uparrow l) /\ X) = l ; ::_thesis: contradiction
hence contradiction by A8; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence l = inf ((uparrow l) /\ X) ; ::_thesis: verum
end;
end;
theorem Th18: :: WAYBEL_6:18
for L being lower-bounded continuous LATTICE
for X being Subset of L st X = (IRR L) \ {(Top L)} holds
X is order-generating
proof
let L be lower-bounded continuous LATTICE; ::_thesis: for X being Subset of L st X = (IRR L) \ {(Top L)} holds
X is order-generating
let X be Subset of L; ::_thesis: ( X = (IRR L) \ {(Top L)} implies X is order-generating )
assume A1: X = (IRR L) \ {(Top L)} ; ::_thesis: X is order-generating
for l1, l2 being Element of L st not l2 <= l1 holds
ex p being Element of L st
( p in X & l1 <= p & not l2 <= p )
proof
let x, y be Element of L; ::_thesis: ( not y <= x implies ex p being Element of L st
( p in X & x <= p & not y <= p ) )
assume not y <= x ; ::_thesis: ex p being Element of L st
( p in X & x <= p & not y <= p )
then consider p being 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 ex p being Element of L st
( p in X & x <= p & not y <= p ) by A3, A4; ::_thesis: verum
end;
hence X is order-generating by Th17; ::_thesis: verum
end;
theorem Th19: :: WAYBEL_6:19
for L being lower-bounded continuous LATTICE
for 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; ::_thesis: for X, Y being Subset of L st X is order-generating & X c= Y holds
Y is order-generating
let X, Y be Subset of L; ::_thesis: ( X is order-generating & X c= Y implies Y is order-generating )
assume that
A1: X is order-generating and
A2: X c= Y ; ::_thesis: Y is order-generating
let x be Element of L; :: according to WAYBEL_6:def_5 ::_thesis: ( ex_inf_of (uparrow x) /\ Y,L & x = inf ((uparrow x) /\ Y) )
thus ex_inf_of (uparrow x) /\ Y,L by YELLOW_0:17; ::_thesis: x = inf ((uparrow x) /\ Y)
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, Def5;
hence x = inf ((uparrow x) /\ Y) by A4, ORDERS_2:2; ::_thesis: verum
end;
begin
definition
let L be non empty RelStr ;
let l be Element of L;
attrl is prime means :Def6: :: WAYBEL_6:def 6
for x, y being Element of L holds
( not x "/\" y <= l or x <= l or y <= l );
end;
:: deftheorem Def6 defines prime WAYBEL_6:def_6_:_
for L being non empty RelStr
for l being Element of L holds
( l is prime iff for x, y being Element of L holds
( not x "/\" y <= l or x <= l or y <= l ) );
definition
let L be non empty RelStr ;
func PRIME L -> Subset of L means :Def7: :: WAYBEL_6:def 7
for x being Element of L holds
( x in it iff x is prime );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is prime )
proof
defpred S1[ 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 S1[x] ) from SUBSET_1:sch_3();
take X ; ::_thesis: for x being Element of L holds
( x in X iff x is prime )
thus for x being Element of L holds
( x in X iff x is prime ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is prime ) ) & ( for x being Element of L holds
( x in b2 iff x is prime ) ) holds
b1 = b2
proof
let X, Y be Subset of L; ::_thesis: ( ( for x being Element of L holds
( x in X iff x is prime ) ) & ( for x being Element of L holds
( x in Y iff x is prime ) ) implies X = Y )
assume that
A2: for x being Element of L holds
( x in X iff x is prime ) and
A3: for x being Element of L holds
( x in Y iff x is prime ) ; ::_thesis: X = Y
thus X c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Y )
assume A4: x in X ; ::_thesis: x in Y
then reconsider x1 = x as Element of L ;
x1 is prime by A2, A4;
hence x in Y by A3; ::_thesis: verum
end;
thus Y c= X ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X )
assume A5: x in Y ; ::_thesis: x in X
then reconsider x1 = x as Element of L ;
x1 is prime by A3, A5;
hence x in X by A2; ::_thesis: verum
end;
end;
end;
:: deftheorem Def7 defines PRIME WAYBEL_6:def_7_:_
for L being non empty RelStr
for b2 being Subset of L holds
( b2 = PRIME L iff for x being Element of L holds
( x in b2 iff x is prime ) );
definition
let L be non empty RelStr ;
let l be Element of L;
attrl is co-prime means :Def8: :: WAYBEL_6:def 8
l ~ is prime ;
end;
:: deftheorem Def8 defines co-prime WAYBEL_6:def_8_:_
for L being non empty RelStr
for l being Element of L holds
( l is co-prime iff l ~ is prime );
theorem Th20: :: WAYBEL_6:20
for L being non empty antisymmetric upper-bounded RelStr holds Top L is prime
proof
let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: Top L is prime
let x, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= Top L or x <= Top L or y <= Top L )
assume x "/\" y <= Top L ; ::_thesis: ( x <= Top L or y <= Top L )
thus ( x <= Top L or y <= Top L ) by YELLOW_0:45; ::_thesis: verum
end;
theorem :: WAYBEL_6:21
for L being non empty antisymmetric lower-bounded RelStr holds Bottom L is co-prime
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: Bottom L is co-prime
Top (L ~) is prime by Th20;
hence (Bottom L) ~ is prime by YELLOW_7:33; :: according to WAYBEL_6:def_8 ::_thesis: verum
end;
registration
let L be non empty antisymmetric upper-bounded RelStr ;
cluster prime for Element of the carrier of L;
existence
ex b1 being Element of L st b1 is prime
proof
take Top L ; ::_thesis: Top L is prime
thus Top L is prime by Th20; ::_thesis: verum
end;
end;
theorem Th22: :: WAYBEL_6:22
for L being Semilattice
for l being Element of L holds
( l is prime iff for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a ) )
proof
let L be Semilattice; ::_thesis: for l being Element of L holds
( l is prime iff for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a ) )
let l be Element of L; ::_thesis: ( l is prime iff for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a ) )
thus ( l is prime implies for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a ) ) ::_thesis: ( ( for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a ) ) implies l is prime )
proof
defpred S1[ set ] means ( not $1 is 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 holds
( not l >= x "/\" y or l >= x or l >= y ) ; :: according to WAYBEL_6:def_6 ::_thesis: for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a )
let A be non empty finite Subset of L; ::_thesis: ( l >= inf A implies ex a being Element of L st
( a in A & l >= a ) )
A2: now__::_thesis:_for_x,_B_being_set_st_x_in_A_&_B_c=_A_&_S1[B]_holds_
S1[B_\/_{x}]
let x, B be set ; ::_thesis: ( x in A & B c= A & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in A and
A4: B c= A and
A5: S1[B] ; ::_thesis: S1[B \/ {x}]
thus S1[B \/ {x}] ::_thesis: verum
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
not B \/ {x} is empty and
A6: l >= "/\" ((B \/ {x}),L) ; ::_thesis: ex k being Element of L st
( k in B \/ {x} & l >= k )
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: ex k being Element of L st
( k in B \/ {x} & l >= k )
then ( "/\" ((B \/ {a}),L) = a & a in B \/ {a} ) by TARSKI:def_1, YELLOW_0:39;
hence ex k being Element of L st
( k in B \/ {x} & l >= k ) by A6; ::_thesis: verum
end;
supposeA7: B <> {} ; ::_thesis: ex k being Element of L st
( k in B \/ {x} & l >= k )
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 ::_thesis: verum
percases ( inf C <= l or a <= l ) by A1, A6, A10, A8;
suppose inf C <= l ; ::_thesis: ex k being Element of L st
( k in B \/ {x} & l >= k )
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 ex k being Element of L st
( k in B \/ {x} & l >= k ) by A12; ::_thesis: verum
end;
supposeA13: a <= l ; ::_thesis: ex k being Element of L st
( k in B \/ {x} & l >= k )
a in {a} by TARSKI:def_1;
then a in B \/ {x} by XBOOLE_0:def_3;
hence ex k being Element of L st
( k in B \/ {x} & l >= k ) by A13; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
A14: S1[ {} ] ;
A15: A is finite ;
S1[A] from FINSET_1:sch_2(A15, A14, A2);
hence ( l >= inf A implies ex a being Element of L st
( a in A & l >= a ) ) ; ::_thesis: verum
end;
assume A16: for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a ) ; ::_thesis: l is prime
let a, b be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not a "/\" b <= l or a <= l or b <= l )
set A = {a,b};
A17: inf {a,b} = a "/\" b by YELLOW_0:40;
assume a "/\" b <= l ; ::_thesis: ( a <= l or b <= l )
then ex k being Element of L st
( k in {a,b} & l >= k ) by A16, A17;
hence ( a <= l or b <= l ) by TARSKI:def_2; ::_thesis: verum
end;
theorem Th23: :: WAYBEL_6:23
for L being sup-Semilattice
for x being Element of L holds
( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) )
proof
let L be sup-Semilattice; ::_thesis: for x being Element of L holds
( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) )
let x be Element of L; ::_thesis: ( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) )
thus ( x is co-prime implies for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) ) ::_thesis: ( ( for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) ) implies x is co-prime )
proof
assume x is co-prime ; ::_thesis: for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a )
then A1: x ~ is prime by Def8;
let A be non empty finite Subset of L; ::_thesis: ( x <= sup A implies ex a being Element of L st
( a in A & x <= a ) )
reconsider A1 = A as non empty finite Subset of (L ~) ;
assume x <= sup A ; ::_thesis: ex a being Element of L st
( a in A & x <= 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__::_thesis:_for_y_being_Element_of_(L_~)_st_y_is_<=_than_A_holds_
y_<=_("\/"_(A,L))_~
let y be Element of (L ~); ::_thesis: ( y is_<=_than A implies y <= ("\/" (A,L)) ~ )
assume y is_<=_than A ; ::_thesis: y <= ("\/" (A,L)) ~
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; ::_thesis: verum
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 ; ::_thesis: ( ~ a in A & x <= ~ a )
thus ( ~ a in A & x <= ~ a ) by A6, YELLOW_7:2; ::_thesis: verum
end;
thus ( ( for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) ) implies x is co-prime ) ::_thesis: verum
proof
assume A7: for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) ; ::_thesis: x is co-prime
now__::_thesis:_for_a,_b_being_Element_of_(L_~)_holds_
(_not_a_"/\"_b_<=_x_~_or_a_<=_x_~_or_b_<=_x_~_)
let a, b be Element of (L ~); ::_thesis: ( not a "/\" b <= x ~ or a <= x ~ or b <= x ~ )
set A = {(~ a),(~ b)};
assume a "/\" b <= x ~ ; ::_thesis: ( a <= x ~ or b <= x ~ )
then x <= ~ (a "/\" b) by YELLOW_7:2;
then ( sup {(~ a),(~ b)} = (~ 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),(~ b)} 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; ::_thesis: verum
end;
then x ~ is prime by Def6;
hence x is co-prime by Def8; ::_thesis: verum
end;
end;
theorem Th24: :: WAYBEL_6:24
for L being LATTICE
for l being Element of L st l is prime holds
l is irreducible
proof
let L be LATTICE; ::_thesis: for l being Element of L st l is prime holds
l is irreducible
let l be Element of L; ::_thesis: ( l is prime implies l is irreducible )
assume A1: l is prime ; ::_thesis: l is irreducible
let x, y be Element of L; :: according to WAYBEL_6:def_2 ::_thesis: ( not l = x "/\" y or x = l or y = l )
assume A2: l = x "/\" y ; ::_thesis: ( x = l or y = l )
then x "/\" y <= l ;
then A3: ( x <= l or y <= l ) by A1, Def6;
( l <= x & l <= y ) by A2, YELLOW_0:23;
hence ( x = l or y = l ) by A3, ORDERS_2:2; ::_thesis: verum
end;
theorem Th25: :: WAYBEL_6:25
for L being LATTICE
for l being Element of L holds
( l is prime iff for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
proof
let L be LATTICE; ::_thesis: for l being Element of L holds
( l is prime iff for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
let l be Element of L; ::_thesis: ( l is prime iff for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) )
thus ( l is prime implies for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) ) ::_thesis: ( ( for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) ) implies l is prime )
proof
assume A1: l is prime ; ::_thesis: for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving )
let x be set ; ::_thesis: for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving )
let f be Function of L,(BoolePoset {x}); ::_thesis: ( ( for p being Element of L holds
( f . p = {} iff p <= l ) ) implies ( f is meet-preserving & f is join-preserving ) )
assume A2: for p being Element of L holds
( f . p = {} iff p <= l ) ; ::_thesis: ( f is meet-preserving & f is join-preserving )
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; ::_thesis: f preserves_inf_of {z,y}
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__::_thesis:_(f_._z)_"/\"_(f_._y)_=_f_._(z_"/\"_y)
percases ( ( f . z = {} & f . y = {} ) or ( f . z = {x} & f . y = {x} ) or ( f . z = {} & f . y = {x} ) or ( f . z = {x} & f . y = {} ) ) by A3, TARSKI:def_2;
supposeA8: ( f . z = {} & f . y = {} ) ; ::_thesis: (f . z) "/\" (f . y) = f . (z "/\" 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 ; ::_thesis: verum
end;
supposeA10: ( f . z = {x} & f . y = {x} ) ; ::_thesis: (f . z) "/\" (f . y) = f . (z "/\" y)
then ( not y <= l & not z <= l ) by A2;
then not z "/\" y <= l by A1, Def6;
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 ; ::_thesis: verum
end;
supposeA12: ( f . z = {} & f . y = {x} ) ; ::_thesis: (f . z) "/\" (f . y) = f . (z "/\" y)
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 ; ::_thesis: verum
end;
supposeA14: ( f . z = {x} & f . y = {} ) ; ::_thesis: (f . z) "/\" (f . y) = f . (z "/\" 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 ; ::_thesis: verum
end;
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 f preserves_inf_of {z,y} by A6, WAYBEL_0:def_30; ::_thesis: verum
end;
hence f is meet-preserving by WAYBEL_0:def_34; ::_thesis: f is join-preserving
for z, y being Element of L holds f preserves_sup_of {z,y}
proof
let z, y be Element of L; ::_thesis: f preserves_sup_of {z,y}
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__::_thesis:_(f_._z)_"\/"_(f_._y)_=_f_._(z_"\/"_y)
percases ( ( f . z = {} & f . y = {} ) or ( f . z = {x} & f . y = {x} ) or ( f . z = {} & f . y = {x} ) or ( f . z = {x} & f . y = {} ) ) by A3, TARSKI:def_2;
supposeA19: ( f . z = {} & f . y = {} ) ; ::_thesis: (f . z) "\/" (f . y) = f . (z "\/" 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 ; ::_thesis: verum
end;
supposeA21: ( f . z = {x} & f . y = {x} ) ; ::_thesis: (f . z) "\/" (f . y) = f . (z "\/" y)
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 ; ::_thesis: verum
end;
supposeA23: ( f . z = {} & f . y = {x} ) ; ::_thesis: (f . z) "\/" (f . y) = f . (z "\/" y)
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 ; ::_thesis: verum
end;
supposeA25: ( f . z = {x} & f . y = {} ) ; ::_thesis: (f . z) "\/" (f . y) = f . (z "\/" 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 ; ::_thesis: verum
end;
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 f preserves_sup_of {z,y} by A17, WAYBEL_0:def_31; ::_thesis: verum
end;
hence f is join-preserving by WAYBEL_0:def_35; ::_thesis: verum
end;
thus ( ( for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) ) implies l is prime ) ::_thesis: verum
proof
defpred S1[ Element of L, set ] means ( $1 <= l iff $2 = {} );
assume A27: for x being set
for f being Function of L,(BoolePoset {x}) st ( for p being Element of L holds
( f . p = {} iff p <= l ) ) holds
( f is meet-preserving & f is join-preserving ) ; ::_thesis: l is prime
let z, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not z "/\" y <= l or z <= l or y <= 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 S1[a,b]
proof
let a be Element of L; ::_thesis: ex b being Element of (BoolePoset {{}}) st S1[a,b]
now__::_thesis:_ex_b_being_Element_of_(BoolePoset_{{}})_st_S1[a,b]
percases ( a <= l or not a <= l ) ;
supposeA30: a <= l ; ::_thesis: ex b being Element of (BoolePoset {{}}) st S1[a,b]
set b = {} ;
reconsider b = {} as Element of (BoolePoset {{}}) by A28, TARSKI:def_2;
( a <= l iff b = {} ) by A30;
hence ex b being Element of (BoolePoset {{}}) st S1[a,b] ; ::_thesis: verum
end;
supposeA31: not a <= l ; ::_thesis: ex b being Element of (BoolePoset {{}}) st S1[a,b]
set b = {{}};
reconsider b = {{}} as Element of (BoolePoset {{}}) by A28, TARSKI:def_2;
( a <= l iff b = {} ) by A31;
hence ex b being Element of (BoolePoset {{}}) st S1[a,b] ; ::_thesis: verum
end;
end;
end;
hence ex b being Element of (BoolePoset {{}}) st S1[a,b] ; ::_thesis: verum
end;
consider f being Function of L,(BoolePoset {{}}) such that
A32: for p being Element of L holds S1[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 WAYBEL_0:def_34, 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 ; ::_thesis: ( z <= l or 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, WAYBEL_0:def_30
.= (f . z) "/\" (f . y) by YELLOW_0:40
.= (f . z) /\ (f . y) by YELLOW_1:17 ;
now__::_thesis:_(_not_f_._z_=_{}_implies_f_._y_=_{}_)
assume ( not f . z = {} & not f . y = {} ) ; ::_thesis: contradiction
then ( f . z = {{}} & f . y = {{}} ) by A28, TARSKI:def_2;
hence contradiction by A35; ::_thesis: verum
end;
hence ( z <= l or y <= l ) by A32; ::_thesis: verum
end;
end;
theorem Th26: :: WAYBEL_6:26
for L being upper-bounded LATTICE
for 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; ::_thesis: for l being Element of L st l <> Top L holds
( l is prime iff (downarrow l) ` is Filter of L )
let l be Element of L; ::_thesis: ( l <> Top L implies ( l is prime iff (downarrow l) ` is Filter of L ) )
set X1 = the carrier of L \ (downarrow l);
reconsider X = the carrier of L \ (downarrow l) as Subset of L ;
assume A1: l <> Top L ; ::_thesis: ( l is prime iff (downarrow l) ` is Filter of L )
thus ( l is prime implies (downarrow l) ` is Filter of L ) ::_thesis: ( (downarrow l) ` is Filter of L implies l is prime )
proof
assume A2: l is prime ; ::_thesis: (downarrow l) ` is Filter of L
A3: now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_X_&_y_in_X_holds_
ex_z_being_Element_of_L_st_
(_z_in_X_&_z_<=_x_&_z_<=_y_)
let x, y be Element of L; ::_thesis: ( x in X & y in X implies ex z being Element of L st
( z in X & z <= x & z <= y ) )
assume that
A4: x in X and
A5: y in X ; ::_thesis: ex z being Element of L st
( z in X & z <= x & z <= y )
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;
now__::_thesis:_not_x_"/\"_y_in_downarrow_l
assume x "/\" y in downarrow l ; ::_thesis: contradiction
then x "/\" y <= l by WAYBEL_0:17;
hence contradiction by A2, A7, A6, Def6; ::_thesis: verum
end;
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; ::_thesis: verum
end;
A9: now__::_thesis:_for_x,_y_being_Element_of_L_st_x_in_X_&_x_<=_y_holds_
y_in_X
let x, y be Element of L; ::_thesis: ( x in X & x <= y implies y in X )
assume that
A10: x in X and
A11: x <= y ; ::_thesis: y in X
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; ::_thesis: verum
end;
now__::_thesis:_not_Top_L_in_downarrow_l
assume Top L in downarrow l ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence (downarrow l) ` is Filter of L by A3, A9, WAYBEL_0:def_2, WAYBEL_0:def_20, XBOOLE_0:def_5; ::_thesis: verum
end;
thus ( (downarrow l) ` is Filter of L implies l is prime ) ::_thesis: verum
proof
l <= l ;
then A12: l in downarrow l by WAYBEL_0:17;
assume A13: (downarrow l) ` is Filter of L ; ::_thesis: l is prime
let x, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= l or x <= l or y <= l )
assume A14: x "/\" y <= l ; ::_thesis: ( x <= l or y <= l )
now__::_thesis:_(_not_x_<=_l_implies_y_<=_l_)
assume that
A15: not x <= l and
A16: not y <= l ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence ( x <= l or y <= l ) ; ::_thesis: verum
end;
end;
theorem Th27: :: WAYBEL_6:27
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; ::_thesis: for l being Element of L holds
( l is prime iff l is irreducible )
let l be Element of L; ::_thesis: ( l is prime iff l is irreducible )
thus ( l is prime implies l is irreducible ) by Th24; ::_thesis: ( l is irreducible implies l is prime )
thus ( l is irreducible implies l is prime ) ::_thesis: verum
proof
assume A1: l is irreducible ; ::_thesis: l is prime
let x, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= l or x <= l or y <= l )
assume x "/\" y <= l ; ::_thesis: ( x <= l or 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, Def2;
hence ( x <= l or y <= l ) by YELLOW_0:24; ::_thesis: verum
end;
end;
theorem Th28: :: WAYBEL_6:28
for L being distributive LATTICE holds PRIME L = IRR L
proof
let L be distributive LATTICE; ::_thesis: PRIME L = IRR L
now__::_thesis:_for_l1_being_set_st_l1_in_PRIME_L_holds_
l1_in_IRR_L
let l1 be set ; ::_thesis: ( l1 in PRIME L implies l1 in IRR L )
assume A1: l1 in PRIME L ; ::_thesis: l1 in IRR L
then reconsider l = l1 as Element of PRIME L ;
reconsider l = 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; ::_thesis: verum
end;
hence PRIME L c= IRR L by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: IRR L c= PRIME L
now__::_thesis:_for_l1_being_set_st_l1_in_IRR_L_holds_
l1_in_PRIME_L
let l1 be set ; ::_thesis: ( l1 in IRR L implies l1 in PRIME L )
assume A2: l1 in IRR L ; ::_thesis: l1 in PRIME L
then reconsider l = l1 as Element of IRR L ;
reconsider l = 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; ::_thesis: verum
end;
hence IRR L c= PRIME L by TARSKI:def_3; ::_thesis: verum
end;
theorem :: WAYBEL_6:29
for L being Boolean LATTICE
for l being Element of L st l <> Top L holds
( l is prime iff for x being Element of L st x > l holds
x = Top L )
proof
let L be Boolean LATTICE; ::_thesis: for l being Element of L st l <> Top L holds
( l is prime iff for x being Element of L st x > l holds
x = Top L )
let l be Element of L; ::_thesis: ( l <> Top L implies ( l is prime iff for x being Element of L st x > l holds
x = Top L ) )
assume A1: l <> Top L ; ::_thesis: ( l is prime iff for x being Element of L st x > l holds
x = Top L )
thus ( l is prime implies for x being Element of L st x > l holds
x = Top L ) ::_thesis: ( ( for x being Element of L st x > l holds
x = Top L ) implies l is prime )
proof
assume A2: l is prime ; ::_thesis: for x being Element of L st x > l holds
x = Top L
let x be Element of L; ::_thesis: ( x > l implies x = Top 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, WAYBEL_1:def_23;
then x "/\" y <= l by YELLOW_0:44;
then A4: ( x <= l or y <= l ) by A2, Def6;
assume x > l ; ::_thesis: x = Top L
then y < x by A4, ORDERS_2:7;
then A5: y <= x by ORDERS_2:def_6;
x "\/" y = Top L by A3, WAYBEL_1:def_23;
hence x = Top L by A5, YELLOW_0:24; ::_thesis: verum
end;
thus ( ( for x being Element of L st x > l holds
x = Top L ) implies l is prime ) ::_thesis: verum
proof
assume A6: for z being Element of L st z > l holds
z = Top L ; ::_thesis: l is prime
let x, y be Element of L; :: according to WAYBEL_6:def_6 ::_thesis: ( not x "/\" y <= l or x <= l or y <= l )
assume x "/\" y <= l ; ::_thesis: ( x <= l or 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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
end;
theorem :: WAYBEL_6:30
for L being lower-bounded distributive continuous 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 lower-bounded distributive continuous LATTICE; ::_thesis: 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 ` )
let l be Element of L; ::_thesis: ( l <> Top L implies ( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` ) )
set F = (downarrow l) ` ;
assume A1: l <> Top L ; ::_thesis: ( l is prime iff ex F being Open Filter of L st l is_maximal_in F ` )
thus ( l is prime implies ex F being Open Filter of L st l is_maximal_in F ` ) ::_thesis: ( ex F being Open Filter of L st l is_maximal_in F ` implies l is prime )
proof
A2: for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ;
A3: now__::_thesis:_for_x_being_Element_of_L_st_x_in_(downarrow_l)_`_holds_
ex_y_being_Element_of_L_st_
(_y_in_(downarrow_l)_`_&_y_<<_x_)
let x be Element of L; ::_thesis: ( x in (downarrow l) ` implies ex y being Element of L st
( y in (downarrow l) ` & y << x ) )
assume x in (downarrow l) ` ; ::_thesis: ex y being Element of L st
( y in (downarrow l) ` & y << x )
then not x in downarrow l by XBOOLE_0:def_5;
then not x <= l by WAYBEL_0:17;
then consider y being 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 (downarrow l) ` by XBOOLE_0:def_5;
hence ex y being Element of L st
( y in (downarrow l) ` & y << x ) by A4; ::_thesis: verum
end;
assume l is prime ; ::_thesis: ex F being Open Filter of L st l is_maximal_in F `
then reconsider F = (downarrow l) ` as Open Filter of L by A1, A3, Def1, Th26;
take F ; ::_thesis: l is_maximal_in F `
A6: now__::_thesis:_for_y_being_Element_of_L_holds_
(_not_y_in_F_`_or_not_y_>_l_)
given y being Element of L such that A7: y in F ` and
A8: y > l ; ::_thesis: contradiction
y <= l by A7, WAYBEL_0:17;
hence contradiction by A8, ORDERS_2:6; ::_thesis: verum
end;
l <= l ;
then l in F ` by WAYBEL_0:17;
hence l is_maximal_in F ` by A6, WAYBEL_4:55; ::_thesis: verum
end;
thus ( ex F being Open Filter of L st l is_maximal_in F ` implies l is prime ) ::_thesis: verum
proof
assume ex O being Open Filter of L st l is_maximal_in O ` ; ::_thesis: l is prime
then A9: l is irreducible by Th13;
now__::_thesis:_for_x,_y_being_Element_of_L_st_x_"/\"_y_<=_l_&_not_x_<=_l_holds_
y_<=_l
let x, y be Element of L; ::_thesis: ( x "/\" y <= l & not x <= l implies y <= l )
assume x "/\" y <= l ; ::_thesis: ( not x <= l implies y <= l )
then l = l "\/" (x "/\" y) by YELLOW_0:24
.= (l "\/" x) "/\" (l "\/" y) by WAYBEL_1:5 ;
then A10: ( l = l "\/" x or l = l "\/" y ) by A9, Def2;
assume ( not x <= l & not y <= l ) ; ::_thesis: contradiction
hence contradiction by A10, YELLOW_0:24; ::_thesis: verum
end;
hence l is prime by Def6; ::_thesis: verum
end;
end;
theorem Th31: :: WAYBEL_6:31
for L being RelStr
for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}})
proof
let L be RelStr ; ::_thesis: for X being Subset of L holds chi (X, the carrier of L) is Function of L,(BoolePoset {{}})
let X be Subset of L; ::_thesis: chi (X, the carrier of L) is Function of L,(BoolePoset {{}})
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 chi (X, the carrier of L) is Function of L,(BoolePoset {{}}) ; ::_thesis: verum
end;
theorem Th32: :: WAYBEL_6:32
for L being non empty RelStr
for 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 ; ::_thesis: for p, x being Element of L holds
( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p )
let p, x be Element of L; ::_thesis: ( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p )
( not x in (downarrow p) ` iff x in downarrow p ) by XBOOLE_0:def_5;
hence ( (chi (((downarrow p) `), the carrier of L)) . x = {} iff x <= p ) by FUNCT_3:def_3, WAYBEL_0:17; ::_thesis: verum
end;
theorem Th33: :: WAYBEL_6:33
for L being upper-bounded LATTICE
for f being Function of L,(BoolePoset {{}})
for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds
( f is meet-preserving & f is join-preserving )
proof
let L be upper-bounded LATTICE; ::_thesis: for f being Function of L,(BoolePoset {{}})
for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds
( f is meet-preserving & f is join-preserving )
let f be Function of L,(BoolePoset {{}}); ::_thesis: for p being prime Element of L st chi (((downarrow p) `), the carrier of L) = f holds
( f is meet-preserving & f is join-preserving )
let p be prime Element of L; ::_thesis: ( chi (((downarrow p) `), the carrier of L) = f implies ( f is meet-preserving & f is join-preserving ) )
assume chi (((downarrow p) `), the carrier of L) = f ; ::_thesis: ( f is meet-preserving & f is join-preserving )
then for x being Element of L holds
( f . x = {} iff x <= p ) by Th32;
hence ( f is meet-preserving & f is join-preserving ) by Th25; ::_thesis: verum
end;
theorem Th34: :: WAYBEL_6:34
for L being complete LATTICE st PRIME L is order-generating holds
( L is distributive & L is meet-continuous )
proof
let L be complete LATTICE; ::_thesis: ( PRIME L is order-generating implies ( L is distributive & L is meet-continuous ) )
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 the prime Element of L) `), the carrier of L) in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ;
now__::_thesis:_for_x_being_set_st_x_in__{__(chi_(((downarrow_p)_`),_the_carrier_of_L))_where_p_is_Element_of_L_:_p_is_prime__}__holds_
x_is_Function
let x be set ; ::_thesis: ( x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } implies x is Function )
assume x in { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } ; ::_thesis: x is Function
then ex p being Element of L st
( x = chi (((downarrow p) `), the carrier of L) & p is prime ) ;
hence x is Function ; ::_thesis: verum
end;
then reconsider H = { (chi (((downarrow p) `), the carrier of L)) where p is Element of L : p is prime } as non empty functional set by A1, FUNCT_1:def_13;
deffunc H1( set ) -> set = { 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 set st x in the carrier of L holds
F . x = H1(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 set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng F or y in the carrier of (BoolePoset H) )
assume y in rng F ; ::_thesis: y in the carrier of (BoolePoset H)
then consider x being set 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;
y c= H
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in y or p in H )
assume p in y ; ::_thesis: p in H
then ex f being Element of H st
( p = f & f . x = 1 ) by A6;
hence p in H ; ::_thesis: verum
end;
hence y in the carrier of (BoolePoset H) by A4; ::_thesis: verum
end;
then reconsider F = 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; :: according to WAYBEL_0:def_34 ::_thesis: F preserves_inf_of {x,y}
assume ex_inf_of {x,y},L ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of F .: {x,y}, BoolePoset H & "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L)) )
thus ex_inf_of F .: {x,y}, BoolePoset H by YELLOW_0:17; ::_thesis: "/\" ((F .: {x,y}),(BoolePoset H)) = F . ("/\" ({x,y},L))
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, YELLOW_0:40;
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { f where f is Element of H : f . (x "/\" y) = 1 } or p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } )
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 } ; ::_thesis: p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 }
then consider g being Element of H such that
A11: g = p and
A12: g . (x "/\" y) = 1 ;
g in H ;
then A13: ex a being Element of L st
( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ;
then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31;
g is meet-preserving by A13, Th33;
then A14: g preserves_inf_of {x,y} by WAYBEL_0:def_34;
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, WAYBEL_0:def_30;
then ( g . y <= Top (BoolePoset {{}}) & g . y >= Top (BoolePoset {{}}) ) by A12, A10, YELLOW_0:23, YELLOW_0: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, YELLOW_0: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 p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } by A17, XBOOLE_0:def_4; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { f where f is Element of H : f . x = 1 } /\ { f where f is Element of H : f . y = 1 } or p in { f where f is Element of H : f . (x "/\" y) = 1 } )
A19: ( ex_inf_of {x,y},L & x "/\" y = inf {x,y} ) by YELLOW_0:17, YELLOW_0: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 } ; ::_thesis: p in { f where f is Element of H : f . (x "/\" y) = 1 }
then p in { f where f is Element of H : f . x = 1 } by XBOOLE_0:def_4;
then consider f1 being 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 being Element of H st
( f2 = p & f2 . y = 1 ) ;
f1 in H ;
then consider a being Element of L such that
A24: chi (((downarrow a) `), the carrier of L) = f1 and
A25: a is prime ;
reconsider f1 = 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} by WAYBEL_0:def_34;
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, WAYBEL_0:def_30
.= 1 by A21, A22, A23, YELLOW_5:2 ;
hence p in { f where f is Element of H : f . (x "/\" y) = 1 } by A21; ::_thesis: verum
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, XBOOLE_0:def_10
.= F . (x "/\" y) by A3
.= F . (inf {x,y}) by YELLOW_0:40 ;
::_thesis: verum
end;
assume A28: PRIME L is order-generating ; ::_thesis: ( L is distributive & L is meet-continuous )
A29: F is V24()
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom F or not x2 in dom F or not F . x1 = F . x2 or x1 = x2 )
assume that
A30: x1 in dom F and
A31: x2 in dom F and
A32: F . x1 = F . x2 ; ::_thesis: x1 = x2
reconsider l2 = x2 as Element of L by A31;
reconsider l1 = x1 as Element of L by A30;
now__::_thesis:_not_l1_<>_l2
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 ; ::_thesis: contradiction
percases ( not l1 <= l2 or not l2 <= l1 ) by A35, ORDERS_2:2;
suppose not l1 <= l2 ; ::_thesis: contradiction
then consider p being 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 chi (((downarrow p) `), the carrier of L) in H ;
then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ;
A39: now__::_thesis:_not_CH_in_F_._l2
assume CH in F . l2 ; ::_thesis: contradiction
then ex f being Element of H st
( f = CH & f . l2 = 1 ) by A33;
hence contradiction by A37, Th32; ::_thesis: verum
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; ::_thesis: verum
end;
suppose not l2 <= l1 ; ::_thesis: contradiction
then consider p being 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 chi (((downarrow p) `), the carrier of L) in H ;
then reconsider CH = chi (((downarrow p) `), the carrier of L) as Element of H ;
A43: now__::_thesis:_not_CH_in_F_._l1
assume CH in F . l1 ; ::_thesis: contradiction
then ex f being Element of H st
( f = CH & f . l1 = 1 ) by A34;
hence contradiction by A41, Th32; ::_thesis: verum
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; ::_thesis: verum
end;
end;
end;
hence x1 = x2 ; ::_thesis: verum
end;
F is join-preserving
proof
let x, y be Element of L; :: according to WAYBEL_0:def_35 ::_thesis: F preserves_sup_of {x,y}
assume ex_sup_of {x,y},L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of F .: {x,y}, BoolePoset H & "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L)) )
thus ex_sup_of F .: {x,y}, BoolePoset H by YELLOW_0:17; ::_thesis: "\/" ((F .: {x,y}),(BoolePoset H)) = F . ("\/" ({x,y},L))
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { f where f is Element of H : f . (x "\/" y) = 1 } or p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } )
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 } ; ::_thesis: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 }
then consider g being Element of H such that
A46: g = p and
A47: g . (x "\/" y) = 1 ;
g in H ;
then A48: ex a being Element of L st
( chi (((downarrow a) `), the carrier of L) = g & a is prime ) ;
then reconsider g = g as Function of L,(BoolePoset {{}}) by Th31;
g is join-preserving by A48, Th33;
then A49: g preserves_sup_of {x,y} by WAYBEL_0:def_35;
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, YELLOW_0:41;
A52: (g . x) "\/" (g . y) = sup {(g . x),(g . y)} by YELLOW_0:41;
A53: now__::_thesis:_(_g_._x_=_{}_implies_not_g_._y_=_{}_)
assume ( g . x = {} & g . y = {} ) ; ::_thesis: contradiction
then (g . x) "\/" (g . y) = {} \/ {} by YELLOW_1:17
.= 0 ;
hence contradiction by A47, A50, A49, A51, A52, WAYBEL_0:def_31; ::_thesis: verum
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 p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } by XBOOLE_0:def_3; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } or p in { f where f is Element of H : f . (x "\/" y) = 1 } )
assume A57: p in { f where f is Element of H : f . x = 1 } \/ { f where f is Element of H : f . y = 1 } ; ::_thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }
percases ( 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 A57, XBOOLE_0:def_3;
suppose p in { f where f is Element of H : f . x = 1 } ; ::_thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }
then consider f1 being Element of H such that
A58: f1 = p and
A59: f1 . x = 1 ;
f1 in H ;
then consider a being Element of L such that
A60: chi (((downarrow a) `), the carrier of L) = f1 and
A61: a is prime ;
reconsider f1 = 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} by WAYBEL_0:def_35;
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, YELLOW_0: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, WAYBEL_0:def_31
.= 1 by A59, A64, YELLOW_0:24 ;
hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A58; ::_thesis: verum
end;
suppose p in { f where f is Element of H : f . y = 1 } ; ::_thesis: p in { f where f is Element of H : f . (x "\/" y) = 1 }
then consider f1 being Element of H such that
A66: f1 = p and
A67: f1 . y = 1 ;
f1 in H ;
then consider b being Element of L such that
A68: chi (((downarrow b) `), the carrier of L) = f1 and
A69: b is prime ;
reconsider f1 = 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} by WAYBEL_0:def_35;
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, YELLOW_0: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, WAYBEL_0:def_31
.= 1 by A67, A72, YELLOW_0:24 ;
hence p in { f where f is Element of H : f . (x "\/" y) = 1 } by A66; ::_thesis: verum
end;
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, XBOOLE_0:def_10
.= F . (x "\/" y) by A3
.= F . (sup {x,y}) by YELLOW_0:41 ;
::_thesis: verum
end;
hence L is distributive by A7, A29, Th3; ::_thesis: L is meet-continuous
F is sups-preserving
proof
let X be Subset of L; :: according to WAYBEL_0:def_33 ::_thesis: F preserves_sup_of X
F preserves_sup_of X
proof
assume ex_sup_of X,L ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of F .: X, BoolePoset H & "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L)) )
thus ex_sup_of F .: X, BoolePoset H by YELLOW_0:17; ::_thesis: "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L))
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not a in sup (F .: X) or a in F . (sup X) )
assume a in sup (F .: X) ; ::_thesis: a in F . (sup X)
then a in union (F .: X) by YELLOW_1:21;
then consider Y being set such that
A76: a in Y and
A77: Y in F .: X by TARSKI:def_4;
consider z being set 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 = z as Element of L by A78;
F . z = { f where f is Element of H : f . z = 1 } by A3;
then consider f being Element of H such that
A81: a = f and
A82: f . z = 1 by A76, A80;
f in H ;
then consider p being Element of L such that
A83: f = chi (((downarrow p) `), the carrier of L) and
p is prime ;
A84: now__::_thesis:_not_f_._(sup_X)_=_0
sup X is_>=_than X by YELLOW_0:32;
then A85: z <= sup X by A79, LATTICE3:def_9;
assume f . (sup X) = 0 ; ::_thesis: contradiction
then sup X <= p by A83, Th32;
then z <= p by A85, ORDERS_2:3;
hence contradiction by A82, A83, Th32; ::_thesis: verum
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 a in F . (sup X) by A74, A81, A84; ::_thesis: verum
end;
F . (sup X) c= sup (F .: X)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in F . (sup X) or a in sup (F .: X) )
assume a in F . (sup X) ; ::_thesis: a in sup (F .: X)
then consider f being Element of H such that
A87: a = f and
A88: f . (sup X) = 1 by A74;
f in H ;
then consider p being 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__::_thesis:_ex_l_being_Element_of_L_st_
(_l_in_X_&_not_l_<=_p_)
assume for l being Element of L st l in X holds
l <= p ; ::_thesis: contradiction
then X is_<=_than p by LATTICE3:def_9;
hence contradiction by A91, YELLOW_0:32; ::_thesis: verum
end;
then consider l being 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 a in sup (F .: X) by YELLOW_1:21; ::_thesis: verum
end;
hence "\/" ((F .: X),(BoolePoset H)) = F . ("\/" (X,L)) by A75, XBOOLE_0:def_10; ::_thesis: verum
end;
hence F preserves_sup_of X ; ::_thesis: verum
end;
hence L is meet-continuous by A7, A29, Th4; ::_thesis: verum
end;
theorem Th35: :: WAYBEL_6:35
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; ::_thesis: ( L is distributive iff PRIME L is order-generating )
thus ( L is distributive implies PRIME L is order-generating ) ::_thesis: ( PRIME L is order-generating implies L is distributive )
proof
assume L is distributive ; ::_thesis: PRIME L is order-generating
then A1: PRIME L = IRR L by Th28;
(IRR L) \ {(Top L)} c= IRR L by XBOOLE_1:36;
hence PRIME L is order-generating by A1, Th18, Th19; ::_thesis: verum
end;
thus ( PRIME L is order-generating implies L is distributive ) by Th34; ::_thesis: verum
end;
theorem :: WAYBEL_6:36
for L being lower-bounded continuous LATTICE holds
( L is distributive iff L is Heyting )
proof
let L be lower-bounded continuous LATTICE; ::_thesis: ( L is distributive iff L is Heyting )
thus ( L is distributive implies L is Heyting ) ::_thesis: ( L is Heyting implies L is distributive )
proof
assume L is distributive ; ::_thesis: L is Heyting
then PRIME L is order-generating by Th35;
then ( L is distributive & L is meet-continuous ) by Th34;
hence L is Heyting ; ::_thesis: verum
end;
thus ( L is Heyting implies L is distributive ) ; ::_thesis: verum
end;
theorem Th37: :: WAYBEL_6:37
for L being complete continuous 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
for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L)
proof
let L be complete continuous LATTICE; ::_thesis: ( ( 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 ) ) ) implies for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) )
defpred S1[ set , set ] means ( $2 c= PRIME (L ~) & $1 = "\/" ($2,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 ) ) ; ::_thesis: for l being Element of L holds l = "\/" (((waybelow l) /\ (PRIME (L opp))),L)
A2: for e being set st e in the carrier of L holds
ex u being set st S1[e,u]
proof
let e be set ; ::_thesis: ( e in the carrier of L implies ex u being set st S1[e,u] )
assume e in the carrier of L ; ::_thesis: ex u being set st S1[e,u]
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__::_thesis:_for_p1_being_set_st_p1_in_X_holds_
p1_in_PRIME_(L_~)
let p1 be set ; ::_thesis: ( p1 in X implies p1 in PRIME (L ~) )
assume A5: p1 in X ; ::_thesis: p1 in PRIME (L ~)
then reconsider p = p1 as Element of L ;
p is co-prime by A4, A5;
then p ~ is prime by Def8;
hence p1 in PRIME (L ~) by Def7; ::_thesis: verum
end;
then X c= PRIME (L ~) by TARSKI:def_3;
hence ex u being set st S1[e,u] by A3; ::_thesis: verum
end;
consider f being Function such that
A6: dom f = the carrier of L and
A7: for e being set st e in the carrier of L holds
S1[e,f . e] from CLASSES1:sch_1(A2);
let l be Element of L; ::_thesis: l = "\/" (((waybelow l) /\ (PRIME (L opp))),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 set ; :: according to TARSKI:def_3 ::_thesis: ( not e in waybelow l or e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } )
assume A10: e in waybelow l ; ::_thesis: e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) }
then f . e c= PRIME (L ~) by A7;
then A11: f . e c= the carrier of (L ~) by XBOOLE_1:1;
( e = "\/" ((f . e),L) & f . e in rng f ) by A6, A7, A10, FUNCT_1:def_3;
hence e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by A10, A11; ::_thesis: verum
end;
defpred S2[ Subset of L] means ( $1 in rng f & sup $1 in waybelow l );
A12: 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 ) } ;
A13: union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } c= (waybelow l) /\ (PRIME (L ~))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } or e in (waybelow l) /\ (PRIME (L ~)) )
assume e in union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ; ::_thesis: e in (waybelow l) /\ (PRIME (L ~))
then consider Y being set such that
A14: e in Y and
A15: Y in { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } by TARSKI:def_4;
consider X being Subset of L such that
A16: Y = X and
A17: X in rng f and
A18: sup X in waybelow l by A15;
reconsider e1 = e as Element of L by A14, A16;
e1 <= sup X by A14, A16, YELLOW_2:22;
then A19: e in waybelow l by A18, WAYBEL_0:def_19;
ex r being set st
( r in dom f & X = f . r ) by A17, FUNCT_1:def_3;
then X c= PRIME (L ~) by A6, A7;
hence e in (waybelow l) /\ (PRIME (L ~)) by A14, A16, A19, XBOOLE_0:def_4; ::_thesis: verum
end;
A20: ex_sup_of union { X where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ,L by YELLOW_0:17;
ex_sup_of waybelow l,L by YELLOW_0:17;
then A21: "\/" (((waybelow l) /\ (PRIME (L ~))),L) <= "\/" ((waybelow l),L) by A8, XBOOLE_1:17, YELLOW_0:34;
{ (sup X) where X is Subset of L : S2[X] } c= waybelow l
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { (sup X) where X is Subset of L : S2[X] } or e in waybelow l )
assume e in { (sup X) where X is Subset of L : ( X in rng f & sup X in waybelow l ) } ; ::_thesis: e in waybelow l
then ex X being Subset of L st
( e = sup X & X in rng f & sup X in waybelow l ) ;
hence e in waybelow l ; ::_thesis: verum
end;
then l = "\/" ( { (sup X) where X is Subset of L : S2[X] } ,L) by A12, A9, XBOOLE_0:def_10
.= "\/" ((union { X where X is Subset of L : S2[X] } ),L) from YELLOW_3:sch_5() ;
then l <= "\/" (((waybelow l) /\ (PRIME (L ~))),L) by A20, A8, A13, YELLOW_0:34;
hence l = "\/" (((waybelow l) /\ (PRIME (L opp))),L) by A12, A21, ORDERS_2:2; ::_thesis: verum
end;
Lm2: for L being complete continuous 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 complete continuous LATTICE; ::_thesis: ( ( 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 ) ) ) implies L is completely-distributive )
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 ) ) ; ::_thesis: L is completely-distributive
thus L is complete ; :: according to WAYBEL_5:def_3 ::_thesis: for b1 being set
for b2 being set
for b3 being ManySortedFunction of b2,b1 --> the carrier of L holds //\ ((\// (b3,L)),L) = \\/ ((/\\ ((Frege b3),L)),L)
let J be non empty set ; ::_thesis: for b1 being set
for b2 being ManySortedFunction of b1,J --> the carrier of L holds //\ ((\// (b2,L)),L) = \\/ ((/\\ ((Frege b2),L)),L)
let K be V19() ManySortedSet of J; ::_thesis: for b1 being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b1,L)),L) = \\/ ((/\\ ((Frege b1),L)),L)
let F be DoubleIndexedSet of K,L; ::_thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L)
set l = Inf ;
set X = (waybelow (Inf )) /\ (PRIME (L ~));
A2: (waybelow (Inf )) /\ (PRIME (L ~)) c= waybelow (Inf ) by XBOOLE_1:17;
reconsider X = (waybelow (Inf )) /\ (PRIME (L ~)) 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; ::_thesis: ( x in X implies x is co-prime )
assume x in X ; ::_thesis: x is co-prime
then x in PRIME (L ~) by XBOOLE_0:def_4;
then x ~ is prime by Def7;
hence x is co-prime by Def8; ::_thesis: verum
end;
A5: inf (rng (Sups )) = Inf by YELLOW_2:def_6;
X is_<=_than Sup
proof
let p be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not p in X or p <= Sup )
defpred S1[ set , set ] means ( $2 in K . $1 & [p,((F . $1) . $2)] in the InternalRel of L );
assume A6: p in X ; ::_thesis: p <= Sup
A7: for j being set st j in J holds
ex k being set st S1[j,k]
proof
let j1 be set ; ::_thesis: ( j1 in J implies ex k being set st S1[j1,k] )
assume j1 in J ; ::_thesis: ex k being set st S1[j1,k]
then reconsider j = j1 as Element of J ;
set k = the Element of K . j;
dom (Sups ) = J by A3, FUNCT_2:def_1;
then A8: (Sups ) . j in rng (Sups ) by FUNCT_1:def_3;
A9: ( p << Inf & Sup = sup (rng (F . j)) ) by A2, A6, WAYBEL_3:7, YELLOW_2:def_5;
Sup = (Sups ) . j by A3, WAYBEL_5:def_1;
then Inf <= Sup 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) . the Element of K . j)},L ) by YELLOW_0:17;
then sup A <= sup (A \/ {((F . j) . the Element of K . j)}) by XBOOLE_1:7, YELLOW_0:34;
then A12: p <= sup (A \/ {((F . j) . the Element of K . j)}) by A11, ORDERS_2:3;
p is co-prime by A4, A6;
then consider a being Element of L such that
A13: a in A \/ {((F . j) . the Element of K . j)} and
A14: p <= a by A12, Th23;
percases ( a in A or a in {((F . j) . the Element of K . j)} ) by A13, XBOOLE_0:def_3;
suppose a in A ; ::_thesis: ex k being set st S1[j1,k]
then consider k1 being set such that
A15: k1 in dom (F . j) and
A16: a = (F . j) . k1 by A10, FUNCT_1:def_3;
reconsider k1 = 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 ex k being set st S1[j1,k] ; ::_thesis: verum
end;
suppose a in {((F . j) . the Element of K . j)} ; ::_thesis: ex k being set st S1[j1,k]
then a = (F . j) . the Element of K . j by TARSKI:def_1;
then [p,((F . j) . the Element of K . j)] in the InternalRel of L by A14, ORDERS_2:def_5;
hence ex k being set st S1[j1,k] ; ::_thesis: verum
end;
end;
end;
consider f1 being Function such that
A17: dom f1 = J and
A18: for j being set st j in J holds
S1[j,f1 . j] from CLASSES1:sch_1(A7);
now__::_thesis:_for_g_being_set_st_g_in_dom_(doms_F)_holds_
g_in_dom_f1
let g be set ; ::_thesis: ( g in dom (doms F) implies g in dom f1 )
assume g in dom (doms F) ; ::_thesis: g in dom f1
then g in F " (SubFuncs (rng F)) by FUNCT_6:def_2;
hence g in dom f1 by A3, A17, FUNCT_6:19; ::_thesis: verum
end;
then A19: dom (doms F) c= dom f1 by TARSKI:def_3;
now__::_thesis:_for_g_being_set_st_g_in_dom_f1_holds_
g_in_dom_(doms_F)
let g be set ; ::_thesis: ( g in dom f1 implies g in dom (doms F) )
A20: F . g is Function ;
assume g in dom f1 ; ::_thesis: g in dom (doms F)
then g in F " (SubFuncs (rng F)) by A3, A17, A20, FUNCT_6:19;
hence g in dom (doms F) by FUNCT_6:def_2; ::_thesis: verum
end;
then dom f1 c= dom (doms F) by TARSKI:def_3;
then A21: dom f1 = dom (doms F) by A19, XBOOLE_0:def_10;
A22: for b being set st b in dom (doms F) holds
f1 . b in (doms F) . b
proof
let b be set ; ::_thesis: ( b in dom (doms F) implies f1 . b in (doms F) . b )
assume A23: b in dom (doms F) ; ::_thesis: f1 . b in (doms F) . b
then A24: 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, A23, FUNCT_6:22
.= K . b by A24, FUNCT_2:def_1 ;
hence f1 . b in (doms F) . b by A17, A18, A19, A23; ::_thesis: verum
end;
then reconsider D = product (doms F) as non empty set by A21, CARD_3:9;
reconsider f = f1 as Element of product (doms F) by A21, A22, CARD_3:9;
A25: f1 in product (doms F) by A21, A22, CARD_3:9;
p is_<=_than rng ((Frege F) . f)
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in rng ((Frege F) . f) or p <= b )
assume b in rng ((Frege F) . f) ; ::_thesis: p <= b
then consider a being set such that
A26: a in dom ((Frege F) . f) and
A27: b = ((Frege F) . f) . a by FUNCT_1:def_3;
reconsider a = a as Element of J by A26;
f in dom (Frege F) by A25, 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 A27, ORDERS_2:def_5; ::_thesis: verum
end;
then p <= inf (rng ((Frege F) . f)) by YELLOW_0:33;
then A28: p <= Inf 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 in rng (Infs ) by WAYBEL_5:14;
then Inf <= sup (rng (Infs )) by YELLOW_2:22;
then Inf <= Sup by YELLOW_2:def_5;
hence p <= Sup by A28, ORDERS_2:3; ::_thesis: verum
end;
then A29: sup X <= Sup by YELLOW_0:32;
( Inf >= Sup & Inf = sup X ) by A1, Th37, WAYBEL_5:16;
hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) by A29, ORDERS_2:2; ::_thesis: verum
end;
Lm3: for L being complete completely-distributive LATTICE holds
( L is distributive & L is continuous & L ~ is continuous )
proof
let L be complete completely-distributive LATTICE; ::_thesis: ( L is distributive & L is continuous & L ~ is continuous )
L ~ is completely-distributive by YELLOW_7:51;
hence ( L is distributive & L is continuous & L ~ is continuous ) ; ::_thesis: verum
end;
Lm4: for L being complete LATTICE st L is distributive & L is 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; ::_thesis: ( L is distributive & L is continuous & L ~ is continuous implies 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 ) ) )
assume that
A1: ( L is distributive & L is continuous ) and
A2: L ~ is continuous ; ::_thesis: 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 ) )
let l be Element of L; ::_thesis: 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 ) )
reconsider L = L as distributive complete continuous LATTICE by A1;
reconsider l1 = l as Element of (L ~) ;
PRIME (L ~) is order-generating by A2, Th35;
then consider Y being Subset of (PRIME (L ~)) such that
A3: l1 = "/\" (Y,(L ~)) by Th15;
reconsider Y = 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
proof
let x be Element of L; ::_thesis: ( x in Y implies x is co-prime )
assume x in Y ; ::_thesis: x is co-prime
then x ~ is prime by Def7;
hence x is co-prime by Def8; ::_thesis: verum
end;
ex_sup_of Y,L by YELLOW_0:17;
then "\/" (Y,L) = "/\" (Y,(L ~)) by YELLOW_7:12;
hence 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 A3, A4; ::_thesis: verum
end;
theorem :: WAYBEL_6:38
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; ::_thesis: ( 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 ) ) ) ) )
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 ) ) ) ) ) ::_thesis: ( 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 ) ) ) implies L is completely-distributive )
proof
assume L is completely-distributive ; ::_thesis: ( 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 ) ) ) )
then reconsider L = L as completely-distributive LATTICE ;
L ~ is continuous by Lm3;
hence ( 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 ) ) ) ) by Lm4; ::_thesis: verum
end;
thus ( 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 ) ) ) implies L is completely-distributive ) by Lm2; ::_thesis: verum
end;
theorem :: WAYBEL_6:39
for L being complete LATTICE holds
( L is completely-distributive iff ( L is distributive & L is continuous & L opp is continuous ) )
proof
let L be complete LATTICE; ::_thesis: ( L is completely-distributive iff ( L is distributive & L is continuous & L opp is continuous ) )
thus ( L is completely-distributive implies ( L is distributive & L is continuous & L ~ is continuous ) ) by Lm3; ::_thesis: ( L is distributive & L is continuous & L opp is continuous implies L is completely-distributive )
assume that
A1: ( L is distributive & L is continuous ) and
A2: L ~ is continuous ; ::_thesis: L is completely-distributive
reconsider L = 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 L is completely-distributive by Lm2; ::_thesis: verum
end;