:: Hahn Banach Theorem
:: by Bogdan Nowak and Andrzej Trybulec
::
:: Received July 8, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem :: HAHNBAN:1
canceled;
theorem :: HAHNBAN:2
canceled;
theorem Th3: :: HAHNBAN:3
theorem Th4: :: HAHNBAN:4
theorem Th5: :: HAHNBAN:5
theorem :: HAHNBAN:6
theorem :: HAHNBAN:7
theorem Th8: :: HAHNBAN:8
theorem Th9: :: HAHNBAN:9
theorem Th10: :: HAHNBAN:10
theorem :: HAHNBAN:11
canceled;
theorem :: HAHNBAN:12
canceled;
theorem Th13: :: HAHNBAN:13
theorem Th14: :: HAHNBAN:14
theorem Th15: :: HAHNBAN:15
theorem Th16: :: HAHNBAN:16
theorem Th17: :: HAHNBAN:17
theorem Th18: :: HAHNBAN:18
theorem Th19: :: HAHNBAN:19
theorem Th20: :: HAHNBAN:20
theorem Th21: :: HAHNBAN:21
theorem Th22: :: HAHNBAN:22
theorem Th23: :: HAHNBAN:23
theorem Th24: :: HAHNBAN:24
theorem Th25: :: HAHNBAN:25
theorem Th26: :: HAHNBAN:26
theorem Th27: :: HAHNBAN:27
theorem Th28: :: HAHNBAN:28
theorem Th29: :: HAHNBAN:29
theorem Th30: :: HAHNBAN:30
:: deftheorem HAHNBAN:def 1 :
canceled;
:: deftheorem HAHNBAN:def 2 :
canceled;
:: deftheorem Def3 defines subadditive HAHNBAN:def 3 :
:: deftheorem Def4 defines additive HAHNBAN:def 4 :
:: deftheorem Def5 defines homogeneous HAHNBAN:def 5 :
:: deftheorem Def6 defines positively_homogeneous HAHNBAN:def 6 :
:: deftheorem Def7 defines semi-homogeneous HAHNBAN:def 7 :
:: deftheorem Def8 defines absolutely_homogeneous HAHNBAN:def 8 :
:: deftheorem Def9 defines 0-preserving HAHNBAN:def 9 :
theorem Th31: :: HAHNBAN:31
theorem Th32: :: HAHNBAN:32
theorem Th33: :: HAHNBAN:33
theorem Th34: :: HAHNBAN:34
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 ) )
Lm2:
for V being RealLinearSpace holds RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is RealLinearSpace
Lm3:
for V, V', W' being RealLinearSpace st V' = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds
for W being Subspace of V st W' = RLSStruct(# the carrier of W,the U2 of W,the addF of W,the Mult of W #) holds
W' is Subspace of V'
Lm4:
for V, V' being RealLinearSpace st V' = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds
for f being linear-Functional of V' holds f is linear-Functional of V
Lm5:
for V, V' being RealLinearSpace st V' = RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds
for f being linear-Functional of V holds f is linear-Functional of V'
theorem Th35: :: HAHNBAN:35
theorem Th36: :: HAHNBAN:36
theorem :: HAHNBAN:37