let S, T be sup-Semilattice; for f being Function of S,T holds
( f is join-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 join-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 join-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 join-preserving )proof
assume A2:
f is
join-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_sup_of {z,y}
by A2;
A4:
(
f .: {z,y} = {(f . z),(f . y)} &
ex_sup_of {z,y},
S )
by A1, FUNCT_1:60, YELLOW_0:20;
thus f . (z "\/" y) =
f . (sup {z,y})
by YELLOW_0:41
.=
sup {(f . z),(f . y)}
by A4, A3
.=
(f . z) "\/" (f . y)
by YELLOW_0:41
;
verum
end;
assume A5:
for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y)
; f is join-preserving
for z, y being Element of S holds f preserves_sup_of {z,y}
proof
let z,
y be
Element of
S;
f preserves_sup_of {z,y}
A6:
f .: {z,y} = {(f . z),(f . y)}
by A1, FUNCT_1:60;
then A7:
(
ex_sup_of {z,y},
S implies
ex_sup_of f .: {z,y},
T )
by YELLOW_0:20;
sup (f .: {z,y}) =
(f . z) "\/" (f . y)
by A6, YELLOW_0:41
.=
f . (z "\/" y)
by A5
.=
f . (sup {z,y})
by YELLOW_0:41
;
hence
f preserves_sup_of {z,y}
by A7;
verum
end;
hence
f is join-preserving
; verum