REAL_NS3: Finite Dimensional Real Normed Spaces are Proper Metric Spaces

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

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines max_norm REAL_NS3:def 1 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines sum_norm REAL_NS3:def 2 :

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;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines max_norm REAL_NS3:def 3 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines sum_norm REAL_NS3:def 4 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines euclid_norm REAL_NS3:def 5 :

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 :

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

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;

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;