let X be RealNormSpace-Sequence; for x being Point of (product X)
for r being Real st 0 < r holds
ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st
( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )
let x be Point of (product X); for r being Real st 0 < r holds
ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st
( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )
let r be Real; ( 0 < r implies ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st
( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) ) )
assume A1:
0 < r
; ex s being FinSequence of REAL ex Y being non-empty non empty FinSequence st
( dom s = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < s . i & s . i < r & Y . i = Ball ((x . i),(s . i)) ) ) )
A2:
product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #)
by PRVECT_2:6;
consider s0 being Real such that
A3:
( 0 < s0 & s0 < r )
and
A4:
sqrt ((s0 * s0) * (len X)) < r
by A1, NDIFF825;
set CST = (len X) |-> s0;
( len X is natural Number & s0 is Element of REAL )
by XREAL_0:def 1;
then reconsider CST = (len X) |-> s0 as Element of (len X) -tuples_on REAL by FINSEQ_2:112;
A5:
for i being Element of dom X holds
( 0 < CST . i & CST . i < r )
defpred S1[ object , object ] means ex i being Element of dom X st
( $1 = i & $2 = Ball ((x . i),(CST . i)) );
A6:
for n being Nat st n in Seg (len X) holds
ex d being object st S1[n,d]
consider Y being FinSequence such that
A7:
( dom Y = Seg (len X) & ( for n being Nat st n in Seg (len X) holds
S1[n,Y . n] ) )
from FINSEQ_1:sch 1(A6);
not {} in rng Y
then reconsider Y = Y as non-empty non empty FinSequence by A7, FINSEQ_1:def 3, RELAT_1:def 9;
take
CST
; ex Y being non-empty non empty FinSequence st
( dom CST = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )
take
Y
; ( dom CST = dom X & dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )
thus dom CST =
Seg (len X)
by FUNCT_2:def 1
.=
dom X
by FINSEQ_1:def 3
; ( dom Y = dom X & product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )
thus A12:
dom Y = dom X
by A7, FINSEQ_1:def 3; ( product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )
A14:
for i being Element of dom X holds Y . i = Ball ((x . i),(CST . i))
for z being object st z in product Y holds
z in Ball (x,r)
proof
let z be
object ;
( z in product Y implies z in Ball (x,r) )
assume
z in product Y
;
z in Ball (x,r)
then consider g being
Function such that A15:
(
z = g &
dom g = dom Y & ( for
i being
object st
i in dom Y holds
g . i in Y . i ) )
by CARD_3:def 5;
A16:
dom (carr X) = dom X
by DCARXX;
A17:
dom g = dom (carr X)
by A12, A15, DCARXX;
A18:
for
i0 being
object st
i0 in dom (carr X) holds
(
g . i0 in (carr X) . i0 & ex
i being
Element of
dom X st
(
i0 = i &
g . i in Ball (
(x . i),
(CST . i)) &
g . i in the
carrier of
(X . i) ) )
then A20:
for
i0 being
object st
i0 in dom (carr X) holds
g . i0 in (carr X) . i0
;
then reconsider x1 =
g as
Point of
(product X) by A2, A17, CARD_3:def 5;
reconsider y1 =
g as
Element of
product (carr X) by A20, A17, CARD_3:def 5;
reconsider xx1 =
x - x1 as
Element of
product (carr X) by A2;
A21:
||.(x - x1).|| = |.(normsequence (X,xx1)).|
by A2, PRVECT_2:def 12;
A22:
len (normsequence (X,xx1)) = len X
by PRVECT_2:def 11;
then A23:
dom (normsequence (X,xx1)) =
Seg (len X)
by FINSEQ_1:def 3
.=
dom X
by FINSEQ_1:def 3
;
now for i0 being Nat st i0 in dom (normsequence (X,xx1)) holds
( 0 <= (normsequence (X,xx1)) . i0 & (normsequence (X,xx1)) . i0 <= s0 )let i0 be
Nat;
( i0 in dom (normsequence (X,xx1)) implies ( 0 <= (normsequence (X,xx1)) . i0 & (normsequence (X,xx1)) . i0 <= s0 ) )assume
i0 in dom (normsequence (X,xx1))
;
( 0 <= (normsequence (X,xx1)) . i0 & (normsequence (X,xx1)) . i0 <= s0 )then reconsider i =
i0 as
Element of
dom X by A23;
reconsider xx1i =
xx1 . i as
Point of
(X . i) ;
reconsider yi =
x . i as
Point of
(X . i) ;
reconsider y1i =
y1 . i as
Point of
(X . i) ;
i in dom X
;
then A24:
i in Seg (len X)
by FINSEQ_1:def 3;
A25:
(normsequence (X,xx1)) . i = ||.xx1i.||
by PRVECT_2:def 11;
hence
0 <= (normsequence (X,xx1)) . i0
;
(normsequence (X,xx1)) . i0 <= s0A26:
xx1 . i = (x . i) - (y1 . i)
by LOPBAN10:26;
ex
j being
Element of
dom X st
(
i = j &
g . j in Ball (
(x . j),
(CST . j)) &
g . j in the
carrier of
(X . j) )
by A16, A18;
then
ex
y being
Point of
(X . i) st
(
y = y1i &
||.((x . i) - y).|| < CST . i )
;
hence
(normsequence (X,xx1)) . i0 <= s0
by A24, A25, A26, FINSEQ_2:57;
verum end;
then
|.(normsequence (X,xx1)).| <= sqrt ((s0 * s0) * (len X))
by A22, NDIFF823;
then
||.(x - x1).|| < r
by A4, A21, XXREAL_0:2;
hence
z in Ball (
x,
r)
by A15;
verum
end;
hence
( product Y c= Ball (x,r) & ( for i being Element of dom X holds
( 0 < CST . i & CST . i < r & Y . i = Ball ((x . i),(CST . i)) ) ) )
by A5, A14, TARSKI:def 3; verum