:: CONVEX3 semantic presentation

definition

let c₁ be RealLinearSpace;
defpred S₁[ set ] means a₁ is Convex_Combination of c₁;
func ConvexComb c₁ -> set means :Def1: :: CONVEX3:def 1
for b₁ being set holds
( b₁ in a₂ iff b₁ is Convex_Combination of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines ConvexComb CONVEX3:def 1 :

definition

let c₁ be RealLinearSpace;
let c₂ be non empty Subset of c₁;
defpred S₁[ set ] means a₁ is Convex_Combination of c₂;
func ConvexComb c₂ -> set means :: CONVEX3:def 2
for b₁ being set holds
( b₁ in a₃ iff b₁ is Convex_Combination of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ConvexComb CONVEX3:def 2 :

theorem Th1: :: CONVEX3:1

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁ ex b₃ being Convex_Combination of b₁ st
( Sum b₃ = b₂ & ( for b₄ being non empty Subset of b₁ st b₂ in b₄ holds
b₃ is Convex_Combination of b₄ ) )

proof end;

theorem Th2: :: CONVEX3:2

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁ st b₂ <> b₃ holds
ex b₄ being Convex_Combination of b₁ st
for b₅ being non empty Subset of b₁ st {b₂,b₃} c= b₅ holds
b₄ is Convex_Combination of b₅

proof end;

theorem Th3: :: CONVEX3:3

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁ st b₂ <> b₃ & b₂ <> b₄ & b₃ <> b₄ holds
ex b₅ being Convex_Combination of b₁ st
for b₆ being non empty Subset of b₁ st {b₂,b₃,b₄} c= b₆ holds
b₅ is Convex_Combination of b₆

proof end;

Lemma3: for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ st { (Sum b₃) where B is Convex_Combination of b₂ : b₃ in ConvexComb b₁ } c= b₂ holds
b₂ is convex

proof end;

Lemma4: for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁
for b₃ being Convex_Combination of b₂ st card (Carrier b₃) >= 2 holds
ex b₄, b₅ being Convex_Combination of b₂ex b₆ being Real st
( 0 < b₆ & b₆ < 1 & b₃ = (b₆ * b₄) + ((1 - b₆) * b₅) & card (Carrier b₄) = 1 & card (Carrier b₅) = (card (Carrier b₃)) - 1 )

proof end;

Lemma5: for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ st b₂ is convex holds
{ (Sum b₃) where B is Convex_Combination of b₂ : b₃ in ConvexComb b₁ } c= b₂

proof end;

theorem Th4: :: CONVEX3:4

for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ holds
( b₂ is convex iff { (Sum b₃) where B is Convex_Combination of b₂ : b₃ in ConvexComb b₁ } c= b₂ ) by Lemma3, Lemma5;

theorem Th5: :: CONVEX3:5

for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ holds conv b₂ = { (Sum b₃) where B is Convex_Combination of b₂ : b₃ in ConvexComb b₁ }

proof end;

definition

let c₁ be non empty RLSStruct ;
let c₂ be Subset of c₁;
attr a₂ is cone means :Def3: :: CONVEX3:def 3
for b₁ being Real
for b₂ being VECTOR of a₁ st b₁ > 0 & b₂ in a₂ holds
b₁ * b₂ in a₂;

end;

:: deftheorem Def3 defines cone CONVEX3:def 3 :

theorem Th6: :: CONVEX3:6

for b₁ being non empty RLSStruct
for b₂ being Subset of b₁ st b₂ = {} holds
b₂ is cone

proof end;

registration

let c₁ be non empty RLSStruct ;
cluster cone Element of K40(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be non empty RLSStruct ;
cluster empty cone Element of K40(the carrier of a₁);
existence

proof end;

end;

registration

let c₁ be RealLinearSpace;
cluster non empty cone Element of K40(the carrier of a₁);
existence

proof end;

end;

theorem Th7: :: CONVEX3:7

for b₁ being non empty RLSStruct
for b₂ being cone Subset of b₁ st b₁ is RealLinearSpace-like holds
( b₂ is convex iff for b₃, b₄ being VECTOR of b₁ st b₃ in b₂ & b₄ in b₂ holds
b₃ + b₄ in b₂ )

proof end;

Lemma9: for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃ being Linear_Combination of b₂ st card (Carrier b₃) >= 1 holds
ex b₄, b₅ being Linear_Combination of b₂ st
( Sum b₃ = (Sum b₄) + (Sum b₅) & card (Carrier b₄) = 1 & card (Carrier b₅) = (card (Carrier b₃)) - 1 & Carrier b₄ c= Carrier b₃ & Carrier b₅ c= Carrier b₃ & ( for b₆ being VECTOR of b₁ st b₆ in Carrier b₄ holds
b₄ . b₆ = b₃ . b₆ ) & ( for b₆ being VECTOR of b₁ st b₆ in Carrier b₅ holds
b₅ . b₆ = b₃ . b₆ ) )

proof end;

theorem Th8: :: CONVEX3:8

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ holds
( ( b₂ is convex & b₂ is cone ) iff for b₃ being Linear_Combination of b₂ st Carrier b₃ <> {} & ( for b₄ being VECTOR of b₁ st b₄ in Carrier b₃ holds
b₃ . b₄ > 0 ) holds
Sum b₃ in b₂ )

proof end;

theorem Th9: :: CONVEX3:9

for b₁ being non empty RLSStruct
for b₂, b₃ being Subset of b₁ st b₂ is cone & b₃ is cone holds
b₂ /\ b₃ is cone

proof end;