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 )

hence F is bounded_below by XXREAL_0:12; :: thesis: verum

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

assume
inf F in REAL
; :: thesis: F is bounded_below
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;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

hence F is bounded_below by XXREAL_0:12; :: thesis: verum