let X be non empty TopSpace; :: thesis: for x being set st x in C_0_Functions X holds
x in BoundedFunctions the carrier of X
let x be set ; :: thesis: ( x in C_0_Functions X implies x in BoundedFunctions the carrier of X )
assume A1: x in C_0_Functions X ; :: thesis: x in BoundedFunctions the carrier of X
consider f being RealMap of X such that
A2: ( f = x & f is continuous & ex Y being non empty Subset of X st
( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) ) by A1;
consider Y being non empty Subset of X such that
A3: ( Y is compact & ( for A being Subset of X st A = support f holds
Cl A is Subset of Y ) ) by A2;
dom f = the carrier of X by FUNCT_2:def 1;
then reconsider A = support f as Subset of X by PRE_POLY:37;
reconsider Y1 = f .: Y as non empty real-bounded Subset of REAL by A2, A3, JORDAN_A:1, RCOMP_1:10;
A4: Y1 c= [.(inf Y1),(sup Y1).] by XXREAL_2:69;
reconsider r1 = inf Y1, r2 = sup Y1 as Real ;
consider r being Real such that
A5: r = (|.r1.| + |.r2.|) + 1 ;
for p being Element of Y holds
( r > 0 & - r < f . p & f . p < r )
proof
let p be Element of Y; :: thesis: ( r > 0 & - r < f . p & f . p < r )
f . p in Y1 by FUNCT_2:35;
then f . p in [.r1,r2.] by A4;
then consider r3 being Real such that
A6: ( r3 = f . p & r1 <= r3 & r3 <= r2 ) ;
A7: ( |.r1.| >= 0 & |.r2.| >= 0 ) by COMPLEX1:46;
- |.r1.| <= r1 by ABSVALUE:4;
then (- |.r1.|) - |.r2.| <= r1 - 0 by A7, XREAL_1:13;
then ((- |.r1.|) - |.r2.|) - 1 < r1 - 0 by XREAL_1:15;
then A8: - r < r1 by A5;
r2 <= |.r2.| by ABSVALUE:4;
then r2 + 0 <= |.r2.| + |.r1.| by A7, XREAL_1:7;
then r2 < r by A5, XREAL_1:8;
hence ( r > 0 & - r < f . p & f . p < r ) by A6, A8, XXREAL_0:2; :: thesis: verum
end;
then consider r being Real such that
A9: for p being Element of Y holds
( r > 0 & - r < f . p & f . p < r ) ;
for x being Point of X holds
( - r < f . x & f . x < r )
proof
let x be Point of X; :: thesis: ( - r < f . x & f . x < r )
per cases ( x in the carrier of X \ Y or x in Y ) by XBOOLE_0:def 5;
suppose A10: x in the carrier of X \ Y ; :: thesis: ( - r < f . x & f . x < r )
A11: Cl A is Subset of Y by A3;
support f c= Cl A by PRE_TOPC:18;
then support f c= Y by A11, XBOOLE_1:1;
then not x in support f by A10, XBOOLE_0:def 5;
then A12: f . x = 0 by PRE_POLY:def 7;
(- 1) * r < (- 1) * 0 by A9, XREAL_1:69;
hence ( - r < f . x & f . x < r ) by A12; :: thesis: verum
end;
suppose x in Y ; :: thesis: ( - r < f . x & f . x < r )
hence ( - r < f . x & f . x < r ) by A9; :: thesis: verum
end;
end;
end;
then consider s1 being Real such that
A13: for x being Point of X holds
( - s1 < f . x & f . x < s1 ) ;
for y being object st y in the carrier of X /\ (dom f) holds
f . y <= s1 by A13;
then A14: f | the carrier of X is bounded_above by RFUNCT_1:70;
for y being object st y in the carrier of X /\ (dom f) holds
- s1 <= f . y by A13;
then A15: f | the carrier of X is bounded_below by RFUNCT_1:71;
the carrier of X /\ the carrier of X = the carrier of X ;
then f | the carrier of X is bounded by A14, A15, RFUNCT_1:75;
hence x in BoundedFunctions the carrier of X by A2; :: thesis: verum