:: Separability of Real Normed Spaces and Its Basic Properties :: by Kazuhisa Nakasho and Noboru Endou :: :: Received February 26, 2015 :: Copyright (c) 2015-2021 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;