let R, S, T be LATTICE; for f being Function of [:R,S:],T st ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) holds
f is antitone
let f be Function of [:R,S:],T; ( ( for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone ) ) implies f is antitone )
assume A1:
for a being Element of R
for b being Element of S holds
( Proj (f,a) is antitone & Proj (f,b) is antitone )
; f is antitone
now for x, y being Element of [:R,S:] st x <= y holds
f . x >= f . ylet x,
y be
Element of
[:R,S:];
( x <= y implies f . x >= f . y )assume A2:
x <= y
;
f . x >= f . ythen A3:
x `1 <= y `1
by YELLOW_3:12;
A4:
x `2 <= y `2
by A2, YELLOW_3:12;
A5:
f . (
(x `1),
(y `2))
= (Proj (f,(x `1))) . (y `2)
by Th7;
(
Proj (
f,
(x `1)) is
antitone &
f . (
(x `1),
(x `2))
= (Proj (f,(x `1))) . (x `2) )
by A1, Th7;
then A6:
f . [(x `1),(x `2)] >= f . [(x `1),(y `2)]
by A4, A5;
A7:
f . (
(y `1),
(y `2))
= (Proj (f,(y `2))) . (y `1)
by Th8;
(
Proj (
f,
(y `2)) is
antitone &
f . (
(x `1),
(y `2))
= (Proj (f,(y `2))) . (x `1) )
by A1, Th8;
then
f . [(x `1),(y `2)] >= f . [(y `1),(y `2)]
by A3, A7;
then A8:
f . [(x `1),(x `2)] >= f . [(y `1),(y `2)]
by A6, YELLOW_0:def 2;
A9:
[: the carrier of R, the carrier of S:] = the
carrier of
[:R,S:]
by YELLOW_3:def 2;
then
f . [(y `1),(y `2)] = f . y
by MCART_1:21;
hence
f . x >= f . y
by A8, A9, MCART_1:21;
verum end;
hence
f is antitone
; verum