:: Separability of Real Normed Spaces and Its Basic Properties
:: by Kazuhisa Nakasho and Noboru Endou
::
:: Received February 26, 2015
:: Copyright (c) 2015-2016 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;
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
:: NORMSP_4:def 1
{Sum l where l is Linear_Combination of A : rng l c= RAT};
end;
theorem :: NORMSP_4:1
for V be RealNormSpace,V1 be SubRealNormSpace of V
holds TopSpaceNorm V1 is SubSpace of TopSpaceNorm V;
theorem :: NORMSP_4:2
for V be RealNormSpace, V1 be SubRealNormSpace of V
holds LinearTopSpaceNorm V1 is SubSpace of LinearTopSpaceNorm V;
theorem :: NORMSP_4:3
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;
theorem :: NORMSP_4:4
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;
theorem :: NORMSP_4:5
for X be addLoopStr, A,B be Subset of X
st A is countable & B is countable
holds A+B is countable;
theorem :: NORMSP_4:6
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;
theorem :: NORMSP_4:7
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;
theorem :: NORMSP_4:8
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;
theorem :: NORMSP_4:9
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;
theorem :: NORMSP_4:10
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;
theorem :: NORMSP_4:11
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);
registration
let X be RealLinearSpace, A be finite Subset of X;
cluster RAT_Sums(A) -> countable;
end;
theorem :: NORMSP_4:12
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 );
registration
let X be RealLinearSpace, x be sequence of X;
cluster RAT_Sums rng x -> countable;
end;
theorem :: NORMSP_4:13
for X be RealNormSpace, x be sequence of X
holds RAT_Sums(rng x) is Subset of the carrier of NLin(rng x);
theorem :: NORMSP_4:14
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);
theorem :: NORMSP_4:15
for X be RealNormSpace, x be sequence of X
holds RAT_Sums(rng x) is countable Subset of the carrier of ClNLin(rng x);
theorem :: NORMSP_4:16
for z,e be Real st 0 < e holds
ex q be Element of RAT st q <> 0 & |. z - q .| < e;
theorem :: NORMSP_4:17
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;
theorem :: NORMSP_4:18
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;
theorem :: NORMSP_4:19
for X be RealNormSpace, x be sequence of X holds
RAT_Sums(rng x) is dense Subset of the carrier of NLin(rng x);
theorem :: NORMSP_4:20
for X be RealNormSpace, x be sequence of X holds
RAT_Sums rng x is dense Subset of the carrier of ClNLin(rng x);
theorem :: NORMSP_4:21
for X be RealNormSpace
st ex D be Subset of the carrier of X st D is dense countable
holds X is separable;
begin :: 2. Basic Properties of Separable Spaces
registration let X be RealNormSpace,
x be sequence of X;
cluster ClNLin rng x -> separable;
end;
theorem :: NORMSP_4:22
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;
theorem :: NORMSP_4:23
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;
theorem :: NORMSP_4:24
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;
theorem :: NORMSP_4:25
for X be RealNormSpace
st X is non trivial & X is Reflexive
holds X is separable iff DualSp DualSp X is separable;
begin :: 3. Completeness and Reflexivity of Sublinear Normed Spaces
theorem :: NORMSP_4:26
for X be RealNormSpace, Y,Z be Subset of X
st Z = the carrier of Lin(Y)
holds the carrier of Lin(Z) = Z;
theorem :: NORMSP_4:27
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) <> {};
theorem :: NORMSP_4:28
for X be RealBanachSpace, Y be Subset of X
holds ClNLin(Y) is RealBanachSpace;
theorem :: NORMSP_4:29
for X be RealBanachSpace, Y be Subset of X st X is Reflexive
holds ClNLin(Y) is Reflexive;