dualsp01.miz
begin
reserve V for non
empty
RealLinearSpace;
definition
let X be
RealLinearSpace;
::
DUALSP01:def1
func
MultF_Real* (X) ->
Function of
[:the
carrier of
F_Real , the
carrier of X:], the
carrier of X equals the
Mult of X;
correctness ;
end
theorem ::
DUALSP01:1
Lm01: for X be
RealLinearSpace holds
ModuleStr (# the
carrier of X, the
addF of X, the
ZeroF of X, (
MultF_Real* X) #) is
VectSp of
F_Real
proof
let X be
RealLinearSpace;
set XP =
ModuleStr (# the
carrier of X, the
addF of X, the
ZeroF of X, (
MultF_Real* X) #);
Q1: XP is
scalar-distributive
vector-distributive
scalar-associative
scalar-unital
proof
now
let x,y be
Element of
F_Real ;
let v be
Element of XP;
reconsider v1 = v as
Element of X;
reconsider x1 = x, y1 = y as
Real;
((x
+ y)
* v)
= ((x1
+ y1)
* v1)
= ((x1
* v1)
+ (y1
* v1)) by
RLVECT_1:def 6;
hence ((x
+ y)
* v)
= ((x
* v)
+ (y
* v));
end;
hence XP is
scalar-distributive;
now
let x be
Element of
F_Real ;
let v,w be
Element of XP;
reconsider v1 = v, w1 = w as
Element of X;
reconsider x1 = x as
Real;
(x
* (v
+ w))
= (x1
* (v1
+ w1))
.= ((x1
* v1)
+ (x1
* w1)) by
RLVECT_1:def 5;
hence (x
* (v
+ w))
= ((x
* v)
+ (x
* w));
end;
hence XP is
vector-distributive;
now
let x,y be
Element of
F_Real ;
let v be
Element of XP;
reconsider v1 = v as
Element of X;
reconsider x1 = x, y1 = y as
Real;
((x
* y)
* v)
= ((x1
* y1)
* v1)
.= (x1
* (y1
* v1)) by
RLVECT_1:def 7;
hence ((x
* y)
* v)
= (x
* (y
* v));
end;
hence XP is
scalar-associative;
now
let v be
Element of XP;
reconsider v1 = v as
Element of X;
((
1.
F_Real )
* v)
= (1
* v1);
hence ((
1.
F_Real )
* v)
= v by
RLVECT_1:def 8;
end;
hence XP is
scalar-unital;
end;
now
let u,v,w be
Element of XP;
reconsider u1 = u, v1 = v, w1 = w as
Element of X;
(u
+ (v
+ w))
= (u1
+ (v1
+ w1))
.= ((u1
+ v1)
+ w1) by
RLVECT_1:def 3;
hence (u
+ (v
+ w))
= ((u
+ v)
+ w);
end;
then
Q2: XP is
add-associative;
now
let v be
Element of XP;
reconsider v1 = v as
Element of X;
(v
+ (
0. XP))
= (v1
+ (
0. X));
hence (v
+ (
0. XP))
= v;
end;
then
Q3: XP is
right_zeroed;
now
let v be
Element of XP;
reconsider v1 = v as
Element of X;
consider w1 be
Element of X such that
A1: (v1
+ w1)
= (
0. X) by
ALGSTR_0:def 11;
reconsider w = w1 as
Element of XP;
(v
+ w)
= (
0. XP) by
A1;
hence v is
right_complementable;
end;
then
Q4: XP is
right_complementable;
now
let v,w be
Element of XP;
reconsider v1 = v, w1 = w as
Element of X;
(v
+ w)
= (v1
+ w1)
.= (w1
+ v1);
hence (v
+ w)
= (w
+ v);
end;
then XP is
Abelian;
hence XP is
VectSp of
F_Real by
Q1,
Q2,
Q3,
Q4;
end;
definition
let X be
RealLinearSpace;
::
DUALSP01:def2
func
RLSp2RVSp X ->
VectSp of
F_Real equals
ModuleStr (# the
carrier of X, the
addF of X, the
ZeroF of X, (
MultF_Real* X) #);
correctness by
Lm01;
end
definition
let X be
ModuleStr over
F_Real ;
::
DUALSP01:def3
func
MultReal* (X) ->
Function of
[:
REAL , the
carrier of X:], the
carrier of X equals the
lmult of X;
correctness ;
end
theorem ::
DUALSP01:2
Lm02: for X be
VectSp of
F_Real holds
RLSStruct (# the
carrier of X, the
ZeroF of X, the
addF of X, (
MultReal* X) #) is
RealLinearSpace
proof
let X be
VectSp of
F_Real ;
set XQ =
RLSStruct (# the
carrier of X, the
ZeroF of X, the
addF of X, (
MultReal* X) #);
A1: for vZ1,wZ1 be
Element of X, v,w be
Element of XQ st v
= vZ1 & w
= wZ1 holds (v
+ w)
= (vZ1
+ wZ1);
XQ is
Abelian
add-associative
right_zeroed
right_complementable
scalar-distributive
vector-distributive
scalar-associative
scalar-unital
proof
hereby
let v,w be
VECTOR of XQ;
reconsider vZ1 = v, wZ1 = w as
Element of X;
thus (v
+ w)
= (wZ1
+ vZ1) by
A1
.= (w
+ v);
end;
hereby
let u,v,w be
VECTOR of XQ;
reconsider uZ1 = u, vZ1 = v, wZ1 = w as
Element of X;
((u
+ v)
+ w)
= ((uZ1
+ vZ1)
+ wZ1)
.= (uZ1
+ (vZ1
+ wZ1)) by
RLVECT_1:def 3;
hence ((u
+ v)
+ w)
= (u
+ (v
+ w));
end;
hereby
let v be
VECTOR of XQ;
reconsider vZ1 = v as
Element of X;
thus (v
+ (
0. XQ))
= (vZ1
+ (
0. X))
.= v;
end;
thus XQ is
right_complementable
proof
let v be
VECTOR of XQ;
reconsider vZ1 = v as
Element of X;
consider wZ1 be
Element of X such that
A2: (vZ1
+ wZ1)
= (
0. X) by
ALGSTR_0:def 11;
reconsider w = wZ1 as
VECTOR of XQ;
take w;
thus (v
+ w)
= (
0. XQ) by
A2;
end;
hereby
let a,b be
Real, v be
VECTOR of XQ;
reconsider vZ1 = v as
Element of X;
reconsider aZ1 = a, bZ1 = b as
Element of
F_Real by
XREAL_0:def 1;
((a
+ b)
* v)
= ((aZ1
+ bZ1)
* vZ1)
.= ((aZ1
* vZ1)
+ (bZ1
* vZ1)) by
VECTSP_1:def 15;
hence ((a
+ b)
* v)
= ((a
* v)
+ (b
* v));
end;
hereby
let a be
Real, v,w be
VECTOR of XQ;
reconsider aZ1 = a as
Element of
F_Real by
XREAL_0:def 1;
reconsider vZ1 = v, wZ1 = w as
Element of X;
(a
* (v
+ w))
= (aZ1
* (vZ1
+ wZ1))
.= ((aZ1
* vZ1)
+ (aZ1
* wZ1)) by
VECTSP_1:def 14;
hence (a
* (v
+ w))
= ((a
* v)
+ (a
* w));
end;
hereby
let a,b be
Real, v be
VECTOR of XQ;
reconsider vZ1 = v as
Element of X;
reconsider aZ1 = a, bZ1 = b as
Element of
F_Real by
XREAL_0:def 1;
((a
* b)
* v)
= ((aZ1
* bZ1)
* vZ1)
.= (aZ1
* (bZ1
* vZ1)) by
VECTSP_1:def 16;
hence ((a
* b)
* v)
= (a
* (b
* v));
end;
let v be
VECTOR of XQ;
reconsider vZ1 = v as
Element of X;
thus (1
* v)
= ((
1.
F_Real )
* vZ1)
.= v by
VECTSP_1:def 17;
end;
hence thesis;
end;
definition
let X be
VectSp of
F_Real ;
::
DUALSP01:def4
func
RVSp2RLSp X ->
RealLinearSpace equals
RLSStruct (# the
carrier of X, the
ZeroF of X, the
addF of X, (
MultReal* X) #);
correctness by
Lm02;
end
theorem ::
DUALSP01:3
for X be
RealLinearSpace, v,w be
Element of X, v1,w1 be
Element of (
RLSp2RVSp X) st v
= v1 & w
= w1 holds (v
+ w)
= (v1
+ w1) & (v
- w)
= (v1
- w1)
proof
let X be
RealLinearSpace, v,w be
Element of X, v1,w1 be
Element of (
RLSp2RVSp X);
assume
AS: v
= v1 & w
= w1;
hence (v
+ w)
= (v1
+ w1);
(
- w)
= ((
- 1)
* w) by
RLVECT_1: 16
.= ((
- (
1.
F_Real ))
* w1) by
AS
.= (
- w1) by
VECTSP_1: 14;
hence (v
- w)
= (v1
- w1) by
AS;
end;
theorem ::
DUALSP01:4
for X be
VectSp of
F_Real , v,w be
Element of X, v1,w1 be
Element of (
RVSp2RLSp X) st v
= v1 & w
= w1 holds (v
+ w)
= (v1
+ w1) & (v
- w)
= (v1
- w1)
proof
let X be
VectSp of
F_Real , v,w be
Element of X, v1,w1 be
Element of (
RVSp2RLSp X);
assume
AS: v
= v1 & w
= w1;
(
- w1)
= ((
- 1)
* w1) by
RLVECT_1: 16
.= ((
- (
1.
F_Real ))
* w) by
AS
.= (
- w) by
VECTSP_1: 14;
hence (v
+ w)
= (v1
+ w1) & (v
- w)
= (v1
- w1) by
AS;
end;
definition
let V be non
empty
RealLinearSpace;
::
DUALSP01:def5
func V
*' ->
strict non
empty
RealLinearSpace means
:
def2: ex X be non
empty
VectSp of
F_Real st X
= (
RLSp2RVSp V) & it
= (
RVSp2RLSp (X
*' ));
correctness
proof
reconsider X = (
RLSp2RVSp V) as non
empty
VectSp of
F_Real ;
(
RVSp2RLSp (X
*' )) is non
empty
RealLinearSpace;
hence thesis;
end;
end
theorem ::
DUALSP01:5
Th1: for x be
object holds x
in the
carrier of (V
*' ) iff x is
linear-Functional of V
proof
let x be
object;
consider X be non
empty
VectSp of
F_Real such that
AS1: X
= (
RLSp2RVSp V) & (V
*' )
= (
RVSp2RLSp (X
*' )) by
def2;
x is
linear-Functional of X iff x is
linear-Functional of V
proof
hereby
assume
A21: x is
linear-Functional of X;
then
reconsider f = x as
Functional of V by
AS1;
reconsider g = x as
linear-Functional of X by
A21;
A1: f is
additive
proof
let v,w be
Element of V;
reconsider v1 = v, w1 = w as
Element of X by
AS1;
(f
. (v
+ w))
= (g
. (v1
+ w1)) by
AS1
.= ((g
. v1)
+ (g
. w1)) by
VECTSP_1:def 20;
hence (f
. (v
+ w))
= ((f
. v)
+ (f
. w));
end;
f is
homogeneous
proof
let v be
VECTOR of V, r be
Real;
reconsider v1 = v as
Element of X by
AS1;
reconsider r1 = r as
Scalar of X by
XREAL_0:def 1;
(f
. (r
* v))
= (g
. (r1
* v1)) by
AS1
.= (r1
* (g
. v1)) by
HAHNBAN1:def 8;
hence (f
. (r
* v))
= (r
* (f
. v));
end;
hence x is
linear-Functional of V by
A1;
end;
assume
A21: x is
linear-Functional of V;
then
reconsider f = x as
Functional of X by
AS1;
reconsider g = x as
linear-Functional of V by
A21;
A1: f is
additive
proof
let v,w be
Element of X;
reconsider v1 = v, w1 = w as
VECTOR of V by
AS1;
(f
. (v
+ w))
= (g
. (v1
+ w1)) by
AS1;
hence (f
. (v
+ w))
= ((f
. v)
+ (f
. w)) by
HAHNBAN:def 2;
end;
f is
homogeneous
proof
let v be
Element of X, r be
Element of
F_Real ;
reconsider v1 = v as
Element of V by
AS1;
reconsider r1 = r as
Element of
REAL ;
(f
. (r
* v))
= (g
. (r1
* v1)) by
AS1;
hence (f
. (r
* v))
= (r
* (f
. v)) by
HAHNBAN:def 3;
end;
hence x is
linear-Functional of X by
A1;
end;
hence thesis by
AS1,
HAHNBAN1:def 10;
end;
registration
let V be non
empty
RealLinearSpace;
cluster (V
*' ) ->
constituted-Functions;
coherence
proof
the
carrier of (V
*' ) is
functional by
Th1;
hence thesis by
MONOID_0: 80;
end;
end
definition
let V be non
empty
RealLinearSpace;
let f be
Element of (V
*' );
let v be
VECTOR of V;
:: original:
.
redefine
func f
. v ->
Element of
REAL ;
coherence
proof
reconsider f as
Functional of V by
Th1;
(f
. v) is
Element of
REAL ;
hence thesis;
end;
end
theorem ::
DUALSP01:6
for V be non
empty
RealLinearSpace, f,g,h be
VECTOR of (V
*' ) holds h
= (f
+ g) iff for x be
VECTOR of V holds (h
. x)
= ((f
. x)
+ (g
. x))
proof
let V be non
empty
RealLinearSpace;
let f,g,h be
VECTOR of (V
*' );
consider Y be non
empty
VectSp of
F_Real such that
AS1: Y
= (
RLSp2RVSp V) & (V
*' )
= (
RVSp2RLSp (Y
*' )) by
def2;
reconsider f1 = f, g1 = g, h1 = h as
linear-Functional of Y by
AS1,
HAHNBAN1:def 10;
A2:
now
assume
A3: h
= (f
+ g);
let x be
Element of V;
reconsider x1 = x as
Element of Y by
AS1;
h1
= (f1
+ g1) by
A3,
AS1,
HAHNBAN1:def 10;
then (h1
. x1)
= ((f1
. x1)
+ (g1
. x1)) by
HAHNBAN1:def 3;
hence (h
. x)
= ((f
. x)
+ (g
. x));
end;
now
assume for x be
Element of V holds (h
. x)
= ((f
. x)
+ (g
. x));
then for x be
Element of Y holds (h1
. x)
= ((f1
. x)
+ (g1
. x)) by
AS1;
then h1
= (f1
+ g1) by
HAHNBAN1:def 3;
hence h
= (f
+ g) by
AS1,
HAHNBAN1:def 10;
end;
hence thesis by
A2;
end;
theorem ::
DUALSP01:7
for V be non
empty
RealLinearSpace, f,h be
VECTOR of (V
*' ), a be
Real holds h
= (a
* f) iff for x be
VECTOR of V holds (h
. x)
= (a
* (f
. x))
proof
let V be non
empty
RealLinearSpace, f,h be
VECTOR of (V
*' ), a be
Real;
reconsider a1 = a as
Element of
F_Real by
XREAL_0:def 1;
consider Y be non
empty
VectSp of
F_Real such that
AS1: Y
= (
RLSp2RVSp V) & (V
*' )
= (
RVSp2RLSp (Y
*' )) by
def2;
reconsider f1 = f, h1 = h as
linear-Functional of Y by
AS1,
HAHNBAN1:def 10;
hereby
assume
A3: h
= (a
* f);
hereby
let x be
Element of V;
reconsider x1 = x as
Element of Y by
AS1;
h1
= (a1
* f1) by
A3,
AS1,
HAHNBAN1:def 10;
then (h1
. x1)
= (a1
* (f1
. x1)) by
HAHNBAN1:def 6;
hence (h
. x)
= (a
* (f
. x));
end;
end;
assume for x be
Element of V holds (h
. x)
= (a
* (f
. x));
then for x be
Element of Y holds (h1
. x)
= (a1
* (f1
. x)) by
AS1;
then h1
= (a1
* f1) by
HAHNBAN1:def 6;
hence h
= (a
* f) by
AS1,
HAHNBAN1:def 10;
end;
theorem ::
DUALSP01:8
for V be non
empty
RealLinearSpace holds (
0. (V
*' ))
= (the
carrier of V
-->
0 )
proof
let V be non
empty
RealLinearSpace;
consider Y be non
empty
VectSp of
F_Real such that
AS1: Y
= (
RLSp2RVSp V) & (V
*' )
= (
RVSp2RLSp (Y
*' )) by
def2;
(
0. (V
*' ))
= (
0. (Y
*' )) by
AS1
.= (
0Functional Y) by
HAHNBAN1:def 10
.= ((
[#] Y)
--> (
0.
F_Real )) by
HAHNBAN1:def 7;
hence (
0. (V
*' ))
= (the
carrier of V
-->
0 ) by
AS1;
end;
theorem ::
DUALSP01:9
Th23: for X be
RealLinearSpace holds (the
carrier of X
-->
0 ) is
linear-Functional of X
proof
let X be
RealLinearSpace;
set f = (the
carrier of X
-->
0 );
reconsider f as
Functional of X by
FUNCOP_1: 45,
XREAL_0:def 1;
A1: f is
additive
proof
let x,y be
VECTOR of X;
thus (f
. (x
+ y))
= ((f
. x)
+ (f
. y));
end;
f is
homogeneous
proof
let x be
VECTOR of X, r be
Real;
thus (f
. (r
* x))
= (r
* (f
. x));
end;
hence thesis by
A1;
end;
definition
let X be
RealLinearSpace;
::
DUALSP01:def6
func
LinearFunctionals X ->
Subset of (
RealVectSpace the
carrier of X) means
:
Def7: for x be
object holds x
in it iff x is
linear-Functional of X;
existence
proof
defpred
P[
object] means $1 is
linear-Functional of X;
consider IT be
set such that
A1: for x be
object holds x
in IT iff x
in (
Funcs (the
carrier of X,
REAL )) &
P[x] from
XBOOLE_0:sch 1;
for x be
object st x
in IT holds x
in (
Funcs (the
carrier of X,
REAL )) by
A1;
then
reconsider IT as
Subset of (
RealVectSpace the
carrier of X) by
TARSKI:def 3;
take IT;
let x be
object;
thus x
in IT implies x is
linear-Functional of X by
A1;
assume
A3: x is
linear-Functional of X;
then x
in (
Funcs (the
carrier of X,
REAL )) by
FUNCT_2: 8;
hence thesis by
A1,
A3;
end;
uniqueness
proof
let X1,X2 be
Subset of (
RealVectSpace the
carrier of X);
assume that
A4: for x be
object holds x
in X1 iff x is
linear-Functional of X and
A5: for x be
object holds x
in X2 iff x is
linear-Functional of X;
now
let x be
object;
assume x
in X1;
then x is
linear-Functional of X by
A4;
hence x
in X2 by
A5;
end;
then
A6: X1
c= X2;
now
let x be
object;
assume x
in X2;
then x is
linear-Functional of X by
A5;
hence x
in X1 by
A4;
end;
then X2
c= X1;
hence thesis by
A6;
end;
end
registration
let X be
RealNormSpace;
cluster (
LinearFunctionals X) -> non
empty;
coherence
proof
(the
carrier of X
-->
0 ) is
linear-Functional of X by
Th23;
hence thesis by
Def7;
end;
end
registration
let X be
RealLinearSpace;
cluster (
LinearFunctionals X) -> non
empty
functional;
coherence
proof
(the
carrier of X
-->
0 ) is
linear-Functional of X by
Th23;
hence (
LinearFunctionals X) is non
empty by
Def7;
let x be
object;
assume x
in (
LinearFunctionals X);
hence thesis;
end;
end
theorem ::
DUALSP01:10
Th17: for X be
RealLinearSpace holds (
LinearFunctionals X) is
linearly-closed
proof
let X be
RealLinearSpace;
set W = (
LinearFunctionals X);
A1: for v,u be
VECTOR of (
RealVectSpace the
carrier of X) st v
in (
LinearFunctionals X) & u
in (
LinearFunctionals X) holds (v
+ u)
in (
LinearFunctionals X)
proof
let v,u be
VECTOR of (
RealVectSpace the
carrier of X) such that
A2: v
in W & u
in W;
reconsider f = (v
+ u) as
Functional of X by
FUNCT_2: 66;
A3: f is
additive
proof
let x,y be
VECTOR of X;
reconsider vZ1 = v, uZ1 = u as
Element of (
Funcs (the
carrier of X,
REAL ));
A4: uZ1 is
linear-Functional of X by
A2,
Def7;
reconsider uZ11 = uZ1 as
additive
homogeneous
Functional of X by
A2,
Def7;
reconsider x1 = x, y1 = y as
Element of X;
A5: vZ1 is
linear-Functional of X by
A2,
Def7;
(f
. (x
+ y))
= ((uZ1
. (x
+ y))
+ (vZ1
. (x
+ y))) by
FUNCSDOM: 1
.= (((uZ1
. x)
+ (uZ1
. y))
+ (vZ1
. (x
+ y))) by
A4,
HAHNBAN:def 2
.= (((uZ1
. x)
+ (uZ1
. y))
+ ((vZ1
. x)
+ (vZ1
. y))) by
A5,
HAHNBAN:def 2
.= ((((uZ1
. x)
+ (vZ1
. x))
+ (uZ1
. y))
+ (vZ1
. y))
.= (((f
. x)
+ (uZ1
. y))
+ (vZ1
. y)) by
FUNCSDOM: 1
.= ((f
. x)
+ ((uZ1
. y)
+ (vZ1
. y)));
hence (f
. (x
+ y))
= ((f
. x)
+ (f
. y)) by
FUNCSDOM: 1;
end;
f is
homogeneous
proof
let x be
VECTOR of X, s be
Real;
reconsider v1 = v, u1 = u as
Element of (
Funcs (the
carrier of X,
REAL ));
A6: u1 is
linear-Functional of X & v1 is
linear-Functional of X by
A2,
Def7;
(f
. (s
* x))
= ((u1
. (s
* x))
+ (v1
. (s
* x))) by
FUNCSDOM: 1
.= ((s
* (u1
. x))
+ (v1
. (s
* x))) by
A6,
HAHNBAN:def 3
.= ((s
* (u1
. x))
+ (s
* (v1
. x))) by
A6,
HAHNBAN:def 3
.= (s
* ((u1
. x)
+ (v1
. x)));
hence (f
. (s
* x))
= (s
* (f
. x)) by
FUNCSDOM: 1;
end;
hence (v
+ u)
in W by
A3,
Def7;
end;
for a be
Real, v be
VECTOR of (
RealVectSpace the
carrier of X) st v
in W holds (a
* v)
in W
proof
let a be
Real;
let v be
VECTOR of (
RealVectSpace the
carrier of X) such that
A8: v
in W;
reconsider f = (a
* v) as
Functional of X by
FUNCT_2: 66;
A9: f is
additive
proof
let x,y be
VECTOR of X;
reconsider vZ1 = v as
Element of (
Funcs (the
carrier of X,
REAL ));
A10: vZ1 is
linear-Functional of X by
Def7,
A8;
(f
. (x
+ y))
= (a
* (vZ1
. (x
+ y))) by
FUNCSDOM: 4
.= (a
* ((vZ1
. x)
+ (vZ1
. y))) by
A10,
HAHNBAN:def 2
.= ((a
* (vZ1
. x))
+ (a
* (vZ1
. y)))
.= ((f
. x)
+ (a
* (vZ1
. y))) by
FUNCSDOM: 4;
hence (f
. (x
+ y))
= ((f
. x)
+ (f
. y)) by
FUNCSDOM: 4;
end;
f is
homogeneous
proof
let x be
VECTOR of X, s be
Real;
reconsider vZ1 = v as
Element of (
Funcs (the
carrier of X,
REAL ));
A11: vZ1 is
linear-Functional of X by
Def7,
A8;
(f
. (s
* x))
= (a
* (vZ1
. (s
* x))) by
FUNCSDOM: 4
.= (a
* (s
* (vZ1
. x))) by
A11,
HAHNBAN:def 3
.= (s
* (a
* (vZ1
. x)));
hence (f
. (s
* x))
= (s
* (f
. x)) by
FUNCSDOM: 4;
end;
hence thesis by
A9,
Def7;
end;
hence thesis by
A1;
end;
theorem ::
DUALSP01:11
for X be
RealLinearSpace holds
RLSStruct (# (
LinearFunctionals X), (
Zero_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))), (
Add_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))), (
Mult_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))) #) is
Subspace of (
RealVectSpace the
carrier of X) by
Th17,
RSSPACE: 11;
registration
let X be
RealLinearSpace;
cluster
RLSStruct (# (
LinearFunctionals X), (
Zero_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))), (
Add_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))), (
Mult_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))) #) ->
Abelian
add-associative
right_zeroed
right_complementable
scalar-distributive
vector-distributive
scalar-associative
scalar-unital;
coherence by
Th17,
RSSPACE: 11;
end
definition
let X be
RealLinearSpace;
::
DUALSP01:def7
func X
*' ->
strict
RealLinearSpace equals
RLSStruct (# (
LinearFunctionals X), (
Zero_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))), (
Add_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))), (
Mult_ ((
LinearFunctionals X),(
RealVectSpace the
carrier of X))) #);
coherence ;
end
registration
let X be
RealLinearSpace;
cluster (X
*' ) ->
constituted-Functions;
coherence by
MONOID_0: 80;
end
definition
let X be
RealLinearSpace;
let f be
Element of (X
*' );
let v be
VECTOR of X;
:: original:
.
redefine
func f
. v ->
Element of
REAL ;
coherence
proof
reconsider f as
Functional of X by
Def7;
(f
. v) is
Element of
REAL ;
hence thesis;
end;
end
theorem ::
DUALSP01:12
Th20b: for X be
RealLinearSpace, f,g,h be
VECTOR of (X
*' ) holds h
= (f
+ g) iff for x be
VECTOR of X holds (h
. x)
= ((f
. x)
+ (g
. x))
proof
let X be
RealLinearSpace, f,g,h be
VECTOR of (X
*' );
A1: (X
*' ) is
Subspace of (
RealVectSpace the
carrier of X) by
Th17,
RSSPACE: 11;
then
reconsider f1 = f, g1 = g, h1 = h as
VECTOR of (
RealVectSpace the
carrier of X) by
RLSUB_1: 10;
hereby
assume
A3: h
= (f
+ g);
let x be
Element of X;
h1
= (f1
+ g1) by
A1,
A3,
RLSUB_1: 13;
hence (h
. x)
= ((f
. x)
+ (g
. x)) by
FUNCSDOM: 1;
end;
assume for x be
Element of X holds (h
. x)
= ((f
. x)
+ (g
. x));
then h1
= (f1
+ g1) by
FUNCSDOM: 1;
hence h
= (f
+ g) by
A1,
RLSUB_1: 13;
end;
theorem ::
DUALSP01:13
Th21b: for X be
RealLinearSpace, f,h be
VECTOR of (X
*' ), a be
Real holds h
= (a
* f) iff for x be
VECTOR of X holds (h
. x)
= (a
* (f
. x))
proof
let X be
RealLinearSpace;
let f,h be
VECTOR of (X
*' );
let a be
Real;
A1: (X
*' ) is
Subspace of (
RealVectSpace the
carrier of X) by
Th17,
RSSPACE: 11;
then
reconsider f1 = f, h1 = h as
VECTOR of (
RealVectSpace the
carrier of X) by
RLSUB_1: 10;
hereby
assume
A3: h
= (a
* f);
let x be
Element of X;
h1
= (a
* f1) by
A1,
A3,
RLSUB_1: 14;
hence (h
. x)
= (a
* (f
. x)) by
FUNCSDOM: 4;
end;
assume for x be
Element of X holds (h
. x)
= (a
* (f
. x));
then h1
= (a
* f1) by
FUNCSDOM: 4;
hence h
= (a
* f) by
A1,
RLSUB_1: 14;
end;
theorem ::
DUALSP01:14
Th22b: for X be
RealLinearSpace holds (
0. (X
*' ))
= (the
carrier of X
-->
0 )
proof
let X be
RealLinearSpace;
A1: (X
*' ) is
Subspace of (
RealVectSpace the
carrier of X) by
Th17,
RSSPACE: 11;
(
0. (
RealVectSpace the
carrier of X))
= (the
carrier of X
-->
0 );
hence thesis by
A1,
RLSUB_1: 11;
end;
begin
reserve S for
Real_Sequence;
reserve k,n,m,m1 for
Nat;
reserve g,h,r,x for
Real;
definition
let S be
Real_Sequence;
let x be
Real;
::
DUALSP01:def8
func S
- x ->
Real_Sequence means
:
Def14: for n holds (it
. n)
= ((S
. n)
- x);
existence
proof
deffunc
F(
Nat) = ((S
. $1)
- x);
consider S be
Real_Sequence such that
A1: for n be
Nat holds (S
. n)
=
F(n) from
SEQ_1:sch 1;
take S;
let n;
thus thesis by
A1;
end;
uniqueness
proof
let S1,S2 be
Real_Sequence;
assume that
A2: for n holds (S1
. n)
= ((S
. n)
- x) and
A3: for n holds (S2
. n)
= ((S
. n)
- x);
for n be
Nat holds (S1
. n)
= (S2
. n)
proof
let n be
Nat;
(S1
. n)
= ((S
. n)
- x) by
A2;
hence thesis by
A3;
end;
hence thesis;
end;
end
theorem ::
DUALSP01:15
Th121: S is
convergent implies (S
- x) is
convergent & (
lim (S
- x))
= ((
lim S)
- x)
proof
assume
B1: S is
convergent;
set g = (
lim S);
set h = (g
- x);
X1:
now
let r;
assume
0
< r;
then
consider m1 such that
A2: for n st m1
<= n holds
|.((S
. n)
- g).|
< r by
B1,
SEQ_2:def 7;
take k = m1;
let n;
assume
B3: k
<= n;
|.((S
. n)
- g).|
=
|.(((S
. n)
- x)
- h).|
.=
|.(((S
- x)
. n)
- h).| by
Def14;
hence
|.(((S
- x)
. n)
- h).|
< r by
A2,
B3;
end;
hence (S
- x) is
convergent;
hence (
lim (S
- x))
= ((
lim S)
- x) by
X1,
SEQ_2:def 7;
end;
definition
let X be
RealNormSpace;
let IT be
Functional of X;
::
DUALSP01:def9
attr IT is
Lipschitzian means
:
Def8: ex K be
Real st
0
<= K & for x be
VECTOR of X holds
|.(IT
. x).|
<= (K
*
||.x.||);
end
theorem ::
DUALSP01:16
Th21: for X be
RealNormSpace, f be
Functional of X st (for x be
VECTOR of X holds (f
. x)
=
0 ) holds f is
Lipschitzian
proof
let X be
RealNormSpace;
let f be
Functional of X;
assume
A1: for x be
VECTOR of X holds (f
. x)
=
0 ;
take
0 ;
thus thesis by
A1,
COMPLEX1: 44;
end;
Th21X: for X be
RealNormSpace, F be
Functional of X st F
= (the
carrier of X
-->
0 ) holds F is
linear-Functional of X & F is
Lipschitzian
proof
let X be
RealNormSpace, F be
Functional of X;
assume
A1: F
= (the
carrier of X
-->
0 );
then
reconsider F as
linear-Functional of X by
Th23;
for x be
VECTOR of X holds (F
. x)
=
0 by
A1;
hence thesis by
Th21;
end;
registration
let X be
RealNormSpace;
cluster
Lipschitzian for
linear-Functional of X;
existence
proof
set f = (the
carrier of X
-->
0 );
reconsider f as
Function of the
carrier of X,
REAL by
FUNCOP_1: 45,
XREAL_0:def 1;
reconsider f as
Functional of X;
reconsider f as
linear-Functional of X by
Th21X;
f is
Lipschitzian by
Th21X;
hence thesis;
end;
end
definition
let X be
RealNormSpace;
::
DUALSP01:def10
func
BoundedLinearFunctionals X ->
Subset of (X
*' ) means
:
Def9: for x be
set holds x
in it iff x is
Lipschitzian
linear-Functional of X;
existence
proof
defpred
P[
object] means $1 is
Lipschitzian
linear-Functional of X;
consider IT be
set such that
A1: for x be
object holds x
in IT iff x
in (
LinearFunctionals X) &
P[x] from
XBOOLE_0:sch 1;
take IT;
for x be
object st x
in IT holds x
in (
LinearFunctionals X) by
A1;
hence IT is
Subset of (X
*' ) by
TARSKI:def 3;
let x be
set;
thus x
in IT implies x is
Lipschitzian
linear-Functional of X by
A1;
assume
A2: x is
Lipschitzian
linear-Functional of X;
then x
in (
LinearFunctionals X) by
Def7;
hence thesis by
A1,
A2;
end;
uniqueness
proof
let X1,X2 be
Subset of (X
*' );
assume that
A3: for x be
set holds x
in X1 iff x is
Lipschitzian
linear-Functional of X and
A4: for x be
set holds x
in X2 iff x is
Lipschitzian
linear-Functional of X;
now
let x be
object;
assume x
in X2;
then x is
Lipschitzian
linear-Functional of X by
A4;
hence x
in X1 by
A3;
end;
then
A5: X2
c= X1;
now
let x be
object;
assume x
in X1;
then x is
Lipschitzian
linear-Functional of X by
A3;
hence x
in X2 by
A4;
end;
then X1
c= X2;
hence thesis by
A5;
end;
end
registration
let X be
RealNormSpace;
cluster (
BoundedLinearFunctionals X) -> non
empty;
coherence
proof
set f = the
Lipschitzian
linear-Functional of X;
f
in (
BoundedLinearFunctionals X) by
Def9;
hence thesis;
end;
end
theorem ::
DUALSP01:17
Th22: for X be
RealNormSpace holds (
BoundedLinearFunctionals X) is
linearly-closed
proof
let X be
RealNormSpace;
set W = (
BoundedLinearFunctionals X);
A1: for v,u be
VECTOR of (X
*' ) st v
in W & u
in W holds (v
+ u)
in W
proof
let v,u be
VECTOR of (X
*' ) such that
A2: v
in W & u
in W;
reconsider f = (v
+ u) as
linear-Functional of X by
Def7;
f is
Lipschitzian
proof
reconsider v1 = v, u1 = u as
Lipschitzian
Functional of X by
A2,
Def9;
consider K2 be
Real such that
A4:
0
<= K2 and
A5: for x be
VECTOR of X holds
|.(v1
. x).|
<= (K2
*
||.x.||) by
Def8;
consider K1 be
Real such that
A6:
0
<= K1 and
A7: for x be
VECTOR of X holds
|.(u1
. x).|
<= (K1
*
||.x.||) by
Def8;
take K3 = (K1
+ K2);
now
let x be
VECTOR of X;
A8:
|.((u1
. x)
+ (v1
. x)).|
<= (
|.(u1
. x).|
+
|.(v1
. x).|) by
COMPLEX1: 56;
A9:
|.(v1
. x).|
<= (K2
*
||.x.||) by
A5;
|.(u1
. x).|
<= (K1
*
||.x.||) by
A7;
then
A10: (
|.(u1
. x).|
+
|.(v1
. x).|)
<= ((K1
*
||.x.||)
+ (K2
*
||.x.||)) by
A9,
XREAL_1: 7;
|.(f
. x).|
=
|.((u1
. x)
+ (v1
. x)).| by
Th20b;
hence
|.(f
. x).|
<= (K3
*
||.x.||) by
A8,
A10,
XXREAL_0: 2;
end;
hence thesis by
A6,
A4;
end;
hence thesis by
Def9;
end;
for a be
Real, v be
VECTOR of (X
*' ) st v
in W holds (a
* v)
in W
proof
let a be
Real;
let v be
VECTOR of (X
*' ) such that
A11: v
in W;
reconsider f = (a
* v) as
linear-Functional of X by
Def7;
f is
Lipschitzian
proof
reconsider v1 = v as
Lipschitzian
Functional of X by
A11,
Def9;
consider K be
Real such that
A12:
0
<= K and
A13: for x be
VECTOR of X holds
|.(v1
. x).|
<= (K
*
||.x.||) by
Def8;
take (
|.a.|
* K);
A14:
now
let x be
VECTOR of X;
0
<=
|.a.| by
COMPLEX1: 46;
then
A15: (
|.a.|
*
|.(v1
. x).|)
<= (
|.a.|
* (K
*
||.x.||)) by
A13,
XREAL_1: 64;
|.(a
* (v1
. x)).|
= (
|.a.|
*
|.(v1
. x).|) by
COMPLEX1: 65;
hence
|.(f
. x).|
<= ((
|.a.|
* K)
*
||.x.||) by
A15,
Th21b;
end;
0
<=
|.a.| by
COMPLEX1: 46;
hence thesis by
A12,
A14;
end;
hence thesis by
Def9;
end;
hence thesis by
A1;
end;
theorem ::
DUALSP01:18
for X be
RealNormSpace holds
RLSStruct (# (
BoundedLinearFunctionals X), (
Zero_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Add_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Mult_ ((
BoundedLinearFunctionals X),(X
*' ))) #) is
Subspace of (X
*' ) by
Th22,
RSSPACE: 11;
registration
let X be
RealNormSpace;
cluster
RLSStruct (# (
BoundedLinearFunctionals X), (
Zero_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Add_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Mult_ ((
BoundedLinearFunctionals X),(X
*' ))) #) ->
Abelian
add-associative
right_zeroed
right_complementable
vector-distributive
scalar-distributive
scalar-associative
scalar-unital;
coherence by
Th22,
RSSPACE: 11;
end
definition
let X be
RealNormSpace;
::
DUALSP01:def11
func
R_VectorSpace_of_BoundedLinearFunctionals X ->
strict
RealLinearSpace equals
RLSStruct (# (
BoundedLinearFunctionals X), (
Zero_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Add_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Mult_ ((
BoundedLinearFunctionals X),(X
*' ))) #);
coherence ;
end
registration
let X be
RealNormSpace;
cluster ->
Function-like
Relation-like for
Element of (
R_VectorSpace_of_BoundedLinearFunctionals X);
coherence ;
end
definition
let X be
RealNormSpace;
let f be
Element of (
R_VectorSpace_of_BoundedLinearFunctionals X);
let v be
VECTOR of X;
:: original:
.
redefine
func f
. v ->
Element of
REAL ;
coherence
proof
reconsider f as
Functional of X by
Def9;
(f
. v) is
Element of
REAL ;
hence thesis;
end;
end
theorem ::
DUALSP01:19
Th24: for X be
RealNormSpace, f,g,h be
VECTOR of (
R_VectorSpace_of_BoundedLinearFunctionals X) holds h
= (f
+ g) iff for x be
VECTOR of X holds (h
. x)
= ((f
. x)
+ (g
. x))
proof
let X be
RealNormSpace;
let f,g,h be
VECTOR of (
R_VectorSpace_of_BoundedLinearFunctionals X);
A1: (
R_VectorSpace_of_BoundedLinearFunctionals X) is
Subspace of (X
*' ) by
Th22,
RSSPACE: 11;
then
reconsider f1 = f, h1 = h, g1 = g as
VECTOR of (X
*' ) by
RLSUB_1: 10;
hereby
assume
A2: h
= (f
+ g);
let x be
Element of X;
h1
= (f1
+ g1) by
A1,
A2,
RLSUB_1: 13;
hence (h
. x)
= ((f
. x)
+ (g
. x)) by
Th20b;
end;
assume for x be
Element of X holds (h
. x)
= ((f
. x)
+ (g
. x));
then h1
= (f1
+ g1) by
Th20b;
hence thesis by
A1,
RLSUB_1: 13;
end;
theorem ::
DUALSP01:20
Th25: for X be
RealNormSpace, f,h be
VECTOR of (
R_VectorSpace_of_BoundedLinearFunctionals X), a be
Real holds h
= (a
* f) iff for x be
VECTOR of X holds (h
. x)
= (a
* (f
. x))
proof
let X be
RealNormSpace;
let f,h be
VECTOR of (
R_VectorSpace_of_BoundedLinearFunctionals X);
let a be
Real;
A1: (
R_VectorSpace_of_BoundedLinearFunctionals X) is
Subspace of (X
*' ) by
Th22,
RSSPACE: 11;
then
reconsider f1 = f, h1 = h as
VECTOR of (X
*' ) by
RLSUB_1: 10;
hereby
assume
A2: h
= (a
* f);
let x be
Element of X;
h1
= (a
* f1) by
A1,
A2,
RLSUB_1: 14;
hence (h
. x)
= (a
* (f
. x)) by
Th21b;
end;
assume for x be
Element of X holds (h
. x)
= (a
* (f
. x));
then h1
= (a
* f1) by
Th21b;
hence thesis by
A1,
RLSUB_1: 14;
end;
theorem ::
DUALSP01:21
Th26: for X be
RealNormSpace holds (
0. (
R_VectorSpace_of_BoundedLinearFunctionals X))
= (the
carrier of X
-->
0 )
proof
let X be
RealNormSpace;
A1: (
0. (X
*' ))
= (the
carrier of X
-->
0 ) by
Th22b;
(
R_VectorSpace_of_BoundedLinearFunctionals X) is
Subspace of (X
*' ) by
Th22,
RSSPACE: 11;
hence thesis by
A1,
RLSUB_1: 11;
end;
definition
let X be
RealNormSpace;
let f be
object;
::
DUALSP01:def12
func
Bound2Lipschitz (f,X) ->
Lipschitzian
linear-Functional of X equals (
In (f,(
BoundedLinearFunctionals X)));
coherence by
Def9;
end
definition
let X be
RealNormSpace;
let u be
linear-Functional of X;
::
DUALSP01:def13
func
PreNorms u -> non
empty
Subset of
REAL equals {
|.(u
. t).| where t be
VECTOR of X :
||.t.||
<= 1 };
coherence
proof
A1:
now
let x be
object;
now
assume x
in {
|.(u
. t).| where t be
VECTOR of X :
||.t.||
<= 1 };
then ex t be
VECTOR of X st x
=
|.(u
. t).| &
||.t.||
<= 1;
hence x
in
REAL by
XREAL_0:def 1;
end;
hence x
in {
|.(u
. t).| where t be
VECTOR of X :
||.t.||
<= 1 } implies x
in
REAL ;
end;
||.(
0. X).||
=
0 ;
then
|.(u
. (
0. X)).|
in {
|.(u
. t).| where t be
VECTOR of X :
||.t.||
<= 1 };
hence thesis by
A1,
TARSKI:def 3;
end;
end
Th27: for X be
RealNormSpace, g be
Lipschitzian
linear-Functional of X holds (
PreNorms g) is
bounded_above
proof
let X be
RealNormSpace;
let g be
Lipschitzian
linear-Functional of X;
consider K be
Real such that
A1:
0
<= K & for x be
VECTOR of X holds
|.(g
. x).|
<= (K
*
||.x.||) by
Def8;
take K;
let r be
ExtReal;
assume r
in (
PreNorms g);
then
consider t be
VECTOR of X such that
A3: r
=
|.(g
. t).| &
||.t.||
<= 1;
A5:
|.(g
. t).|
<= (K
*
||.t.||) by
A1;
(K
*
||.t.||)
<= (K
* 1) by
A1,
A3,
XREAL_1: 64;
hence r
<= K by
A3,
A5,
XXREAL_0: 2;
end;
registration
let X be
RealNormSpace, g be
Lipschitzian
linear-Functional of X;
cluster (
PreNorms g) ->
bounded_above;
coherence by
Th27;
end
theorem ::
DUALSP01:22
for X be
RealNormSpace, g be
linear-Functional of X holds g is
Lipschitzian iff (
PreNorms g) is
bounded_above
proof
let X be
RealNormSpace;
let g be
linear-Functional of X;
now
reconsider K = (
upper_bound (
PreNorms g)) as
Real;
assume
A1: (
PreNorms g) is
bounded_above;
A2:
now
let t be
VECTOR of X;
per cases ;
suppose
A3: t
= (
0. X);
then
A4:
||.t.||
=
0 ;
(g
. t)
= (g
. (
0
* (
0. X))) by
A3
.= (
0
* (g
. (
0. X))) by
HAHNBAN:def 3
.=
0 ;
hence
|.(g
. t).|
<= (K
*
||.t.||) by
A4,
COMPLEX1: 44;
end;
suppose
A5: t
<> (
0. X);
reconsider t1 = ((
||.t.||
" )
* t) as
VECTOR of X;
A6:
||.t.||
<>
0 by
A5,
NORMSP_0:def 5;
A7: ((
|.(g
. t).|
/
||.t.||)
*
||.t.||)
= ((
|.(g
. t).|
* (
||.t.||
" ))
*
||.t.||) by
XCMPLX_0:def 9
.= (
|.(g
. t).|
* ((
||.t.||
" )
*
||.t.||))
.= (
|.(g
. t).|
* 1) by
A6,
XCMPLX_0:def 7
.=
|.(g
. t).|;
A8:
|.(
||.t.||
" ).|
=
|.(1
* (
||.t.||
" )).|
.=
|.(1
/
||.t.||).| by
XCMPLX_0:def 9
.= (1
/
||.t.||) by
ABSVALUE:def 1
.= (1
* (
||.t.||
" )) by
XCMPLX_0:def 9
.= (
||.t.||
" );
||.t1.||
= (
|.(
||.t.||
" ).|
*
||.t.||) by
NORMSP_1:def 1
.= 1 by
A6,
A8,
XCMPLX_0:def 7;
then
A9:
|.(g
. t1).|
in {
|.(g
. s).| where s be
VECTOR of X :
||.s.||
<= 1 };
(
|.(g
. t).|
/
||.t.||)
= (
|.(g
. t).|
* (
||.t.||
" )) by
XCMPLX_0:def 9
.=
|.((
||.t.||
" )
* (g
. t)).| by
A8,
COMPLEX1: 65
.=
|.(g
. t1).| by
HAHNBAN:def 3;
then (
|.(g
. t).|
/
||.t.||)
<= K by
A1,
A9,
SEQ_4:def 1;
hence
|.(g
. t).|
<= (K
*
||.t.||) by
A7,
XREAL_1: 64;
end;
end;
take K;
0
<= K
proof
consider r0 be
object such that
A10: r0
in (
PreNorms g) by
XBOOLE_0:def 1;
reconsider r0 as
Real by
A10;
now
let r be
Real;
assume r
in (
PreNorms g);
then ex t be
VECTOR of X st r
=
|.(g
. t).| &
||.t.||
<= 1;
hence
0
<= r by
COMPLEX1: 46;
end;
then
0
<= r0 by
A10;
hence thesis by
A1,
A10,
SEQ_4:def 1;
end;
hence g is
Lipschitzian by
A2;
end;
hence thesis;
end;
definition
let X be
RealNormSpace;
::
DUALSP01:def14
func
BoundedLinearFunctionalsNorm X ->
Function of (
BoundedLinearFunctionals X),
REAL means
:
Def13: for x be
object st x
in (
BoundedLinearFunctionals X) holds (it
. x)
= (
upper_bound (
PreNorms (
Bound2Lipschitz (x,X))));
existence
proof
deffunc
F(
object) = (
upper_bound (
PreNorms (
Bound2Lipschitz ($1,X))));
A1: for z be
object st z
in (
BoundedLinearFunctionals X) holds
F(z)
in
REAL by
XREAL_0:def 1;
thus ex f be
Function of (
BoundedLinearFunctionals X),
REAL st for x be
object st x
in (
BoundedLinearFunctionals X) holds (f
. x)
=
F(x) from
FUNCT_2:sch 2(
A1);
end;
uniqueness
proof
let NORM1,NORM2 be
Function of (
BoundedLinearFunctionals X),
REAL such that
A2: for x be
object st x
in (
BoundedLinearFunctionals X) holds (NORM1
. x)
= (
upper_bound (
PreNorms (
Bound2Lipschitz (x,X)))) and
A3: for x be
object st x
in (
BoundedLinearFunctionals X) holds (NORM2
. x)
= (
upper_bound (
PreNorms (
Bound2Lipschitz (x,X))));
for z be
object st z
in (
BoundedLinearFunctionals X) holds (NORM1
. z)
= (NORM2
. z)
proof
let z be
object such that
A5: z
in (
BoundedLinearFunctionals X);
(NORM1
. z)
= (
upper_bound (
PreNorms (
Bound2Lipschitz (z,X)))) by
A2,
A5;
hence thesis by
A3,
A5;
end;
hence thesis;
end;
end
theorem ::
DUALSP01:23
Th29: for X be
RealNormSpace, f be
Lipschitzian
linear-Functional of X holds (
Bound2Lipschitz (f,X))
= f
proof
let X be
RealNormSpace;
let f be
Lipschitzian
linear-Functional of X;
f
in (
BoundedLinearFunctionals X) by
Def9;
hence thesis by
SUBSET_1:def 8;
end;
theorem ::
DUALSP01:24
Th30: for X be
RealNormSpace, f be
Lipschitzian
linear-Functional of X holds ((
BoundedLinearFunctionalsNorm X)
. f)
= (
upper_bound (
PreNorms f))
proof
let X be
RealNormSpace;
let f be
Lipschitzian
linear-Functional of X;
reconsider f9 = f as
set;
f
in (
BoundedLinearFunctionals X) by
Def9;
hence ((
BoundedLinearFunctionalsNorm X)
. f)
= (
upper_bound (
PreNorms (
Bound2Lipschitz (f9,X)))) by
Def13
.= (
upper_bound (
PreNorms f)) by
Th29;
end;
definition
let X be
RealNormSpace;
::
DUALSP01:def15
func
DualSp X -> non
empty
NORMSTR equals
NORMSTR (# (
BoundedLinearFunctionals X), (
Zero_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Add_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Mult_ ((
BoundedLinearFunctionals X),(X
*' ))), (
BoundedLinearFunctionalsNorm X) #);
coherence ;
end
theorem ::
DUALSP01:25
Th31: for X be
RealNormSpace holds (the
carrier of X
-->
0 )
= (
0. (
DualSp X))
proof
let X be
RealNormSpace;
(the
carrier of X
-->
0 )
= (
0. (
R_VectorSpace_of_BoundedLinearFunctionals X)) by
Th26
.= (
0. (
DualSp X));
hence thesis;
end;
theorem ::
DUALSP01:26
Th32: for X be
RealNormSpace, f be
Point of (
DualSp X), g be
Lipschitzian
linear-Functional of X st g
= f holds for t be
VECTOR of X holds
|.(g
. t).|
<= (
||.f.||
*
||.t.||)
proof
let X be
RealNormSpace;
let f be
Point of (
DualSp X);
let g be
Lipschitzian
linear-Functional of X such that
A1: g
= f;
now
let t be
VECTOR of X;
per cases ;
suppose
A3: t
= (
0. X);
then
A4:
||.t.||
=
0 ;
(g
. t)
= (g
. (
0
* (
0. X))) by
A3
.= (
0
* (g
. (
0. X))) by
HAHNBAN:def 3
.=
0 ;
hence
|.(g
. t).|
<= (
||.f.||
*
||.t.||) by
A4,
COMPLEX1: 44;
end;
suppose
A5: t
<> (
0. X);
reconsider t1 = ((
||.t.||
" )
* t) as
VECTOR of X;
A6:
||.t.||
<>
0 by
A5,
NORMSP_0:def 5;
A7:
|.(
||.t.||
" ).|
=
|.(1
* (
||.t.||
" )).|
.=
|.(1
/
||.t.||).| by
XCMPLX_0:def 9
.= (1
/
||.t.||) by
ABSVALUE:def 1
.= (1
* (
||.t.||
" )) by
XCMPLX_0:def 9
.= (
||.t.||
" );
A8: (
|.(g
. t).|
/
||.t.||)
= (
|.(g
. t).|
* (
||.t.||
" )) by
XCMPLX_0:def 9
.=
|.((
||.t.||
" )
* (g
. t)).| by
A7,
COMPLEX1: 65
.=
|.(g
. t1).| by
HAHNBAN:def 3;
||.t1.||
= (
|.(
||.t.||
" ).|
*
||.t.||) by
NORMSP_1:def 1
.= 1 by
A6,
A7,
XCMPLX_0:def 7;
then (
|.(g
. t).|
/
||.t.||)
in {
|.(g
. s).| where s be
VECTOR of X :
||.s.||
<= 1 } by
A8;
then (
|.(g
. t).|
/
||.t.||)
<= (
upper_bound (
PreNorms g)) by
SEQ_4:def 1;
then
A9: (
|.(g
. t).|
/
||.t.||)
<=
||.f.|| by
A1,
Th30;
((
|.(g
. t).|
/
||.t.||)
*
||.t.||)
= ((
|.(g
. t).|
* (
||.t.||
" ))
*
||.t.||) by
XCMPLX_0:def 9
.= (
|.(g
. t).|
* ((
||.t.||
" )
*
||.t.||))
.= (
|.(g
. t).|
* 1) by
A6,
XCMPLX_0:def 7
.=
|.(g
. t).|;
hence
|.(g
. t).|
<= (
||.f.||
*
||.t.||) by
A9,
XREAL_1: 64;
end;
end;
hence thesis;
end;
theorem ::
DUALSP01:27
Th33: for X be
RealNormSpace, f be
Point of (
DualSp X) holds
0
<=
||.f.||
proof
let X be
RealNormSpace;
let f be
Point of (
DualSp X);
reconsider g = f as
Lipschitzian
linear-Functional of X by
Def9;
consider r0 be
object such that
A1: r0
in (
PreNorms g) by
XBOOLE_0:def 1;
reconsider r0 as
Real by
A1;
A3: ((
BoundedLinearFunctionalsNorm X)
. f)
= (
upper_bound (
PreNorms g)) by
Th30;
now
let r be
Real;
assume r
in (
PreNorms g);
then ex t be
VECTOR of X st r
=
|.(g
. t).| &
||.t.||
<= 1;
hence
0
<= r by
COMPLEX1: 46;
end;
then
0
<= r0 by
A1;
hence thesis by
A1,
SEQ_4:def 1,
A3;
end;
theorem ::
DUALSP01:28
Th34: for X,Y be
RealNormSpace holds for f be
Point of (
DualSp X) st f
= (
0. (
DualSp X)) holds
0
=
||.f.||
proof
let X,Y be
RealNormSpace;
let f be
Point of (
DualSp X) such that
A1: f
= (
0. (
DualSp X));
thus
||.f.||
=
0
proof
reconsider g = f as
Lipschitzian
linear-Functional of X by
Def9;
set z = (the
carrier of X
-->
0 );
reconsider z as
Function of the
carrier of X,
REAL by
FUNCOP_1: 45,
XREAL_0:def 1;
consider r0 be
object such that
A2: r0
in (
PreNorms g) by
XBOOLE_0:def 1;
reconsider r0 as
Real by
A2;
A3: (for s be
Real st s
in (
PreNorms g) holds s
<=
0 ) implies (
upper_bound (
PreNorms g))
<=
0 by
SEQ_4: 45;
A5: z
= g by
A1,
Th31;
A6:
now
let r be
Real;
assume r
in (
PreNorms g);
then ex t be
VECTOR of X st r
=
|.(g
. t).| &
||.t.||
<= 1;
hence
0
<= r & r
<=
0 by
A5,
COMPLEX1: 44;
end;
then
0
<= r0 by
A2;
then (
upper_bound (
PreNorms g))
=
0 by
A6,
A2,
A3,
SEQ_4:def 1;
hence thesis by
Th30;
end;
end;
registration
let X be
RealNormSpace;
cluster ->
Function-like
Relation-like for
Element of (
DualSp X);
coherence ;
end
definition
let X be
RealNormSpace;
let f be
Element of (
DualSp X);
let v be
VECTOR of X;
:: original:
.
redefine
func f
. v ->
Element of
REAL ;
coherence
proof
reconsider f as
linear-Functional of X by
Def9;
(f
. v) is
Element of
REAL ;
hence thesis;
end;
end
theorem ::
DUALSP01:29
Th35: for X be
RealNormSpace, f,g,h be
Point of (
DualSp X) holds h
= (f
+ g) iff for x be
VECTOR of X holds (h
. x)
= ((f
. x)
+ (g
. x))
proof
let X be
RealNormSpace;
let f,g,h be
Point of (
DualSp X);
reconsider f1 = f, g1 = g, h1 = h as
VECTOR of (
R_VectorSpace_of_BoundedLinearFunctionals X);
h
= (f
+ g) iff h1
= (f1
+ g1);
hence thesis by
Th24;
end;
theorem ::
DUALSP01:30
Th36: for X be
RealNormSpace, f,h be
Point of (
DualSp X), a be
Real holds h
= (a
* f) iff for x be
VECTOR of X holds (h
. x)
= (a
* (f
. x))
proof
let X be
RealNormSpace;
let f,h be
Point of (
DualSp X);
let a be
Real;
reconsider f1 = f, h1 = h as
VECTOR of (
R_VectorSpace_of_BoundedLinearFunctionals X);
h
= (a
* f) iff h1
= (a
* f1);
hence thesis by
Th25;
end;
theorem ::
DUALSP01:31
Th37: for X be
RealNormSpace, f,g be
Point of (
DualSp X), a be
Real holds (
||.f.||
=
0 iff f
= (
0. (
DualSp X))) &
||.(a
* f).||
= (
|.a.|
*
||.f.||) &
||.(f
+ g).||
<= (
||.f.||
+
||.g.||)
proof
let X be
RealNormSpace;
let f,g be
Point of (
DualSp X);
let a be
Real;
A1:
now
assume
A2: f
= (
0. (
DualSp X));
reconsider g = f as
Lipschitzian
linear-Functional of X by
Def9;
set z = (the
carrier of X
-->
0 );
reconsider z as
Function of the
carrier of X,
REAL by
FUNCOP_1: 45,
XREAL_0:def 1;
consider r0 be
object such that
A3: r0
in (
PreNorms g) by
XBOOLE_0:def 1;
reconsider r0 as
Real by
A3;
A4: (for s be
Real st s
in (
PreNorms g) holds s
<=
0 ) implies (
upper_bound (
PreNorms g))
<=
0 by
SEQ_4: 45;
A6: z
= g by
A2,
Th31;
A7:
now
let r be
Real;
assume r
in (
PreNorms g);
then
consider t be
VECTOR of X such that
A8: r
=
|.(g
. t).| and
||.t.||
<= 1;
thus
0
<= r & r
<=
0 by
A8,
A6,
COMPLEX1: 44;
end;
then
0
<= r0 by
A3;
then (
upper_bound (
PreNorms g))
=
0 by
A7,
A3,
A4,
SEQ_4:def 1;
hence
||.f.||
=
0 by
Th30;
end;
A9:
||.(f
+ g).||
<= (
||.f.||
+
||.g.||)
proof
reconsider f1 = f, g1 = g, h1 = (f
+ g) as
Lipschitzian
linear-Functional of X by
Def9;
A10: (for s be
Real st s
in (
PreNorms h1) holds s
<= (
||.f.||
+
||.g.||)) implies (
upper_bound (
PreNorms h1))
<= (
||.f.||
+
||.g.||) by
SEQ_4: 45;
A11:
now
let t be
VECTOR of X such that
A12:
||.t.||
<= 1;
0
<=
||.f.|| &
0
<=
||.g.|| by
Th33;
then (
||.f.||
*
||.t.||)
<= (
||.f.||
* 1) & (
||.g.||
*
||.t.||)
<= (
||.g.||
* 1) by
A12,
XREAL_1: 64;
then
A14: ((
||.f.||
*
||.t.||)
+ (
||.g.||
*
||.t.||))
<= ((
||.f.||
* 1)
+ (
||.g.||
* 1)) by
XREAL_1: 7;
A15:
|.((f1
. t)
+ (g1
. t)).|
<= (
|.(f1
. t).|
+
|.(g1
. t).|) by
COMPLEX1: 56;
|.(g1
. t).|
<= (
||.g.||
*
||.t.||) &
|.(f1
. t).|
<= (
||.f.||
*
||.t.||) by
Th32;
then (
|.(f1
. t).|
+
|.(g1
. t).|)
<= ((
||.f.||
*
||.t.||)
+ (
||.g.||
*
||.t.||)) by
XREAL_1: 7;
then
A17: (
|.(f1
. t).|
+
|.(g1
. t).|)
<= (
||.f.||
+
||.g.||) by
A14,
XXREAL_0: 2;
|.(h1
. t).|
=
|.((f1
. t)
+ (g1
. t)).| by
Th35;
hence
|.(h1
. t).|
<= (
||.f.||
+
||.g.||) by
A15,
A17,
XXREAL_0: 2;
end;
now
let r be
Real;
assume r
in (
PreNorms h1);
then ex t be
VECTOR of X st r
=
|.(h1
. t).| &
||.t.||
<= 1;
hence r
<= (
||.f.||
+
||.g.||) by
A11;
end;
hence thesis by
A10,
Th30;
end;
A19:
||.(a
* f).||
= (
|.a.|
*
||.f.||)
proof
reconsider f1 = f, h1 = (a
* f) as
Lipschitzian
linear-Functional of X by
Def9;
A21:
now
A22:
0
<=
||.f.|| by
Th33;
let t be
VECTOR of X;
assume
||.t.||
<= 1;
then
A23: (
||.f.||
*
||.t.||)
<= (
||.f.||
* 1) by
A22,
XREAL_1: 64;
|.(f1
. t).|
<= (
||.f.||
*
||.t.||) by
Th32;
then
A24:
|.(f1
. t).|
<=
||.f.|| by
A23,
XXREAL_0: 2;
A25:
|.(a
* (f1
. t)).|
= (
|.a.|
*
|.(f1
. t).|) by
COMPLEX1: 65;
A26:
0
<=
|.a.| by
COMPLEX1: 46;
|.(h1
. t).|
=
|.(a
* (f1
. t)).| by
Th36;
hence
|.(h1
. t).|
<= (
|.a.|
*
||.f.||) by
A25,
A24,
A26,
XREAL_1: 64;
end;
A27:
now
let r be
Real;
assume r
in (
PreNorms h1);
then ex t be
VECTOR of X st r
=
|.(h1
. t).| &
||.t.||
<= 1;
hence r
<= (
|.a.|
*
||.f.||) by
A21;
end;
A28:
now
per cases ;
case
A29: a
<>
0 ;
A30:
now
A31:
0
<=
||.(a
* f).|| by
Th33;
let t be
VECTOR of X;
assume
||.t.||
<= 1;
then
A32: (
||.(a
* f).||
*
||.t.||)
<= (
||.(a
* f).||
* 1) by
A31,
XREAL_1: 64;
|.(h1
. t).|
<= (
||.(a
* f).||
*
||.t.||) by
Th32;
then
A33:
|.(h1
. t).|
<=
||.(a
* f).|| by
A32,
XXREAL_0: 2;
(h1
. t)
= (a
* (f1
. t)) by
Th36;
then
A34: ((a
" )
* (h1
. t))
= (((a
" )
* a)
* (f1
. t))
.= (1
* (f1
. t)) by
A29,
XCMPLX_0:def 7
.= (f1
. t);
A35:
|.(a
" ).|
=
|.(1
* (a
" )).|
.=
|.(1
/ a).| by
XCMPLX_0:def 9
.= (1
/
|.a.|) by
ABSVALUE: 7
.= (1
* (
|.a.|
" )) by
XCMPLX_0:def 9
.= (
|.a.|
" );
A36:
0
<=
|.(a
" ).| by
COMPLEX1: 46;
|.((a
" )
* (h1
. t)).|
= (
|.(a
" ).|
*
|.(h1
. t).|) by
COMPLEX1: 65;
hence
|.(f1
. t).|
<= ((
|.a.|
" )
*
||.(a
* f).||) by
A34,
A33,
A36,
A35,
XREAL_1: 64;
end;
A37:
now
let r be
Real;
assume r
in (
PreNorms f1);
then ex t be
VECTOR of X st r
=
|.(f1
. t).| &
||.t.||
<= 1;
hence r
<= ((
|.a.|
" )
*
||.(a
* f).||) by
A30;
end;
A38: (for s be
Real st s
in (
PreNorms f1) holds s
<= ((
|.a.|
" )
*
||.(a
* f).||)) implies (
upper_bound (
PreNorms f1))
<= ((
|.a.|
" )
*
||.(a
* f).||) by
SEQ_4: 45;
A39:
0
<=
|.a.| by
COMPLEX1: 46;
||.f.||
<= ((
|.a.|
" )
*
||.(a
* f).||) by
A37,
A38,
Th30;
then (
|.a.|
*
||.f.||)
<= (
|.a.|
* ((
|.a.|
" )
*
||.(a
* f).||)) by
A39,
XREAL_1: 64;
then
A40: (
|.a.|
*
||.f.||)
<= ((
|.a.|
* (
|.a.|
" ))
*
||.(a
* f).||);
|.a.|
<>
0 by
A29,
COMPLEX1: 47;
then (
|.a.|
*
||.f.||)
<= (1
*
||.(a
* f).||) by
A40,
XCMPLX_0:def 7;
hence (
|.a.|
*
||.f.||)
<=
||.(a
* f).||;
end;
case
A41: a
=
0 ;
reconsider fz = f as
VECTOR of (
R_VectorSpace_of_BoundedLinearFunctionals X);
A42: (a
* f)
= (a
* fz)
.= (
0. (
R_VectorSpace_of_BoundedLinearFunctionals X)) by
A41,
RLVECT_1: 10
.= (
0. (
DualSp X));
thus (
|.a.|
*
||.f.||)
= (
0
*
||.f.||) by
A41,
ABSVALUE: 2
.=
||.(a
* f).|| by
A42,
Th34;
end;
end;
((
BoundedLinearFunctionalsNorm X)
. (a
* f))
= (
upper_bound (
PreNorms h1)) by
Th30;
then
||.(a
* f).||
<= (
|.a.|
*
||.f.||) by
A27,
SEQ_4: 45;
hence thesis by
A28,
XXREAL_0: 1;
end;
now
reconsider g = f as
Lipschitzian
linear-Functional of X by
Def9;
set z = (the
carrier of X
-->
0 );
reconsider z as
Function of the
carrier of X,
REAL by
FUNCOP_1: 45,
XREAL_0:def 1;
assume
A43:
||.f.||
=
0 ;
now
let t be
VECTOR of X;
|.(g
. t).|
<= (
||.f.||
*
||.t.||) by
Th32;
then
|.(g
. t).|
=
0 by
A43,
COMPLEX1: 46;
hence (g
. t)
=
0 by
COMPLEX1: 45
.= (z
. t);
end;
then g
= z;
hence f
= (
0. (
DualSp X)) by
Th31;
end;
hence thesis by
A1,
A19,
A9;
end;
registration
let X be
RealNormSpace;
cluster (
DualSp X) ->
reflexive
discerning
RealNormSpace-like;
correctness by
Th37;
end
theorem ::
DUALSP01:32
Th39: for X be
RealNormSpace holds (
DualSp X) is
RealNormSpace
proof
let X be
RealNormSpace;
RLSStruct (# (
BoundedLinearFunctionals X), (
Zero_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Add_ ((
BoundedLinearFunctionals X),(X
*' ))), (
Mult_ ((
BoundedLinearFunctionals X),(X
*' ))) #) is
RealLinearSpace;
hence thesis by
RSSPACE3: 2;
end;
registration
let X be
RealNormSpace;
cluster (
DualSp X) ->
reflexive
discerning
RealNormSpace-like
vector-distributive
scalar-distributive
scalar-associative
scalar-unital
Abelian
add-associative
right_zeroed
right_complementable;
coherence by
Th39;
end
theorem ::
DUALSP01:33
Th40: for X be
RealNormSpace, f,g,h be
Point of (
DualSp X) holds h
= (f
- g) iff for x be
VECTOR of X holds (h
. x)
= ((f
. x)
- (g
. x))
proof
let X be
RealNormSpace;
let f,g,h be
Point of (
DualSp X);
reconsider f9 = f, g9 = g, h9 = h as
Lipschitzian
linear-Functional of X by
Def9;
hereby
assume h
= (f
- g);
then (h
+ g)
= (f
- (g
- g)) by
RLVECT_1: 29;
then
A11: (h
+ g)
= (f
- (
0. (
DualSp X))) by
RLVECT_1: 15;
now
let x be
VECTOR of X;
(f9
. x)
= ((h9
. x)
+ (g9
. x)) by
A11,
Th35;
hence ((f9
. x)
- (g9
. x))
= (h9
. x);
end;
hence for x be
VECTOR of X holds (h
. x)
= ((f
. x)
- (g
. x));
end;
assume
A2: for x be
VECTOR of X holds (h
. x)
= ((f
. x)
- (g
. x));
now
let x be
VECTOR of X;
(h9
. x)
= ((f9
. x)
- (g9
. x)) by
A2;
hence ((h9
. x)
+ (g9
. x))
= (f9
. x);
end;
then f
= (h
+ g) by
Th35;
then (f
- g)
= (h
+ (g
- g)) by
RLVECT_1:def 3;
then (f
- g)
= (h
+ (
0. (
DualSp X))) by
RLVECT_1: 15;
hence thesis;
end;
Lm3: for e be
Real, seq be
Real_Sequence st (seq is
convergent & ex k be
Nat st for i be
Nat st k
<= i holds (seq
. i)
<= e) holds (
lim seq)
<= e
proof
let e be
Real;
let seq be
Real_Sequence such that
A1: seq is
convergent and
A2: ex k be
Nat st for i be
Nat st k
<= i holds (seq
. i)
<= e;
consider k be
Nat such that
A3: for i be
Nat st k
<= i holds (seq
. i)
<= e by
A2;
reconsider ee = e as
Element of
REAL by
XREAL_0:def 1;
set cseq = (
seq_const e);
A4: (
lim cseq)
= (cseq
.
0 ) by
SEQ_4: 26
.= e;
A5:
now
let i be
Nat;
A6: ((seq
^\ k)
. i)
= (seq
. (k
+ i)) by
NAT_1:def 3;
(seq
. (k
+ i))
<= e by
A3,
NAT_1: 11;
hence ((seq
^\ k)
. i)
<= (cseq
. i) by
A6,
SEQ_1: 57;
end;
(
lim (seq
^\ k))
= (
lim seq) by
A1,
SEQ_4: 20;
hence thesis by
A1,
A5,
A4,
SEQ_2: 18;
end;
definition
let X be
RealNormSpace;
let s be
sequence of (
DualSp X), n be
Nat;
:: original:
.
redefine
func s
. n ->
Element of (
DualSp X) ;
coherence
proof
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
(s
. n) is
Element of (
DualSp X);
hence thesis;
end;
end
theorem ::
DUALSP01:34
Th42: for X be
RealNormSpace, seq be
sequence of (
DualSp X) st seq is
Cauchy_sequence_by_Norm holds seq is
convergent
proof
let X be
RealNormSpace;
let vseq be
sequence of (
DualSp X) such that
A2: vseq is
Cauchy_sequence_by_Norm;
defpred
P[
set,
set] means ex xseq be
sequence of
REAL st (for n be
Nat holds (xseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. $1)) & xseq is
convergent & $2
= (
lim xseq);
A3: for x be
Element of X holds ex y be
Element of
REAL st
P[x, y]
proof
let x be
Element of X;
deffunc
F(
Nat) = ((
Bound2Lipschitz ((vseq
. $1),X))
. x);
consider xseq be
Real_Sequence such that
A4: for n be
Nat holds (xseq
. n)
=
F(n) from
SEQ_1:sch 1;
reconsider y = (
lim xseq) as
Element of
REAL by
XREAL_0:def 1;
take y;
A6: for m,k be
Nat holds
|.((xseq
. m)
- (xseq
. k)).|
<= (
||.((vseq
. m)
- (vseq
. k)).||
*
||.x.||)
proof
let m,k be
Nat;
reconsider h1 = ((vseq
. m)
- (vseq
. k)) as
Lipschitzian
linear-Functional of X by
Def9;
A7: (xseq
. k)
= ((
Bound2Lipschitz ((vseq
. k),X))
. x) & (xseq
. m)
= ((
Bound2Lipschitz ((vseq
. m),X))
. x) by
A4;
(vseq
. m) is
Lipschitzian
linear-Functional of X & (vseq
. k) is
Lipschitzian
linear-Functional of X by
Def9;
then (
Bound2Lipschitz ((vseq
. m),X))
= (vseq
. m) & (
Bound2Lipschitz ((vseq
. k),X))
= (vseq
. k) by
Th29;
then ((xseq
. m)
- (xseq
. k))
= (h1
. x) by
A7,
Th40;
hence thesis by
Th32;
end;
now
let e be
Real such that
A10: e
>
0 ;
per cases ;
suppose
A11: x
= (
0. X);
reconsider k =
0 as
Nat;
take k;
thus for n be
Nat st n
>= k holds
|.((xseq
. n)
- (xseq
. k)).|
< e
proof
let n be
Nat such that n
>= k;
A12: (xseq
. k)
= ((
Bound2Lipschitz ((vseq
. k),X))
. (
0
* x)) by
A4,
A11
.= (
0
* ((
Bound2Lipschitz ((vseq
. k),X))
. x)) by
HAHNBAN:def 3;
(xseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. (
0
* x)) by
A4,
A11
.= (
0
* ((
Bound2Lipschitz ((vseq
. n),X))
. x)) by
HAHNBAN:def 3;
hence thesis by
A10,
A12,
COMPLEX1: 44;
end;
end;
suppose x
<> (
0. X);
then
A13:
||.x.||
<>
0 by
NORMSP_0:def 5;
then
consider k be
Nat such that
X2: for n,m be
Nat st n
>= k & m
>= k holds
||.((vseq
. n)
- (vseq
. m)).||
< (e
/
||.x.||) by
A10,
A2,
RSSPACE3: 8;
take k;
thus for n be
Nat st n
>= k holds
|.((xseq
. n)
- (xseq
. k)).|
< e
proof
let n be
Nat;
assume n
>= k;
then
||.((vseq
. n)
- (vseq
. k)).||
< (e
/
||.x.||) by
X2;
then
A18: (
||.((vseq
. n)
- (vseq
. k)).||
*
||.x.||)
< ((e
/
||.x.||)
*
||.x.||) by
A13,
XREAL_1: 68;
A19: ((e
/
||.x.||)
*
||.x.||)
= ((e
* (
||.x.||
" ))
*
||.x.||) by
XCMPLX_0:def 9
.= (e
* ((
||.x.||
" )
*
||.x.||))
.= (e
* 1) by
A13,
XCMPLX_0:def 7;
|.((xseq
. n)
- (xseq
. k)).|
<= (
||.((vseq
. n)
- (vseq
. k)).||
*
||.x.||) by
A6;
hence thesis by
A18,
A19,
XXREAL_0: 2;
end;
end;
end;
hence thesis by
A4,
SEQ_4: 41;
end;
consider f be
Function of the
carrier of X,
REAL such that
A20: for x be
Element of X holds
P[x, (f
. x)] from
FUNCT_2:sch 3(
A3);
reconsider tseq = f as
Function of the
carrier of X,
REAL ;
A21:
now
let x,y be
VECTOR of X;
consider xseq be
sequence of
REAL such that
A22: (for n be
Nat holds (xseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. x)) & xseq is
convergent & (tseq
. x)
= (
lim xseq) by
A20;
consider zseq be
sequence of
REAL such that
A25: (for n be
Nat holds (zseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. (x
+ y))) & zseq is
convergent & (tseq
. (x
+ y))
= (
lim zseq) by
A20;
consider yseq be
sequence of
REAL such that
A27: (for n be
Nat holds (yseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. y)) & yseq is
convergent & (tseq
. y)
= (
lim yseq) by
A20;
now
let n be
Nat;
thus (zseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. (x
+ y)) by
A25
.= (((
Bound2Lipschitz ((vseq
. n),X))
. x)
+ ((
Bound2Lipschitz ((vseq
. n),X))
. y)) by
HAHNBAN:def 2
.= ((xseq
. n)
+ ((
Bound2Lipschitz ((vseq
. n),X))
. y)) by
A22
.= ((xseq
. n)
+ (yseq
. n)) by
A27;
end;
then zseq
= (xseq
+ yseq) by
SEQ_1: 7;
hence (tseq
. (x
+ y))
= ((tseq
. x)
+ (tseq
. y)) by
A22,
A27,
A25,
SEQ_2: 6;
end;
now
let x be
VECTOR of X;
let a be
Real;
consider xseq be
sequence of
REAL such that
A30: (for n be
Nat holds (xseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. x)) & xseq is
convergent & (tseq
. x)
= (
lim xseq) by
A20;
consider zseq be
sequence of
REAL such that
A33: (for n be
Nat holds (zseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. (a
* x))) & zseq is
convergent & (tseq
. (a
* x))
= (
lim zseq) by
A20;
now
let n be
Nat;
thus (zseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. (a
* x)) by
A33
.= (a
* ((
Bound2Lipschitz ((vseq
. n),X))
. x)) by
HAHNBAN:def 3
.= (a
* (xseq
. n)) by
A30;
end;
then zseq
= (a
(#) xseq) by
SEQ_1: 9;
hence (tseq
. (a
* x))
= (a
* (tseq
. x)) by
A30,
A33,
SEQ_2: 8;
end;
then
reconsider tseq as
linear-Functional of X by
A21,
HAHNBAN:def 2,
HAHNBAN:def 3;
B40:
now
let e be
Real;
assume e
>
0 ;
then
consider k be
Nat such that
A36: for n,m be
Nat st n
>= k & m
>= k holds
||.((vseq
. n)
- (vseq
. m)).||
< e by
A2,
RSSPACE3: 8;
take k;
hereby
let m be
Nat;
assume m
>= k;
then
A37:
||.((vseq
. m)
- (vseq
. k)).||
< e by
A36;
A38:
||.(vseq
. m).||
= (
||.vseq.||
. m) &
||.(vseq
. k).||
= (
||.vseq.||
. k) by
NORMSP_0:def 4;
|.(
||.(vseq
. m).||
-
||.(vseq
. k).||).|
<=
||.((vseq
. m)
- (vseq
. k)).|| by
NORMSP_1: 9;
hence
|.((
||.vseq.||
. m)
- (
||.vseq.||
. k)).|
< e by
A38,
A37,
XXREAL_0: 2;
end;
end;
then
A40:
||.vseq.|| is
convergent by
SEQ_4: 41;
A41: tseq is
Lipschitzian
proof
take (
lim
||.vseq.||);
A42:
now
let x be
VECTOR of X;
consider xseq be
sequence of
REAL such that
A43: (for n be
Nat holds (xseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. x)) & xseq is
convergent & (tseq
. x)
= (
lim xseq) by
A20;
A46:
|.(tseq
. x).|
= (
lim
|.xseq.|) by
A43,
SEQ_4: 14;
A49: for n be
Nat holds (
|.xseq.|
. n)
<= ((
||.x.||
(#)
||.vseq.||)
. n)
proof
let n be
Nat;
A50: (
|.xseq.|
. n)
=
|.(xseq
. n).| by
SEQ_1: 12;
A51:
||.(vseq
. n).||
= (
||.vseq.||
. n) by
NORMSP_0:def 4;
A48: (xseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. x) by
A43;
(vseq
. n) is
Lipschitzian
linear-Functional of X by
Def9;
then
|.(xseq
. n).|
<= (
||.(vseq
. n).||
*
||.x.||) by
A48,
Th29,
Th32;
hence thesis by
A50,
A51,
SEQ_1: 9;
end;
(
lim (
||.x.||
(#)
||.vseq.||))
= ((
lim
||.vseq.||)
*
||.x.||) by
B40,
SEQ_4: 41,
SEQ_2: 8;
hence
|.(tseq
. x).|
<= ((
lim
||.vseq.||)
*
||.x.||) by
A46,
A49,
A40,
SEQ_2: 18,
A43;
end;
now
let n be
Nat;
||.(vseq
. n).||
>=
0 ;
hence (
||.vseq.||
. n)
>=
0 by
NORMSP_0:def 4;
end;
hence thesis by
B40,
SEQ_4: 41,
A42,
SEQ_2: 17;
end;
A54: for e be
Real st e
>
0 holds ex k be
Nat st for n be
Nat st n
>= k holds for x be
VECTOR of X holds
|.(((
Bound2Lipschitz ((vseq
. n),X))
. x)
- (tseq
. x)).|
<= (e
*
||.x.||)
proof
let e be
Real;
assume e
>
0 ;
then
consider k be
Nat such that
A55: for n,m be
Nat st n
>= k & m
>= k holds
||.((vseq
. n)
- (vseq
. m)).||
< e by
A2,
RSSPACE3: 8;
take k;
now
let n be
Nat such that
A56: n
>= k;
now
let x be
VECTOR of X;
consider xseq be
sequence of
REAL such that
A57: for n be
Nat holds (xseq
. n)
= ((
Bound2Lipschitz ((vseq
. n),X))
. x) & xseq is
convergent & (tseq
. x)
= (
lim xseq) by
A20;
A60: for m,k be
Nat holds
|.((xseq
. m)
- (xseq
. k)).|
<= (
||.((vseq
. m)
- (vseq
. k)).||
*
||.x.||)
proof
let m,k be
Nat;
reconsider h1 = ((vseq
. m)
- (vseq
. k)) as
Lipschitzian
linear-Functional of X by
Def9;
A61: (xseq
. k)
= ((
Bound2Lipschitz ((vseq
. k),X))
. x) & (xseq
. m)
= ((
Bound2Lipschitz ((vseq
. m),X))
. x) by
A57;
(vseq
. m) is
Lipschitzian
linear-Functional of X & (vseq
. k) is
Lipschitzian
linear-Functional of X by
Def9;
then (
Bound2Lipschitz ((vseq
. m),X))
= (vseq
. m) & (
Bound2Lipschitz ((vseq
. k),X))
= (vseq
. k) by
Th29;
then ((xseq
. m)
- (xseq
. k))
= (h1
. x) by
A61,
Th40;
hence thesis by
Th32;
end;
A64: for m be
Nat st m
>= k holds
|.((xseq
. n)
- (xseq
. m)).|
<= (e
*
||.x.||)
proof
let m be
Nat;
assume m
>= k;
then
||.((vseq
. n)
- (vseq
. m)).||
< e by
A55,
A56;
then
A66: (
||.((vseq
. n)
- (vseq
. m)).||
*
||.x.||)
<= (e
*
||.x.||) by
XREAL_1: 64;
|.((xseq
. n)
- (xseq
. m)).|
<= (
||.((vseq
. n)
- (vseq
. m)).||
*
||.x.||) by
A60;
hence thesis by
A66,
XXREAL_0: 2;
end;
|.((xseq
. n)
- (tseq
. x)).|
<= (e
*
||.x.||)
proof
deffunc
F(
Nat) =
|.((xseq
. $1)
- (xseq
. n)).|;
consider rseq be
Real_Sequence such that
A67: for m be
Nat holds (rseq
. m)
=
F(m) from
SEQ_1:sch 1;
now
let x be
object;
assume x
in
NAT ;
then
reconsider k = x as
Nat;
thus (rseq
. x)
=
|.((xseq
. k)
- (xseq
. n)).| by
A67
.=
|.((xseq
- (xseq
. n))
. k).| by
Def14
.= (
|.(xseq
- (xseq
. n)).|
. x) by
SEQ_1: 12;
end;
then
A68: rseq
=
|.(xseq
- (xseq
. n)).|;
A69: (xseq
- (xseq
. n)) is
convergent by
A57,
Th121;
(
lim (xseq
- (xseq
. n)))
= ((tseq
. x)
- (xseq
. n)) by
A57,
Th121;
then
A70: (
lim rseq)
=
|.((tseq
. x)
- (xseq
. n)).| by
A57,
Th121,
A68,
SEQ_4: 14;
for m be
Nat st m
>= k holds (rseq
. m)
<= (e
*
||.x.||)
proof
let m be
Nat such that
A71: m
>= k;
(rseq
. m)
=
|.((xseq
. m)
- (xseq
. n)).| by
A67
.=
|.((xseq
. n)
- (xseq
. m)).| by
COMPLEX1: 60;
hence thesis by
A64,
A71;
end;
then (
lim rseq)
<= (e
*
||.x.||) by
A69,
A68,
Lm3;
hence thesis by
A70,
COMPLEX1: 60;
end;
hence
|.(((
Bound2Lipschitz ((vseq
. n),X))
. x)
- (tseq
. x)).|
<= (e
*
||.x.||) by
A57;
end;
hence for x be
VECTOR of X holds
|.(((
Bound2Lipschitz ((vseq
. n),X))
. x)
- (tseq
. x)).|
<= (e
*
||.x.||);
end;
hence thesis;
end;
reconsider tseq as
Lipschitzian
linear-Functional of X by
A41;
reconsider tv = tseq as
Point of (
DualSp X) by
Def9;
A72: for e be
Real st e
>
0 holds ex k be
Nat st for n be
Nat st n
>= k holds
||.((vseq
. n)
- tv).||
<= e
proof
let e be
Real such that
A73: e
>
0 ;
consider k be
Nat such that
A74: for n be
Nat st n
>= k holds for x be
VECTOR of X holds
|.(((
Bound2Lipschitz ((vseq
. n),X))
. x)
- (tseq
. x)).|
<= (e
*
||.x.||) by
A54,
A73;
now
set g1 = tseq;
let n be
Nat such that
A75: n
>= k;
reconsider h1 = ((vseq
. n)
- tv) as
Lipschitzian
linear-Functional of X by
Def9;
set f1 = (
Bound2Lipschitz ((vseq
. n),X));
A76:
now
let t be
VECTOR of X;
assume
||.t.||
<= 1;
then
A77: (e
*
||.t.||)
<= (e
* 1) by
A73,
XREAL_1: 64;
A78:
|.((f1
. t)
- (g1
. t)).|
<= (e
*
||.t.||) by
A74,
A75;
(vseq
. n) is
Lipschitzian
linear-Functional of X by
Def9;
then (
Bound2Lipschitz ((vseq
. n),X))
= (vseq
. n) by
Th29;
then
|.(h1
. t).|
=
|.((f1
. t)
- (g1
. t)).| by
Th40;
hence
|.(h1
. t).|
<= e by
A78,
A77,
XXREAL_0: 2;
end;
A79:
now
let r be
Real;
assume r
in (
PreNorms h1);
then ex t be
VECTOR of X st r
=
|.(h1
. t).| &
||.t.||
<= 1;
hence r
<= e by
A76;
end;
(for s be
Real st s
in (
PreNorms h1) holds s
<= e) implies (
upper_bound (
PreNorms h1))
<= e by
SEQ_4: 45;
hence
||.((vseq
. n)
- tv).||
<= e by
A79,
Th30;
end;
hence thesis;
end;
for e be
Real st e
>
0 holds ex m be
Nat st for n be
Nat st n
>= m holds
||.((vseq
. n)
- tv).||
< e
proof
let e be
Real;
assume
A81: e
>
0 ;
then
consider m be
Nat such that
A82: for n be
Nat st n
>= m holds
||.((vseq
. n)
- tv).||
<= (e
/ 2) by
A72;
take m;
hereby
let n be
Nat;
assume n
>= m;
then
||.((vseq
. n)
- tv).||
<= (e
/ 2) & (e
/ 2)
< e by
A82,
A81,
XREAL_1: 216;
hence
||.((vseq
. n)
- tv).||
< e by
XXREAL_0: 2;
end;
end;
hence thesis;
end;
theorem ::
DUALSP01:35
Th43: for X be
RealNormSpace holds (
DualSp X) is
RealBanachSpace
proof
let X be
RealNormSpace;
for seq be
sequence of (
DualSp X) st seq is
Cauchy_sequence_by_Norm holds seq is
convergent by
Th42;
hence thesis by
LOPBAN_1:def 15;
end;
registration
let X be
RealNormSpace;
cluster (
DualSp X) ->
complete;
coherence by
Th43;
end
begin
definition
let V be
RealNormSpace;
::
DUALSP01:def16
mode
SubRealNormSpace of V ->
RealNormSpace means
:
DefSubSP: the
carrier of it
c= the
carrier of V & (
0. it )
= (
0. V) & the
addF of it
= (the
addF of V
|| the
carrier of it ) & the
Mult of it
= (the
Mult of V
|
[:
REAL , the
carrier of it :]) & the
normF of it
= (the
normF of V
| the
carrier of it );
existence
proof
the
addF of V
= (the
addF of V
|| the
carrier of V) & the
Mult of V
= (the
Mult of V
|
[:
REAL , the
carrier of V:]) & the
normF of V
= (the
normF of V
| the
carrier of V);
hence thesis;
end;
end
theorem ::
DUALSP01:36
Th44: for V be
RealNormSpace, X be
SubRealNormSpace of V, f be
Lipschitzian
linear-Functional of X, F be
Point of (
DualSp X) st f
= F holds ex g be
Lipschitzian
linear-Functional of V, G be
Point of (
DualSp V) st g
= G & (g
| the
carrier of X)
= f &
||.G.||
=
||.F.||
proof
let V be
RealNormSpace, X be
SubRealNormSpace of V, f be
Lipschitzian
linear-Functional of X, F be
Point of (
DualSp X) such that
A1: f
= F;
reconsider X0 = X as
RealLinearSpace;
B1: the
carrier of X0
c= the
carrier of V & (
0. X0)
= (
0. V) & the
addF of X0
= (the
addF of V
|| the
carrier of X0) & the
Mult of X0
= (the
Mult of V
|
[:
REAL , the
carrier of X0:]) by
DefSubSP;
then
reconsider X0 as
Subspace of V by
RLSUB_1:def 2;
reconsider fi0 = f as
linear-Functional of X0;
deffunc
F(
Element of the
carrier of V) = (
||.F.||
*
||.$1.||);
D0: for v be
Element of the
carrier of V holds
F(v)
in
REAL by
XREAL_0:def 1;
consider q be
Function of the
carrier of V,
REAL such that
D1: for v be
Element of the
carrier of V holds (q
. v)
=
F(v) from
FUNCT_2:sch 8(
D0);
q is
Banach-Functional of V
proof
E0: q is
subadditive
proof
let x,y be
VECTOR of V;
E2: (q
. x)
= (
||.F.||
*
||.x.||) & (q
. y)
= (
||.F.||
*
||.y.||) by
D1;
(
||.F.||
*
||.(x
+ y).||)
<= (
||.F.||
* (
||.x.||
+
||.y.||)) by
XREAL_1: 64,
NORMSP_1:def 1;
hence thesis by
D1,
E2;
end;
q is
absolutely_homogeneous
proof
let x be
VECTOR of V, r be
Real;
E5:
||.(r
* x).||
= (
|.r.|
*
||.x.||) by
NORMSP_1:def 1;
(q
. (r
* x))
= (
||.F.||
*
||.(r
* x).||) by
D1
.= (
|.r.|
* (
||.F.||
*
||.x.||)) by
E5;
hence thesis by
D1;
end;
hence thesis by
E0;
end;
then
reconsider q as
Banach-Functional of V;
for x be
VECTOR of X0, v be
VECTOR of V st x
= v holds (fi0
. x)
<= (q
. v)
proof
let x0 be
VECTOR of X0, v be
VECTOR of V;
assume
D21: x0
= v;
reconsider x = x0 as
VECTOR of X;
D22: (fi0
. x0)
<=
|.(fi0
. x0).| by
ABSVALUE: 4;
D23:
|.(fi0
. x).|
<= (
||.F.||
*
||.x.||) by
A1,
Th32;
||.x.||
= ((the
normF of V
| the
carrier of X)
. v) by
D21,
DefSubSP
.=
||.v.|| by
FUNCT_1: 49,
D21;
then
|.(fi0
. x0).|
<= (q
. v) by
D1,
D23;
hence thesis by
D22,
XXREAL_0: 2;
end;
then
consider g be
linear-Functional of V such that
A3: (g
| the
carrier of X0)
= fi0 & for x be
VECTOR of V holds (g
. x)
<= (q
. x) by
HAHNBAN: 22;
B4: for x be
VECTOR of V holds
|.(g
. x).|
<= (
||.F.||
*
||.x.||)
proof
let x be
VECTOR of V;
(g
. x)
<= (q
. x) by
A3;
then
A31: (g
. x)
<= (
||.F.||
*
||.x.||) by
D1;
A32: (
- (g
. x))
= ((
- 1)
* (g
. x))
.= (g
. ((
- 1)
* x)) by
HAHNBAN:def 3;
(g
. ((
- 1)
* x))
<= (q
. ((
- 1)
* x)) by
A3;
then (g
. ((
- 1)
* x))
<= (
||.F.||
*
||.((
- 1)
* x).||) by
D1;
then (g
. ((
- 1)
* x))
<= (
||.F.||
*
||.(
- x).||) by
RLVECT_1: 16;
then (
- (g
. x))
<= (
||.F.||
*
||.x.||) by
A32,
NORMSP_1: 2;
then (
- (
||.F.||
*
||.x.||))
<= (g
. x) by
XREAL_1: 26;
hence thesis by
ABSVALUE: 5,
A31;
end;
then
reconsider g as
Lipschitzian
linear-Functional of V by
Def8;
reconsider G = g as
Point of (
DualSp V) by
Def9;
now
let r be
Real;
assume r
in (
PreNorms g);
then
consider t be
VECTOR of V such that
C1: r
=
|.(g
. t).| and
C2:
||.t.||
<= 1;
C3:
|.(g
. t).|
<= (
||.F.||
*
||.t.||) by
B4;
(
||.F.||
*
||.t.||)
<= (
||.F.||
* 1) by
C2,
XREAL_1: 64;
hence r
<=
||.F.|| by
C1,
C3,
XXREAL_0: 2;
end;
then (
upper_bound (
PreNorms g))
<= ((
BoundedLinearFunctionalsNorm X)
. f) by
A1,
SEQ_4: 45;
then
A41: ((
BoundedLinearFunctionalsNorm V)
. g)
<= ((
BoundedLinearFunctionalsNorm X)
. f) by
Th30;
now
let r be
object;
assume r
in (
PreNorms f);
then
consider t be
VECTOR of X such that
C1: r
=
|.(f
. t).| and
C2:
||.t.||
<= 1;
reconsider td = t as
VECTOR of V by
B1;
||.t.||
= ((the
normF of V
| the
carrier of X)
. td) by
DefSubSP
.=
||.td.|| by
FUNCT_1: 49;
then r
=
|.(g
. td).| &
||.td.||
<= 1 by
C1,
A3,
FUNCT_1: 49,
C2;
hence r
in (
PreNorms g);
end;
then
A42: (
PreNorms f)
c= (
PreNorms g);
(
upper_bound (
PreNorms f))
<= (
upper_bound (
PreNorms g)) by
A42,
SEQ_4: 48;
then ((
BoundedLinearFunctionalsNorm X)
. f)
<= (
upper_bound (
PreNorms g)) by
Th30;
then
B4: ((
BoundedLinearFunctionalsNorm X)
. f)
<= ((
BoundedLinearFunctionalsNorm V)
. g) by
Th30;
take g, G;
thus thesis by
A3,
A1,
A41,
XXREAL_0: 1,
B4;
end;
::$Notion-Name
theorem ::
DUALSP01:37
for V be
RealNormSpace, X be
SubRealNormSpace of V, f be
Lipschitzian
linear-Functional of X, F be
Point of (
DualSp X) st (f
= F & for x be
VECTOR of X, v be
VECTOR of V st x
= v holds (f
. x)
<=
||.v.||) holds ex g be
Lipschitzian
linear-Functional of V, G be
Point of (
DualSp V) st g
= G & (g
| the
carrier of X)
= f & for x be
VECTOR of V holds (g
. x)
<=
||.x.|| &
||.G.||
=
||.F.||
proof
let V be
RealNormSpace, X be
SubRealNormSpace of V, f be
Lipschitzian
linear-Functional of X, F be
Point of (
DualSp X) such that
A11: f
= F and
A12: for x be
VECTOR of X, v be
VECTOR of V st x
= v holds (f
. x)
<=
||.v.||;
consider g be
Lipschitzian
linear-Functional of V, G be
Point of (
DualSp V) such that
A2: g
= G & (g
| the
carrier of X)
= f &
||.G.||
=
||.F.|| by
A11,
Th44;
reconsider X0 = X as
RealLinearSpace;
B1: the
carrier of X0
c= the
carrier of V & (
0. X0)
= (
0. V) & the
addF of X0
= (the
addF of V
|| the
carrier of X0) & the
Mult of X0
= (the
Mult of V
|
[:
REAL , the
carrier of X0:]) by
DefSubSP;
now
let r be
Real;
assume r
in (
PreNorms f);
then
consider t be
VECTOR of X such that
C1: r
=
|.(f
. t).| &
||.t.||
<= 1;
reconsider td = t as
VECTOR of V by
B1;
C7:
||.t.||
= ((the
normF of V
| the
carrier of X)
. td) by
DefSubSP
.=
||.td.|| by
FUNCT_1: 49;
C5: (
- (f
. t))
= ((
- 1)
* (f
. t))
.= (f
. ((
- 1)
* t)) by
HAHNBAN:def 3;
reconsider t0 = t as
VECTOR of X0;
D6: X0 is
Subspace of V by
B1,
RLSUB_1:def 2;
((
- 1)
* td)
= (
- td) & ((
- 1)
* t)
= (
- t) by
RLVECT_1: 16;
then ((
- 1)
* td)
= ((
- 1)
* t) by
RLSUB_1: 15,
D6;
then (f
. ((
- 1)
* t))
<=
||.((
- 1)
* td).|| by
A12;
then (f
. ((
- 1)
* t))
<=
||.(
- td).|| by
RLVECT_1: 16;
then (
- (f
. t))
<=
||.td.|| by
C5,
NORMSP_1: 2;
then (
-
||.td.||)
<= (f
. t) by
XREAL_1: 26;
then
|.(f
. t).|
<=
||.td.|| by
A12,
ABSVALUE: 5;
hence r
<= 1 by
C1,
C7,
XXREAL_0: 2;
end;
then (
upper_bound (
PreNorms f))
<= 1 by
SEQ_4: 45;
then
A3:
||.G.||
<= 1 by
A2,
A11,
Th30;
for x be
VECTOR of V holds (g
. x)
<=
||.x.||
proof
let x be
VECTOR of V;
C1: (g
. x)
<=
|.(g
. x).| by
ABSVALUE: 4;
|.(g
. x).|
<= (
||.G.||
*
||.x.||) by
A2,
Th32;
then
C2: (g
. x)
<= (
||.G.||
*
||.x.||) by
C1,
XXREAL_0: 2;
(
||.G.||
*
||.x.||)
<= (1
*
||.x.||) by
A3,
XREAL_1: 64;
hence thesis by
C2,
XXREAL_0: 2;
end;
hence thesis by
A2;
end;