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_{1}[ object ] 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 object holds

( x in Z iff ( x in the carrier of S & S_{1}[x] ) )
from XBOOLE_0:sch 1();

Z c= the carrier of S by A4;

then reconsider Z = Z as Subset of S ;

ex Y being finite Subset of X st

( ex_inf_of Y,S & x = "/\" (Y,S) ) by A4;

then A8: Z is filtered by A5, A6, Th56;

A9: ex_inf_of Z,S by A3, A5, A6, A7, Th58;

( Z = {} or Z <> {} ) ;

then A10: f preserves_inf_of Z by A1, A2, A8;

then A11: ex_inf_of f .: Z,T by A9;

A12: inf (f .: Z) = f . (inf Z) by A9, A10;

A13: inf Z = inf X by A3, A5, A6, A7, Th59;

X c= Z

A17: f .: Z is_>=_than f . (inf X) by A11, A12, A13, YELLOW_0:31;

A18: f .: X is_>=_than f . (inf X) by A16, A17;

hence inf (f .: X) = f . (inf X) by A18, A19, YELLOW_0:def 10; :: thesis: verum

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

( ex_inf_of Y,S & $1 = "/\" (Y,S) );

consider Z being set such that

A4: for x being object holds

( x in Z iff ( x in the carrier of S & S

Z c= the carrier of S by A4;

then reconsider Z = Z as Subset of S ;

A5: now :: thesis: for Y being finite Subset of X st Y <> {} holds

ex_inf_of Y,S

ex_inf_of Y,S

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;Y is Subset of S by XBOOLE_1:1;

hence ( Y <> {} implies ex_inf_of Y,S ) by YELLOW_0:55; :: thesis: verum

A6: now :: thesis: for Y being finite Subset of X st Y <> {} holds

"/\" (Y,S) in Z

A7:
for x being Element of S st x in Z holds "/\" (Y,S) in Z

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "/\" (Y,S) in Z )

reconsider Y9 = Y as Subset of S by XBOOLE_1:1;

assume Y <> {} ; :: thesis: "/\" (Y,S) in Z

then ex_inf_of Y9,S by YELLOW_0:55;

hence "/\" (Y,S) in Z by A4; :: thesis: verum

end;reconsider Y9 = Y as Subset of S by XBOOLE_1:1;

assume Y <> {} ; :: thesis: "/\" (Y,S) in Z

then ex_inf_of Y9,S by YELLOW_0:55;

hence "/\" (Y,S) in Z by A4; :: thesis: verum

ex Y being finite Subset of X st

( ex_inf_of Y,S & x = "/\" (Y,S) ) by A4;

then A8: Z is filtered by A5, A6, Th56;

A9: ex_inf_of Z,S by A3, A5, A6, A7, Th58;

( Z = {} or Z <> {} ) ;

then A10: f preserves_inf_of Z by A1, A2, A8;

then A11: ex_inf_of f .: Z,T by A9;

A12: inf (f .: Z) = f . (inf Z) by A9, A10;

A13: inf Z = inf X by A3, A5, A6, A7, Th59;

X c= Z

proof

then A16:
f .: X c= f .: Z
by RELAT_1:123;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )

assume A14: x in X ; :: thesis: x in Z

then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;

reconsider x = x as Element of S by A14;

Y is Subset of S by XBOOLE_1:1;

then A15: ex_inf_of Y,S by YELLOW_0:55;

x = "/\" (Y,S) by YELLOW_0:39;

hence x in Z by A4, A15; :: thesis: verum

end;assume A14: x in X ; :: thesis: x in Z

then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;

reconsider x = x as Element of S by A14;

Y is Subset of S by XBOOLE_1:1;

then A15: ex_inf_of Y,S by YELLOW_0:55;

x = "/\" (Y,S) by YELLOW_0:39;

hence x in Z by A4, A15; :: thesis: verum

A17: f .: Z is_>=_than f . (inf X) by A11, A12, A13, YELLOW_0:31;

A18: f .: X is_>=_than f . (inf X) by A16, A17;

A19: now :: thesis: for b being Element of T st f .: X is_>=_than b holds

f . (inf X) >= b

hence
ex_inf_of f .: X,T
by A18, YELLOW_0:16; :: thesis: inf (f .: X) = f . (inf X)f . (inf X) >= b

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

assume A20: f .: X is_>=_than b ; :: thesis: f . (inf X) >= b

f .: Z is_>=_than b

end;assume A20: f .: X is_>=_than b ; :: thesis: f . (inf X) >= b

f .: Z is_>=_than b

proof

hence
f . (inf X) >= b
by A11, A12, A13, YELLOW_0:31; :: thesis: verum
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 object such that

x in dom f and

A21: x in Z and

A22: a = f . x by FUNCT_1:def 6;

consider Y being finite Subset of X such that

A23: ex_inf_of Y,S and

A24: x = "/\" (Y,S) by A4, A21;

reconsider Y = Y as Subset of S by XBOOLE_1:1;

A25: f .: Y c= f .: X by RELAT_1:123;

A26: f preserves_inf_of Y by A1;

A27: b is_<=_than f .: Y by A20, A25;

A28: a = "/\" ((f .: Y),T) by A22, A23, A24, A26;

ex_inf_of f .: Y,T by A23, A26;

hence b <= a by A27, A28, YELLOW_0:def 10; :: thesis: verum

end;assume a in f .: Z ; :: thesis: b <= a

then consider x being object such that

x in dom f and

A21: x in Z and

A22: a = f . x by FUNCT_1:def 6;

consider Y being finite Subset of X such that

A23: ex_inf_of Y,S and

A24: x = "/\" (Y,S) by A4, A21;

reconsider Y = Y as Subset of S by XBOOLE_1:1;

A25: f .: Y c= f .: X by RELAT_1:123;

A26: f preserves_inf_of Y by A1;

A27: b is_<=_than f .: Y by A20, A25;

A28: a = "/\" ((f .: Y),T) by A22, A23, A24, A26;

ex_inf_of f .: Y,T by A23, A26;

hence b <= a by A27, A28, YELLOW_0:def 10; :: thesis: verum

hence inf (f .: X) = f . (inf X) by A18, A19, YELLOW_0:def 10; :: thesis: verum