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