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
lower_bound (f | Y) <= lower_bound (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
lower_bound (f | Y) <= lower_bound (f | X)
let Y be compact Subset of T; :: thesis: for f being continuous RealMap of T st X c= Y holds
lower_bound (f | Y) <= lower_bound (f | X)
let f be continuous RealMap of T; :: thesis: ( X c= Y implies lower_bound (f | Y) <= lower_bound (f | X) )
A1: (f | Y) .: the carrier of (T | Y) = (f | Y) .: Y by PRE_TOPC:8
.= f .: Y by RELAT_1:129 ;
assume A2: X c= Y ; :: thesis: lower_bound (f | Y) <= lower_bound (f | X)
then reconsider Y1 = Y as non empty compact Subset of T ;
A3: (f | X) .: the carrier of (T | X) = (f | X) .: X by PRE_TOPC:8
.= f .: X by RELAT_1:129 ;
(f | Y1) .: the carrier of (T | Y1) is bounded_below by MEASURE6:def 10;
hence lower_bound (f | Y) <= lower_bound (f | X) by A2, A1, A3, RELAT_1:123, SEQ_4:47; :: thesis: verum