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
sup (f | X) <= sup (f | Y)
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
sup (f | X) <= sup (f | Y)
let Y be compact Subset of T; :: thesis: for f being continuous RealMap of T st X c= Y holds
sup (f | X) <= sup (f | Y)
let f be continuous RealMap of T; :: thesis: ( X c= Y implies sup (f | X) <= sup (f | Y) )
assume A1: X c= Y ; :: thesis: sup (f | X) <= sup (f | Y)
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_above by Def12;
hence sup (f | X) <= sup (f | Y) by A1, A2, A3, RELAT_1:156, SEQ_4:65; :: thesis: verum