let X be Subset of REAL; ( X is real-bounded iff ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) ) )
thus
( X is real-bounded implies ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) ) )
( ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) ) implies X is real-bounded )proof
assume A1:
X is
real-bounded
;
ex s being Real st
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) )
then consider s1 being
Real such that A2:
s1 is
UpperBound of
X
by XXREAL_2:def 10;
A3:
for
r being
Real st
r in X holds
r <= s1
by A2, XXREAL_2:def 1;
consider s2 being
Real such that A4:
s2 is
LowerBound of
X
by A1, XXREAL_2:def 9;
A5:
for
r being
Real st
r in X holds
s2 <= r
by A4, XXREAL_2:def 2;
take s =
(|.s1.| + |.s2.|) + 1;
( 0 < s & ( for r being Real st r in X holds
|.r.| < s ) )
A6:
0 <= |.s1.|
by COMPLEX1:46;
A7:
0 <= |.s2.|
by COMPLEX1:46;
hence
0 < s
by A6;
for r being Real st r in X holds
|.r.| < s
let r be
Real;
( r in X implies |.r.| < s )
assume A8:
r in X
;
|.r.| < s
(
s1 <= |.s1.| &
r <= s1 )
by A3, A8, ABSVALUE:4;
then
r <= |.s1.|
by XXREAL_0:2;
then
r + 0 <= |.s1.| + |.s2.|
by A7, XREAL_1:7;
then A9:
r < s
by XREAL_1:8;
(
- |.s2.| <= s2 &
s2 <= r )
by A5, A8, ABSVALUE:4;
then
- |.s2.| <= r
by XXREAL_0:2;
then
(- |.s1.|) + (- |.s2.|) <= 0 + r
by A6, XREAL_1:7;
then A10:
((- |.s1.|) - |.s2.|) + (- 1) < r + 0
by XREAL_1:8;
((- |.s1.|) - |.s2.|) - 1
= - ((|.s1.| + |.s2.|) + 1)
;
hence
|.r.| < s
by A9, A10, SEQ_2:1;
verum
end;
given s being Real such that
0 < s
and
A11:
for r being Real st r in X holds
|.r.| < s
; X is real-bounded
thus
X is bounded_below
XXREAL_2:def 11 X is bounded_above
take
s
; XXREAL_2:def 10 s is UpperBound of X
let r be ExtReal; XXREAL_2:def 1 ( not r in X or r <= s )
assume A14:
r in X
; r <= s
then reconsider r = r as Real ;
r <= |.r.|
by ABSVALUE:4;
hence
r <= s
by A11, A14, XXREAL_0:2; verum