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

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

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

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)

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

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 )

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

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

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;

::: for x,y be FinSequence of REAL

::: holds abs(x^y) = (abs x)^(abs y) by TOPREAL7:11 goes by FINSEQOP:9;

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

ex b_{1} being Function of (REAL n),REAL st

for x being Element of REAL n holds

( b_{1} . x in rng (abs x) & ( for i being Nat st i in dom x holds

(abs x) . i <= b_{1} . x ) )

for b_{1}, b_{2} being Function of (REAL n),REAL st ( for x being Element of REAL n holds

( b_{1} . x in rng (abs x) & ( for i being Nat st i in dom x holds

(abs x) . i <= b_{1} . x ) ) ) & ( for x being Element of REAL n holds

( b_{2} . x in rng (abs x) & ( for i being Nat st i in dom x holds

(abs x) . i <= b_{2} . x ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being Element of REAL n holds

( b

(abs x) . i <= b

proof end;

uniqueness for b

( b

(abs x) . i <= b

( b

(abs x) . i <= b

b

proof end;

:: deftheorem Def1 defines max_norm REAL_NS3:def 1 :

for n being Nat st not n is empty holds

for b_{2} being Function of (REAL n),REAL holds

( b_{2} = max_norm n iff for x being Element of REAL n holds

( b_{2} . x in rng (abs x) & ( for i being Nat st i in dom x holds

(abs x) . i <= b_{2} . x ) ) );

for n being Nat st not n is empty holds

for b

( b

( b

(abs x) . i <= b

definition

let n be Nat;

assume not n is empty ;

ex b_{1} being Function of (REAL n),REAL st

for x being Element of REAL n holds b_{1} . x = Sum (abs x)

for b_{1}, b_{2} being Function of (REAL n),REAL st ( for x being Element of REAL n holds b_{1} . x = Sum (abs x) ) & ( for x being Element of REAL n holds b_{2} . x = Sum (abs x) ) holds

b_{1} = b_{2}

end;
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 for x being Element of REAL n holds it . x = Sum (abs x);

ex b

for x being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines sum_norm REAL_NS3:def 2 :

for n being Nat st not n is empty holds

for b_{2} being Function of (REAL n),REAL holds

( b_{2} = sum_norm n iff for x being Element of REAL n holds b_{2} . x = Sum (abs x) );

for n being Nat st not n is empty holds

for b

( b

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

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

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

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 )

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 )

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;

correctness

coherence

RLSp2RVSp X is finite-dimensional ;

by REAL_NS2:82;

end;
correctness

coherence

RLSp2RVSp X is finite-dimensional ;

by REAL_NS2:82;

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)

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;

ex b_{1} 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 & b_{1} . x = (max_norm (dim X)) . z )

for b_{1}, b_{2} 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 & b_{1} . 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 & b_{2} . x = (max_norm (dim X)) . z ) ) holds

b_{1} = b_{2}

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

ex b

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 & b

proof end;

uniqueness for b

( x = y & z = y |-- b & b

( x = y & z = y |-- b & b

b

proof end;

:: deftheorem Def3 defines max_norm REAL_NS3:def 3 :

for X being finite-dimensional RealLinearSpace

for b being OrdBasis of RLSp2RVSp X

for b_{3} being Function of X,REAL holds

( b_{3} = 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 & b_{3} . x = (max_norm (dim X)) . z ) );

for X being finite-dimensional RealLinearSpace

for b being OrdBasis of RLSp2RVSp X

for b

( b

( x = y & z = y |-- b & b

definition

let X be finite-dimensional RealLinearSpace;

let b be OrdBasis of RLSp2RVSp X;

ex b_{1} 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 & b_{1} . x = (sum_norm (dim X)) . z )

for b_{1}, b_{2} 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 & b_{1} . 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 & b_{2} . x = (sum_norm (dim X)) . z ) ) holds

b_{1} = b_{2}

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

ex b

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 & b

proof end;

uniqueness for b

( x = y & z = y |-- b & b

( x = y & z = y |-- b & b

b

proof end;

:: deftheorem Def4 defines sum_norm REAL_NS3:def 4 :

for X being finite-dimensional RealLinearSpace

for b being OrdBasis of RLSp2RVSp X

for b_{3} being Function of X,REAL holds

( b_{3} = 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 & b_{3} . x = (sum_norm (dim X)) . z ) );

for X being finite-dimensional RealLinearSpace

for b being OrdBasis of RLSp2RVSp X

for b

( b

( x = y & z = y |-- b & b

definition

let X be finite-dimensional RealLinearSpace;

let b be OrdBasis of RLSp2RVSp X;

ex b_{1} 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 & b_{1} . x = |.z.| )

for b_{1}, b_{2} 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 & b_{1} . 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 & b_{2} . x = |.z.| ) ) holds

b_{1} = b_{2}

end;
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 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.| );

ex b

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 & b

proof end;

uniqueness for b

( x = y & z = y |-- b & b

( x = y & z = y |-- b & b

b

proof end;

:: deftheorem Def5 defines euclid_norm REAL_NS3:def 5 :

for X being finite-dimensional RealLinearSpace

for b being OrdBasis of RLSp2RVSp X

for b_{3} being Function of X,REAL holds

( b_{3} = 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 & b_{3} . x = |.z.| ) );

for X being finite-dimensional RealLinearSpace

for b being OrdBasis of RLSp2RVSp X

for b

( b

( x = y & z = y |-- b & b

theorem :: REAL_NS3:17

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

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

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

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 )

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

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

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.|| ) ) )

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.|| ) ) )

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).|| ) ) )

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;

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

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 )

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 )

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 ;

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;

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

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

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

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 )

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 )

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 )

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 )

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

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;