:: Finite Dimensional Real Normed Spaces are Proper Metric Spaces :: by Kazuhisa Nakasho , Hiroyuki Okazaki and Yasunari Shidama :: :: Received September 30, 2021 :: Copyright (c) 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 ARYTM_1, ARYTM_3, CARD_1, CARD_3, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_1, FUNCT_2, TOPMETR4, MATRIX_1, MATRLIN, NAT_1, NUMBERS, ORDINAL4, PARTFUN1, PRE_TOPC, PRVECT_1, RANKNULL, RELAT_1, RLSUB_1, RLVECT_1, RLVECT_5, RVSUM_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, VALUED_0, VECTSP_1, XBOOLE_0, XXREAL_0, FUNCT_7, REAL_NS1, FUNCSDOM, FUNCOP_1, ZFMISC_1, REAL_1, NORMSP_2, PCOMPS_1, METRIC_1, MSSUBFAM, UNIALG_1, COMPLEX1, NORMSP_1, LOPBAN_1, DUALSP01, RCOMP_1, FCONT_1, SEQ_1, SEQ_2, ORDINAL2, XXREAL_2, SQUARE_1, SEQ_4, REAL_NS3, CFCONT_1; notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, PARTFUN2, ORDINAL1, FUNCT_2, BINOP_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, FINSEQOP, SEQ_1, SEQ_2, RVSUM_1, SEQ_4, RCOMP_1, STRUCT_0, PRE_TOPC, RLVECT_1, RLSUB_1, VECTSP_1, COMPTS_1, FUNCSDOM, METRIC_1, NORMSP_0, NORMSP_1, MATRIX_1, FVSUM_1, MATRLIN, PCOMPS_1, RLVECT_5, EUCLID, LOPBAN_1, VECTSP_9, RANKNULL, PRVECT_1, NFCONT_1, REAL_NS1, NORMSP_2, DUALSP01, TOPMETR4; constructors FVSUM_1, MATRIX13, MONOID_0, RANKNULL, RELSET_1, RLAFFIN1, VECTSP10, PCOMPS_1, SQUARE_1, BINOP_2, REAL_NS1, RLVECT_5, REAL_1, VECTSP_9, NFCONT_1, NORMSP_2, COMPTS_1, TBSP_1, COMSEQ_2, LOPBAN_1, DUALSP01, SEQ_2, TOPMETR4, SEQ_4, PARTFUN2, RCOMP_1, FINSOP_1, VFUNCT_1; registrations CARD_1, EUCLID, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_1, FUNCT_2, MATRIX13, MATRLIN, NAT_1, NUMBERS, PRVECT_1, RELAT_1, RELSET_1, COMPLEX1, RVSUM_1, STRUCT_0, VALUED_0, VECTSP_1, COMPTS_1, HAUSDORF, XREAL_0, XXREAL_0, SQUARE_1, ORDINAL1, REAL_NS1, NORMSP_1, RLVECT_5, XBOOLE_0, REAL_NS2; requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET; begin :: Bolzano-Weierstrass Theorem and Its Corollary reserve X for set, n,m,k for Nat, K for Field, f for n-element real-valued FinSequence, M for Matrix of n,m,F_Real; theorem :: REAL_NS3:1 for x be Element of REAL(n + 1), y be Element of REAL n st y = x | n holds |.y.| <= |.x.|; theorem :: REAL_NS3:2 for x be Element of REAL(n+1), w be Element of REAL st w = x.(n+1) holds |.w.| <= |.x.|; theorem :: REAL_NS3:3 for x be Element of REAL(n+1), y be Element of REAL n, w be Element of REAL st y = x | n & w = x.(n+1) holds |.x.| <= |.y.| + |.w.|; theorem :: REAL_NS3:4 for x,y be Element of REAL n, m be Nat st m <= n holds (x-y) | m = x|m - y|m; ::Bolzano-Weierstrass Theorem n dimension theorem :: REAL_NS3:5 for n be Nat, x be sequence of REAL-NS n st ex K be Real st for i be Nat holds ||. x.i .|| < K holds ex x0 be subsequence of x st x0 is convergent; theorem :: REAL_NS3:6 for Nrm be RealNormSpace, X be Subset of Nrm st X is compact holds X is closed & ex r be Real st for y be Point of Nrm st y in X holds ||.y.|| < r; theorem :: REAL_NS3:7 for X be Subset of REAL-NS n holds X is compact iff X is closed & ex r be Real st for y be Point of REAL-NS n st y in X holds ||.y.|| < r; begin :: L1-norm and Maximum Norm theorem :: REAL_NS3:8 for n be non empty Nat, x be Element of REAL n holds ex xMAX be Real st xMAX in rng(abs x) & for i be Nat st i in dom x holds abs(x).i <= xMAX; theorem :: REAL_NS3:9 for x be real-valued FinSequence holds 0 <= Sum abs x; ::: for x,y be FinSequence of REAL ::: holds abs(x^y) = (abs x)^(abs y) by TOPREAL7:11 goes by FINSEQOP:9; definition let n be Nat; assume n is non empty; func max_norm(n) -> Function of REAL n,REAL means :: REAL_NS3:def 1 for x be Element of REAL n holds it.x in rng(abs x) & for i be Nat st i in dom x holds abs(x).i <= it.x; end; definition let n be Nat; assume n is non empty; func sum_norm(n) -> Function of REAL n,REAL means :: REAL_NS3:def 2 for x be Element of REAL n holds it.x = Sum(abs x); end; theorem :: REAL_NS3:10 for x be Element of REAL n, xMAX be Real st xMAX in rng (abs x) & for i be Nat st i in dom x holds abs(x).i <= xMAX holds Sum(abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum(abs x); theorem :: REAL_NS3:11 for n be non empty Nat, x,y be Element of REAL n, a be Real holds 0 <= (max_norm(n)).x & ((max_norm(n)).x = 0 iff x = 0*n) & (max_norm(n)).(a * x) = |.a.| * (max_norm(n)).x & (max_norm(n)).(x + y) <= (max_norm(n)).x + (max_norm(n)).y; theorem :: REAL_NS3:12 for n be non empty Nat, x, y be Element of REAL n, a be Real holds 0 <= (sum_norm(n)).x & ((sum_norm(n)).x = 0 iff x = 0*n) & (sum_norm(n)).(a*x) = |.a.| * (sum_norm(n)).x & (sum_norm(n)).(x+y) <= (sum_norm(n)).x + (sum_norm(n)).y; theorem :: REAL_NS3:13 for n be non empty Nat, x be Element of REAL n holds (sum_norm(n)).x <= n * (max_norm(n)).x & (max_norm(n)).x <= |.x.| & |.x.| <= (sum_norm(n)).x; theorem :: REAL_NS3:14 the RLSStruct of REAL-NS(n) = RealVectSpace(Seg n); theorem :: REAL_NS3:15 for a be Real, x,y be Element of REAL-NS(n), x0,y0 be Element of RealVectSpace(Seg n) st x = x0 & y = y0 holds the carrier of REAL-NS(n) = the carrier of RealVectSpace(Seg n) & 0. REAL-NS(n) = 0.RealVectSpace(Seg n) & x + y = x0 + y0 & a * x = a * x0 & -x = -x0 & x - y = x0 - y0; registration let X be finite-dimensional RealLinearSpace; cluster RLSp2RVSp(X) -> finite-dimensional; end; theorem :: REAL_NS3:16 for X be finite-dimensional RealLinearSpace, b be OrdBasis of RLSp2RVSp(X), y be Element of RLSp2RVSp(X) holds y |-- b is Element of REAL(dim X); definition let X be finite-dimensional RealLinearSpace; let b be OrdBasis of RLSp2RVSp(X); func max_norm(X,b) -> Function of X,REAL means :: REAL_NS3:def 3 for x be Element of X ex y be Element of RLSp2RVSp(X), z be Element of REAL(dim X) st x = y & z = y |-- b & it.x = (max_norm(dim X)).z; end; definition let X be finite-dimensional RealLinearSpace; let b be OrdBasis of RLSp2RVSp(X); func sum_norm(X,b) -> Function of X,REAL means :: REAL_NS3:def 4 for x be Element of X ex y be Element of RLSp2RVSp(X), z be Element of REAL(dim X) st x = y & z = y |-- b & it.x = (sum_norm(dim X)).z; end; definition let X be finite-dimensional RealLinearSpace; let b be OrdBasis of RLSp2RVSp (X); func euclid_norm(X,b) -> Function of X,REAL means :: REAL_NS3:def 5 for x be Element of X ex y be Element of RLSp2RVSp(X), z be Element of REAL(dim X) st x = y & z = y |-- b & it.x = |.z.|; end; theorem :: REAL_NS3:17 for n be Nat, a be Element of REAL, a1 be Element of F_Real, x,y be Element of REAL n, x1,y1 be Element of n-tuples_on the carrier of F_Real st a = a1 & x = x1 & y = y1 holds a * x = a1 * x1 & x + y = x1 + y1; theorem :: REAL_NS3:18 for X be finite-dimensional RealLinearSpace, b be OrdBasis of RLSp2RVSp(X), x,y be Element of X, a be Real st dim X <> 0 holds 0 <= (max_norm(X,b)).x & ((max_norm(X,b)).x = 0 iff x = 0.X) & (max_norm(X,b)).(a*x) = |.a.| * (max_norm(X,b)).x & (max_norm(X,b)).(x+y) <= (max_norm(X,b)).x + (max_norm(X,b)).y; theorem :: REAL_NS3:19 for X be finite-dimensional RealLinearSpace, b be OrdBasis of RLSp2RVSp(X), x,y be Element of X, a be Real st dim X <> 0 holds 0 <= (sum_norm(X,b)).x & ((sum_norm(X,b)).x = 0 iff x=0.X) & (sum_norm(X,b)).(a*x) = |.a.| * (sum_norm(X,b)).x & (sum_norm(X,b)).(x+y) <= (sum_norm(X,b)).x + (sum_norm(X,b)).y; theorem :: REAL_NS3:20 for X be finite-dimensional RealLinearSpace, b be OrdBasis of RLSp2RVSp(X), x, y be Element of X, a be Real holds 0 <= (euclid_norm(X,b)).x & ((euclid_norm(X,b)).x = 0 iff x = 0.X) & (euclid_norm(X,b)).(a*x) = |.a.| * (euclid_norm(X,b)).x & (euclid_norm(X,b)).(x+y) <= (euclid_norm(X,b)).x + (euclid_norm(X,b)).y; theorem :: REAL_NS3:21 for X be finite-dimensional RealLinearSpace, b be OrdBasis of RLSp2RVSp (X), x be Element of X st dim X <> 0 holds (sum_norm(X,b)).x <= (dim X)* (max_norm(X,b)).x & (max_norm(X,b)).x <= (euclid_norm(X,b)).x & (euclid_norm(X,b)).x <= (sum_norm(X,b)).x; theorem :: REAL_NS3:22 for V be finite-dimensional RealLinearSpace, b be OrdBasis of RLSp2RVSp(V) st dim V <> 0 holds ex S be LinearOperator of V, REAL-NS(dim V) st S is bijective & for x be Element of RLSp2RVSp(V) holds S.x = x |-- b; theorem :: REAL_NS3:23 for V be finite-dimensional RealNormSpace st dim V <> 0 holds ex S be LinearOperator of V, REAL-NS(dim V), W be finite-dimensional VectSp of F_Real, b be OrdBasis of W st W = RLSp2RVSp(V) & S is bijective & for x be Element of W holds S.x = x |-- b; theorem :: REAL_NS3:24 for V be RealNormSpace, W be finite-dimensional RealLinearSpace, b be OrdBasis of RLSp2RVSp(W) st V is finite-dimensional & dim V <> 0 & the RLSStruct of V = the RLSStruct of W holds ex k1,k2 be Real st 0 < k1 & 0 < k2 & for x be Point of V holds ||.x.|| <= k1 * max_norm(W,b).x & max_norm(W,b).x <= k2 * ||.x.||; theorem :: REAL_NS3:25 for X, Y be RealNormSpace st the RLSStruct of X = the RLSStruct of Y & X is finite-dimensional & dim X <> 0 holds ex k1,k2 be Real st 0 < k1 & 0 < k2 & for x be Element of X, y be Element of Y st x = y holds ||.x.|| <= k1 * ||.y.|| & ||.y.|| <= k2 * ||.x.||; theorem :: REAL_NS3:26 for V be RealNormSpace st V is finite-dimensional & dim V <> 0 holds ex k1,k2 be Real, S be LinearOperator of V, REAL-NS(dim V) st S is bijective & 0 <= k1 & 0 <= k2 & for x be Element of V holds ||.S.x.|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.S.x.||; begin :: Linear Isometry and Its Topological Properties definition let V,W be RealNormSpace, L be LinearOperator of V,W; attr L is isometric-like means :: REAL_NS3:def 6 ex k1,k2 be Real st 0 <= k1 & 0 <= k2 & for x be Element of V holds ||.L.x.|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.L.x.||; end; theorem :: REAL_NS3:27 for V be finite-dimensional RealNormSpace st dim V <> 0 holds ex L be LinearOperator of V,REAL-NS(dim V) st L is one-to-one onto isometric-like; theorem :: REAL_NS3:28 for V,W be RealNormSpace, L be LinearOperator of V,W st L is one-to-one onto isometric-like holds ex K be LinearOperator of W,V st K = L" & K is one-to-one onto isometric-like; theorem :: REAL_NS3:29 for V,W be RealNormSpace, L be LinearOperator of V,W st L is one-to-one onto isometric-like holds L is Lipschitzian; theorem :: REAL_NS3:30 for V,W be RealNormSpace, L be LinearOperator of V,W st L is one-to-one onto isometric-like holds L is_continuous_on the carrier of V; theorem :: REAL_NS3:31 for S, T be RealNormSpace, I be LinearOperator of S,T, x be Point of S st I is one-to-one onto isometric-like holds I is_continuous_in x; theorem :: REAL_NS3:32 for S, T be RealNormSpace, I be LinearOperator of S,T, Z be Subset of S st I is one-to-one onto isometric-like holds I is_continuous_on Z; theorem :: REAL_NS3:33 for S, T be RealNormSpace, I be LinearOperator of S, T, s1 be sequence of S st I is one-to-one onto isometric-like & s1 is convergent holds I * s1 is convergent & lim (I*s1) = I.lim s1; theorem :: REAL_NS3:34 for S, T be RealNormSpace, I be LinearOperator of S, T, s1 be sequence of S st I is one-to-one onto isometric-like holds (s1 is convergent iff I*s1 is convergent); theorem :: REAL_NS3:35 for S,T be RealNormSpace, I be LinearOperator of S,T, Z be Subset of S st I is one-to-one onto isometric-like holds Z is closed iff I.:Z is closed; theorem :: REAL_NS3:36 for S,T be RealNormSpace, I be LinearOperator of S,T, Z be Subset of S st I is one-to-one onto isometric-like holds Z is open iff I.:Z is open; theorem :: REAL_NS3:37 for S,T be RealNormSpace, I be LinearOperator of S,T, Z be Subset of S st I is one-to-one onto isometric-like holds Z is compact iff I.:Z is compact; theorem :: REAL_NS3:38 for V be finite-dimensional RealNormSpace, X be Subset of V st dim V <> 0 holds X is compact iff X is closed & ex r be Real st for y be Point of V st y in X holds ||.y.|| < r;