let X be strict RealNormSpace; :: thesis: ( DualSp X is separable implies X is separable )
set Y = DualSp X;
assume DualSp X is separable ; :: thesis: 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]
proof
let n be Element of NAT ; :: thesis: ex x being Point of X st S1[n,x]
per cases ( ||.(Yseq . n).|| = 0 or ||.(Yseq . n).|| <> 0 ) ;
suppose A1: ||.(Yseq . n).|| = 0 ; :: thesis: ex x being Point of X st S1[n,x]
set x = 0. X;
take 0. X ; :: thesis: S1[n, 0. X]
thus ||.(Yseq . n).|| / 2 <= |.((Yseq . n) . (0. X)).| by A1, COMPLEX1:46; :: thesis: ||.(0. X).|| <= 1
thus ||.(0. X).|| <= 1 ; :: thesis: verum
end;
suppose A21: ||.(Yseq . n).|| <> 0 ; :: thesis: ex x being Point of X st S1[n,x]
assume A31: for x being Point of X holds
( not ||.(Yseq . n).|| / 2 <= |.((Yseq . n) . x).| or not ||.x.|| <= 1 ) ; :: thesis: contradiction
reconsider f = Yseq . n as Lipschitzian linear-Functional of X by DUALSP01:def 10;
now :: thesis: for r being Real st r in PreNorms f holds
r <= ||.(Yseq . n).|| / 2
let r be Real; :: thesis: ( r in PreNorms f implies r <= ||.(Yseq . n).|| / 2 )
assume r in PreNorms f ; :: thesis: r <= ||.(Yseq . n).|| / 2
then ex x being Point of X st
( r = |.(f . x).| & ||.x.|| <= 1 ) ;
hence r <= ||.(Yseq . n).|| / 2 by A31; :: thesis: verum
end;
then upper_bound (PreNorms f) <= ||.(Yseq . n).|| / 2 by SEQ_4:45;
then ||.(Yseq . n).|| <= ||.(Yseq . n).|| / 2 by DUALSP01:24;
hence contradiction by XREAL_1:216, A21; :: thesis: verum
end;
end;
end;
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 )
proof
let n be Nat; :: thesis: ( ||.(Yseq . n).|| / 2 <= |.((Yseq . n) . (Xseq . n)).| & ||.(Xseq . n).|| <= 1 )
n is Element of NAT by ORDINAL1:def 12;
hence ( ||.(Yseq . n).|| / 2 <= |.((Yseq . n) . (Xseq . n)).| & ||.(Xseq . n).|| <= 1 ) by D4; :: thesis: verum
end;
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); :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: ((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; :: thesis: verum
end;
then B5: lim ((1 / 2) (#) ||.seq.||) <= 0 by B1, B2, SEQ_2:18;
reconsider rseq = ||.seq.|| as Real_Sequence ;
B6: now :: thesis: for n being Nat holds 0 <= ((1 / 2) (#) rseq) . n
let n be Nat; :: thesis: 0 <= ((1 / 2) (#) rseq) . n
0 <= (1 / 2) * ||.(seq . n).|| ;
then 0 <= (1 / 2) * (rseq . n) by NORMSP_0:def 4;
hence 0 <= ((1 / 2) (#) rseq) . n by SEQ_1:9; :: thesis: verum
end;
(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; :: thesis: verum
end;
then ClNLin (rng Xseq) = X by Lm73;
hence X is separable ; :: thesis: verum