:: 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;