let T be non empty TopSpace; :: thesis: for X being non empty Subset of T
for Y being compact Subset of T
for f being continuous RealMap of T st X c= Y holds
inf (f | Y) <= inf (f | X)
let X be non empty Subset of T; :: thesis: for Y being compact Subset of T
for f being continuous RealMap of T st X c= Y holds
inf (f | Y) <= inf (f | X)
let Y be compact Subset of T; :: thesis: for f being continuous RealMap of T st X c= Y holds
inf (f | Y) <= inf (f | X)
let f be continuous RealMap of T; :: thesis: ( X c= Y implies inf (f | Y) <= inf (f | X) )
assume A1: X c= Y ; :: thesis: inf (f | Y) <= inf (f | X)
then reconsider Y1 = Y as non empty compact Subset of T ;
A2: (f | Y) .: the carrier of (T | Y) = (f | Y) .: Y by PRE_TOPC:29
.= f .: Y by RELAT_1:162 ;
A3: (f | X) .: the carrier of (T | X) = (f | X) .: X by PRE_TOPC:29
.= f .: X by RELAT_1:162 ;
(f | Y1) .: the carrier of (T | Y1) is bounded_below by Def11;
hence inf (f | Y) <= inf (f | X) by A1, A2, A3, RELAT_1:156, SEQ_4:64; :: thesis: verum