:: Separability of Real Normed Spaces and Its Basic Properties
:: by Kazuhisa Nakasho and Noboru Endou
::
:: Received February 26, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RLSUB_1, HAHNBAN, UNIALG_1, DUALSP01, INT_1, MOD_4, CARD_3,
FINSET_1, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, REAL_1, TARSKI,
MSSUBFAM, STRUCT_0, REALSET1, FCONT_1, SEQ_2, LOPBAN_1, ORDINAL2,
ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, METRIC_1, PRE_TOPC, SUBSET_1,
ZFMISC_1, ORDINAL1, NUMBERS, XBOOLE_0, CARD_1, SUPINF_2, COMPLEX1,
XXREAL_0, NAT_1, RCOMP_1, NORMSP_2, RLVECT_3, NORMSP_3, RLVECT_2, TOPS_1,
TOPGEN_1, RAT_1, DUALSP02, NORMSP_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, REALSET1, FINSET_1, CARD_1, CARD_3,
NUMBERS, XCMPLX_0, XXREAL_0, RAT_1, XREAL_0, INT_1, COMPLEX1, STRUCT_0,
ALGSTR_0, METRIC_1, TOPMETR, PRE_TOPC, TOPS_1, RLVECT_1, RLSUB_1,
RLVECT_2, RLVECT_3, NORMSP_0, NORMSP_1, HAHNBAN, RSSPACE, LOPBAN_1,
NFCONT_1, TOPGEN_1, NORMSP_2, DUALSP01, NORMSP_3, DUALSP02, IDEAL_1;
constructors REAL_1, REALSET1, RSSPACE3, NFCONT_1, HAHNBAN1, NORMSP_2,
PCOMPS_1, RLVECT_2, RLVECT_3, NORMSP_3, TOPS_1, TOPGEN_1, DUALSP02,
TOPMETR, IDEAL_1;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, XXREAL_0,
VALUED_0, RLVECT_1, RLVECT_2, FUNCT_2, RELSET_1, NORMSP_3, DUALSP02,
FINSET_1, XCMPLX_0, NORMSP_0, NAT_1, NORMSP_1, DUALSP01, XBOOLE_0,
SUBSET_1, NORMSP_2, CARD_1, CARD_3, LOPBAN_1, TOPGEN_4, RAT_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions HAHNBAN;
equalities BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_2, ORDINAL1, NORMSP_3,
PCOMPS_1, NORMSP_2;
expansions FUNCT_1, TARSKI, XBOOLE_0, FUNCT_2, STRUCT_0, NORMSP_3, INT_1,
PRE_TOPC, CARD_3, DUALSP01;
theorems FUNCT_1, ABSVALUE, COMPLEX1, TARSKI, XREAL_0, XXREAL_0, NORMSP_1,
FUNCT_2, XBOOLE_0, XREAL_1, RLVECT_1, HAHNBAN, RLSUB_1, RSSPACE,
NORMSP_0, ORDINAL1, NAT_1, NDIFF_1, NORMSP_3, ZFMISC_1, XBOOLE_1,
TOPGEN_1, DUALSP01, RELAT_1, XCMPLX_1, NORMSP_2, NUMBERS, RLVECT_3,
DUALSP02, PRE_TOPC, CARD_1, CARD_2, CARD_3, CARD_4, RLVECT_2, TOPMETR,
RAT_1, CARD_5, BORSUK_5, IDEAL_1;
schemes FUNCT_2, NAT_1;
begin :: 1. Separability of Real Normed Spaces
definition
let X be RealLinearSpace, A be Subset of X;
func RAT_Sums(A) -> Subset of X equals
{Sum l where l is Linear_Combination of A : rng l c= RAT};
correctness
proof
set S = {Sum l where l is Linear_Combination of A : rng l c= RAT};
now
let x be object;
assume x in S; then
ex l being Linear_Combination of A st x = Sum l & rng l c= RAT;
hence x in [#]X;
end; then
S c= [#]X;
hence thesis;
end;
end;
theorem Th1:
for V be RealNormSpace,V1 be SubRealNormSpace of V
holds TopSpaceNorm V1 is SubSpace of TopSpaceNorm V
proof
let V be RealNormSpace,V1 be SubRealNormSpace of V;
A1: the carrier of (MetricSpaceNorm V1)
c= the carrier of (MetricSpaceNorm V) by DUALSP01:def 16;
for x, y being Point of (MetricSpaceNorm V1) holds
(the distance of (MetricSpaceNorm V1)) . (x,y)
= (the distance of (MetricSpaceNorm V)) . (x,y)
proof
let x,y being Point of (MetricSpaceNorm V1);
reconsider x1=x,y1=y as Point of V1;
reconsider x2=x,y2=y as Point of V by A1;
-y1 = (-1) * y1 by RLVECT_1:16
.= (-1) * y2 by NORMSP_3:28
.= -y2 by RLVECT_1:16; then
A2: x1-y1 = x2-y2 by NORMSP_3:28;
thus (the distance of (MetricSpaceNorm V1)) . (x,y)
= ||.x1-y1.|| by NORMSP_2:def 1
.= ||.x2-y2.|| by A2,NORMSP_3:28
.= (the distance of (MetricSpaceNorm V)) . (x,y) by NORMSP_2:def 1;
end; then
MetricSpaceNorm V1 is SubSpace of (MetricSpaceNorm V) by A1,TOPMETR:def 1;
hence TopSpaceNorm V1 is SubSpace of TopSpaceNorm V by TOPMETR:13;
end;
theorem Th2:
for V be RealNormSpace, V1 be SubRealNormSpace of V
holds LinearTopSpaceNorm V1 is SubSpace of LinearTopSpaceNorm V
proof
let V be RealNormSpace, V1 be SubRealNormSpace of V;
the carrier of (LinearTopSpaceNorm V1) = the carrier of V1
& the carrier of (LinearTopSpaceNorm V) = the carrier of V
by NORMSP_2:def 4; then
the TopStruct of (LinearTopSpaceNorm V1)
= the TopStruct of (TopSpaceNorm V1)
& the TopStruct of (LinearTopSpaceNorm V)
= the TopStruct of (TopSpaceNorm V) by NORMSP_2:def 4;
hence thesis by Th1,PRE_TOPC:10;
end;
theorem Th3:
for X be RealNormSpace, Y,Z be SubRealNormSpace of X
st ex A be Subset of X
st A = the carrier of Y & Cl(A) = the carrier of Z
holds
for D0 be Subset of Y, D be Subset of Z st D0 is dense & D0 = D
holds D is dense
proof
let X be RealNormSpace, Y,Z be SubRealNormSpace of X;
given A be Subset of X such that
A1: A = the carrier of Y & Cl(A) = the carrier of Z;
let D0 be Subset of Y, D be Subset of Z;
assume
A2: D0 is dense & D0 = D;
A3: the carrier of (LinearTopSpaceNorm Z) = the carrier of Z
& the carrier of (LinearTopSpaceNorm Y) = the carrier of Y
& the carrier of (LinearTopSpaceNorm X) = the carrier of X
by NORMSP_2:def 4;
A4: LinearTopSpaceNorm Z is SubSpace of LinearTopSpaceNorm X
& LinearTopSpaceNorm Y is SubSpace of LinearTopSpaceNorm X by Th2;
for S be Subset of Z st S <> {} & S is open holds D meets S
proof
let S be Subset of Z;
assume
A5: S <> {} & S is open;
reconsider SZL = S as Subset of LinearTopSpaceNorm Z by NORMSP_2:def 4;
reconsider SZT = SZL as Subset of TopSpaceNorm Z;
SZT is open by A5,NORMSP_2:16; then
SZL is open by NORMSP_2:20; then
consider SXL be Subset of LinearTopSpaceNorm X such that
A6: SXL in the topology of LinearTopSpaceNorm X
& SZL = SXL /\ [#](LinearTopSpaceNorm Z) by A4,PRE_TOPC:def 4;
reconsider SYL = SXL /\ [#](LinearTopSpaceNorm Y)
as Subset of (LinearTopSpaceNorm Y);
reconsider SX = SXL as Subset of X by NORMSP_2:def 4;
reconsider SXT = SXL as Subset of TopSpaceNorm X by NORMSP_2:def 4;
reconsider SY = SYL as Subset of Y by NORMSP_2:def 4;
reconsider SYT = SYL as Subset of TopSpaceNorm Y by NORMSP_2:def 4;
SXL is open by A6; then
SXT is open by NORMSP_2:20; then
A7: SX is open by NORMSP_2:16;
SX /\ Cl(A) <> {} by A1,A5,A6,NORMSP_2:def 4; then
consider v be object such that
A8: v in SX /\ Cl(A) by XBOOLE_0:def 1;
v in SX & v in Cl(A) by A8,XBOOLE_0:def 4; then
SX meets A by A7,NORMSP_3:5; then
A9: SYL <> {} by A1,NORMSP_2:def 4;
SYL is open by A4,A6,PRE_TOPC:def 4; then
SYT is open by NORMSP_2:20; then
SY is open by NORMSP_2:16; then
A10: D0 meets SY by A2,A9,NORMSP_3:17;
SYL c= SZL by A1,A3,A6,NORMSP_3:4,XBOOLE_1:26; then
D /\ SYL c= D /\ SZL by XBOOLE_1:26;
hence thesis by A2,A10;
end;
hence thesis by NORMSP_3:17;
end;
theorem Th4:
for X be addLoopStr, A,B be Subset of X holds
ex F be Function of A+B,[:A,B:] st F is one-to-one
proof
let X be addLoopStr, A,B be Subset of X;
set D = A+B;
defpred P[object,object] means
ex a,b be Point of X st $1 = a+b & a in A & b in B & $2 = [a,b];
A2: for x being object st x in D
ex y being object st y in [:A,B:] & P[x,y]
proof
let x be object;
assume x in D; then
x in {a+b where a,b is Element of X : a in A & b in B}
by IDEAL_1:def 19; then
consider a,b be Element of X such that
A3: x = a+b & a in A & b in B;
take y = [a,b];
thus y in [:A,B:] by A3,ZFMISC_1:87;
thus P[x,y] by A3;
end;
consider F be Function of D,[:A,B:] such that
A4: for x be object st x in D holds P[x,F.x] from FUNCT_2:sch 1(A2);
take F;
for x1,x2 be object st x1 in dom F & x2 in dom F & F.x1 = F.x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A5: x1 in dom F & x2 in dom F & F.x1 = F.x2; then
A6: ex a1,b1 be Point of X
st x1 = a1+b1 & a1 in A & b1 in B & F.x1 = [a1,b1] by A4;
ex a2,b2 be Point of X
st x2 = a2+b2 & a2 in A & b2 in B & F.x2 = [a2,b2] by A4,A5;
hence x1 = x2 by A5,A6;
end;
hence F is one-to-one;
end;
theorem Th5:
for X be addLoopStr, A,B be Subset of X
st A is countable & B is countable
holds A+B is countable
proof
let X be addLoopStr, A,B be Subset of X;
assume
A1: A is countable & B is countable;
set D = A+B;
per cases;
suppose
A2: not (A is non empty & B is non empty);
now
assume D <> {}; then
consider x be object such that
A3: x in D by XBOOLE_0:def 1;
D = {a+b where a,b is Point of X : a in A & b in B} by IDEAL_1:def 19;
then ex a,b be Point of X st x = a+b & a in A & b in B by A3;
hence contradiction by A2;
end;
hence thesis;
end;
suppose
A4: A is non empty & B is non empty;
consider F be Function of D,[:A,B:] such that
A5: F is one-to-one by Th4;
dom F = D & rng F c= [:A,B:] by A4,FUNCT_2:def 1; then
A6: card D c= card [:A,B:] by A5,CARD_1:10;
[:A,B:] is countable by A1,CARD_4:7; then
card [:A,B:] c= omega; then
card D c= omega by A6;
hence thesis;
end;
end;
Lm6:
for X be RealLinearSpace, v be Element of the carrier of X
holds RAT_Sums({v}) is countable
proof
let X be RealLinearSpace, v be Element of the carrier of X;
set D = RAT_Sums({v});
defpred P[object,object] means
ex l be Linear_Combination of {v} st $1 = Sum l & rng l c= RAT & $2 = l.v;
A2: for x being object st x in D
ex y being object st y in RAT & P[x,y]
proof
let x be object;
assume x in D; then
consider l being Linear_Combination of {v} such that
A3: x = Sum l & rng l c= RAT;
take y = l.v;
dom l = the carrier of X by FUNCT_2:def 1;
hence y in RAT by A3,FUNCT_1:3;
thus P[x,y] by A3;
end;
consider F being Function of D,RAT such that
A4: for x being object st x in D holds P[x,F.x] from FUNCT_2:sch 1(A2);
now
let x1,x2 be object;
assume
A5: x1 in dom F & x2 in dom F & F.x1 = F.x2; then
consider l1 being Linear_Combination of {v} such that
A6: x1 = Sum l1 & rng l1 c= RAT & F.x1 = l1.v by A4;
consider l2 being Linear_Combination of {v} such that
A7: x2 = Sum l2 & rng l2 c= RAT & F.x2 = l2.v by A4,A5;
x1 = l1.v * v & x2 = l2.v * v by A6,A7,RLVECT_2:32;
hence x1 = x2 by A5,A6,A7;
end; then
A8: F is one-to-one;
A9: dom F = D by FUNCT_2:def 1;
rng F is countable; then
A10: card D c= card RAT by A8,A9,CARD_1:10;
card RAT c= omega by CARD_3:def 14; then
card D c= omega by A10;
hence D is countable;
end;
theorem Th7:
for X be non empty addLoopStr, A,B be Subset of X,
l1 be Linear_Combination of A, l2 be Linear_Combination of B
st A misses B holds
ex l be Linear_Combination of (A \/ B)
st Carrier l = Carrier l1 \/ Carrier l2 & l = l1 + l2
proof
let X be non empty addLoopStr, A,B be Subset of X,
l1 be Linear_Combination of A, l2 be Linear_Combination of B;
assume
A1: A misses B;
A2: Carrier l1 c= A & Carrier l2 c= B by RLVECT_2:def 6;
defpred P[object,object] means
($1 in Carrier l1 implies $2 = l1.$1)
& ($1 in Carrier l2 implies $2 = l2.$1)
& (not $1 in Carrier l1 & not $1 in Carrier l2 implies $2 = 0);
A4: now
let x be object;
assume x in the carrier of X;
thus ex y being object st y in REAL & P[x,y]
proof
per cases by A1,A2,XBOOLE_0:3;
suppose
A5: x in Carrier l1 & not x in Carrier l2;
take y = l1.x;
thus y in REAL & P[x,y] by A5,FUNCT_2:5;
end;
suppose
A6: not x in Carrier l1 & x in Carrier l2;
take y = l2.x;
thus y in REAL & P[x,y] by A6,FUNCT_2:5;
end;
suppose
A7: not x in Carrier l1 & not x in Carrier l2;
take y = 0;
thus y in REAL & P[x,y] by A7,XREAL_0:def 1;
end;
end;
end;
consider l being Function of the carrier of X,REAL such that
A8: for x being object st x in the carrier of X holds P[x,l.x]
from FUNCT_2:sch 1(A4);
reconsider l as Element of Funcs(the carrier of X,REAL) by FUNCT_2:8;
reconsider T = Carrier l1 \/ Carrier l2 as finite Subset of X;
for x be Element of X st not x in T holds l.x = 0
proof
let x be Element of X;
assume not x in T; then
not x in Carrier l1 & not x in Carrier l2 by XBOOLE_0:def 3;
hence l.x = 0 by A8;
end; then
reconsider l as Linear_Combination of X by RLVECT_2:def 3;
now
let x be object;
assume x in Carrier l; then
consider p be Element of X such that
A9: x = p & l.p <> 0;
x in Carrier l1 or x in Carrier l2 by A8,A9;
hence x in Carrier l1 \/ Carrier l2 by XBOOLE_0:def 3;
end; then
A10: Carrier l c= Carrier l1 \/ Carrier l2;
now
let x be object;
assume x in Carrier l1 \/ Carrier l2; then
per cases by XBOOLE_0:def 3;
suppose
A11: x in Carrier l1; then
consider p be Element of X such that
A12: x = p & l1.p <> 0;
l.x <> 0 by A8,A11,A12;
hence x in Carrier l by A12;
end;
suppose
A13: x in Carrier l2; then
consider p be Element of X such that
A14: x = p & l2.p <> 0;
l.x <> 0 by A8,A13,A14;
hence x in Carrier l by A14;
end;
end; then
A15: Carrier l1 \/ Carrier l2 c= Carrier l; then
A16: Carrier l = Carrier l1 \/ Carrier l2 by A10; then
reconsider l as Linear_Combination of (A \/ B)
by A2,RLVECT_2:def 6,XBOOLE_1:13;
take l;
thus Carrier l = Carrier l1 \/ Carrier l2 by A10,A15;
for v be Element of X holds l.v = l1.v + l2.v
proof
let v be Element of X;
per cases by A10,XBOOLE_0:def 3;
suppose
A17: v in Carrier l1; then
not v in Carrier l2 by A1,A2,XBOOLE_0:3; then
l.v = l1.v & l2.v = 0 by A8,A17;
hence l.v = l1.v + l2.v;
end;
suppose
A18: v in Carrier l2; then
not v in Carrier l1 by A1,A2,XBOOLE_0:3; then
l.v = l2.v & l1.v = 0 by A8,A18;
hence l.v = l1.v + l2.v;
end;
suppose
A19: not v in Carrier l; then
not v in Carrier l1 & not v in Carrier l2 by A16,XBOOLE_0:def 3; then
l1.v = 0 & l2.v = 0;
hence l.v = l1.v + l2.v by A19;
end;
end;
hence l = l1 + l2 by RLVECT_2:def 10;
end;
theorem Th8:
for X be non empty addLoopStr, A,B be Subset of X,
l be Linear_Combination of (A \/ B) holds
ex l1 be Linear_Combination of A st Carrier l1 = Carrier l \ B
& for x be Element of X st x in Carrier l1 holds l1.x = l.x
proof
let X be non empty addLoopStr, A,B be Subset of X,
l be Linear_Combination of (A \/ B);
reconsider T1 = Carrier l \ B as finite Subset of X;
defpred P1[object,object] means
($1 in T1 implies $2 = l.$1) & (not $1 in T1 implies $2 = 0);
A1: now let x be object;
assume x in the carrier of X;
thus ex y be object st y in REAL & P1[x,y]
proof
per cases;
suppose
A2: x in T1;
take y = l.x;
thus y in REAL & P1[x,y] by A2,FUNCT_2:5;
end;
suppose
A3: not x in T1;
take y = 0;
thus y in REAL & P1[x,y] by A3,XREAL_0:def 1;
end;
end;
end;
consider l1 be Function of the carrier of X,REAL such that
A4: for x being object st x in the carrier of X holds P1[x,l1.x]
from FUNCT_2:sch 1(A1);
reconsider l1 as Element of Funcs(the carrier of X,REAL) by FUNCT_2:8;
for x be Element of X st not x in T1 holds l1.x = 0 by A4; then
reconsider l1 as Linear_Combination of X by RLVECT_2:def 3;
now
let x be object;
assume x in Carrier l1; then
ex v be Element of X st x = v & l1.v <> 0;
hence x in T1 by A4;
end; then
A5: Carrier l1 c= T1;
now
let x be object;
assume
A6: x in T1; then
x in Carrier l by XBOOLE_0:def 5; then
l.x <> 0 by RLVECT_2:19; then
l1.x <> 0 by A4,A6;
hence x in Carrier l1 by A6;
end; then
A7: T1 c= Carrier l1; then
A8: T1 = Carrier l1 by A5;
T1 c= Carrier l & Carrier l c= A \/ B by RLVECT_2:def 6,XBOOLE_1:36; then
T1 c= A \/ B & T1 misses B by XBOOLE_1:79; then
reconsider l1 as Linear_Combination of A by A8,RLVECT_2:def 6,XBOOLE_1:73;
take l1;
thus Carrier l1 = Carrier l \ B by A5,A7;
thus for x be Element of X st x in Carrier l1 holds l1.x = l.x by A4,A5;
end;
theorem Th9:
for X be non empty addLoopStr, A,B be Subset of X,
l be Linear_Combination of (A \/ B)
st A misses B holds
ex l1 be Linear_Combination of A, l2 be Linear_Combination of B
st Carrier l = Carrier l1 \/ Carrier l2 & l = l1 + l2
& Carrier l1 = Carrier l \ B & Carrier l2 = Carrier l \ A
proof
let X be non empty addLoopStr, A,B be Subset of X,
l be Linear_Combination of (A \/ B);
assume
A2: A misses B;
consider l1 be Linear_Combination of A such that
A3: Carrier l1 = Carrier l \ B
& for x be Element of X st x in Carrier l1 holds l1.x = l.x by Th8;
consider l2 be Linear_Combination of B such that
A4: Carrier l2 = Carrier l \ A
& for x be Element of X st x in Carrier l2 holds l2.x = l.x by Th8;
take l1,l2;
A5: Carrier l1 \/ Carrier l2 = Carrier l \ (A /\ B) by A3,A4,XBOOLE_1:54;
hence Carrier l1 \/ Carrier l2 = Carrier l by A2;
A6: Carrier l1 c= A & Carrier l2 c= B by RLVECT_2:def 6;
now
let x be Element of X;
per cases by A2,A5,XBOOLE_0:def 3;
suppose
A7: x in Carrier l1; then
not x in Carrier l2 by A2,A6,XBOOLE_0:3; then
l1.x = l.x & l2.x = 0 by A3,A7;
hence l.x = l1.x + l2.x;
end;
suppose
A8: x in Carrier l2; then
not x in Carrier l1 by A2,A6,XBOOLE_0:3; then
l1.x = 0 & l2.x = l.x by A4,A8;
hence l.x = l1.x + l2.x;
end;
suppose
A9: not x in Carrier l; then
not x in Carrier l1 & not x in Carrier l2 by A2,A5,XBOOLE_0:def 3; then
l.x = 0 & l1.x = 0 & l2.x = 0 by A9;
hence l.x = l1.x + l2.x;
end;
end;
hence l = l1+l2 by RLVECT_2:def 10;
thus thesis by A3,A4;
end;
theorem Th10:
for X be RealLinearSpace, A,B be Subset of X,
l1 be Linear_Combination of A, l2 be Linear_Combination of B
st rng l1 c= RAT & rng l2 c= RAT & A misses B holds
ex l be Linear_Combination of (A \/ B)
st Carrier l = Carrier l1 \/ Carrier l2
& rng l c= RAT & Sum l = Sum l1 + Sum l2
proof
let X be RealLinearSpace, A,B be Subset of X,
l1 be Linear_Combination of A, l2 be Linear_Combination of B;
assume that
A1: rng l1 c= RAT & rng l2 c= RAT and
A2: A misses B;
consider l be Linear_Combination of (A \/ B) such that
A3: Carrier l = Carrier l1 \/ Carrier l2 & l = l1 + l2 by A2,Th7;
take l;
thus Carrier l = Carrier l1 \/ Carrier l2 by A3;
now
let y be object;
assume y in rng l; then
consider x be object such that
A4: x in dom l & y = l.x by FUNCT_1:def 3;
A5: x in the carrier of X by A4;
A6: l.x = l1.x + l2.x by A3,A4,RLVECT_2:def 10;
x in dom l1 & x in dom l2 by A5,FUNCT_2:def 1; then
l1.x in rng l1 & l2.x in rng l2 by FUNCT_1:3;
hence y in RAT by A1,A4,A6,RAT_1:def 2;
end;
hence rng l c= RAT;
thus Sum l = Sum l1 + Sum l2 by A3,RLVECT_3:1;
end;
theorem Th11:
for X be RealLinearSpace, A,B be Subset of X,
l be Linear_Combination of (A \/ B)
st rng l c= RAT & A misses B holds
ex l1 be Linear_Combination of A, l2 be Linear_Combination of B
st rng l1 c= RAT & rng l2 c= RAT & Sum l = Sum l1 + Sum l2
proof
let X be RealLinearSpace, A,B be Subset of X,
l be Linear_Combination of (A \/ B);
assume that
A1: rng l c= RAT and
A3: A misses B;
consider l1 be Linear_Combination of A, l2 be Linear_Combination of B
such that
A4: Carrier l = Carrier l1 \/ Carrier l2 & l = l1 + l2
& Carrier l1 = Carrier l \ B
& Carrier l2 = Carrier l \ A by A3,Th9;
take l1,l2;
A5: Carrier l1 c= A & Carrier l2 c= B by RLVECT_2:def 6;
now
let y be object;
assume y in rng l1; then
consider x be object such that
A6: x in dom l1 & y = l1.x by FUNCT_1:def 3;
x in the carrier of X by A6; then
x in dom l & x in dom l2 by FUNCT_2:def 1; then
A7: l.x in rng l & l2.x in rng l2 & l.x = l1.x + l2.x
by A4,FUNCT_1:3,RLVECT_2:def 10;
per cases;
suppose
x in Carrier l1; then
not x in Carrier l2 by A3,A5,XBOOLE_0:3; then
l2.x = 0 by A6;
hence y in RAT by A1,A6,A7;
end;
suppose
not x in Carrier l1; then
l1.x = 0 by A6;
hence y in RAT by A6,RAT_1:def 2;
end;
end;
hence rng l1 c= RAT;
now
let y be object;
assume y in rng l2; then
consider x be object such that
A8: x in dom l2 & y = l2.x by FUNCT_1:def 3;
x in the carrier of X by A8; then
x in dom l & x in dom l1 by FUNCT_2:def 1; then
A9: l.x in rng l & l1.x in rng l1 & l.x = l1.x + l2.x
by A4,FUNCT_1:3,RLVECT_2:def 10;
per cases;
suppose
x in Carrier l2; then
not x in Carrier l1 by A3,A5,XBOOLE_0:3; then
l1.x = 0 by A8;
hence y in RAT by A1,A8,A9;
end;
suppose
not x in Carrier l2; then
l2.x = 0 by A8;
hence y in RAT by A8,RAT_1:def 2;
end;
end;
hence rng l2 c= RAT;
thus thesis by A4,RLVECT_3:1;
end;
theorem Th12:
for X be RealLinearSpace, A,B be finite Subset of X st A misses B
holds RAT_Sums(A) + RAT_Sums(B) = RAT_Sums(A \/ B)
proof
let X be RealLinearSpace, A,B be finite Subset of X;
assume
A3: A misses B;
set D1 = RAT_Sums(A);
set D2 = RAT_Sums(B);
set S1 = RAT_Sums(A) + RAT_Sums(B);
set S2 = RAT_Sums(A \/ B);
A4: S1 = {a+b where a,b is Point of X : a in D1 & b in D2}
by IDEAL_1:def 19;
now
let p be object;
assume p in S1; then
consider a,b be Point of X such that
A5: p = a+b & a in D1 & b in D2 by A4;
consider l1 be Linear_Combination of A such that
A6: a = Sum l1 & rng l1 c= RAT by A5;
consider l2 be Linear_Combination of B such that
A7: b = Sum l2 & rng l2 c= RAT by A5;
ex l be Linear_Combination of (A \/ B)
st Carrier l = Carrier l1 \/ Carrier l2
& rng l c= RAT & Sum l = Sum l1 + Sum l2 by A3,A6,A7,Th10;
hence p in S2 by A5,A6,A7;
end; then
A8: S1 c= S2;
now
let p be object;
assume p in S2; then
consider l be Linear_Combination of (A \/ B) such that
A9: p = Sum l & rng l c= RAT;
consider l1 be Linear_Combination of A, l2 be Linear_Combination of B
such that
A10: rng l1 c= RAT & rng l2 c= RAT & Sum l = Sum l1 + Sum l2
by A3,A9,Th11;
Sum l1 in D1 & Sum l2 in D2 by A10;
hence p in S1 by A4,A9,A10;
end; then
S2 c= S1;
hence thesis by A8;
end;
Lm13:
for X be RealLinearSpace holds RAT_Sums({}X) is countable
proof
let X be RealLinearSpace;
set A = {}X;
set D = RAT_Sums(A);
now
let x be object;
hereby
assume x in D; then
consider l be Linear_Combination of A such that
A3: x = Sum l & rng l c= RAT;
Carrier l c= A by RLVECT_2:def 6; then
Carrier l = {};
hence x = 0.X by A3,RLVECT_2:34;
end;
assume
A4: x = 0.X;
A5: ZeroLC(X) is Linear_Combination of A by RLVECT_2:22;
A6: Sum ZeroLC(X) = 0.X by RLVECT_2:30;
now
let a be object;
assume a in rng ZeroLC(X); then
ex x be Element of X
st a = ZeroLC(X) .x by FUNCT_2:113; then
a = 0 by RLVECT_2:20;
hence a in RAT by RAT_1:def 2;
end; then
A7: rng ZeroLC(X) c= RAT;
thus x in D by A4,A5,A6,A7;
end; then
D = {0.X} by TARSKI:def 1;
hence D is countable;
end;
Th14:
for X be RealLinearSpace, A be finite Subset of X
holds RAT_Sums(A) is countable
proof
let X be RealLinearSpace, A be finite Subset of X;
set D = RAT_Sums(A);
defpred P[Nat] means
for B be finite Subset of X st card B <= $1
holds RAT_Sums(B) is countable;
A2: now
let B be finite Subset of X, E be set;
assume card B <= 0; then
B = {}X;
hence RAT_Sums(B) is countable by Lm13;
end; then
A4: P[0];
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A6: P[k];
hereby
let B be finite Subset of X;
assume
A7: card B <= k+1;
set E = RAT_Sums(B);
per cases;
suppose
card B = 0;
hence E is countable by A2;
end;
suppose
card B <> 0; then
B <> {}; then
consider v be object such that
A8: v in B by XBOOLE_0:def 1;
reconsider v as Element of X by A8;
A9: (B \ {v}) \/ {v} = B by A8,XBOOLE_1:45,ZFMISC_1:31;
v in {v} by TARSKI:def 1; then
not v in B \ {v} by XBOOLE_0:def 5; then
A10: card((B \ {v}) \/ {v}) = card(B \ {v}) + 1 by CARD_2:41;
set D1 = RAT_Sums(B \ {v});
set D2 = RAT_Sums({v});
A11: E = D1+D2 by A9,Th12,XBOOLE_1:79;
D1 is countable & D2 is countable by A6,A7,A9,A10,Lm6,XREAL_1:6;
hence E is countable by A11,Th5;
end;
end;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); then
P[card A];
hence D is countable;
end;
registration
let X be RealLinearSpace, A be finite Subset of X;
cluster RAT_Sums(A) -> countable;
coherence by Th14;
end;
theorem Th15:
for X be RealLinearSpace, x be sequence of X, A be finite Subset of X
st A c= rng x
holds ex n be Nat st A c= rng ( x | Segm n )
proof
let X be RealLinearSpace, x be sequence of X;
defpred P[Nat] means
for A be finite Subset of X st card A = $1 & A c= rng x
holds ex n be Nat st A c= rng (x | Segm n);
A1: P[0]
proof
let A be finite Subset of the carrier of X;
assume
A2: card A = 0 & A c= rng x;
set n = the Nat;
take n;
thus A c= rng (x | Segm n) by A2;
end;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
let A be finite Subset of the carrier of X;
assume
A5: card A = k+1 & A c= rng x; then
A <> {}; then
consider w be object such that
A6: w in A by XBOOLE_0:def 1;
reconsider w as Element of the carrier of X by A6;
A7: card(A \ {w}) = card(A) - card({w}) by A6,CARD_2:44,ZFMISC_1:31
.= k + 1 - 1 by A5,CARD_2:42;
reconsider A0 =A \ {w} as finite Subset of X;
A0 c= A by XBOOLE_1:36; then
A0 c= rng x by A5; then
consider n0 be Nat such that
A8: A0 c= rng ( x | Segm n0 ) by A4,A7;
consider n1 be object such that
A9: n1 in NAT & w = x.n1 by A5,A6,FUNCT_2:11;
reconsider n1 as Nat by A9;
set n = n0 + n1 + 1;
take n;
A10: A = A0 \/ {w} by A6,XBOOLE_1:45,ZFMISC_1:31;
n0 < n by NAT_1:11,13; then
x | Segm n0 c= x | Segm n by NAT_1:39,RELAT_1:75; then
rng ( x | Segm n0 ) c= rng ( x | Segm n ) by RELAT_1:11; then
A11: A0 c= rng ( x | Segm n ) by A8;
n1 < n by NAT_1:11,13; then
n1 in Segm n & dom x = NAT by FUNCT_2:def 1,NAT_1:44; then
{w} c= rng ( x | Segm n ) by A9,FUNCT_1:50,ZFMISC_1:31;
hence A c= rng ( x | Segm n ) by A10,A11,XBOOLE_1:8;
end;
A12: for k be Nat holds P[k] from NAT_1:sch 2(A1,A3);
let A be finite Subset of the carrier of X;
assume
A13: A c= rng x;
card A is Nat;
hence ex n be Nat st A c= rng ( x | Segm n ) by A12,A13;
end;
Th16:
for X be RealLinearSpace, x be sequence of X
holds RAT_Sums(rng x) is countable
proof
let X be RealLinearSpace, x be sequence of X;
set D = RAT_Sums(rng x);
defpred P[Nat,object] means
$2 = RAT_Sums(rng(x | Segm $1));
A2: for n be Element of NAT holds
ex X1 be Element of bool the carrier of X st P[n,X1];
consider E be Function of NAT,bool the carrier of X such that
A3: for n be Element of NAT holds P[n,E.n] from FUNCT_2:sch 3(A2);
for z be object st z in RAT_Sums(rng x) holds z in Union E
proof
let z be object;
assume z in RAT_Sums(rng x); then
consider l be Linear_Combination of rng x such that
A4: z = Sum l & rng l c= RAT;
consider nmax be Nat such that
A5: Carrier l c= rng (x | Segm nmax) by RLVECT_2:def 6,Th15;
reconsider nmax as Element of NAT by ORDINAL1:def 12;
A6: E.nmax = RAT_Sums(rng(x | Segm nmax)) by A3;
l is Linear_Combination of rng (x | nmax) by A5,RLVECT_2:def 6; then
A7: z in E.nmax by A4,A6;
dom E = NAT by FUNCT_2:def 1;
hence z in Union E by A7,CARD_5:2;
end; then
A8: RAT_Sums(rng x) c= Union E;
for n be set st n in dom E holds E.n is countable
proof
let n be set;
assume n in dom E; then
reconsider n1 = n as Element of NAT;
E.n = RAT_Sums( rng(x | Segm n1) ) by A3;
hence E.n is countable;
end; then
Union E is countable by CARD_4:11;
hence D is countable by A8;
end;
registration
let X be RealLinearSpace, x be sequence of X;
cluster RAT_Sums rng x -> countable;
coherence by Th16;
end;
theorem Th17:
for X be RealNormSpace, x be sequence of X
holds RAT_Sums(rng x) is Subset of the carrier of NLin(rng x)
proof
let X be RealNormSpace, x be sequence of X;
set D = RAT_Sums(rng x);
for z be object st z in D holds z in the carrier of NLin(rng x)
proof
let z be object;
assume z in D; then
consider l be Linear_Combination of rng x such that
A2: z = Sum l & rng l c= RAT;
z in Lin(rng x) by A2,RLVECT_3:14;
hence z in the carrier of NLin(rng x);
end;
hence thesis by TARSKI:def 3;
end;
theorem Th18:
for X be RealNormSpace, Y be Subset of X holds
the carrier of NLin(Y) c= the carrier of ClNLin(Y)
& ex Z be Subset of X
st Z = the carrier of NLin(Y) & Cl(Z) = the carrier of ClNLin(Y)
proof
let X be RealNormSpace, Y be Subset of X;
ex Z be Subset of X
st Z = the carrier of Lin(Y)
& ClNLin(Y) = NORMSTR(# Cl(Z), Zero_(Cl(Z),X), Add_(Cl(Z),X),
Mult_(Cl(Z),X), Norm_(Cl(Z),X) #) by NORMSP_3:def 20;
hence thesis by NORMSP_3:4;
end;
theorem Th19:
for X be RealNormSpace, x be sequence of X
holds RAT_Sums(rng x) is countable Subset of the carrier of ClNLin(rng x)
proof
let X be RealNormSpace, x be sequence of X;
set D = RAT_Sums(rng x);
A1: D is Subset of the carrier of NLin(rng x) by Th17;
the carrier of NLin(rng x) c= the carrier of ClNLin(rng x) by Th18;
hence thesis by A1,XBOOLE_1:1;
end;
theorem Th21:
for z,e be Real st 0 < e holds
ex q be Element of RAT st q <> 0 & |. z - q .| < e
proof
let z be Real,e be Real;
assume
A1: 0 < e; then
0 + z < z + e by XREAL_1:8; then
consider p1, p2 being Rational such that
A2: z < p1 & p1 < p2 & p2 < z + e by BORSUK_5:26;
per cases;
suppose
A3: 0 <= z;
p1 < z + e by A2,XXREAL_0:2; then
p1 - z < z + e - z by XREAL_1:14; then
A4: |. p1 - z .| < e by ABSVALUE:def 1,A2,XREAL_1:48;
reconsider p1 as Element of RAT by RAT_1:def 2;
take p1;
thus p1 <> 0 by A2,A3;
thus |. z - p1 .| < e by A4,COMPLEX1:60;
end;
suppose
A5: z < 0;
z - e < z - 0 by A1,XREAL_1:15; then
consider p1,p2 being Rational such that
A6: z - e < p1 & p1 < p2 & p2 < z by BORSUK_5:26;
z - e - z < p1 - z by A6,XREAL_1:14; then
A7: 0 - (p1 - z) < 0 - (-e) by XREAL_1:15;
A8: p1 < z by A6,XXREAL_0:2;
reconsider p1 as Element of RAT by RAT_1:def 2;
take p1;
thus p1 <> 0 by A5,A6;
thus |. z - p1 .| < e by A7,A8,ABSVALUE:def 1,XREAL_1:48;
end;
end;
theorem Th22:
for X be RealNormSpace, w be Point of X, e be Real,
l be Linear_Combination of {w} st 0 < e holds
ex m be Linear_Combination of {w}
st Carrier m = Carrier l & rng m c= RAT & ||. Sum l - Sum m .|| < e
proof
let X be RealNormSpace, w be Point of X, e be Real,
l be Linear_Combination of {w};
assume
A1: 0 < e;
A2: Carrier l c= {w} by RLVECT_2:def 6;
per cases;
suppose
A3: not w in Carrier l;
set m = l;
take m;
thus Carrier m = Carrier l;
for y be object st y in rng m holds y in RAT
proof
let y be object;
assume y in rng m; then
consider x be object such that
A4: x in dom m & y = m.x by FUNCT_1:def 3;
reconsider x as Point of X by A4;
not x in Carrier l by A2,A3,TARSKI:def 1; then
y is integer by A4;
hence y in RAT by NUMBERS:14;
end;
hence rng m c= RAT;
Sum l - Sum m = 0.X by RLVECT_1:15;
hence ||. Sum l - Sum m .|| < e by A1;
end;
suppose
A5: w in Carrier l; then
A6: Carrier l = {w} & l.w <> 0 by RLVECT_2:19,def 6,ZFMISC_1:31;
per cases;
suppose
A7: w = 0.X;
A8: Sum l = (l.w * w) by RLVECT_2:32;
set m = (1/(l.w)) * l;
Carrier m = Carrier l by A6,RLVECT_2:42; then
reconsider m as Linear_Combination of {w} by RLVECT_2:def 6;
take m;
thus Carrier m = Carrier l by A6,RLVECT_2:42;
for y be object st y in rng m holds y in RAT
proof
let y be object;
assume y in rng m; then
consider x be object such that
A9: x in dom m & y = m.x by FUNCT_1:def 3;
reconsider x as Point of X by A9;
per cases;
suppose
not x in Carrier l; then
A10: l.x = 0;
y = (1/(l.w)) * l.x by A9,RLVECT_2:def 11; then
y is integer by A10;
hence y in RAT by NUMBERS:14;
end;
suppose
x in Carrier l; then
x = w by A6,TARSKI:def 1; then
y = (1/(l.w)) * l.w by A9,RLVECT_2:def 11; then
y is integer by A5,RLVECT_2:19,XCMPLX_1:87;
hence y in RAT by NUMBERS:14;
end;
end;
hence rng m c= RAT;
Sum m = (1/(l.w)) * Sum(l) by RLVECT_3:2;
hence ||. Sum l - Sum m .|| < e by A1,A7,A8;
end;
suppose
A11: w <> 0.X; then
A12: ||.w.|| <> 0 by NORMSP_0:def 5; then
consider q be Element of RAT such that
A13: q <> 0 & |. l.w - q .| < e / ||.w.|| by A1,Th21;
set m = (q/(l.w)) * l;
Carrier m = Carrier l by A6,A13,RLVECT_2:42; then
reconsider m as Linear_Combination of {w} by RLVECT_2:def 6;
take m;
thus Carrier m = Carrier l by A6,A13,RLVECT_2:42;
for y be object st y in rng m holds y in RAT
proof
let y be object;
assume y in rng m; then
consider x be object such that
A14: x in dom m & y = m.x by FUNCT_1:def 3;
reconsider x as Point of X by A14;
per cases;
suppose
not x in Carrier l; then
A15: l.x = 0;
y = (q/(l.w)) * l.x by A14,RLVECT_2:def 11; then
y is integer by A15;
hence y in RAT by NUMBERS:14;
end;
suppose
x in Carrier l; then
x = w by A6,TARSKI:def 1; then
y = (q/(l.w)) * l.w by A14,RLVECT_2:def 11; then
y = q by A5,RLVECT_2:19,XCMPLX_1:87;
hence y in RAT;
end;
end;
hence rng m c= RAT;
A16: Sum (m) = (q/(l.w)) * Sum(l) by RLVECT_3:2
.= (q/(l.w)) * (l.w * w) by RLVECT_2:32
.= ((q/(l.w)) * l.w) * w by RLVECT_1:def 7
.= q * w by A5,RLVECT_2:19,XCMPLX_1:87;
Sum l - Sum m = (l.w * w) - Sum m by RLVECT_2:32
.= (l.w - q) * w by A16,RLVECT_1:35; then
A17: ||. Sum l - Sum m .|| = |. l.w - q .| * ||.w.|| by NORMSP_1:def 1;
|. l.w - q .| * ||.w.|| < e / ||.w.|| * ||.w.|| by A12,A13,XREAL_1:68;
hence ||. Sum l - Sum m .|| < e by A11,A17,NORMSP_0:def 5,XCMPLX_1:87;
end;
end;
end;
theorem Th23:
for X be RealNormSpace, A be Subset of X, e be Real,
l be Linear_Combination of A st 0 < e holds
ex m be Linear_Combination of A
st Carrier m = Carrier l & rng m c= RAT & ||. Sum l - Sum m .|| < e
proof
let X be RealNormSpace, A be Subset of X;
defpred P[Nat] means
for e be Real, l be Linear_Combination of A
st 0 < e & card (Carrier l) = $1 holds
ex m be Linear_Combination of A
st Carrier m = Carrier l & rng m c= RAT & ||. Sum l - Sum m .|| < e;
A1: P[0]
proof
let e be Real, l be Linear_Combination of A;
assume
A2: 0 < e & card (Carrier l) = 0; then
Carrier l = {}; then
A3: Sum l = 0.X by RLVECT_2:34;
reconsider a = 1 as Real;
reconsider m = a*l as Linear_Combination of A by RLVECT_2:44;
take m;
thus Carrier m = Carrier l by RLVECT_2:42;
for y be object st y in rng m holds y in RAT
proof
let y be object;
assume y in rng m; then
consider x be object such that
A4: x in dom m & y = m.x by FUNCT_1:def 3;
reconsider x as Point of X by A4;
A5: not x in Carrier l by A2;
y = a * l.x by A4,RLVECT_2:def 11; then
y is integer by A5;
hence y in RAT by NUMBERS:14;
end;
hence rng m c= RAT;
Sum m = a * Sum(l) by RLVECT_3:2;
hence ||. Sum l - Sum m .|| < e by A2,A3;
end;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A7: P[k];
let e be Real, l be Linear_Combination of A;
assume
A8: 0 < e & card (Carrier l) = k+1; then
(Carrier l) <> {}; then
consider w be object such that
A9: w in Carrier l by XBOOLE_0:def 1;
reconsider w as Element of the carrier of X by A9;
A10: card((Carrier l) \ {w})
= card(Carrier l) - card({w}) by A9,CARD_2:44,ZFMISC_1:31
.= k + 1 - 1 by A8,CARD_2:42;
reconsider A0 = (Carrier l) \ {w} as finite Subset of X;
reconsider B0 = {w} as finite Subset of X;
A0 \/ B0 = (Carrier l) \/ B0 by XBOOLE_1:39; then
A0 \/ B0 = Carrier l by A9,XBOOLE_1:12,ZFMISC_1:31; then
A11: l is Linear_Combination of (A0 \/ B0) by RLVECT_2:def 6;
consider l1 be Linear_Combination of A0, l2 be Linear_Combination of B0
such that
A13: Carrier l = Carrier l1 \/ Carrier l2 & l = l1 + l2
& Carrier l1 = Carrier l \ B0 & Carrier l2 = Carrier l \ A0
by A11,Th9,XBOOLE_1:79;
A14: Carrier l c= A by RLVECT_2:def 6;
Carrier l1 c= Carrier l by A13,XBOOLE_1:36; then
Carrier l1 c= A by A14; then
l1 is Linear_Combination of A by RLVECT_2:def 6; then
consider m1 be Linear_Combination of A such that
A15: Carrier m1 = Carrier l1 & rng m1 c= RAT
& ||. Sum l1 - Sum m1 .|| < e/2 by A7,A8,A10,A13;
A16: m1 is Linear_Combination of A0 by A15,RLVECT_2:def 6;
consider m2 be Linear_Combination of {w} such that
A17: Carrier m2 = Carrier l2 & rng m2 c= RAT
& ||. Sum l2 - Sum m2 .|| < e/2 by A8,Th22;
consider m be Linear_Combination of (A0 \/ {w}) such that
A18: Carrier m = Carrier m1 \/ Carrier m2
& rng m c= RAT & Sum m = Sum m1 + Sum m2
by XBOOLE_1:79,A15,A16,A17,Th10;
A19: m is Linear_Combination of A by A13,A15,A17,A18,RLVECT_2:def 6;
Sum l - Sum m = Sum l1 + Sum l2 - Sum m by A13,RLVECT_3:1
.= Sum l1 + Sum l2 - Sum m1 - Sum m2 by A18,RLVECT_1:27
.= Sum l2 + (Sum l1 - Sum m1) - Sum m2 by RLVECT_1:28
.= (Sum l1 - Sum m1) + (Sum l2 - Sum m2) by RLVECT_1:28;
then
A20: ||. Sum l - Sum m .||
<= ||. Sum l1 - Sum m1 .|| + ||. Sum l2 - Sum m2 .|| by NORMSP_1:def 1;
||. Sum l1 - Sum m1 .|| + ||. Sum l2 - Sum m2 .||
< e/2 + e/2 by A15,A17,XREAL_1:8; then
||. Sum l - Sum m .|| < e by A20,XXREAL_0:2;
hence thesis by A13,A15,A17,A18,A19;
end;
A21: for k be Nat holds P[k] from NAT_1:sch 2(A1,A6);
let e be Real,l be Linear_Combination of A;
assume
A22: 0 < e;
card (Carrier l) is Nat;
hence thesis by A21,A22;
end;
Th24:
for X be RealNormSpace, x be sequence of X,
D be Subset of the carrier of NLin(rng x)
st D = RAT_Sums(rng x)
holds D is dense
proof
let X be RealNormSpace, x be sequence of X,
D be Subset of the carrier of NLin(rng x);
assume
A1: D = RAT_Sums(rng x);
for S be Subset of NLin(rng x) st S <> {} & S is open holds D meets S
proof
let S be Subset of NLin(rng x);
assume
A2: S <> {} & S is open;
consider z be object such that
A3: z in S by A2,XBOOLE_0:def 1;
reconsider z as Point of NLin(rng x) by A3;
consider e be Real such that
A4: 0 < e & {y where y is Point of NLin(rng x) : ||.y-z.|| < e} c= S
by A2,A3,NDIFF_1:3;
z in Lin(rng x); then
consider l be Linear_Combination of (rng x) such that
A5: z = Sum l by RLVECT_3:14;
consider m be Linear_Combination of (rng x) such that
A6: Carrier m = Carrier l & rng m c= RAT & ||. Sum l - Sum m .|| < e
by A4,Th23;
Sum m in Lin(rng x) by RLVECT_3:14; then
reconsider y = Sum m as Point of NLin(rng x);
-(Sum m) = (-1) * (Sum m) by RLVECT_1:16
.= (-1) * y by NORMSP_3:28
.= -y by RLVECT_1:16; then
Sum l - Sum m = z-y by A5,NORMSP_3:28; then
||. Sum l - Sum m .|| = ||.z-y.|| by NORMSP_3:28; then
||.y-z.|| < e by A6,NORMSP_1:7; then
A8: y in {v where v is Point of NLin(rng x) : ||.v-z.|| < e};
y in D by A1,A6;
hence D meets S by A4,A8,XBOOLE_0:def 4;
end;
hence thesis by NORMSP_3:17;
end;
theorem
for X be RealNormSpace, x be sequence of X holds
RAT_Sums(rng x) is dense Subset of the carrier of NLin(rng x)
by Th17,Th24;
Th25:
for X be RealNormSpace, x be sequence of X,
D be Subset of the carrier of ClNLin(rng x)
st D = RAT_Sums(rng x) holds D is dense
proof
let X be RealNormSpace, x be sequence of X,
D be Subset of the carrier of ClNLin(rng x);
assume
A1: D = RAT_Sums(rng x);
then reconsider D0 = D as Subset of the carrier of NLin(rng x) by Th17;
A2: D0 is dense by A1,Th24;
ex Z be Subset of X
st Z = the carrier of NLin(rng x) & Cl(Z) = the carrier of ClNLin(rng x)
by Th18;
hence D is dense by A2,Th3;
end;
theorem
for X be RealNormSpace, x be sequence of X holds
RAT_Sums rng x is dense Subset of the carrier of ClNLin(rng x)
by Th19,Th25;
theorem Th26:
for X be RealNormSpace
st ex D be Subset of the carrier of X st D is dense countable
holds X is separable
proof
let X be RealNormSpace;
set Y = LinearTopSpaceNorm X;
given D0 be Subset of the carrier of X such that
A1: D0 is dense countable;
reconsider D = D0 as Subset of Y by NORMSP_2:def 4;
D is dense by A1,NORMSP_3:15; then
A2: density Y c= card D by TOPGEN_1:def 12;
card D c= omega by A1; then
density Y c= omega by A2;
hence thesis by TOPGEN_1:def 13;
end;
begin :: 2. Basic Properties of Separable Spaces
registration let X be RealNormSpace,
x be sequence of X;
cluster ClNLin rng x -> separable;
coherence
proof
RAT_Sums rng x is countable Subset of the carrier of ClNLin(rng x)
by Th19;
hence ClNLin(rng x) is separable by Th25,Th26;
end;
end;
theorem
for X be RealNormSpace, Y be SubRealNormSpace of X,
L be Lipschitzian linear-Functional of X
holds L | (the carrier of Y) is Lipschitzian linear-Functional of Y
proof
let X be RealNormSpace, Y be SubRealNormSpace of X,
L be Lipschitzian linear-Functional of X;
set Y1 = the carrier of Y;
A1: the carrier of Y c= the carrier of X by DUALSP01:def 16; then
reconsider L1 = L|Y1 as Functional of Y by FUNCT_2:32;
A2: L1 is additive
proof
let x,y be Point of Y;
reconsider x1 = x, y1 = y as Point of X by A1;
thus L1.(x + y) = L.(x + y) by FUNCT_1:49
.= L.(x1 + y1) by NORMSP_3:28
.= L.x1 + L.y1 by HAHNBAN:def 2
.= L1.x + L.y by FUNCT_1:49
.= L1.x + L1.y by FUNCT_1:49;
end;
A3: L1 is homogeneous
proof
let x be Point of Y, r be Real;
reconsider x1 = x as Point of X by A1;
thus L1.(r * x) = L.(r * x) by FUNCT_1:49
.= L.(r * x1) by NORMSP_3:28
.= r * L.x1 by HAHNBAN:def 3
.= r * L1.x by FUNCT_1:49;
end;
consider K be Real such that
A4: 0 <= K
& for x be Point of X holds |. L.x .| <= K * ||.x.|| by DUALSP01:def 9;
for x be Point of Y holds |. L1.x .| <= K * ||.x.||
proof
let x be Point of Y;
reconsider x1 = x as Point of X by A1;
|. L.x1 .| <= K * ||.x1.|| by A4; then
|. L.x1 .| <= K * ||.x.|| by NORMSP_3:28;
hence thesis by FUNCT_1:49;
end; then
L1 is Lipschitzian by A4;
hence thesis by A2,A3;
end;
Th29:
for X,Y be RealNormSpace, A be Subset of X, B be Subset of Y,
L be Lipschitzian LinearOperator of X,Y
st L is isomorphism & B = L.:A & A is dense
holds B is dense
proof
let X,Y be RealNormSpace, A be Subset of X, B be Subset of Y,
L be Lipschitzian LinearOperator of X,Y;
assume
A1: L is isomorphism & B = L.:A & A is dense;
for y be Point of Y ex seq be sequence of Y
st rng seq c= B & seq is convergent & lim seq = y
proof
let y be Point of Y;
y in the carrier of Y; then
y in rng L by A1,FUNCT_2:def 3; then
consider x be Point of X such that
A2: y = L.x by FUNCT_2:113;
consider seq be sequence of X such that
A3: rng seq c= A & seq is convergent & lim seq = x by A1,NORMSP_3:14;
reconsider seq1 = L * seq as sequence of Y;
L.:(rng seq) c= L.: A by A3,RELAT_1:123; then
A4: rng seq1 c= B by A1,RELAT_1:127;
seq1 is convergent & lim seq1 = L.(lim seq) by A3,NORMSP_3:38;
hence thesis by A2,A3,A4;
end;
hence B is dense by NORMSP_3:14;
end;
theorem Th30:
for X,Y be RealNormSpace, A be Subset of X, B be Subset of Y,
L be Lipschitzian LinearOperator of X,Y
st L is isomorphism & B = L.:A
holds A is dense iff B is dense
proof
let X,Y be RealNormSpace, A be Subset of X, B be Subset of Y,
L be Lipschitzian LinearOperator of X,Y;
assume
A1: L is isomorphism & B = L.:A; then
consider K be Lipschitzian LinearOperator of Y,X such that
A2: K = L" & K is isomorphism by NORMSP_3:37;
thus A is dense implies B is dense by A1,Th29;
assume
A3: B is dense;
A c= the carrier of X; then
A c= dom L by FUNCT_2:def 1; then
K.:B = A by A1,A2,FUNCT_1:107;
hence A is dense by A2,A3,Th29;
end;
theorem Th31:
for X,Y be RealNormSpace
st ex L be Lipschitzian LinearOperator of X,Y
st L is isomorphism
holds X is separable iff Y is separable
proof
let X,Y be RealNormSpace;
given L be Lipschitzian LinearOperator of X,Y such that
A1: L is isomorphism;
consider K be Lipschitzian LinearOperator of Y,X such that
A2: K = L" & K is isomorphism by A1,NORMSP_3:37;
hereby
assume X is separable; then
consider seq be sequence of X such that
A3: rng seq is dense by NORMSP_3:21;
reconsider seq1 = L * seq as sequence of Y;
rng seq1 = L.:(rng seq) by RELAT_1:127; then
rng seq1 is dense by A1,A3,Th30;
hence Y is separable by NORMSP_3:21;
end;
assume Y is separable; then
consider seq be sequence of Y such that
A4: rng seq is dense by NORMSP_3:21;
reconsider seq1 = K * seq as sequence of X;
rng seq1 = K.:(rng seq) by RELAT_1:127; then
rng seq1 is dense by A2,A4,Th30;
hence X is separable by NORMSP_3:21;
end;
theorem
for X be RealNormSpace
st X is non trivial & X is Reflexive
holds X is separable iff DualSp DualSp X is separable
proof
let X be RealNormSpace;
assume
A1: X is non trivial & X is Reflexive; then
consider DuX be SubRealNormSpace of DualSp DualSp X,
L be Lipschitzian LinearOperator of X, DuX such that
A2: L is bijective & DuX = Im(BidualFunc X)
& (for x be Point of X holds L.x = BiDual x)
& for x be Point of X holds ||.x.|| = ||. L.x .|| by DUALSP02:10;
A3: Im (BidualFunc X) = DualSp DualSp X by A1,DUALSP02:22;then
reconsider L as Lipschitzian LinearOperator of X,DualSp DualSp X by A2;
L is isomorphism by A2,A3;
hence thesis by Th31;
end;
begin :: 3. Completeness and Reflexivity of Sublinear Normed Spaces
theorem
for X be RealNormSpace, Y,Z be Subset of X
st Z = the carrier of Lin(Y)
holds the carrier of Lin(Z) = Z by RLVECT_3:18;
theorem Th35:
for X be RealBanachSpace, Y be Subset of X holds
ex Z be Subset of X
st Z = the carrier of Lin(Y) & ClNLin(Y) = NLin(Cl(Z))
& Cl(Z) is linearly-closed & Cl(Z) <> {}
proof
let X be RealBanachSpace, Y be Subset of X;
consider Z be Subset of X such that
A1: Z = the carrier of Lin(Y)
& ClNLin(Y) = NORMSTR(# Cl(Z), Zero_(Cl(Z),X), Add_(Cl(Z),X),
Mult_(Cl(Z),X), Norm_(Cl(Z),X) #) by NORMSP_3:def 20;
A2: the carrier of Lin(Cl(Z)) = Cl(Z) by A1,NORMSP_3:13,31;
A3: NLin(Cl(Z))= NORMSTR(# the carrier of Lin(Cl(Z)), 0.Lin(Cl(Z)),
the addF of Lin(Cl(Z)), the Mult of Lin(Cl(Z)),
Norm_(the carrier of Lin(Cl(Z)),X) #);
A4: Zero_(Cl(Z),X) = 0.X by A1,NORMSP_3:13,RSSPACE:def 10
.= 0.Lin(Cl(Z)) by RLSUB_1:def 2;
A5: Add_(Cl(Z),X) = (the addF of X) || (Cl(Z))
by A1,NORMSP_3:13,RSSPACE:def 8
.= the addF of Lin(Cl(Z)) by A2,RLSUB_1:def 2;
A6: Mult_(Cl(Z),X) = (the Mult of X) | [:REAL,Cl(Z):]
by A1,NORMSP_3:13,RSSPACE:def 9
.= the Mult of Lin(Cl(Z)) by A2,RLSUB_1:def 2;
Norm_(Cl(Z), X) = Norm_(the carrier of Lin(Cl(Z)),X) by A1,NORMSP_3:13,31;
hence thesis by A1,A3,A4,A5,A6,NORMSP_3:13;
end;
theorem
for X be RealBanachSpace, Y be Subset of X
holds ClNLin(Y) is RealBanachSpace
proof
let X be RealBanachSpace, Y be Subset of X;
ex Z be Subset of X
st Z = the carrier of Lin(Y) & ClNLin(Y) = NLin(Cl(Z))
& Cl(Z) is linearly-closed & Cl(Z) <> {} by Th35;
hence thesis by NORMSP_3:49;
end;
theorem
for X be RealBanachSpace, Y be Subset of X st X is Reflexive
holds ClNLin(Y) is Reflexive
proof
let X be RealBanachSpace, Y be Subset of X;
assume A1: X is Reflexive;
ex Z be Subset of X
st Z = the carrier of Lin(Y) & ClNLin(Y) = NLin(Cl(Z))
& Cl(Z) is linearly-closed & Cl(Z) <> {} by Th35;
hence thesis by A1,DUALSP02:24;
end;