let X be non empty set ; :: thesis: for Y being non empty Subset of ExtREAL
for F being Function of X,Y st Y c= REAL holds
( F is bounded_below iff inf F in REAL )
let Y be non empty Subset of ExtREAL; :: thesis: for F being Function of X,Y st Y c= REAL holds
( F is bounded_below iff inf F in REAL )
let F be Function of X,Y; :: thesis: ( Y c= REAL implies ( F is bounded_below iff inf F in REAL ) )
assume A1: Y c= REAL ; :: thesis: ( F is bounded_below iff inf F in REAL )
thus ( F is bounded_below implies inf F in REAL ) :: thesis: ( inf F in REAL implies F is bounded_below )
proof
set x = the Element of X;
X = dom F by FUNCT_2:def 1;
then A2: F . the Element of X in rng F by FUNCT_1:def 3;
rng F c= Y by RELAT_1:def 19;
then F . the Element of X in Y by A2;
then A3: not inf F = +infty by A1, Th26, XXREAL_0:9;
assume a4: F is bounded_below ; :: thesis: inf F in REAL
( inf F in REAL or inf F in {-infty,+infty} ) by XBOOLE_0:def 3;
hence inf F in REAL by a4, A3, TARSKI:def 2; :: thesis: verum
end;
assume inf F in REAL ; :: thesis: F is bounded_below
hence F is bounded_below by XXREAL_0:12; :: thesis: verum