:: Dual Spaces and Hahn-Banach's Theorem
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received March 31, 2014
:: Copyright (c) 2014-2018 Association of Mizar Users

definition
let X be RealLinearSpace;
func MultF_Real* X -> Function of [: the carrier of F_Real, the carrier of X:], the carrier of X equals :: DUALSP01:def 1
the Mult of X;
correctness
coherence
the Mult of X is Function of [: the carrier of F_Real, the carrier of X:], the carrier of X
;
;
end;

:: deftheorem defines MultF_Real* DUALSP01:def 1 :
for X being RealLinearSpace holds MultF_Real* X = the Mult of X;

theorem Lm01: :: DUALSP01:1
for X being RealLinearSpace holds ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) is VectSp of F_Real
proof end;

definition
let X be RealLinearSpace;
func RLSp2RVSp X -> VectSp of F_Real equals :: DUALSP01:def 2
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #);
correctness
coherence
ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #) is VectSp of F_Real
;
by Lm01;
end;

:: deftheorem defines RLSp2RVSp DUALSP01:def 2 :
for X being RealLinearSpace holds RLSp2RVSp X = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X,() #);

definition
let X be ModuleStr over F_Real ;
func MultReal* X -> Function of [:REAL, the carrier of X:], the carrier of X equals :: DUALSP01:def 3
the lmult of X;
correctness
coherence
the lmult of X is Function of [:REAL, the carrier of X:], the carrier of X
;
;
end;

:: deftheorem defines MultReal* DUALSP01:def 3 :
for X being ModuleStr over F_Real holds MultReal* X = the lmult of X;

theorem Lm02: :: DUALSP01:2
for X being VectSp of F_Real holds RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,() #) is RealLinearSpace
proof end;

definition
let X be VectSp of F_Real ;
func RVSp2RLSp X -> RealLinearSpace equals :: DUALSP01:def 4
RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,() #);
correctness
coherence
RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,() #) is RealLinearSpace
;
by Lm02;
end;

:: deftheorem defines RVSp2RLSp DUALSP01:def 4 :
for X being VectSp of F_Real holds RVSp2RLSp X = RLSStruct(# the carrier of X, the ZeroF of X, the addF of X,() #);

theorem :: DUALSP01:3
for X being RealLinearSpace
for v, w being Element of X
for v1, w1 being Element of () st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )
proof end;

theorem :: DUALSP01:4
for X being VectSp of F_Real
for v, w being Element of X
for v1, w1 being Element of () st v = v1 & w = w1 holds
( v + w = v1 + w1 & v - w = v1 - w1 )
proof end;

definition
let V be RealLinearSpace;
func V *' -> strict RealLinearSpace means :def2: :: DUALSP01:def 5
ex X being VectSp of F_Real st
( X = RLSp2RVSp V & it = RVSp2RLSp (X *') );
correctness
existence
ex b1 being strict RealLinearSpace ex X being VectSp of F_Real st
( X = RLSp2RVSp V & b1 = RVSp2RLSp (X *') )
;
uniqueness
for b1, b2 being strict RealLinearSpace st ex X being VectSp of F_Real st
( X = RLSp2RVSp V & b1 = RVSp2RLSp (X *') ) & ex X being VectSp of F_Real st
( X = RLSp2RVSp V & b2 = RVSp2RLSp (X *') ) holds
b1 = b2
;
proof end;
end;

:: deftheorem def2 defines *' DUALSP01:def 5 :
for V being RealLinearSpace
for b2 being strict RealLinearSpace holds
( b2 = V *' iff ex X being VectSp of F_Real st
( X = RLSp2RVSp V & b2 = RVSp2RLSp (X *') ) );

theorem Th1: :: DUALSP01:5
for V being RealLinearSpace
for x being object holds
( x in the carrier of (V *') iff x is linear-Functional of V )
proof end;

registration
let V be RealLinearSpace;
coherence
proof end;
end;

definition
let V be RealLinearSpace;
let f be Element of (V *');
let v be VECTOR of V;
:: original: .
redefine func f . v -> Element of REAL ;
coherence
f . v is Element of REAL
proof end;
end;

theorem :: DUALSP01:6
for V being RealLinearSpace
for f, g, h being VECTOR of (V *') holds
( h = f + g iff for x being VECTOR of V holds h . x = (f . x) + (g . x) )
proof end;

theorem :: DUALSP01:7
for V being RealLinearSpace
for f, h being VECTOR of (V *')
for a being Real holds
( h = a * f iff for x being VECTOR of V holds h . x = a * (f . x) )
proof end;

theorem :: DUALSP01:8
for V being RealLinearSpace holds 0. (V *') = the carrier of V --> 0
proof end;

theorem Th23: :: DUALSP01:9
for X being RealLinearSpace holds the carrier of X --> 0 is linear-Functional of X
proof end;

definition
let X be RealLinearSpace;
func LinearFunctionals X -> Subset of (RealVectSpace the carrier of X) means :Def7: :: DUALSP01:def 6
for x being object holds
( x in it iff x is linear-Functional of X );
existence
ex b1 being Subset of (RealVectSpace the carrier of X) st
for x being object holds
( x in b1 iff x is linear-Functional of X )
proof end;
uniqueness
for b1, b2 being Subset of (RealVectSpace the carrier of X) st ( for x being object holds
( x in b1 iff x is linear-Functional of X ) ) & ( for x being object holds
( x in b2 iff x is linear-Functional of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines LinearFunctionals DUALSP01:def 6 :
for X being RealLinearSpace
for b2 being Subset of (RealVectSpace the carrier of X) holds
( b2 = LinearFunctionals X iff for x being object holds
( x in b2 iff x is linear-Functional of X ) );

registration
let X be RealNormSpace;
coherence
not LinearFunctionals X is empty
proof end;
end;

registration
let X be RealLinearSpace;
coherence
( not LinearFunctionals X is empty & LinearFunctionals X is functional )
proof end;
end;

theorem Th17: :: DUALSP01:10
for X being RealLinearSpace holds LinearFunctionals X is linearly-closed
proof end;

theorem :: DUALSP01:11
for X being RealLinearSpace holds RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is Subspace of RealVectSpace the carrier of X by ;

registration
let X be RealLinearSpace;
cluster RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
( RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is Abelian & RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is add-associative & RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is right_zeroed & RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is right_complementable & RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is scalar-distributive & RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is vector-distributive & RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is scalar-associative & RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is scalar-unital )
by ;
end;

definition
let X be RealLinearSpace;
func X *' -> strict RealLinearSpace equals :: DUALSP01:def 7
RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #);
coherence
RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #) is strict RealLinearSpace
;
end;

:: deftheorem defines *' DUALSP01:def 7 :
for X being RealLinearSpace holds X *' = RLSStruct(# ,(Zero_ (,(RealVectSpace the carrier of X))),(Add_ (,(RealVectSpace the carrier of X))),(Mult_ (,(RealVectSpace the carrier of X))) #);

registration
let X be RealLinearSpace;
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
f . v is Element of REAL
proof end;
end;

theorem Th20b: :: DUALSP01:12
for X being RealLinearSpace
for f, g, h being VECTOR of (X *') holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th21b: :: DUALSP01:13
for X being RealLinearSpace
for f, h being VECTOR of (X *')
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof end;

theorem Th22b: :: DUALSP01:14
for X being RealLinearSpace holds 0. (X *') = the carrier of X --> 0
proof end;

definition
let S be Real_Sequence;
let x be Real;
func S - x -> Real_Sequence means :Def14: :: DUALSP01:def 8
for n being Nat holds it . n = (S . n) - x;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (S . n) - x
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (S . n) - x ) & ( for n being Nat holds b2 . n = (S . n) - x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines - DUALSP01:def 8 :
for S being Real_Sequence
for x being Real
for b3 being Real_Sequence holds
( b3 = S - x iff for n being Nat holds b3 . n = (S . n) - x );

theorem Th121: :: DUALSP01:15
for S being Real_Sequence
for x being Real st S is convergent holds
( S - x is convergent & lim (S - x) = (lim S) - x )
proof end;

definition
let X be RealNormSpace;
let IT be Functional of X;
attr IT is Lipschitzian means :Def8: :: DUALSP01:def 9
ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds |.(IT . x).| <= K * ) );
end;

:: deftheorem Def8 defines Lipschitzian DUALSP01:def 9 :
for X being RealNormSpace
for IT being Functional of X holds
( IT is Lipschitzian iff ex K being Real st
( 0 <= K & ( for x being VECTOR of X holds |.(IT . x).| <= K * ) ) );

theorem Th21: :: DUALSP01:16
for X being RealNormSpace
for f being Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds
f is Lipschitzian
proof end;

Th21X: for X being RealNormSpace
for F being Functional of X st F = the carrier of X --> 0 holds
( F is linear-Functional of X & F is Lipschitzian )

proof end;

registration
let X be RealNormSpace;
existence
ex b1 being linear-Functional of X st b1 is Lipschitzian
proof end;
end;

definition
let X be RealNormSpace;
func BoundedLinearFunctionals X -> Subset of (X *') means :Def9: :: DUALSP01:def 10
for x being set holds
( x in it iff x is Lipschitzian linear-Functional of X );
existence
ex b1 being Subset of (X *') st
for x being set holds
( x in b1 iff x is Lipschitzian linear-Functional of X )
proof end;
uniqueness
for b1, b2 being Subset of (X *') st ( for x being set holds
( x in b1 iff x is Lipschitzian linear-Functional of X ) ) & ( for x being set holds
( x in b2 iff x is Lipschitzian linear-Functional of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines BoundedLinearFunctionals DUALSP01:def 10 :
for X being RealNormSpace
for b2 being Subset of (X *') holds
( b2 = BoundedLinearFunctionals X iff for x being set holds
( x in b2 iff x is Lipschitzian linear-Functional of X ) );

registration
let X be RealNormSpace;
coherence
proof end;
end;

theorem Th22: :: DUALSP01:17
for X being RealNormSpace holds BoundedLinearFunctionals X is linearly-closed
proof end;

theorem :: DUALSP01:18
for X being RealNormSpace holds RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is Subspace of X *' by ;

registration
let X be RealNormSpace;
coherence
( RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is Abelian & RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is add-associative & RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is right_zeroed & RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is right_complementable & RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is vector-distributive & RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is scalar-distributive & RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is scalar-associative & RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is scalar-unital )
by ;
end;

definition
let X be RealNormSpace;
func R_VectorSpace_of_BoundedLinearFunctionals X -> strict RealLinearSpace equals :: DUALSP01:def 11
RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #);
coherence
RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #) is strict RealLinearSpace
;
end;

:: deftheorem defines R_VectorSpace_of_BoundedLinearFunctionals DUALSP01:def 11 :
for X being RealNormSpace holds R_VectorSpace_of_BoundedLinearFunctionals X = RLSStruct(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))) #);

registration
let X be RealNormSpace;
coherence
for b1 being Element of holds
( b1 is Function-like & b1 is Relation-like )
;
end;

definition
let X be RealNormSpace;
let f be Element of ;
let v be VECTOR of X;
:: original: .
redefine func f . v -> Element of REAL ;
coherence
f . v is Element of REAL
proof end;
end;

theorem Th24: :: DUALSP01:19
for X being RealNormSpace
for f, g, h being VECTOR of holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th25: :: DUALSP01:20
for X being RealNormSpace
for f, h being VECTOR of
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof end;

theorem Th26: :: DUALSP01:21
for X being RealNormSpace holds 0. = the carrier of X --> 0
proof end;

definition
let X be RealNormSpace;
let f be object ;
func Bound2Lipschitz (f,X) -> Lipschitzian linear-Functional of X equals :: DUALSP01:def 12
In (f,);
coherence
In (f,) is Lipschitzian linear-Functional of X
by Def9;
end;

:: deftheorem defines Bound2Lipschitz DUALSP01:def 12 :
for X being RealNormSpace
for f being object holds Bound2Lipschitz (f,X) = In (f,);

definition
let X be RealNormSpace;
let u be linear-Functional of X;
func PreNorms u -> non empty Subset of REAL equals :: DUALSP01:def 13
{ |.(u . t).| where t is VECTOR of X : <= 1 } ;
coherence
{ |.(u . t).| where t is VECTOR of X : <= 1 } is non empty Subset of REAL
proof end;
end;

:: deftheorem defines PreNorms DUALSP01:def 13 :
for X being RealNormSpace
for u being linear-Functional of X holds PreNorms u = { |.(u . t).| where t is VECTOR of X : <= 1 } ;

Th27: for X being RealNormSpace
for g being Lipschitzian linear-Functional of X holds PreNorms g is bounded_above

proof end;

registration
let X be RealNormSpace;
let g be Lipschitzian linear-Functional of X;
coherence by Th27;
end;

theorem :: DUALSP01:22
for X being RealNormSpace
for g being linear-Functional of X holds
( g is Lipschitzian iff PreNorms g is bounded_above )
proof end;

definition
let X be RealNormSpace;
func BoundedLinearFunctionalsNorm X -> Function of ,REAL means :Def13: :: DUALSP01:def 14
for x being object st x in BoundedLinearFunctionals X holds
it . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)));
existence
ex b1 being Function of ,REAL st
for x being object st x in BoundedLinearFunctionals X holds
b1 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X)))
proof end;
uniqueness
for b1, b2 being Function of ,REAL st ( for x being object st x in BoundedLinearFunctionals X holds
b1 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) & ( for x being object st x in BoundedLinearFunctionals X holds
b2 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines BoundedLinearFunctionalsNorm DUALSP01:def 14 :
for X being RealNormSpace
for b2 being Function of ,REAL holds
( b2 = BoundedLinearFunctionalsNorm X iff for x being object st x in BoundedLinearFunctionals X holds
b2 . x = upper_bound (PreNorms (Bound2Lipschitz (x,X))) );

theorem Th29: :: DUALSP01:23
for X being RealNormSpace
for f being Lipschitzian linear-Functional of X holds Bound2Lipschitz (f,X) = f
proof end;

theorem Th30: :: DUALSP01:24
for X being RealNormSpace
for f being Lipschitzian linear-Functional of X holds . f = upper_bound ()
proof end;

definition
let X be RealNormSpace;
func DualSp X -> non empty NORMSTR equals :: DUALSP01:def 15
NORMSTR(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))), #);
coherence
NORMSTR(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))), #) is non empty NORMSTR
;
end;

:: deftheorem defines DualSp DUALSP01:def 15 :
for X being RealNormSpace holds DualSp X = NORMSTR(# ,(Zero_ (,(X *'))),(Add_ (,(X *'))),(Mult_ (,(X *'))), #);

theorem Th31: :: DUALSP01:25
for X being RealNormSpace holds the carrier of X --> 0 = 0. ()
proof end;

theorem Th32: :: DUALSP01:26
for X being RealNormSpace
for f being Point of ()
for g being Lipschitzian linear-Functional of X st g = f holds
for t being VECTOR of X holds |.(g . t).| <= *
proof end;

theorem Th33: :: DUALSP01:27
for X being RealNormSpace
for f being Point of () holds 0 <=
proof end;

theorem Th34: :: DUALSP01:28
for X, Y being RealNormSpace
for f being Point of () st f = 0. () holds
0 =
proof end;

registration
let X be RealNormSpace;
cluster -> Relation-like Function-like for Element of ();
coherence
for b1 being Element of () holds
( b1 is Function-like & b1 is Relation-like )
;
end;

definition
let X be RealNormSpace;
let f be Element of ();
let v be VECTOR of X;
:: original: .
redefine func f . v -> Element of REAL ;
coherence
f . v is Element of REAL
proof end;
end;

theorem Th35: :: DUALSP01:29
for X being RealNormSpace
for f, g, h being Point of () holds
( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )
proof end;

theorem Th36: :: DUALSP01:30
for X being RealNormSpace
for f, h being Point of ()
for a being Real holds
( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )
proof end;

theorem Th37: :: DUALSP01:31
for X being RealNormSpace
for f, g being Point of ()
for a being Real holds
( ( = 0 implies f = 0. () ) & ( f = 0. () implies = 0 ) & ||.(a * f).|| = |.a.| * & ||.(f + g).|| <= + )
proof end;

registration
let X be RealNormSpace;
correctness
coherence ;
by Th37;
end;

theorem Th39: :: DUALSP01:32
for X being RealNormSpace holds DualSp X is RealNormSpace
proof end;

registration
let X be RealNormSpace;
coherence by Th39;
end;

theorem Th40: :: DUALSP01:33
for X being RealNormSpace
for f, g, h being Point of () holds
( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )
proof end;

Lm3: for e being Real
for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e

proof end;

definition
let X be RealNormSpace;
let s be sequence of ();
let n be Nat;
:: original: .
redefine func s . n -> Element of ();
coherence
s . n is Element of ()
proof end;
end;

theorem Th42: :: DUALSP01:34
for X being RealNormSpace
for seq being sequence of () st seq is Cauchy_sequence_by_Norm holds
seq is convergent
proof end;

theorem Th43: :: DUALSP01:35
for X being RealNormSpace holds DualSp X is RealBanachSpace
proof end;

registration
let X be RealNormSpace;
cluster DualSp X -> non empty complete ;
coherence by Th43;
end;

definition
let V be RealNormSpace;
mode SubRealNormSpace of V -> RealNormSpace means :DefSubSP: :: DUALSP01:def 16
( 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
ex b1 being RealNormSpace st
( the carrier of b1 c= the carrier of V & 0. b1 = 0. V & the addF of b1 = the addF of V || the carrier of b1 & the Mult of b1 = the Mult of V | [:REAL, the carrier of b1:] & the normF of b1 = the normF of V | the carrier of b1 )
proof end;
end;

:: deftheorem DefSubSP defines SubRealNormSpace DUALSP01:def 16 :
for V, b2 being RealNormSpace holds
( b2 is SubRealNormSpace of V iff ( the carrier of b2 c= the carrier of V & 0. b2 = 0. V & the addF of b2 = the addF of V || the carrier of b2 & the Mult of b2 = the Mult of V | [:REAL, the carrier of b2:] & the normF of b2 = the normF of V | the carrier of b2 ) );

theorem Th44: :: DUALSP01:36
for V being RealNormSpace
for X being SubRealNormSpace of V
for f being Lipschitzian linear-Functional of X
for F being Point of () st f = F holds
ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & = )
proof end;

:: Hahn-Banach's extension theorem (real normed spaces)
theorem :: DUALSP01:37
for V being RealNormSpace
for X being SubRealNormSpace of V
for f being Lipschitzian linear-Functional of X
for F being Point of () st f = F & ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
f . x <= ) holds
ex g being Lipschitzian linear-Functional of V ex G being Point of () st
( g = G & g | the carrier of X = f & ( for x being VECTOR of V holds
( g . x <= & = ) ) )
proof end;