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


theorem Th1: :: REAL_NS3:1
for n being Nat
for x being Element of REAL (n + 1)
for y being Element of REAL n st y = x | n holds
|.y.| <= |.x.|
proof end;

theorem Th2: :: REAL_NS3:2
for n being Nat
for x being Element of REAL (n + 1)
for w being Element of REAL st w = x . (n + 1) holds
|.w.| <= |.x.|
proof end;

theorem Th3: :: REAL_NS3:3
for n being Nat
for x being Element of REAL (n + 1)
for y being Element of REAL n
for w being Element of REAL st y = x | n & w = x . (n + 1) holds
|.x.| <= |.y.| + |.w.|
proof end;

theorem Th4: :: REAL_NS3:4
for n being Nat
for x, y being Element of REAL n
for m being Nat st m <= n holds
(x - y) | m = (x | m) - (y | m)
proof end;

::Bolzano-Weierstrass Theorem n dimension
theorem Th5: :: REAL_NS3:5
for n being Nat
for x being sequence of (REAL-NS n) st ex K being Real st
for i being Nat holds ||.(x . i).|| < K holds
ex x0 being subsequence of x st x0 is convergent
proof end;

Lm3: for n being Nat
for X being Subset of (REAL-NS n) st X is closed & ex r being Real st
for y being Point of (REAL-NS n) st y in X holds
||.y.|| < r holds
X is compact

proof end;

theorem Th6: :: REAL_NS3:6
for Nrm being RealNormSpace
for X being Subset of Nrm st X is compact holds
( X is closed & ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r )
proof end;

theorem :: REAL_NS3:7
for n being Nat
for X being Subset of (REAL-NS n) holds
( X is compact iff ( X is closed & ex r being Real st
for y being Point of (REAL-NS n) st y in X holds
||.y.|| < r ) ) by Lm3, Th6;

theorem Th8: :: REAL_NS3:8
for n being non empty Nat
for x being Element of REAL n ex xMAX being Real st
( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) )
proof end;

theorem Th9: :: REAL_NS3:9
for x being real-valued FinSequence holds 0 <= Sum (abs x)
proof end;

::: 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 A1: not n is empty ;
func max_norm n -> Function of (REAL n),REAL means :Def1: :: REAL_NS3:def 1
for x being Element of REAL n holds
( it . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= it . x ) );
existence
ex b1 being Function of (REAL n),REAL st
for x being Element of REAL n holds
( b1 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= b1 . x ) )
proof end;
uniqueness
for b1, b2 being Function of (REAL n),REAL st ( for x being Element of REAL n holds
( b1 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= b1 . x ) ) ) & ( for x being Element of REAL n holds
( b2 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= b2 . x ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines max_norm REAL_NS3:def 1 :
for n being Nat st not n is empty holds
for b2 being Function of (REAL n),REAL holds
( b2 = max_norm n iff for x being Element of REAL n holds
( b2 . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= b2 . x ) ) );

definition
let n be Nat;
assume not n is empty ;
func sum_norm n -> Function of (REAL n),REAL means :Def2: :: REAL_NS3:def 2
for x being Element of REAL n holds it . x = Sum (abs x);
existence
ex b1 being Function of (REAL n),REAL st
for x being Element of REAL n holds b1 . x = Sum (abs x)
proof end;
uniqueness
for b1, b2 being Function of (REAL n),REAL st ( for x being Element of REAL n holds b1 . x = Sum (abs x) ) & ( for x being Element of REAL n holds b2 . x = Sum (abs x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines sum_norm REAL_NS3:def 2 :
for n being Nat st not n is empty holds
for b2 being Function of (REAL n),REAL holds
( b2 = sum_norm n iff for x being Element of REAL n holds b2 . x = Sum (abs x) );

theorem Th11: :: REAL_NS3:10
for n being Nat
for x being Element of REAL n
for xMAX being Real st xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) holds
( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )
proof end;

theorem Th12: :: REAL_NS3:11
for n being non empty Nat
for x, y being Element of REAL n
for a being Real holds
( 0 <= (max_norm n) . x & ( (max_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (max_norm n) . x = 0 ) & (max_norm n) . (a * x) = |.a.| * ((max_norm n) . x) & (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y) )
proof end;

theorem Th13: :: REAL_NS3:12
for n being non empty Nat
for x, y being Element of REAL n
for a being Real holds
( 0 <= (sum_norm n) . x & ( (sum_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (sum_norm n) . x = 0 ) & (sum_norm n) . (a * x) = |.a.| * ((sum_norm n) . x) & (sum_norm n) . (x + y) <= ((sum_norm n) . x) + ((sum_norm n) . y) )
proof end;

theorem Th14: :: REAL_NS3:13
for n being non empty Nat
for x being Element of REAL n holds
( (sum_norm n) . x <= n * ((max_norm n) . x) & (max_norm n) . x <= |.x.| & |.x.| <= (sum_norm n) . x )
proof end;

theorem Th15: :: REAL_NS3:14
for n being Nat holds RLSStruct(# the carrier of (REAL-NS n), the ZeroF of (REAL-NS n), the U5 of (REAL-NS n), the Mult of (REAL-NS n) #) = RealVectSpace (Seg n)
proof end;

theorem Th16: :: REAL_NS3:15
for n being Nat
for a being Real
for x, y being Element of (REAL-NS n)
for x0, y0 being 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 )
proof end;

registration
let X be finite-dimensional RealLinearSpace;
cluster RLSp2RVSp X -> finite-dimensional ;
correctness
coherence
RLSp2RVSp X is finite-dimensional
;
by REAL_NS2:82;
end;

theorem Th17: :: REAL_NS3:16
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for y being Element of (RLSp2RVSp X) holds y |-- b is Element of REAL (dim X)
proof end;

definition
let X be finite-dimensional RealLinearSpace;
let b be OrdBasis of RLSp2RVSp X;
func max_norm (X,b) -> Function of X,REAL means :Def3: :: REAL_NS3:def 3
for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & it . x = (max_norm (dim X)) . z );
existence
ex b1 being Function of X,REAL st
for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b1 . x = (max_norm (dim X)) . z )
proof end;
uniqueness
for b1, b2 being Function of X,REAL st ( for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b1 . x = (max_norm (dim X)) . z ) ) & ( for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b2 . x = (max_norm (dim X)) . z ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines max_norm REAL_NS3:def 3 :
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for b3 being Function of X,REAL holds
( b3 = max_norm (X,b) iff for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b3 . x = (max_norm (dim X)) . z ) );

definition
let X be finite-dimensional RealLinearSpace;
let b be OrdBasis of RLSp2RVSp X;
func sum_norm (X,b) -> Function of X,REAL means :Def4: :: REAL_NS3:def 4
for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & it . x = (sum_norm (dim X)) . z );
existence
ex b1 being Function of X,REAL st
for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b1 . x = (sum_norm (dim X)) . z )
proof end;
uniqueness
for b1, b2 being Function of X,REAL st ( for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b1 . x = (sum_norm (dim X)) . z ) ) & ( for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b2 . x = (sum_norm (dim X)) . z ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines sum_norm REAL_NS3:def 4 :
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for b3 being Function of X,REAL holds
( b3 = sum_norm (X,b) iff for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b3 . x = (sum_norm (dim X)) . z ) );

definition
let X be finite-dimensional RealLinearSpace;
let b be OrdBasis of RLSp2RVSp X;
func euclid_norm (X,b) -> Function of X,REAL means :Def5: :: REAL_NS3:def 5
for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & it . x = |.z.| );
existence
ex b1 being Function of X,REAL st
for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b1 . x = |.z.| )
proof end;
uniqueness
for b1, b2 being Function of X,REAL st ( for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b1 . x = |.z.| ) ) & ( for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b2 . x = |.z.| ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines euclid_norm REAL_NS3:def 5 :
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for b3 being Function of X,REAL holds
( b3 = euclid_norm (X,b) iff for x being Element of X ex y being Element of (RLSp2RVSp X) ex z being Element of REAL (dim X) st
( x = y & z = y |-- b & b3 . x = |.z.| ) );

theorem :: REAL_NS3:17
for n being Nat
for a being Element of REAL
for a1 being Element of F_Real
for x, y being Element of REAL n
for x1, y1 being 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 Th19: :: REAL_NS3:18
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for x, y being Element of X
for a being Real st dim X <> 0 holds
( 0 <= (max_norm (X,b)) . x & ( (max_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (max_norm (X,b)) . x = 0 ) & (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) )
proof end;

theorem :: REAL_NS3:19
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for x, y being Element of X
for a being Real st dim X <> 0 holds
( 0 <= (sum_norm (X,b)) . x & ( (sum_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (sum_norm (X,b)) . x = 0 ) & (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) )
proof end;

theorem :: REAL_NS3:20
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for x, y being Element of X
for a being Real holds
( 0 <= (euclid_norm (X,b)) . x & ( (euclid_norm (X,b)) . x = 0 implies x = 0. X ) & ( x = 0. X implies (euclid_norm (X,b)) . x = 0 ) & (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) )
proof end;

theorem Th22: :: REAL_NS3:21
for X being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp X
for x being 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 )
proof end;

theorem Th23: :: REAL_NS3:22
for V being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp V st dim V <> 0 holds
ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & ( for x being Element of (RLSp2RVSp V) holds S . x = x |-- b ) )
proof end;

theorem Th24: :: REAL_NS3:23
for V being finite-dimensional RealNormSpace st dim V <> 0 holds
ex S being LinearOperator of V,(REAL-NS (dim V)) ex W being finite-dimensional VectSp of F_Real ex b being OrdBasis of W st
( W = RLSp2RVSp V & S is bijective & ( for x being Element of W holds S . x = x |-- b ) )
proof end;

theorem Th25: :: REAL_NS3:24
for V being RealNormSpace
for W being finite-dimensional RealLinearSpace
for b being OrdBasis of RLSp2RVSp W st V is finite-dimensional & dim V <> 0 & RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) holds
ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Point of V holds
( ||.x.|| <= k1 * ((max_norm (W,b)) . x) & (max_norm (W,b)) . x <= k2 * ||.x.|| ) ) )
proof end;

theorem :: REAL_NS3:25
for X, Y being RealNormSpace st RLSStruct(# the carrier of X, the ZeroF of X, the U5 of X, the Mult of X #) = RLSStruct(# the carrier of Y, the ZeroF of Y, the U5 of Y, the Mult of Y #) & X is finite-dimensional & dim X <> 0 holds
ex k1, k2 being Real st
( 0 < k1 & 0 < k2 & ( for x being Element of X
for y being Element of Y st x = y holds
( ||.x.|| <= k1 * ||.y.|| & ||.y.|| <= k2 * ||.x.|| ) ) )
proof end;

theorem Th27: :: REAL_NS3:26
for V being RealNormSpace st V is finite-dimensional & dim V <> 0 holds
ex k1, k2 being Real ex S being LinearOperator of V,(REAL-NS (dim V)) st
( S is bijective & 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(S . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(S . x).|| ) ) )
proof end;

definition
let V, W be RealNormSpace;
let L be LinearOperator of V,W;
attr L is isometric-like means :: REAL_NS3:def 6
ex k1, k2 being Real st
( 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(L . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(L . x).|| ) ) );
end;

:: deftheorem defines isometric-like REAL_NS3:def 6 :
for V, W being RealNormSpace
for L being LinearOperator of V,W holds
( L is isometric-like iff ex k1, k2 being Real st
( 0 <= k1 & 0 <= k2 & ( for x being Element of V holds
( ||.(L . x).|| <= k1 * ||.x.|| & ||.x.|| <= k2 * ||.(L . x).|| ) ) ) );

theorem Th28: :: REAL_NS3:27
for V being finite-dimensional RealNormSpace st dim V <> 0 holds
ex L being LinearOperator of V,(REAL-NS (dim V)) st
( L is one-to-one & L is onto & L is isometric-like )
proof end;

theorem Th29: :: REAL_NS3:28
for V, W being RealNormSpace
for L being LinearOperator of V,W st L is one-to-one & L is onto & L is isometric-like holds
ex K being LinearOperator of W,V st
( K = L " & K is one-to-one & K is onto & K is isometric-like )
proof end;

theorem Th30: :: REAL_NS3:29
for V, W being RealNormSpace
for L being LinearOperator of V,W st L is one-to-one & L is onto & L is isometric-like holds
L is Lipschitzian ;

theorem :: REAL_NS3:30
for V, W being RealNormSpace
for L being LinearOperator of V,W st L is one-to-one & L is onto & L is isometric-like holds
L is_continuous_on the carrier of V by Th30, LOPBAN_7:6;

theorem Th32: :: REAL_NS3:31
for S, T being RealNormSpace
for I being LinearOperator of S,T
for x being Point of S st I is one-to-one & I is onto & I is isometric-like holds
I is_continuous_in x
proof end;

theorem Th33: :: REAL_NS3:32
for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like holds
I is_continuous_on Z
proof end;

theorem Th34: :: REAL_NS3:33
for S, T being RealNormSpace
for I being LinearOperator of S,T
for s1 being sequence of S st I is one-to-one & I is onto & I is isometric-like & s1 is convergent holds
( I * s1 is convergent & lim (I * s1) = I . (lim s1) )
proof end;

theorem Th35: :: REAL_NS3:34
for S, T being RealNormSpace
for I being LinearOperator of S,T
for s1 being sequence of S st I is one-to-one & I is onto & I is isometric-like holds
( s1 is convergent iff I * s1 is convergent )
proof end;

Lm4: for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like & Z is closed holds
I .: Z is closed

proof end;

theorem Th36: :: REAL_NS3:35
for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like holds
( Z is closed iff I .: Z is closed )
proof end;

theorem :: REAL_NS3:36
for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like holds
( Z is open iff I .: Z is open )
proof end;

Lm5: for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like & Z is compact holds
I .: Z is compact

proof end;

theorem Th38: :: REAL_NS3:37
for S, T being RealNormSpace
for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like holds
( Z is compact iff I .: Z is compact )
proof end;

theorem :: REAL_NS3:38
for V being finite-dimensional RealNormSpace
for X being Subset of V st dim V <> 0 holds
( X is compact iff ( X is closed & ex r being Real st
for y being Point of V st y in X holds
||.y.|| < r ) )
proof end;