let f be real-valued Function; :: thesis: ( f is bounded iff ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r )
thus
( f is bounded implies ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r )
:: thesis: ( ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r implies f is bounded )proof
assume A1:
f is
bounded
;
:: thesis: ex r being real number st
for c being set st c in dom f holds
abs (f . c) <= r
then consider r1 being
real number such that A2:
for
c being
set st
c in dom f holds
f . c < r1
by SEQ_2:def 1;
consider r2 being
real number such that A3:
for
c being
set st
c in dom f holds
r2 < f . c
by A1, SEQ_2:def 2;
take g =
(abs r1) + (abs r2);
:: thesis: for c being set st c in dom f holds
abs (f . c) <= g
let c be
set ;
:: thesis: ( c in dom f implies abs (f . c) <= g )
assume A4:
c in dom f
;
:: thesis: abs (f . c) <= g
A5:
0 <= abs r1
by COMPLEX1:132;
A6:
0 <= abs r2
by COMPLEX1:132;
A7:
r1 <= abs r1
by ABSVALUE:11;
f . c <= abs r1
by A7, A2, A4, XXREAL_0:2;
then A8:
(f . c) + 0 <= (abs r1) + (abs r2)
by A6, XREAL_1:9;
A9:
- (abs r2) <= r2
by ABSVALUE:11;
- (abs r2) <= f . c
by A9, A3, A4, XXREAL_0:2;
then A11:
(- (abs r1)) + (- (abs r2)) <= 0 + (f . c)
by A5, XREAL_1:9;
(- (abs r1)) + (- (abs r2)) = - g
;
hence
abs (f . c) <= g
by A8, A11, ABSVALUE:12;
:: thesis: verum
end;
given r being real number such that A12:
for c being set st c in dom f holds
abs (f . c) <= r
; :: thesis: f is bounded
thus
f is bounded_above
:: according to SEQ_2:def 8 :: thesis: f is bounded_below
take
- (r + 1)
; :: according to SEQ_2:def 2 :: thesis: for b1 being set holds
( not b1 in dom f or not f . b1 <= - (r + 1) )
let c be set ; :: thesis: ( not c in dom f or not f . c <= - (r + 1) )
assume
c in dom f
; :: thesis: not f . c <= - (r + 1)
then
abs (f . c) < r + 1
by A12, XREAL_1:41;
then A15:
- (r + 1) < - (abs (f . c))
by XREAL_1:26;
- (abs (f . c)) <= f . c
by ABSVALUE:11;
hence
not f . c <= - (r + 1)
by A15, XXREAL_0:2; :: thesis: verum