let S be Semilattice; :: thesis: for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
let T be non empty Poset; :: thesis: for f being Function of S,T st ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
let f be Function of S,T; :: thesis: ( ( for X being finite Subset of S holds f preserves_inf_of X ) & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) implies f is infs-preserving )
assume that
A1: for X being finite Subset of S holds f preserves_inf_of X and
A2: for X being non empty filtered Subset of S holds f preserves_inf_of X ; :: thesis: f is infs-preserving
let X be Subset of S; :: according to WAYBEL_0:def 32 :: thesis: f preserves_inf_of X
assume A3: ex_inf_of X,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of f .: X,T & inf (f .: X) = f . (inf X) )
defpred S₁[ set ] means ex Y being finite Subset of X st
( ex_inf_of Y,S & $1 = "/\" Y,S );
consider Z being set such that
A4: for x being set holds
( x in Z iff ( x in the carrier of S & S₁[x] ) ) from XBOOLE_0:sch 1();
Z c= the carrier of S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in the carrier of S )
thus ( not x in Z or x in the carrier of S ) by A4; :: thesis: verum

end;

then reconsider Z = Z as Subset of S ;

A5: now

let Y be finite Subset of X; :: thesis: ( Y <> {} implies ex_inf_of Y,S )
Y is Subset of S by XBOOLE_1:1;
hence ( Y <> {} implies ex_inf_of Y,S ) by YELLOW_0:55; :: thesis: verum

end;

A6: now

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "/\" Y,S in Z )
reconsider Y' = Y as Subset of S by XBOOLE_1:1;
assume Y <> {} ; :: thesis: "/\" Y,S in Z
then ex_inf_of Y',S by YELLOW_0:55;
hence "/\" Y,S in Z by A4; :: thesis: verum

end;

for x being Element of S st x in Z holds
ex Y being finite Subset of X st
( ex_inf_of Y,S & x = "/\" Y,S ) by A4;
then A7: ( Z is filtered & ex_inf_of Z,S & inf Z = inf X & ( Z = {} or Z <> {} ) ) by A3, A5, A6, Th56, Th58, Th59;
then f preserves_inf_of Z by A1, A2;
then A8: ( ex_inf_of f .: Z,T & inf (f .: Z) = f . (inf Z) & inf Z = inf X ) by A7, Def30;
X c= Z

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )
assume A9: x in X ; :: thesis: x in Z
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:37;
reconsider x = x as Element of S by A9;
Y is Subset of S by XBOOLE_1:1;
then ( ex_inf_of Y,S & x = "/\" Y,S ) by YELLOW_0:39, YELLOW_0:55;
hence x in Z by A4; :: thesis: verum

end;

then A10: f .: X c= f .: Z by RELAT_1:156;
A11: f .: Z is_>=_than f . (inf X) by A8, YELLOW_0:31;
A12: f .: X is_>=_than f . (inf X)

proof

let x be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not x in f .: X or f . (inf X) <= x )
assume x in f .: X ; :: thesis: f . (inf X) <= x
hence f . (inf X) <= x by A10, A11, LATTICE3:def 8; :: thesis: verum

end;

A13: now

let b be Element of T; :: thesis: ( f .: X is_>=_than b implies f . (inf X) >= b )
assume A14: f .: X is_>=_than b ; :: thesis: f . (inf X) >= b
f .: Z is_>=_than b

proof

let a be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not a in f .: Z or b <= a )
assume a in f .: Z ; :: thesis: b <= a
then consider x being set such that
A15: ( x in dom f & x in Z & a = f . x ) by FUNCT_1:def 12;
consider Y being finite Subset of X such that
A16: ( ex_inf_of Y,S & x = "/\" Y,S ) by A4, A15;
reconsider Y = Y as Subset of S by XBOOLE_1:1;
( f .: Y c= f .: X & f preserves_inf_of Y ) by A1, RELAT_1:156;
then ( b is_<=_than f .: Y & a = "/\" (f .: Y),T & ex_inf_of f .: Y,T ) by A14, A15, A16, Def30, YELLOW_0:9;
hence b <= a by YELLOW_0:def 10; :: thesis: verum

end;

hence f . (inf X) >= b by A8, YELLOW_0:31; :: thesis: verum

end;

hence ex_inf_of f .: X,T by A12, YELLOW_0:16; :: thesis: inf (f .: X) = f . (inf X)
hence inf (f .: X) = f . (inf X) by A12, A13, YELLOW_0:def 10; :: thesis: verum