let E, F be RealNormSpace; for E1 being SubRealNormSpace of E
for f being Point of (R_NormSpace_of_BoundedLinearOperators (E1,F)) st F is complete & ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) holds
( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )
let E1 be SubRealNormSpace of E; for f being Point of (R_NormSpace_of_BoundedLinearOperators (E1,F)) st F is complete & ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) holds
( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )
let f be Point of (R_NormSpace_of_BoundedLinearOperators (E1,F)); ( F is complete & ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense ) implies ( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) ) )
assume that
A1:
F is complete
and
A2:
ex E0 being Subset of E st
( E0 = the carrier of E1 & E0 is dense )
; ( ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) ) & ( for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2 ) )
consider E0 being Subset of E such that
A3:
( E0 = the carrier of E1 & E0 is dense )
by A2;
reconsider L = f as Lipschitzian LinearOperator of E1,F by LOPBAN_1:def 9;
A4:
( dom L = the carrier of E1 & rng L c= the carrier of F )
by FUNCT_2:def 1;
then
L in PFuncs ( the carrier of E, the carrier of F)
by A3, PARTFUN1:def 3;
then reconsider Lf = L as PartFunc of E,F by PARTFUN1:46;
A5:
dom Lf = E0
by A3, FUNCT_2:def 1;
consider K being Real such that
A6:
( 0 <= K & ( for x being VECTOR of E1 holds ||.(L . x).|| <= K * ||.x.|| ) )
by LOPBAN_1:def 8;
set r = K + 1;
A7:
K + 0 < K + 1
by XREAL_1:8;
for x1, x2 being Point of E st x1 in E0 & x2 in E0 holds
||.((Lf /. x1) - (Lf /. x2)).|| <= (K + 1) * ||.(x1 - x2).||
then
Lf is_Lipschitzian_on E0
by A3, A6, FUNCT_2:def 1;
then A15:
Lf is_uniformly_continuous_on E0
by NFCONT_2:9;
A16:
( ex Pg being Function of E,F st
( Pg | E0 = Lf & Pg is_uniformly_continuous_on the carrier of E & ( for x being Point of E ex seq being sequence of E st
( rng seq c= E0 & seq is convergent & lim seq = x & Lf /* seq is convergent & Pg . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & Pg . x = lim (Lf /* seq) ) ) ) & ( for Pg1, Pg2 being Function of E,F st Pg1 | E0 = Lf & Pg1 is_continuous_on the carrier of E & Pg2 | E0 = Lf & Pg2 is_continuous_on the carrier of E holds
Pg1 = Pg2 ) )
by A1, A3, A5, A15, Th020;
consider Pg being Function of E,F such that
A17:
Pg | E0 = Lf
and
A18:
Pg is_uniformly_continuous_on the carrier of E
and
A19:
for x being Point of E ex seq being sequence of E st
( rng seq c= E0 & seq is convergent & lim seq = x & Lf /* seq is convergent & Pg . x = lim (Lf /* seq) )
and
A20:
for x being Point of E
for seq being sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & Pg . x = lim (Lf /* seq) )
and
A21:
for x being Point of E ex seq being sequence of E st
( rng seq c= E0 & seq is convergent & lim seq = x & Lf /* seq is convergent & Pg . x = lim (Lf /* seq) )
and
A22:
for x being Point of E
for seq being sequence of E st rng seq c= E0 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & Pg . x = lim (Lf /* seq) )
by A16;
A23:
for x, y being Point of E holds Pg . (x + y) = (Pg . x) + (Pg . y)
proof
let x,
y be
Point of
E;
Pg . (x + y) = (Pg . x) + (Pg . y)
consider xseq being
sequence of
E such that A24:
(
rng xseq c= E0 &
xseq is
convergent &
lim xseq = x &
Lf /* xseq is
convergent &
Pg . x = lim (Lf /* xseq) )
by A19;
consider yseq being
sequence of
E such that A25:
(
rng yseq c= E0 &
yseq is
convergent &
lim yseq = y &
Lf /* yseq is
convergent &
Pg . y = lim (Lf /* yseq) )
by A19;
A29:
rng (xseq + yseq) c= E0
A30:
xseq + yseq is
convergent
by A24, A25, NORMSP_1:19;
A31:
lim (xseq + yseq) = x + y
by A24, A25, NORMSP_1:25;
A32:
rng (xseq + yseq) c= dom Lf
by A3, A29, FUNCT_2:def 1;
A33:
rng xseq c= dom Lf
by A3, A24, FUNCT_2:def 1;
A34:
rng yseq c= dom Lf
by A3, A25, FUNCT_2:def 1;
B34:
for
n being
Nat holds
(Lf /* (xseq + yseq)) . n = ((Lf /* xseq) . n) + ((Lf /* yseq) . n)
proof
let n be
Nat;
(Lf /* (xseq + yseq)) . n = ((Lf /* xseq) . n) + ((Lf /* yseq) . n)
A35:
n in NAT
by ORDINAL1:def 12;
(
xseq . n in rng xseq &
yseq . n in rng yseq )
by FUNCT_2:4, ORDINAL1:def 12;
then reconsider xn =
xseq . n,
yn =
yseq . n as
Point of
E1 by A3, A24, A25;
A37:
(xseq . n) + (yseq . n) = xn + yn
by NORMSP_3:28;
then
(xseq . n) + (yseq . n) in the
carrier of
E1
;
then A39:
(xseq . n) + (yseq . n) in dom L
by FUNCT_2:def 1;
thus (Lf /* (xseq + yseq)) . n =
Lf /. ((xseq + yseq) . n)
by A32, A35, FUNCT_2:109
.=
Lf /. ((xseq . n) + (yseq . n))
by NORMSP_1:def 2
.=
L . (xn + yn)
by A37, A39, PARTFUN1:def 6
.=
(L /. xn) + (L /. yn)
by VECTSP_1:def 20
.=
((Lf /* xseq) . n) + (Lf /. (yseq . n))
by A33, A35, FUNCT_2:109
.=
((Lf /* xseq) . n) + ((Lf /* yseq) . n)
by A34, A35, FUNCT_2:109
;
verum
end;
A41:
lim (Lf /* (xseq + yseq)) =
lim ((Lf /* xseq) + (Lf /* yseq))
by B34, NORMSP_1:def 2
.=
(lim (Lf /* xseq)) + (lim (Lf /* yseq))
by A24, A25, NORMSP_1:25
;
thus
Pg . (x + y) = (Pg . x) + (Pg . y)
by A20, A24, A25, A29, A30, A31, A41;
verum
end;
for x being Point of E
for a being Real holds Pg . (a * x) = a * (Pg . x)
proof
let x be
Point of
E;
for a being Real holds Pg . (a * x) = a * (Pg . x)let a be
Real;
Pg . (a * x) = a * (Pg . x)
consider xseq being
sequence of
E such that A42:
(
rng xseq c= E0 &
xseq is
convergent &
lim xseq = x &
Lf /* xseq is
convergent &
Pg . x = lim (Lf /* xseq) )
by A19;
A46:
rng (a * xseq) c= E0
A47:
a * xseq is
convergent
by A42, NORMSP_1:22;
A48:
lim (a * xseq) = a * x
by A42, NORMSP_1:28;
A49:
rng (a * xseq) c= dom Lf
by A3, A46, FUNCT_2:def 1;
A50:
rng xseq c= dom Lf
by A3, A42, FUNCT_2:def 1;
B50:
for
n being
Nat holds
(Lf /* (a * xseq)) . n = a * ((Lf /* xseq) . n)
lim (Lf /* (a * xseq)) =
lim (a * (Lf /* xseq))
by B50, NORMSP_1:def 5
.=
a * (lim (Lf /* xseq))
by A42, NORMSP_1:28
;
hence
Pg . (a * x) = a * (Pg . x)
by A20, A42, A46, A47, A48;
verum
end;
then reconsider Pg = Pg as LinearOperator of E,F by A23, LOPBAN_1:def 5, VECTSP_1:def 20;
reconsider Pg = Pg as Lipschitzian LinearOperator of E,F by A18, NFCONT_2:7, LOPBAN_7:6;
reconsider g = Pg as Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) by LOPBAN_1:def 9;
A58:
dom g = the carrier of E
by FUNCT_2:def 1;
A61: ||.f.|| =
upper_bound (PreNorms (modetrans (f,E1,F)))
by LOPBAN_1:def 13
.=
upper_bound (PreNorms L)
by LOPBAN_1:29
;
A63: ||.g.|| =
upper_bound (PreNorms (modetrans (g,E,F)))
by LOPBAN_1:def 13
.=
upper_bound (PreNorms Pg)
by LOPBAN_1:29
;
for t being Real st t in PreNorms L holds
t <= ||.g.||
then A69:
||.f.|| <= ||.g.||
by A61, SEQ_4:45;
for t being Real st t in PreNorms Pg holds
t <= ||.f.||
proof
let t be
Real;
( t in PreNorms Pg implies t <= ||.f.|| )
assume
t in PreNorms Pg
;
t <= ||.f.||
then consider x being
Point of
E such that A70:
(
t = ||.(Pg . x).|| &
||.x.|| <= 1 )
;
consider xseq being
sequence of
E such that A71:
(
rng xseq c= E0 &
xseq is
convergent &
lim xseq = x &
Lf /* xseq is
convergent &
Pg . x = lim (Lf /* xseq) )
by A19;
A72:
||.(Pg . x).|| = lim ||.(Lf /* xseq).||
by A71, LOPBAN_1:20;
A73:
(
||.xseq.|| is
convergent &
lim ||.xseq.|| = ||.(lim xseq).|| )
by A71, LOPBAN_1:20;
A74:
||.(Lf /* xseq).|| is
convergent
by A71, NORMSP_1:23;
A75:
||.f.|| (#) ||.xseq.|| is
convergent
by A71, LOPBAN_1:20, SEQ_2:7;
for
n being
Nat holds
||.(Lf /* xseq).|| . n <= (||.f.|| (#) ||.xseq.||) . n
then
lim ||.(Lf /* xseq).|| <= lim (||.f.|| (#) ||.xseq.||)
by A74, A75, SEQ_2:18;
then A82:
lim ||.(Lf /* xseq).|| <= ||.f.|| * ||.x.||
by A71, A73, SEQ_2:8;
||.f.|| * ||.x.|| <= ||.f.|| * 1
by A70, XREAL_1:64;
hence
t <= ||.f.||
by A70, A72, A82, XXREAL_0:2;
verum
end;
then
||.g.|| <= ||.f.||
by A63, SEQ_4:45;
hence
ex g being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st
( dom g = the carrier of E & g | the carrier of E1 = f & ||.g.|| = ||.f.|| & ex Lf being PartFunc of E,F st
( Lf = f & ( for x being Point of E ex seq being sequence of E st
( rng seq c= the carrier of E1 & seq is convergent & lim seq = x & Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) & ( for x being Point of E
for seq being sequence of E st rng seq c= the carrier of E1 & seq is convergent & lim seq = x holds
( Lf /* seq is convergent & g . x = lim (Lf /* seq) ) ) ) )
by A3, A17, A21, A22, A58, A69, XXREAL_0:1; for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2
thus
for g1, g2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F)) st g1 | the carrier of E1 = f & g2 | the carrier of E1 = f holds
g1 = g2
verumproof
let g1,
g2 be
Point of
(R_NormSpace_of_BoundedLinearOperators (E,F));
( g1 | the carrier of E1 = f & g2 | the carrier of E1 = f implies g1 = g2 )
assume A84:
(
g1 | the
carrier of
E1 = f &
g2 | the
carrier of
E1 = f )
;
g1 = g2
reconsider Pg1 =
g1,
Pg2 =
g2 as
Lipschitzian LinearOperator of
E,
F by LOPBAN_1:def 9;
A85:
Pg1 is_continuous_on the
carrier of
E
by LMCONT1, NFCONT_2:7;
Pg2 is_continuous_on the
carrier of
E
by LMCONT1, NFCONT_2:7;
hence
g1 = g2
by A1, A3, A5, A15, A84, A85, Th020;
verum
end;