let S, T be non empty Poset; :: thesis: for f being Function of S,T st ( for X being Filter of S holds f preserves_inf_of X ) holds

f is filtered-infs-preserving

let f be Function of S,T; :: thesis: ( ( for X being Filter of S holds f preserves_inf_of X ) implies f is filtered-infs-preserving )

assume A1: for X being Filter of S holds f preserves_inf_of X ; :: thesis: f is filtered-infs-preserving

let X be Subset of S; :: according to WAYBEL_0:def 36 :: thesis: ( not X is empty & X is filtered implies f preserves_inf_of X )

assume that

A2: ( not X is empty & X is filtered ) and

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) )

reconsider Y = X as non empty filtered Subset of S by A2;

uparrow Y is Filter of S ;

then A4: f preserves_inf_of uparrow X by A1;

A5: ex_inf_of uparrow X,S by A3, Th37;

then A6: ex_inf_of f .: (uparrow X),T by A4;

A7: inf (f .: (uparrow X)) = f . (inf (uparrow X)) by A4, A5;

A8: inf (uparrow X) = inf X by A3, Th38;

A9: f .: X c= f .: (uparrow X) by Th16, RELAT_1:123;

A10: f .: (uparrow X) is_>=_than f . (inf X) by A6, A7, A8, YELLOW_0:31;

A11: f .: X is_>=_than f . (inf X) by A9, A10;

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

f is filtered-infs-preserving

let f be Function of S,T; :: thesis: ( ( for X being Filter of S holds f preserves_inf_of X ) implies f is filtered-infs-preserving )

assume A1: for X being Filter of S holds f preserves_inf_of X ; :: thesis: f is filtered-infs-preserving

let X be Subset of S; :: according to WAYBEL_0:def 36 :: thesis: ( not X is empty & X is filtered implies f preserves_inf_of X )

assume that

A2: ( not X is empty & X is filtered ) and

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) )

reconsider Y = X as non empty filtered Subset of S by A2;

uparrow Y is Filter of S ;

then A4: f preserves_inf_of uparrow X by A1;

A5: ex_inf_of uparrow X,S by A3, Th37;

then A6: ex_inf_of f .: (uparrow X),T by A4;

A7: inf (f .: (uparrow X)) = f . (inf (uparrow X)) by A4, A5;

A8: inf (uparrow X) = inf X by A3, Th38;

A9: f .: X c= f .: (uparrow X) by Th16, RELAT_1:123;

A10: f .: (uparrow X) is_>=_than f . (inf X) by A6, A7, A8, YELLOW_0:31;

A11: f .: X is_>=_than f . (inf X) by A9, A10;

A12: 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 A11, 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 A13: f .: X is_>=_than b ; :: thesis: f . (inf X) >= b

f .: (uparrow X) is_>=_than b

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

f .: (uparrow X) is_>=_than b

proof

hence
f . (inf X) >= b
by A6, A7, A8, YELLOW_0:31; :: thesis: verum
let a be Element of T; :: according to LATTICE3:def 8 :: thesis: ( not a in f .: (uparrow X) or b <= a )

assume a in f .: (uparrow X) ; :: thesis: b <= a

then consider x being object such that

x in dom f and

A14: x in uparrow X and

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

uparrow X = { z where z is Element of S : ex y being Element of S st

( z >= y & y in X ) } by Th15;

then consider z being Element of S such that

A16: x = z and

A17: ex y being Element of S st

( z >= y & y in X ) by A14;

consider y being Element of S such that

A18: z >= y and

A19: y in X by A17;

A20: f is monotone by A1, Th69;

A21: f . y in f .: X by A19, FUNCT_2:35;

A22: f . z >= f . y by A18, A20;

f . y >= b by A13, A21;

hence b <= a by A15, A16, A22, ORDERS_2:3; :: thesis: verum

end;assume a in f .: (uparrow X) ; :: thesis: b <= a

then consider x being object such that

x in dom f and

A14: x in uparrow X and

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

uparrow X = { z where z is Element of S : ex y being Element of S st

( z >= y & y in X ) } by Th15;

then consider z being Element of S such that

A16: x = z and

A17: ex y being Element of S st

( z >= y & y in X ) by A14;

consider y being Element of S such that

A18: z >= y and

A19: y in X by A17;

A20: f is monotone by A1, Th69;

A21: f . y in f .: X by A19, FUNCT_2:35;

A22: f . z >= f . y by A18, A20;

f . y >= b by A13, A21;

hence b <= a by A15, A16, A22, ORDERS_2:3; :: thesis: verum

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