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
upper_bound (f | X) <= upper_bound (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
upper_bound (f | X) <= upper_bound (f | Y)
let Y be compact Subset of T; :: thesis: for f being continuous RealMap of T st X c= Y holds
upper_bound (f | X) <= upper_bound (f | Y)
let f be continuous RealMap of T; :: thesis: ( X c= Y implies upper_bound (f | X) <= upper_bound (f | Y) )
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: upper_bound (f | X) <= upper_bound (f | Y)
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_above by MEASURE6:def 11;
hence upper_bound (f | X) <= upper_bound (f | Y) by A2, A1, A3, RELAT_1:123, SEQ_4:48; :: thesis: verum