let S, T be Semilattice; for f being Function of S,T holds
( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )
let f be Function of S,T; ( f is meet-preserving iff for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )
A1:
dom f = the carrier of S
by FUNCT_2:def 1;
thus
( f is meet-preserving implies for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) )
( ( for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y) ) implies f is meet-preserving )proof
assume A2:
f is
meet-preserving
;
for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y)
let z,
y be
Element of
S;
f . (z "/\" y) = (f . z) "/\" (f . y)
A3:
f preserves_inf_of {z,y}
by A2;
A4:
(
f .: {z,y} = {(f . z),(f . y)} &
ex_inf_of {z,y},
S )
by A1, FUNCT_1:60, YELLOW_0:21;
thus f . (z "/\" y) =
f . (inf {z,y})
by YELLOW_0:40
.=
inf {(f . z),(f . y)}
by A4, A3
.=
(f . z) "/\" (f . y)
by YELLOW_0:40
;
verum
end;
assume A5:
for x, y being Element of S holds f . (x "/\" y) = (f . x) "/\" (f . y)
; f is meet-preserving
for z, y being Element of S holds f preserves_inf_of {z,y}
proof
let z,
y be
Element of
S;
f preserves_inf_of {z,y}
A6:
f .: {z,y} = {(f . z),(f . y)}
by A1, FUNCT_1:60;
then A7:
(
ex_inf_of {z,y},
S implies
ex_inf_of f .: {z,y},
T )
by YELLOW_0:21;
inf (f .: {z,y}) =
(f . z) "/\" (f . y)
by A6, YELLOW_0:40
.=
f . (z "/\" y)
by A5
.=
f . (inf {z,y})
by YELLOW_0:40
;
hence
f preserves_inf_of {z,y}
by A7;
verum
end;
hence
f is meet-preserving
; verum