let X be strict RealNormSpace; ( DualSp X is separable implies X is separable )
set Y = DualSp X;
assume
DualSp X is separable
; X is separable
then consider Yseq being sequence of (DualSp X) such that
P1:
rng Yseq is dense
by NORMSP_3:21;
defpred S1[ Nat, Point of X] means ( ||.(Yseq . $1).|| / 2 <= |.((Yseq . $1) . $2).| & ||.$2.|| <= 1 );
F2:
for n being Element of NAT ex x being Point of X st S1[n,x]
consider Xseq being Function of NAT, the carrier of X such that
D4:
for n being Element of NAT holds S1[n,Xseq . n]
from FUNCT_2:sch 3(F2);
for n being Nat holds
( ||.(Yseq . n).|| / 2 <= |.((Yseq . n) . (Xseq . n)).| & ||.(Xseq . n).|| <= 1 )
then consider Xseq being sequence of X such that
P2:
for n being Nat holds
( ||.(Yseq . n).|| / 2 <= |.((Yseq . n) . (Xseq . n)).| & ||.(Xseq . n).|| <= 1 )
;
set X1 = rng Xseq;
set M = ClNLin (rng Xseq);
set Y1 = rng Yseq;
for f being Point of (DualSp X) st ( for x being Point of X st x in rng Xseq holds
(Bound2Lipschitz (f,X)) . x = 0 ) holds
Bound2Lipschitz (f,X) = 0. (DualSp X)
proof
let f be
Point of
(DualSp X);
( ( for x being Point of X st x in rng Xseq holds
(Bound2Lipschitz (f,X)) . x = 0 ) implies Bound2Lipschitz (f,X) = 0. (DualSp X) )
assume AS:
for
x being
Point of
X st
x in rng Xseq holds
(Bound2Lipschitz (f,X)) . x = 0
;
Bound2Lipschitz (f,X) = 0. (DualSp X)
reconsider f1 =
f as
Lipschitzian linear-Functional of
X by DUALSP01:def 10;
A1:
f1 = Bound2Lipschitz (
f,
X)
by DUALSP01:23;
consider seq being
sequence of
(DualSp X) such that B0:
(
rng seq c= rng Yseq &
seq is
convergent &
lim seq = f )
by P1, NORMSP_3:14;
B1:
(
||.(seq - f).|| is
convergent &
lim ||.(seq - f).|| = 0 )
by B0, NORMSP_1:24;
B2:
||.seq.|| is
convergent
by B0, LOPBAN_1:20;
for
n being
Nat holds
((1 / 2) (#) ||.seq.||) . n <= ||.(seq - f).|| . n
proof
let n be
Nat;
((1 / 2) (#) ||.seq.||) . n <= ||.(seq - f).|| . n
seq . n in rng seq
by FUNCT_2:4, ORDINAL1:def 12;
then consider m being
object such that E1:
(
m in NAT &
Yseq . m = seq . n )
by FUNCT_2:11, B0;
reconsider m =
m as
Nat by E1;
reconsider x1 =
Xseq . m as
Point of
X ;
C1:
f1 . x1 = 0
by A1, AS, E1, FUNCT_2:4;
C2:
|.(((seq . n) . x1) - (f . x1)).| = |.(((seq . n) - f) . x1).|
by DUALSP01:33;
reconsider g =
(seq . n) - f as
Lipschitzian linear-Functional of
X by DUALSP01:def 10;
C3:
|.(g . x1).| <= ||.((seq . n) - f).|| * ||.x1.||
by DUALSP01:26;
||.((seq . n) - f).|| * ||.x1.|| <= ||.((seq . n) - f).|| * 1
by P2, XREAL_1:64;
then C4:
|.(((seq . n) . x1) - (f . x1)).| <= ||.((seq . n) - f).||
by C2, C3, XXREAL_0:2;
||.(seq . n).|| / 2
<= |.((seq . n) . x1).|
by P2, E1;
then C71:
(1 / 2) * ||.(seq . n).|| <= ||.((seq . n) - f).||
by C4, XXREAL_0:2, C1;
C8:
||.((seq . n) - f).|| =
||.((seq - f) . n).||
by NORMSP_1:def 4
.=
||.(seq - f).|| . n
by NORMSP_0:def 4
;
(1 / 2) * (||.seq.|| . n) = ((1 / 2) (#) ||.seq.||) . n
by SEQ_1:9;
hence
((1 / 2) (#) ||.seq.||) . n <= ||.(seq - f).|| . n
by C71, NORMSP_0:def 4, C8;
verum
end;
then B5:
lim ((1 / 2) (#) ||.seq.||) <= 0
by B1, B2, SEQ_2:18;
reconsider rseq =
||.seq.|| as
Real_Sequence ;
(1 / 2) * (lim rseq) = lim ((1 / 2) (#) rseq)
by B0, LOPBAN_1:20, SEQ_2:8;
then
lim ||.seq.|| = 0
by B5, B6, B2, SEQ_2:17;
then
||.f.|| = 0
by B0, LOPBAN_1:20;
then
f1 = 0. (DualSp X)
by DUALSP01:31;
hence
Bound2Lipschitz (
f,
X)
= 0. (DualSp X)
by DUALSP01:23;
verum
end;
then
ClNLin (rng Xseq) = X
by Lm73;
hence
X is separable
; verum