:: HAHNBAN semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: HAHNBAN:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: HAHNBAN:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: HAHNBAN:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for b being set st A <> {b} holds
ex a being Element of A st a <> b
proof end;

theorem Th4: :: HAHNBAN:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for B being non empty Subset of (PFuncs X,Y) holds B is non empty functional set
proof end;

theorem Th5: :: HAHNBAN:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for B being non empty functional set
for f being Function st f = union B holds
( dom f = union { (dom g) where g is Element of B : verum } & rng f = union { (rng g) where g is Element of B : verum } )
proof end;

theorem :: HAHNBAN:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty Subset of ExtREAL st ( for r being R_eal st r in A holds
r <=' -infty ) holds
A = {-infty }
proof end;

theorem :: HAHNBAN:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty Subset of ExtREAL st ( for r being R_eal st r in A holds
+infty <=' r ) holds
A = {+infty }
proof end;

theorem Th8: :: HAHNBAN:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty Subset of ExtREAL
for r being R_eal st r <' sup A holds
ex s being R_eal st
( s in A & r <' s )
proof end;

theorem Th9: :: HAHNBAN:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty Subset of ExtREAL
for r being R_eal st inf A <' r holds
ex s being R_eal st
( s in A & s <' r )
proof end;

theorem Th10: :: HAHNBAN:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being non empty Subset of ExtREAL st ( for r, s being R_eal st r in A & s in B holds
r <=' s ) holds
sup A <=' inf B
proof end;

registration
let A be non empty set ;
cluster non empty c=-linear Element of bool A;
existence
ex b1 being Subset of A st
( b1 is c=-linear & not b1 is empty )
proof end;
end;

theorem :: HAHNBAN:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: HAHNBAN:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th13: :: HAHNBAN:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for B being c=-linear Subset of (PFuncs X,Y) holds union B in PFuncs X,Y
proof end;

theorem Th14: :: HAHNBAN:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for W1, W2 being Subspace of V holds the carrier of W1 c= the carrier of (W1 + W2)
proof end;

theorem Th15: :: HAHNBAN:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
proof end;

theorem Th16: :: HAHNBAN:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th17: :: HAHNBAN:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th18: :: HAHNBAN:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
proof end;

theorem Th19: :: HAHNBAN:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
proof end;

theorem Th20: :: HAHNBAN:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
proof end;

theorem Th21: :: HAHNBAN:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th22: :: HAHNBAN:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th23: :: HAHNBAN:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem Th24: :: HAHNBAN:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem Th25: :: HAHNBAN:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
proof end;

theorem Th26: :: HAHNBAN:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
proof end;

theorem Th27: :: HAHNBAN:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]
proof end;

theorem Th28: :: HAHNBAN:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
proof end;

theorem Th29: :: HAHNBAN:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
proof end;

theorem Th30: :: HAHNBAN:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
proof end;

definition
let V be RLSStruct ;
mode Functional of V is Function of the carrier of V, REAL ;
end;

definition
let V be RealLinearSpace;
let IT be Functional of V;
canceled;
canceled;
attr IT is subadditive means :Def3: :: HAHNBAN:def 3
for x, y being VECTOR of V holds IT . (x + y) <= (IT . x) + (IT . y);
attr IT is additive means :Def4: :: HAHNBAN:def 4
for x, y being VECTOR of V holds IT . (x + y) = (IT . x) + (IT . y);
attr IT is homogeneous means :Def5: :: HAHNBAN:def 5
for x being VECTOR of V
for r being Real holds IT . (r * x) = r * (IT . x);
attr IT is positively_homogeneous means :Def6: :: HAHNBAN:def 6
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 :Def7: :: HAHNBAN:def 7
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 :Def8: :: HAHNBAN:def 8
for x being VECTOR of V
for r being Real holds IT . (r * x) = (abs r) * (IT . x);
attr IT is 0-preserving means :Def9: :: HAHNBAN:def 9
IT . (0. V) = 0;
end;

:: deftheorem HAHNBAN:def 1 :
canceled;

:: deftheorem HAHNBAN:def 2 :
canceled;

:: deftheorem Def3 defines subadditive HAHNBAN:def 3 :
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 Def4 defines additive HAHNBAN:def 4 :
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 Def5 defines homogeneous HAHNBAN:def 5 :
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 Def6 defines positively_homogeneous HAHNBAN:def 6 :
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 Def7 defines semi-homogeneous HAHNBAN:def 7 :
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 Def8 defines absolutely_homogeneous HAHNBAN:def 8 :
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 Def9 defines 0-preserving HAHNBAN:def 9 :
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;
cluster additive -> subadditive M5(the carrier of V, REAL );
coherence
for b1 being Functional of V st b1 is additive holds
b1 is subadditive
proof end;
cluster homogeneous -> positively_homogeneous M5(the carrier of V, REAL );
coherence
for b1 being Functional of V st b1 is homogeneous holds
b1 is positively_homogeneous
proof end;
cluster semi-homogeneous -> positively_homogeneous M5(the carrier of V, REAL );
coherence
for b1 being Functional of V st b1 is semi-homogeneous holds
b1 is positively_homogeneous
proof end;
cluster semi-homogeneous -> 0-preserving M5(the carrier of V, REAL );
coherence
for b1 being Functional of V st b1 is semi-homogeneous holds
b1 is 0-preserving
proof end;
cluster absolutely_homogeneous -> semi-homogeneous M5(the carrier of V, REAL );
coherence
for b1 being Functional of V st b1 is absolutely_homogeneous holds
b1 is semi-homogeneous
proof end;
cluster positively_homogeneous 0-preserving -> semi-homogeneous M5(the carrier of V, REAL );
coherence
for b1 being Functional of V st b1 is 0-preserving & b1 is positively_homogeneous holds
b1 is semi-homogeneous
proof end;
end;

registration
let V be RealLinearSpace;
cluster subadditive additive homogeneous positively_homogeneous semi-homogeneous absolutely_homogeneous 0-preserving M5(the carrier of V, REAL );
existence
ex b1 being Functional of V st
( b1 is additive & b1 is absolutely_homogeneous & b1 is homogeneous )
proof end;
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;

theorem Th31: :: HAHNBAN:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being homogeneous Functional of V
for v being VECTOR of V holds L . (- v) = - (L . v)
proof end;

theorem Th32: :: HAHNBAN:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th33: :: HAHNBAN:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealLinearSpace
for L being additive Functional of V holds L . (0. V) = 0
proof end;

theorem Th34: :: HAHNBAN:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

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 Zero of V,the add of V,the Mult of V #) is RealLinearSpace
proof end;

Lm3: for V, V', W' being RealLinearSpace st V' = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) holds
for W being Subspace of V st W' = RLSStruct(# the carrier of W,the Zero of W,the add of W,the Mult of W #) holds
W' is Subspace of V'
proof end;

Lm4: for V, V' being RealLinearSpace st V' = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) holds
for f being linear-Functional of V' holds f is linear-Functional of V
proof end;

Lm5: for V, V' being RealLinearSpace st V' = RLSStruct(# the carrier of V,the Zero of V,the add of V,the Mult of V #) holds
for f being linear-Functional of V holds f is linear-Functional of V'
proof end;

theorem Th35: :: HAHNBAN:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th36: :: HAHNBAN:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being RealNormSpace holds the norm of V is subadditive absolutely_homogeneous Functional of V
proof end;

theorem :: HAHNBAN:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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.|| ) )
proof end;