let S, T be Semilattice; for f being Function of S,T st f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) holds
for X being non empty Subset of S holds f preserves_inf_of X
let f be Function of S,T; ( f is meet-preserving & ( for X being non empty filtered Subset of S holds f preserves_inf_of X ) implies for X being non empty Subset of S holds f preserves_inf_of X )
assume that
A1:
f is meet-preserving
and
A2:
for X being non empty filtered Subset of S holds f preserves_inf_of X
; for X being non empty Subset of S holds f preserves_inf_of X
let X be non empty Subset of S; f preserves_inf_of X
assume A3:
ex_inf_of X,S
; WAYBEL_0:def 30 ( ex_inf_of f .: X,T & "/\" ((f .: X),T) = f . ("/\" (X,S)) )
defpred S1[ object ] means ex Y being non empty 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 & S1[x] ) )
from XBOOLE_0:sch 1();
set a = the Element of X;
reconsider a9 = the Element of X as Element of S ;
A5:
ex_inf_of { the Element of X},S
by YELLOW_0:38;
A6:
inf {a9} = the Element of X
by YELLOW_0:39;
Z c= the carrier of S
by A4;
then reconsider Z = Z as non empty Subset of S by A4, A5, A6;
then A11:
Z is filtered
by A7, A8, WAYBEL_0:56;
A12:
ex_inf_of Z,S
by A3, A7, A8, A10, WAYBEL_0:58;
A13:
f preserves_inf_of Z
by A2, A11;
then A14:
ex_inf_of f .: Z,T
by A12;
A15:
inf (f .: Z) = f . (inf Z)
by A12, A13;
A16:
inf Z = inf X
by A3, A7, A8, A10, WAYBEL_0:59;
X c= Z
then A19:
f .: X c= f .: Z
by RELAT_1:123;
A20:
f .: Z is_>=_than f . (inf X)
by A14, A15, A16, YELLOW_0:31;
A21:
f .: X is_>=_than f . (inf X)
by A19, A20;
A22:
now for b being Element of T st f .: X is_>=_than b holds
f . (inf X) >= blet b be
Element of
T;
( f .: X is_>=_than b implies f . (inf X) >= b )assume A23:
f .: X is_>=_than b
;
f . (inf X) >= b
f .: Z is_>=_than b
proof
let a be
Element of
T;
LATTICE3:def 8 ( not a in f .: Z or b <= a )
assume
a in f .: Z
;
b <= a
then consider x being
object such that
x in dom f
and A24:
x in Z
and A25:
a = f . x
by FUNCT_1:def 6;
consider Y being non
empty finite Subset of
X such that A26:
ex_inf_of Y,
S
and A27:
x = "/\" (
Y,
S)
by A4, A24;
reconsider Y =
Y as
Subset of
S by XBOOLE_1:1;
A28:
f .: Y c= f .: X
by RELAT_1:123;
A29:
f preserves_inf_of Y
by A1, Th2;
A30:
b is_<=_than f .: Y
by A23, A28;
A31:
a = "/\" (
(f .: Y),
T)
by A25, A26, A27, A29;
ex_inf_of f .: Y,
T
by A26, A29;
hence
b <= a
by A30, A31, YELLOW_0:def 10;
verum
end; hence
f . (inf X) >= b
by A14, A15, A16, YELLOW_0:31;
verum end;
hence
ex_inf_of f .: X,T
by A21, YELLOW_0:16; "/\" ((f .: X),T) = f . ("/\" (X,S))
hence
inf (f .: X) = f . (inf X)
by A21, A22, YELLOW_0:def 10; verum