let S be non empty lower-bounded Poset; :: thesis: for T being non empty Poset
for f being monotone Function of S,T holds Image f is lower-bounded
let T be non empty Poset; :: thesis: for f being monotone Function of S,T holds Image f is lower-bounded
let f be monotone Function of S,T; :: thesis: Image f is lower-bounded
thus Image f is lower-bounded :: thesis: verum
proof
consider x being Element of S such that
A1: x is_<=_than the carrier of S by YELLOW_0:def 4;
dom f = the carrier of S by FUNCT_2:def 1;
then f . x in rng f by FUNCT_1:def 3;
then reconsider fx = f . x as Element of (Image f) by YELLOW_0:def 15;
take fx ; :: according to YELLOW_0:def 4 :: thesis: fx is_<=_than the carrier of (Image f)
let b be Element of (Image f); :: according to LATTICE3:def 8 :: thesis: ( not b in the carrier of (Image f) or fx <= b )
b in the carrier of (subrelstr (rng f)) ;
then b in rng f by YELLOW_0:def 15;
then consider c being object such that
A2: c in dom f and
A3: f . c = b by FUNCT_1:def 3;
A4: the carrier of (Image f) c= the carrier of T by YELLOW_0:def 13;
assume b in the carrier of (Image f) ; :: thesis: fx <= b
reconsider b1 = b as Element of T by A4;
reconsider c = c as Element of S by A2;
x <= c by A1;
then f . x <= b1 by A3, ORDERS_3:def 5;
hence fx <= b by YELLOW_0:60; :: thesis: verum
end;