:: HAHNBAN semantic presentation

theorem Th1: :: HAHNBAN:1

canceled;

theorem Th2: :: HAHNBAN:2

canceled;

theorem Th3: :: HAHNBAN:3

for b₁ being non empty set
for b₂ being set st b₁ <> {b₂} holds
ex b₃ being Element of b₁ st b₃ <> b₂

proof end;

theorem Th4: :: HAHNBAN:4

for b₁, b₂ being set
for b₃ being non empty Subset of (PFuncs b₁,b₂) holds b₃ is non empty functional set

proof end;

theorem Th5: :: HAHNBAN:5

for b₁ being non empty functional set
for b₂ being Function st b₂ = union b₁ holds
( dom b₂ = union { (dom b₃) where B is Element of b₁ : verum } & rng b₂ = union { (rng b₃) where B is Element of b₁ : verum } )

proof end;

theorem Th6: :: HAHNBAN:6

for b₁ being non empty Subset of ExtREAL st ( for b₂ being R_eal st b₂ in b₁ holds
b₂ <=' -infty ) holds
b₁ = {-infty }

proof end;

theorem Th7: :: HAHNBAN:7

for b₁ being non empty Subset of ExtREAL st ( for b₂ being R_eal st b₂ in b₁ holds
+infty <=' b₂ ) holds
b₁ = {+infty }

proof end;

theorem Th8: :: HAHNBAN:8

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal st b₂ <' sup b₁ holds
ex b₃ being R_eal st
( b₃ in b₁ & b₂ <' b₃ )

proof end;

theorem Th9: :: HAHNBAN:9

for b₁ being non empty Subset of ExtREAL
for b₂ being R_eal st inf b₁ <' b₂ holds
ex b₃ being R_eal st
( b₃ in b₁ & b₃ <' b₂ )

proof end;

theorem Th10: :: HAHNBAN:10

for b₁, b₂ being non empty Subset of ExtREAL st ( for b₃, b₄ being R_eal st b₃ in b₁ & b₄ in b₂ holds
b₃ <=' b₄ ) holds
sup b₁ <=' inf b₂

proof end;

registration

let c₁ be non empty set ;
cluster non empty c=-linear Element of bool a₁;
existence

proof end;

end;

theorem Th11: :: HAHNBAN:11

canceled;

theorem Th12: :: HAHNBAN:12

canceled;

theorem Th13: :: HAHNBAN:13

for b₁, b₂ being set
for b₃ being c=-linear Subset of (PFuncs b₁,b₂) holds union b₃ in PFuncs b₁,b₂

proof end;

theorem Th14: :: HAHNBAN:14

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds the carrier of b₂ c= the carrier of (b₂ + b₃)

proof end;

theorem Th15: :: HAHNBAN:15

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
for b₄, b₅, b₆ being VECTOR of b₁ st b₅ in b₂ & b₆ in b₃ & b₄ = b₅ + b₆ holds
b₄ |-- b₂,b₃ = [b₅,b₆]

proof end;

theorem Th16: :: HAHNBAN:16

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
for b₄, b₅, b₆ being VECTOR of b₁ st b₄ |-- b₂,b₃ = [b₅,b₆] holds
b₄ = b₅ + b₆

proof end;

theorem Th17: :: HAHNBAN:17

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
for b₄, b₅, b₆ being VECTOR of b₁ st b₄ |-- b₂,b₃ = [b₅,b₆] holds
( b₅ in b₂ & b₆ in b₃ )

proof end;

theorem Th18: :: HAHNBAN:18

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
for b₄, b₅, b₆ being VECTOR of b₁ st b₄ |-- b₂,b₃ = [b₅,b₆] holds
b₄ |-- b₃,b₂ = [b₆,b₅]

proof end;

theorem Th19: :: HAHNBAN:19

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
for b₄ being VECTOR of b₁ st b₄ in b₂ holds
b₄ |-- b₂,b₃ = [b₄,(0. b₁)]

proof end;

theorem Th20: :: HAHNBAN:20

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ st b₁ is_the_direct_sum_of b₂,b₃ holds
for b₄ being VECTOR of b₁ st b₄ in b₃ holds
b₄ |-- b₂,b₃ = [(0. b₁),b₄]

proof end;

theorem Th21: :: HAHNBAN:21

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Subspace of b₂
for b₄ being VECTOR of b₁ st b₄ in b₃ holds
b₄ is VECTOR of b₂

proof end;

theorem Th22: :: HAHNBAN:22

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being Subspace of b₁
for b₅, b₆ being Subspace of b₄ st b₅ = b₂ & b₆ = b₃ holds
b₅ + b₆ = b₂ + b₃

proof end;

theorem Th23: :: HAHNBAN:23

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁
for b₄ being VECTOR of b₂ st b₃ = b₄ holds
Lin {b₄} = Lin {b₃}

proof end;

theorem Th24: :: HAHNBAN:24

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁ st not b₂ in b₃ holds
for b₄ being VECTOR of (b₃ + (Lin {b₂}))
for b₅ being Subspace of b₃ + (Lin {b₂}) st b₂ = b₄ & b₅ = b₃ holds
b₃ + (Lin {b₂}) is_the_direct_sum_of b₅, Lin {b₄}

proof end;

theorem Th25: :: HAHNBAN:25

proof end;

theorem Th26: :: HAHNBAN:26

proof end;

theorem Th27: :: HAHNBAN:27

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃, b₄ being Subspace of b₁ ex b₅, b₆ being VECTOR of b₁ st b₂ |-- b₃,b₄ = [b₅,b₆]

proof end;

theorem Th28: :: HAHNBAN:28

proof end;

theorem Th29: :: HAHNBAN:29

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁
for b₄ being VECTOR of (b₃ + (Lin {b₂}))
for b₅ being Subspace of b₃ + (Lin {b₂}) st b₂ = b₄ & b₃ = b₅ & not b₂ in b₃ holds
for b₆, b₇ being VECTOR of (b₃ + (Lin {b₂}))
for b₈, b₉ being VECTOR of b₃
for b₁₀, b₁₁ being Real st b₆ |-- b₅,(Lin {b₄}) = [b₈,(b₁₀ * b₂)] & b₇ |-- b₅,(Lin {b₄}) = [b₉,(b₁₁ * b₂)] holds
(b₆ + b₇) |-- b₅,(Lin {b₄}) = [(b₈ + b₉),((b₁₀ + b₁₁) * b₂)]

proof end;

theorem Th30: :: HAHNBAN:30

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Subspace of b₁
for b₄ being VECTOR of (b₃ + (Lin {b₂}))
for b₅ being Subspace of b₃ + (Lin {b₂}) st b₂ = b₄ & b₃ = b₅ & not b₂ in b₃ holds
for b₆ being VECTOR of (b₃ + (Lin {b₂}))
for b₇ being VECTOR of b₃
for b₈, b₉ being Real st b₆ |-- b₅,(Lin {b₄}) = [b₇,(b₉ * b₂)] holds
(b₈ * b₆) |-- b₅,(Lin {b₄}) = [(b₈ * b₇),((b₈ * b₉) * b₂)]

proof end;

definition

let c₁ be RLSStruct ;
mode Functional of a₁ is Function of the carrier of a₁, REAL ;

end;

definition

let c₁ be RealLinearSpace;
let c₂ be Functional of c₁;
canceled;
canceled;
attr a₂ is subadditive means :Def3: :: HAHNBAN:def 3
for b₁, b₂ being VECTOR of a₁ holds a₂ . (b₁ + b₂) <= (a₂ . b₁) + (a₂ . b₂);
attr a₂ is additive means :Def4: :: HAHNBAN:def 4
for b₁, b₂ being VECTOR of a₁ holds a₂ . (b₁ + b₂) = (a₂ . b₁) + (a₂ . b₂);
attr a₂ is homogeneous means :Def5: :: HAHNBAN:def 5
for b₁ being VECTOR of a₁
for b₂ being Real holds a₂ . (b₂ * b₁) = b₂ * (a₂ . b₁);
attr a₂ is positively_homogeneous means :Def6: :: HAHNBAN:def 6
for b₁ being VECTOR of a₁
for b₂ being Real st b₂ > 0 holds
a₂ . (b₂ * b₁) = b₂ * (a₂ . b₁);
attr a₂ is semi-homogeneous means :Def7: :: HAHNBAN:def 7
for b₁ being VECTOR of a₁
for b₂ being Real st b₂ >= 0 holds
a₂ . (b₂ * b₁) = b₂ * (a₂ . b₁);
attr a₂ is absolutely_homogeneous means :Def8: :: HAHNBAN:def 8
for b₁ being VECTOR of a₁
for b₂ being Real holds a₂ . (b₂ * b₁) = (abs b₂) * (a₂ . b₁);
attr a₂ is 0-preserving means :Def9: :: HAHNBAN:def 9
a₂ . (0. a₁) = 0;

end;

:: deftheorem Def1 HAHNBAN:def 1 :

:: deftheorem Def2 HAHNBAN:def 2 :

:: 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 :

registration

let c₁ be RealLinearSpace;
cluster additive -> subadditive M5(the carrier of a₁, REAL );
coherence

proof end;

cluster homogeneous -> positively_homogeneous M5(the carrier of a₁, REAL );
coherence

proof end;

cluster semi-homogeneous -> positively_homogeneous M5(the carrier of a₁, REAL );
coherence

proof end;

cluster semi-homogeneous -> 0-preserving M5(the carrier of a₁, REAL );
coherence

proof end;

cluster absolutely_homogeneous -> semi-homogeneous M5(the carrier of a₁, REAL );
coherence

proof end;

cluster positively_homogeneous 0-preserving -> semi-homogeneous M5(the carrier of a₁, REAL );
coherence

proof end;

end;

registration

let c₁ be RealLinearSpace;
cluster subadditive additive homogeneous positively_homogeneous semi-homogeneous absolutely_homogeneous 0-preserving M5(the carrier of a₁, REAL );
existence

proof end;

end;

definition

let c₁ be RealLinearSpace;
mode Banach-Functional of a₁ is subadditive positively_homogeneous Functional of a₁;
mode linear-Functional of a₁ is additive homogeneous Functional of a₁;

end;

theorem Th31: :: HAHNBAN:31

for b₁ being RealLinearSpace
for b₂ being homogeneous Functional of b₁
for b₃ being VECTOR of b₁ holds b₂ . (- b₃) = - (b₂ . b₃)

proof end;

theorem Th32: :: HAHNBAN:32

for b₁ being RealLinearSpace
for b₂ being linear-Functional of b₁
for b₃, b₄ being VECTOR of b₁ holds b₂ . (b₃ - b₄) = (b₂ . b₃) - (b₂ . b₄)

proof end;

theorem Th33: :: HAHNBAN:33

for b₁ being RealLinearSpace
for b₂ being additive Functional of b₁ holds b₂ . (0. b₁) = 0

proof end;

theorem Th34: :: HAHNBAN:34

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being linear-Functional of b₂
for b₄ being VECTOR of b₁
for b₅ being VECTOR of (b₂ + (Lin {b₄})) st b₄ = b₅ & not b₄ in b₂ holds
for b₆ being Real ex b₇ being linear-Functional of (b₂ + (Lin {b₄})) st
( b₇ | the carrier of b₂ = b₃ & b₇ . b₅ = b₆ )

proof end;

Lemma36: for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being VECTOR of b₁ st not b₃ in the carrier of b₂ holds
for b₄ being Banach-Functional of b₁
for b₅ being linear-Functional of b₂ st ( for b₆ being VECTOR of b₂
for b₇ being VECTOR of b₁ st b₆ = b₇ holds
b₅ . b₆ <= b₄ . b₇ ) holds
ex b₆ being linear-Functional of (b₂ + (Lin {b₃})) st
( b₆ | the carrier of b₂ = b₅ & ( for b₇ being VECTOR of (b₂ + (Lin {b₃}))
for b₈ being VECTOR of b₁ st b₇ = b₈ holds
b₆ . b₇ <= b₄ . b₈ ) )

proof end;

Lemma37: for b₁ being RealLinearSpace holds RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) is RealLinearSpace

proof end;

Lemma38: for b₁, b₂, b₃ being RealLinearSpace st b₂ = RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) holds
for b₄ being Subspace of b₁ st b₃ = RLSStruct(# the carrier of b₄,the Zero of b₄,the add of b₄,the Mult of b₄ #) holds
b₃ is Subspace of b₂

proof end;

Lemma39: for b₁, b₂ being RealLinearSpace st b₂ = RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) holds
for b₃ being linear-Functional of b₂ holds b₃ is linear-Functional of b₁

proof end;

Lemma40: for b₁, b₂ being RealLinearSpace st b₂ = RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) holds
for b₃ being linear-Functional of b₁ holds b₃ is linear-Functional of b₂

proof end;

theorem Th35: :: HAHNBAN:35

for b₁ being RealLinearSpace
for b₂ being Subspace of b₁
for b₃ being Banach-Functional of b₁
for b₄ being linear-Functional of b₂ st ( for b₅ being VECTOR of b₂
for b₆ being VECTOR of b₁ st b₅ = b₆ holds
b₄ . b₅ <= b₃ . b₆ ) holds
ex b₅ being linear-Functional of b₁ st
( b₅ | the carrier of b₂ = b₄ & ( for b₆ being VECTOR of b₁ holds b₅ . b₆ <= b₃ . b₆ ) )

proof end;

theorem Th36: :: HAHNBAN:36

for b₁ being RealNormSpace holds the norm of b₁ is subadditive absolutely_homogeneous Functional of b₁

proof end;

theorem Th37: :: HAHNBAN:37

for b₁ being RealNormSpace
for b₂ being Subspace of b₁
for b₃ being linear-Functional of b₂ st ( for b₄ being VECTOR of b₂
for b₅ being VECTOR of b₁ st b₄ = b₅ holds
b₃ . b₄ <= ||.b₅.|| ) holds
ex b₄ being linear-Functional of b₁ st
( b₄ | the carrier of b₂ = b₃ & ( for b₅ being VECTOR of b₁ holds b₄ . b₅ <= ||.b₅.|| ) )

proof end;