let n be Element of NAT ; for f being PartFunc of REAL,(REAL n)
for g being PartFunc of REAL,(REAL-NS n) st f = g holds
( f is bounded iff g is bounded )
let f be PartFunc of REAL,(REAL n); for g being PartFunc of REAL,(REAL-NS n) st f = g holds
( f is bounded iff g is bounded )
let g be PartFunc of REAL,(REAL-NS n); ( f = g implies ( f is bounded iff g is bounded ) )
assume A1:
f = g
; ( f is bounded iff g is bounded )
thus
( f is bounded implies g is bounded )
( g is bounded implies f is bounded )proof
assume A2:
f is
bounded
;
g is bounded
defpred S1[
Nat,
Element of
REAL ]
means for
y being
set st
y in dom ((proj ($1,n)) * f) holds
|.(((proj ($1,n)) * f) . y).| < $2;
A3:
for
i being
Nat st
i in Seg n holds
ex
di being
Element of
REAL st
S1[
i,
di]
consider d being
FinSequence of
REAL such that A5:
(
dom d = Seg n & ( for
k being
Nat st
k in Seg n holds
S1[
k,
d /. k] ) )
from RECDEF_1:sch 17(A3);
set K =
max d;
for
y being
set st
y in dom g holds
||.(g /. y).|| < (n * (max d)) + 1
proof
let y be
set ;
( y in dom g implies ||.(g /. y).|| < (n * (max d)) + 1 )
assume A6:
y in dom g
;
||.(g /. y).|| < (n * (max d)) + 1
set s =
f /. y;
now for i being Element of NAT st 1 <= i & i <= n holds
|.((f /. y) . i).| <= max dlet i be
Element of
NAT ;
( 1 <= i & i <= n implies |.((f /. y) . i).| <= max d )set P =
proj (
i,
n);
assume A7:
( 1
<= i &
i <= n )
;
|.((f /. y) . i).| <= max dthen A8:
i in Seg n
;
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then
rng f c= dom (proj (i,n))
;
then A9:
y in dom ((proj (i,n)) * f)
by A6, A1, RELAT_1:27;
then A10:
|.(((proj (i,n)) * f) . y).| < d /. i
by A8, A5;
f . y = f /. y
by A6, A1, PARTFUN1:def 6;
then
((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y)
by A9, FUNCT_1:12;
then A11:
|.((f /. y) . i).| < d /. i
by A10, PDIFF_1:def 1;
len d = n
by A5, FINSEQ_1:def 3;
then
d . i <= max d
by A7, RFINSEQ2:1;
then
d /. i <= max d
by A8, A5, PARTFUN1:def 6;
hence
|.((f /. y) . i).| <= max d
by A11, XXREAL_0:2;
verum end;
then A12:
|.(f /. y).| < (n * (max d)) + 1
by PDIFF_8:15, XREAL_1:145;
g /. y =
g . y
by A6, PARTFUN1:def 6
.=
f /. y
by A1, A6, PARTFUN1:def 6
;
hence
||.(g /. y).|| < (n * (max d)) + 1
by A12, REAL_NS1:1;
verum
end;
hence
g is
bounded
;
verum
end;
assume A13:
g is bounded
; f is bounded
consider r being Real such that
A14:
for y being set st y in dom g holds
||.(g /. y).|| < r
by A13;
let i be Element of NAT ; INTEGR15:def 15 ( not i in Seg n or (proj (i,n)) * f is bounded )
set P = proj (i,n);
assume A15:
i in Seg n
; (proj (i,n)) * f is bounded
for y being set st y in dom ((proj (i,n)) * f) holds
|.(((proj (i,n)) * f) . y).| < r
proof
let y be
set ;
( y in dom ((proj (i,n)) * f) implies |.(((proj (i,n)) * f) . y).| < r )
assume A16:
y in dom ((proj (i,n)) * f)
;
|.(((proj (i,n)) * f) . y).| < r
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then
rng f c= dom (proj (i,n))
;
then A17:
y in dom f
by A16, RELAT_1:27;
then A18:
||.(g /. y).|| < r
by A14, A1;
set s =
f /. y;
g /. y =
g . y
by A17, A1, PARTFUN1:def 6
.=
f /. y
by A1, A17, PARTFUN1:def 6
;
then A19:
|.(f /. y).| < r
by A18, REAL_NS1:1;
|.((f /. y) . i).| <= |.(f /. y).|
by A15, REAL_NS1:8;
then A20:
|.((f /. y) . i).| < r
by A19, XXREAL_0:2;
f . y = f /. y
by A17, PARTFUN1:def 6;
then
((proj (i,n)) * f) . y = (proj (i,n)) . (f /. y)
by A16, FUNCT_1:12;
hence
|.(((proj (i,n)) * f) . y).| < r
by A20, PDIFF_1:def 1;
verum
end;
hence
(proj (i,n)) * f is bounded
by COMSEQ_2:def 3; verum