let L be lower-bounded LATTICE; :: thesis: ( L is continuous implies ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving ) )

assume A1: L is continuous ; :: thesis: ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving )

reconsider A = InclPoset (Ids L) as lower-bounded arithmetic LATTICE by WAYBEL13:14;

take A ; :: thesis: ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving )

reconsider g = SupMap L as Function of A,L ;

take g ; :: thesis: ( g is onto & g is infs-preserving & g is directed-sups-preserving )

the carrier of L c= rng g

hence g is onto by FUNCT_2:def 3; :: thesis: ( g is infs-preserving & g is directed-sups-preserving )

thus g is infs-preserving by A1, WAYBEL13:33; :: thesis: g is directed-sups-preserving

g is sups-preserving by A1, WAYBEL13:33;

hence g is directed-sups-preserving ; :: thesis: verum

( g is onto & g is infs-preserving & g is directed-sups-preserving ) )

assume A1: L is continuous ; :: thesis: ex A being lower-bounded arithmetic LATTICE ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving )

reconsider A = InclPoset (Ids L) as lower-bounded arithmetic LATTICE by WAYBEL13:14;

take A ; :: thesis: ex g being Function of A,L st

( g is onto & g is infs-preserving & g is directed-sups-preserving )

reconsider g = SupMap L as Function of A,L ;

take g ; :: thesis: ( g is onto & g is infs-preserving & g is directed-sups-preserving )

the carrier of L c= rng g

proof

then
rng g = the carrier of L
by XBOOLE_0:def 10;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of L or y in rng g )

assume y in the carrier of L ; :: thesis: y in rng g

then reconsider y9 = y as Element of L ;

downarrow y9 is Element of A by YELLOW_2:41;

then downarrow y9 in the carrier of A ;

then A2: downarrow y9 in dom g by FUNCT_2:def 1;

g . (downarrow y9) = sup (downarrow y9) by YELLOW_2:def 3

.= y9 by WAYBEL_0:34 ;

hence y in rng g by A2, FUNCT_1:def 3; :: thesis: verum

end;assume y in the carrier of L ; :: thesis: y in rng g

then reconsider y9 = y as Element of L ;

downarrow y9 is Element of A by YELLOW_2:41;

then downarrow y9 in the carrier of A ;

then A2: downarrow y9 in dom g by FUNCT_2:def 1;

g . (downarrow y9) = sup (downarrow y9) by YELLOW_2:def 3

.= y9 by WAYBEL_0:34 ;

hence y in rng g by A2, FUNCT_1:def 3; :: thesis: verum

hence g is onto by FUNCT_2:def 3; :: thesis: ( g is infs-preserving & g is directed-sups-preserving )

thus g is infs-preserving by A1, WAYBEL13:33; :: thesis: g is directed-sups-preserving

g is sups-preserving by A1, WAYBEL13:33;

hence g is directed-sups-preserving ; :: thesis: verum