let S be non empty TopSpace; :: thesis: for T being NormedLinearTopSpace
for f being Function of S,T
for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is continuous holds
ex K being Real st
( 0 <= K & ( for x being Point of S st x in Y holds
||.(f . x).|| <= K ) )
let T be NormedLinearTopSpace; :: thesis: for f being Function of S,T
for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is continuous holds
ex K being Real st
( 0 <= K & ( for x being Point of S st x in Y holds
||.(f . x).|| <= K ) )
let f be Function of S,T; :: thesis: for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is continuous holds
ex K being Real st
( 0 <= K & ( for x being Point of S st x in Y holds
||.(f . x).|| <= K ) )
let Y be Subset of S; :: thesis: ( Y <> {} & Y c= dom f & Y is compact & f is continuous implies ex K being Real st
( 0 <= K & ( for x being Point of S st x in Y holds
||.(f . x).|| <= K ) ) )
assume that
A1: Y <> {} and
A2: Y c= dom f and
A3: Y is compact and
A4: f is continuous ; :: thesis: ex K being Real st
( 0 <= K & ( for x being Point of S st x in Y holds
||.(f . x).|| <= K ) )
consider RNS being RealNormSpace such that
A5: ( RNS = NORMSTR(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T, the normF of T #) & the topology of T = the topology of (TopSpaceNorm RNS) ) by Def7;
reconsider g = the normF of RNS as Function of the carrier of RNS,REAL ;
A6: for x being Point of RNS st x in the carrier of RNS holds
g /. x = ||.x.|| ;
A7: the carrier of RNS = dom g by FUNCT_2:def 1;
reconsider g = g as PartFunc of RNS,REAL ;
reconsider FY = f .: Y as Subset of RNS by A5;
A8: g is_continuous_on FY by A7, NFCONT_1:54, A6, Th33;
A9: f .: Y is compact by A3, A4, WEIERSTR:8;
A10: dom (g | FY) = (dom g) /\ FY by RELAT_1:61
.= FY by A7, XBOOLE_1:28 ;
A11: g | FY is_continuous_on FY
proof
thus FY c= dom (g | FY) by A10; :: according to NFCONT_1:def 8 :: thesis: for b1 being Element of the carrier of RNS holds
( not b1 in FY or (g | FY) | FY is_continuous_in b1 )
let r be Point of RNS; :: thesis: ( not r in FY or (g | FY) | FY is_continuous_in r )
assume r in FY ; :: thesis: (g | FY) | FY is_continuous_in r
then g | FY is_continuous_in r by A8;
hence (g | FY) | FY is_continuous_in r by RELAT_1:72; :: thesis: verum
end;
A12: dom (g | FY) is compact by A9, A5, Th32, A10;
A13: g .: FY = rng (g | FY) by RELAT_1:115;
then A14: g .: FY is real-bounded by RCOMP_1:10, A12, A10, A11, NFCONT_1:31;
consider x1, x2 being Point of RNS such that
A15: ( x1 in dom (g | FY) & x2 in dom (g | FY) ) and
A16: ( (g | FY) /. x1 = upper_bound (rng (g | FY)) & (g | FY) /. x2 = lower_bound (rng (g | FY)) ) by A10, A11, A12, NFCONT_1:33, A1;
set K = (g | FY) /. x1;
set L = (g | FY) /. x2;
A17: (g | FY) /. x1 = (g | FY) . x1 by A15, PARTFUN1:def 6;
take (g | FY) /. x1 ; :: thesis: ( 0 <= (g | FY) /. x1 & ( for x being Point of S st x in Y holds
||.(f . x).|| <= (g | FY) /. x1 ) )
(g | FY) /. x1 = ||.x1.|| by FUNCT_1:47, A15, A17;
hence 0 <= (g | FY) /. x1 ; :: thesis: for x being Point of S st x in Y holds
||.(f . x).|| <= (g | FY) /. x1
thus for x being Point of S st x in Y holds
||.(f . x).|| <= (g | FY) /. x1 :: thesis: verum
proof
let z be Point of S; :: thesis: ( z in Y implies ||.(f . z).|| <= (g | FY) /. x1 )
assume A18: z in Y ; :: thesis: ||.(f . z).|| <= (g | FY) /. x1
A19: f . z in dom (g | FY) by A10, A18, FUNCT_1:def 6, A2;
then A20: (g | FY) . (f . z) in rng (g | FY) by FUNCT_1:3;
A21: (g | FY) . (f . z) = g . (f . z) by A19, FUNCT_1:47
.= g /. (f . z) by A5, PARTFUN1:def 6, A7 ;
reconsider fz = f . z as Point of RNS by A5;
g /. fz = ||.fz.|| by A6
.= ||.(f . z).|| by A5 ;
hence ||.(f . z).|| <= (g | FY) /. x1 by A21, A20, A16, A14, A13, SEQ_4:def 1; :: thesis: verum
end;