:: by Bogdan Nowak and Andrzej Trybulec

::

:: Received July 8, 1993

:: Copyright (c) 1993-2012 Association of Mizar Users

begin

theorem Th1: :: HAHNBAN:1

for V being RealLinearSpace

for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)

for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)

proof end;

theorem Th2: :: HAHNBAN:2

for V being RealLinearSpace

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v, v1, v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds

v |-- (W1,W2) = [v1,v2]

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v, v1, v2 being VECTOR of V st v1 in W1 & v2 in W2 & v = v1 + v2 holds

v |-- (W1,W2) = [v1,v2]

proof end;

theorem Th3: :: HAHNBAN:3

for V being RealLinearSpace

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds

v = v1 + v2

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds

v = v1 + v2

proof end;

theorem Th4: :: HAHNBAN:4

for V being RealLinearSpace

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds

( v1 in W1 & v2 in W2 )

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds

( v1 in W1 & v2 in W2 )

proof end;

theorem Th5: :: HAHNBAN:5

for V being RealLinearSpace

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds

v |-- (W2,W1) = [v2,v1]

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v, v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2] holds

v |-- (W2,W1) = [v2,v1]

proof end;

theorem Th6: :: HAHNBAN:6

for V being RealLinearSpace

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v being VECTOR of V st v in W1 holds

v |-- (W1,W2) = [v,(0. V)]

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v being VECTOR of V st v in W1 holds

v |-- (W1,W2) = [v,(0. V)]

proof end;

theorem Th7: :: HAHNBAN:7

for V being RealLinearSpace

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v being VECTOR of V st v in W2 holds

v |-- (W1,W2) = [(0. V),v]

for W1, W2 being Subspace of V st V is_the_direct_sum_of W1,W2 holds

for v being VECTOR of V st v in W2 holds

v |-- (W1,W2) = [(0. V),v]

proof end;

theorem Th8: :: HAHNBAN:8

for V being RealLinearSpace

for V1 being Subspace of V

for W1 being Subspace of V1

for v being VECTOR of V st v in W1 holds

v is VECTOR of V1

for V1 being Subspace of V

for W1 being Subspace of V1

for v being VECTOR of V st v in W1 holds

v is VECTOR of V1

proof end;

theorem Th9: :: HAHNBAN:9

for V being RealLinearSpace

for V1, V2, W being Subspace of V

for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds

W1 + W2 = V1 + V2

for V1, V2, W being Subspace of V

for W1, W2 being Subspace of W st W1 = V1 & W2 = V2 holds

W1 + W2 = V1 + V2

proof end;

theorem Th10: :: HAHNBAN:10

for V being RealLinearSpace

for W being Subspace of V

for v being VECTOR of V

for w being VECTOR of W st v = w holds

Lin {w} = Lin {v}

for W being Subspace of V

for v being VECTOR of V

for w being VECTOR of W st v = w holds

Lin {w} = Lin {v}

proof end;

theorem Th11: :: HAHNBAN:11

for V being RealLinearSpace

for v being VECTOR of V

for X being Subspace of V st not v in X holds

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & W = X holds

X + (Lin {v}) is_the_direct_sum_of W, Lin {y}

for v being VECTOR of V

for X being Subspace of V st not v in X holds

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & W = X holds

X + (Lin {v}) is_the_direct_sum_of W, Lin {y}

proof end;

theorem Th12: :: HAHNBAN:12

for V being RealLinearSpace

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

y |-- (W,(Lin {y})) = [(0. W),y]

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

y |-- (W,(Lin {y})) = [(0. W),y]

proof end;

theorem Th13: :: HAHNBAN:13

for V being RealLinearSpace

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

for w being VECTOR of (X + (Lin {v})) st w in X holds

w |-- (W,(Lin {y})) = [w,(0. V)]

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

for w being VECTOR of (X + (Lin {v})) st w in X holds

w |-- (W,(Lin {y})) = [w,(0. V)]

proof end;

theorem Th14: :: HAHNBAN:14

for V being RealLinearSpace

for v being VECTOR of V

for W1, W2 being Subspace of V ex v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2]

for v being VECTOR of V

for W1, W2 being Subspace of V ex v1, v2 being VECTOR of V st v |-- (W1,W2) = [v1,v2]

proof end;

theorem Th15: :: HAHNBAN:15

for V being RealLinearSpace

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

for w being VECTOR of (X + (Lin {v})) ex x being VECTOR of X ex r being Real st w |-- (W,(Lin {y})) = [x,(r * v)]

proof end;

theorem Th16: :: HAHNBAN:16

for V being RealLinearSpace

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

for w1, w2 being VECTOR of (X + (Lin {v}))

for x1, x2 being VECTOR of X

for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds

(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

for w1, w2 being VECTOR of (X + (Lin {v}))

for x1, x2 being VECTOR of X

for r1, r2 being Real st w1 |-- (W,(Lin {y})) = [x1,(r1 * v)] & w2 |-- (W,(Lin {y})) = [x2,(r2 * v)] holds

(w1 + w2) |-- (W,(Lin {y})) = [(x1 + x2),((r1 + r2) * v)]

proof end;

theorem Th17: :: HAHNBAN:17

for V being RealLinearSpace

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

for w being VECTOR of (X + (Lin {v}))

for x being VECTOR of X

for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds

(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]

for v being VECTOR of V

for X being Subspace of V

for y being VECTOR of (X + (Lin {v}))

for W being Subspace of X + (Lin {v}) st v = y & X = W & not v in X holds

for w being VECTOR of (X + (Lin {v}))

for x being VECTOR of X

for t, r being Real st w |-- (W,(Lin {y})) = [x,(r * v)] holds

(t * w) |-- (W,(Lin {y})) = [(t * x),((t * r) * v)]

proof end;

begin

definition

let V be RealLinearSpace;

let IT be Functional of V;

end;
let IT be Functional of V;

attr IT is subadditive means :Def1: :: HAHNBAN:def 1

for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y);

for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y);

attr IT is additive means :Def2: :: HAHNBAN:def 2

for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y);

for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y);

attr IT is homogeneous means :Def3: :: HAHNBAN:def 3

for x being VECTOR of V

for r being Real holds IT . (r * x) = r * (IT . x);

for x being VECTOR of V

for r being Real holds IT . (r * x) = r * (IT . x);

attr IT is positively_homogeneous means :Def4: :: HAHNBAN:def 4

for x being VECTOR of V

for r being Real st r > 0 holds

IT . (r * x) = r * (IT . x);

for x being VECTOR of V

for r being Real st r > 0 holds

IT . (r * x) = r * (IT . x);

attr IT is semi-homogeneous means :Def5: :: HAHNBAN:def 5

for x being VECTOR of V

for r being Real st r >= 0 holds

IT . (r * x) = r * (IT . x);

for x being VECTOR of V

for r being Real st r >= 0 holds

IT . (r * x) = r * (IT . x);

attr IT is absolutely_homogeneous means :Def6: :: HAHNBAN:def 6

for x being VECTOR of V

for r being Real holds IT . (r * x) = (abs r) * (IT . x);

for x being VECTOR of V

for r being Real holds IT . (r * x) = (abs r) * (IT . x);

:: deftheorem Def1 defines subadditive HAHNBAN:def 1 :

for V being RealLinearSpace

for IT being Functional of V holds

( IT is subadditive iff for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y) );

for V being RealLinearSpace

for IT being Functional of V holds

( IT is subadditive iff for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y) );

:: deftheorem Def2 defines additive HAHNBAN:def 2 :

for V being RealLinearSpace

for IT being Functional of V holds

( IT is additive iff for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y) );

for V being RealLinearSpace

for IT being Functional of V holds

( IT is additive iff for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y) );

:: deftheorem Def3 defines homogeneous HAHNBAN:def 3 :

for V being RealLinearSpace

for IT being Functional of V holds

( IT is homogeneous iff for x being VECTOR of V

for r being Real holds IT . (r * x) = r * (IT . x) );

for V being RealLinearSpace

for IT being Functional of V holds

( IT is homogeneous iff for x being VECTOR of V

for r being Real holds IT . (r * x) = r * (IT . x) );

:: deftheorem Def4 defines positively_homogeneous HAHNBAN:def 4 :

for V being RealLinearSpace

for IT being Functional of V holds

( IT is positively_homogeneous iff for x being VECTOR of V

for r being Real st r > 0 holds

IT . (r * x) = r * (IT . x) );

for V being RealLinearSpace

for IT being Functional of V holds

( IT is positively_homogeneous iff for x being VECTOR of V

for r being Real st r > 0 holds

IT . (r * x) = r * (IT . x) );

:: deftheorem Def5 defines semi-homogeneous HAHNBAN:def 5 :

for V being RealLinearSpace

for IT being Functional of V holds

( IT is semi-homogeneous iff for x being VECTOR of V

for r being Real st r >= 0 holds

IT . (r * x) = r * (IT . x) );

for V being RealLinearSpace

for IT being Functional of V holds

( IT is semi-homogeneous iff for x being VECTOR of V

for r being Real st r >= 0 holds

IT . (r * x) = r * (IT . x) );

:: deftheorem Def6 defines absolutely_homogeneous HAHNBAN:def 6 :

for V being RealLinearSpace

for IT being Functional of V holds

( IT is absolutely_homogeneous iff for x being VECTOR of V

for r being Real holds IT . (r * x) = (abs r) * (IT . x) );

for V being RealLinearSpace

for IT being Functional of V holds

( IT is absolutely_homogeneous iff for x being VECTOR of V

for r being Real holds IT . (r * x) = (abs r) * (IT . x) );

:: deftheorem Def7 defines 0-preserving HAHNBAN:def 7 :

for V being RealLinearSpace

for IT being Functional of V holds

( IT is 0-preserving iff IT . (0. V) = 0 );

for V being RealLinearSpace

for IT being Functional of V holds

( IT is 0-preserving iff IT . (0. V) = 0 );

registration

let V be RealLinearSpace;

for b_{1} being Functional of V st b_{1} is additive holds

b_{1} is subadditive

for b_{1} being Functional of V st b_{1} is homogeneous holds

b_{1} is positively_homogeneous

for b_{1} being Functional of V st b_{1} is semi-homogeneous holds

b_{1} is positively_homogeneous

for b_{1} being Functional of V st b_{1} is semi-homogeneous holds

b_{1} is 0-preserving

for b_{1} being Functional of V st b_{1} is absolutely_homogeneous holds

b_{1} is semi-homogeneous

for b_{1} being Functional of V st b_{1} is 0-preserving & b_{1} is positively_homogeneous holds

b_{1} is semi-homogeneous

end;
cluster Function-like V18( the carrier of V, REAL ) additive -> subadditive for Element of bool [: the carrier of V,REAL:];

coherence for b

b

proof end;

cluster Function-like V18( the carrier of V, REAL ) homogeneous -> positively_homogeneous for Element of bool [: the carrier of V,REAL:];

coherence for b

b

proof end;

cluster Function-like V18( the carrier of V, REAL ) semi-homogeneous -> positively_homogeneous for Element of bool [: the carrier of V,REAL:];

coherence for b

b

proof end;

cluster Function-like V18( the carrier of V, REAL ) semi-homogeneous -> 0-preserving for Element of bool [: the carrier of V,REAL:];

coherence for b

b

proof end;

cluster Function-like V18( the carrier of V, REAL ) absolutely_homogeneous -> semi-homogeneous for Element of bool [: the carrier of V,REAL:];

coherence for b

b

proof end;

cluster Function-like V18( the carrier of V, REAL ) positively_homogeneous 0-preserving -> semi-homogeneous for Element of bool [: the carrier of V,REAL:];

coherence for b

b

proof end;

registration

let V be RealLinearSpace;

ex b_{1} being Functional of V st

( b_{1} is additive & b_{1} is absolutely_homogeneous & b_{1} is homogeneous )

end;
cluster Relation-like the carrier of V -defined REAL -valued Function-like non empty total V18( the carrier of V, REAL ) additive homogeneous absolutely_homogeneous for Element of bool [: the carrier of V,REAL:];

existence ex b

( b

proof end;

definition

let V be RealLinearSpace;

mode Banach-Functional of V is subadditive positively_homogeneous Functional of V;

mode linear-Functional of V is additive homogeneous Functional of V;

end;
mode Banach-Functional of V is subadditive positively_homogeneous Functional of V;

mode linear-Functional of V is additive homogeneous Functional of V;

theorem Th18: :: HAHNBAN:18

for V being RealLinearSpace

for L being homogeneous Functional of V

for v being VECTOR of V holds L . (- v) = - (L . v)

for L being homogeneous Functional of V

for v being VECTOR of V holds L . (- v) = - (L . v)

proof end;

theorem Th19: :: HAHNBAN:19

for V being RealLinearSpace

for L being linear-Functional of V

for v1, v2 being VECTOR of V holds L . (v1 - v2) = (L . v1) - (L . v2)

for L being linear-Functional of V

for v1, v2 being VECTOR of V holds L . (v1 - v2) = (L . v1) - (L . v2)

proof end;

theorem Th21: :: HAHNBAN:21

for V being RealLinearSpace

for X being Subspace of V

for fi being linear-Functional of X

for v being VECTOR of V

for y being VECTOR of (X + (Lin {v})) st v = y & not v in X holds

for r being Real ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

for X being Subspace of V

for fi being linear-Functional of X

for v being VECTOR of V

for y being VECTOR of (X + (Lin {v})) st v = y & not v in X holds

for r being Real ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & psi . y = r )

proof end;

begin

Lm1: for V being RealLinearSpace

for X being Subspace of V

for v being VECTOR of V st not v in the carrier of X holds

for q being Banach-Functional of V

for fi being linear-Functional of X st ( for x being VECTOR of X

for v being VECTOR of V st x = v holds

fi . x <= q . v ) holds

ex psi being linear-Functional of (X + (Lin {v})) st

( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))

for v being VECTOR of V st x = v holds

psi . x <= q . v ) )

proof end;

Lm2: for V being RealLinearSpace holds RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace

proof end;

Lm3: for V, V9, W9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds

for W being Subspace of V st W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) holds

W9 is Subspace of V9

proof end;

Lm4: for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds

for f being linear-Functional of V9 holds f is linear-Functional of V

proof end;

Lm5: for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds

for f being linear-Functional of V holds f is linear-Functional of V9

proof end;

theorem Th22: :: HAHNBAN:22

for V being RealLinearSpace

for X being Subspace of V

for q being Banach-Functional of V

for fi being linear-Functional of X st ( for x being VECTOR of X

for v being VECTOR of V st x = v holds

fi . x <= q . v ) holds

ex psi being linear-Functional of V st

( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )

for X being Subspace of V

for q being Banach-Functional of V

for fi being linear-Functional of X st ( for x being VECTOR of X

for v being VECTOR of V st x = v holds

fi . x <= q . v ) holds

ex psi being linear-Functional of V st

( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= q . x ) )

proof end;

theorem Th23: :: HAHNBAN:23

for V being RealNormSpace holds the normF of V is subadditive absolutely_homogeneous Functional of V

proof end;

:: Hahn-Banach Theorem (real spaces)

theorem :: HAHNBAN:24

for V being RealNormSpace

for X being Subspace of V

for fi being linear-Functional of X st ( for x being VECTOR of X

for v being VECTOR of V st x = v holds

fi . x <= ||.v.|| ) holds

ex psi being linear-Functional of V st

( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= ||.x.|| ) )

for X being Subspace of V

for fi being linear-Functional of X st ( for x being VECTOR of X

for v being VECTOR of V st x = v holds

fi . x <= ||.v.|| ) holds

ex psi being linear-Functional of V st

( psi | the carrier of X = fi & ( for x being VECTOR of V holds psi . x <= ||.x.|| ) )

proof end;