:: CONVEX2 semantic presentation

theorem Th1: :: CONVEX2:1

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

proof end;

theorem Th2: :: CONVEX2:2

for b₁ being non empty RealUnitarySpace-like UNITSTR
for b₂ being Subset of b₁
for b₃ being FinSequence of the carrier of b₁
for b₄ being FinSequence of REAL st b₂ = { b₅ where B is VECTOR of b₁ : for b₁ being Nat st b₆ in (dom b₃) /\ (dom b₄) holds
ex b₂ being VECTOR of b₁ st
( b₇ = b₃ . b₆ & b₅ .|. b₇ <= b₄ . b₆ ) } holds
b₂ is convex

proof end;

theorem Th3: :: CONVEX2:3

proof end;

theorem Th4: :: CONVEX2:4

proof end;

theorem Th5: :: CONVEX2:5

proof end;

Lemma1: for b₁ being RealLinearSpace
for b₂ being convex Subset of b₁
for b₃ being Subset of b₁
for b₄ being Linear_Combination of b₃ st b₄ is convex & b₃ c= b₂ holds
Sum b₄ in b₂

proof end;

Lemma2: for b₁ being RealLinearSpace
for b₂ being Subset of b₁ st ( for b₃ being Subset of b₁
for b₄ being Linear_Combination of b₃ st b₄ is convex & b₃ c= b₂ holds
Sum b₄ in b₂ ) holds
b₂ is convex

proof end;

theorem Th6: :: CONVEX2:6

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ holds
( ( for b₃ being Subset of b₁
for b₄ being Linear_Combination of b₃ st b₄ is convex & b₃ c= b₂ holds
Sum b₄ in b₂ ) iff b₂ is convex ) by Lemma1, Lemma2;

definition

let c₁ be RealLinearSpace;
let c₂ be Subset of c₁;
defpred S₁[ set ] means a₁ is Linear_Combination of c₂;
func LinComb c₂ -> set means :: CONVEX2:def 1
for b₁ being set holds
( b₁ in a₃ iff b₁ is Linear_Combination of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines LinComb CONVEX2:def 1 :

Lemma3: for b₁ being RealLinearSpace ex b₂ being Linear_Combination of b₁ st b₂ is convex

proof end;

registration

let c₁ be RealLinearSpace;
cluster convex Linear_Combination of a₁;
existence by Lemma3;

end;

definition

let c₁ be RealLinearSpace;
mode Convex_Combination of a₁ is convex Linear_Combination of a₁;

end;

Lemma4: for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ ex b₃ being Linear_Combination of b₂ st b₃ is convex

proof end;

registration

let c₁ be RealLinearSpace;
let c₂ be non empty Subset of c₁;
cluster convex Linear_Combination of a₂;
existence by Lemma4;

end;

definition

let c₁ be RealLinearSpace;
let c₂ be non empty Subset of c₁;
mode Convex_Combination of a₂ is convex Linear_Combination of a₂;

end;

Lemma5: for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds Up (b₂ + b₃) = (Up b₂) + (Up b₃)

proof end;

Lemma6: for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds Up (b₂ /\ b₃) = (Up b₂) /\ (Up b₃)

proof end;

theorem Th7: :: CONVEX2:7

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ holds Convex-Family b₂ <> {}

proof end;

theorem Th8: :: CONVEX2:8

for b₁ being RealLinearSpace
for b₂ being Subset of b₁ holds b₂ c= conv b₂

proof end;

Lemma8: for b₁ being RealLinearSpace
for b₂, b₃ being Convex_Combination of b₁
for b₄, b₅ being Real st b₄ * b₅ > 0 holds
Carrier ((b₄ * b₂) + (b₅ * b₃)) = (Carrier (b₄ * b₂)) \/ (Carrier (b₅ * b₃))

proof end;

Lemma9: for b₁, b₂ being Function st b₁,b₂ are_fiberwise_equipotent holds
for b₃, b₄ being set st b₃ in dom b₁ & b₄ in dom b₁ & b₃ <> b₄ holds
ex b₅, b₆ being set st
( b₅ in dom b₂ & b₆ in dom b₂ & b₅ <> b₆ & b₁ . b₃ = b₂ . b₅ & b₁ . b₄ = b₂ . b₆ )

proof end;

Lemma10: for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being Subset of b₁ st b₃ c= Carrier b₂ holds
ex b₄ being Linear_Combination of b₁ st Carrier b₄ = b₃

proof end;

theorem Th9: :: CONVEX2:9

for b₁ being RealLinearSpace
for b₂, b₃ being Convex_Combination of b₁
for b₄ being Real st 0 < b₄ & b₄ < 1 holds
(b₄ * b₂) + ((1 - b₄) * b₃) is Convex_Combination of b₁

proof end;

theorem Th10: :: CONVEX2:10

for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁
for b₃, b₄ being Convex_Combination of b₂
for b₅ being Real st 0 < b₅ & b₅ < 1 holds
(b₅ * b₃) + ((1 - b₅) * b₄) is Convex_Combination of b₂

proof end;

theorem Th11: :: CONVEX2:11

for b₁ being RealLinearSpace ex b₂ being Linear_Combination of b₁ st b₂ is convex by Lemma3;

theorem Th12: :: CONVEX2:12

for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ ex b₃ being Linear_Combination of b₂ st b₃ is convex by Lemma4;

theorem Th13: :: CONVEX2:13

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds Up (b₂ + b₃) = (Up b₂) + (Up b₃) by Lemma5;

theorem Th14: :: CONVEX2:14

for b₁ being RealLinearSpace
for b₂, b₃ being Subspace of b₁ holds Up (b₂ /\ b₃) = (Up b₂) /\ (Up b₃) by Lemma6;

theorem Th15: :: CONVEX2:15

for b₁ being RealLinearSpace
for b₂, b₃ being Convex_Combination of b₁
for b₄, b₅ being Real st b₄ * b₅ > 0 holds
Carrier ((b₄ * b₂) + (b₅ * b₃)) = (Carrier (b₄ * b₂)) \/ (Carrier (b₅ * b₃)) by Lemma8;

theorem Th16: :: CONVEX2:16

for b₁, b₂ being Function st b₁,b₂ are_fiberwise_equipotent holds
for b₃, b₄ being set st b₃ in dom b₁ & b₄ in dom b₁ & b₃ <> b₄ holds
ex b₅, b₆ being set st
( b₅ in dom b₂ & b₆ in dom b₂ & b₅ <> b₆ & b₁ . b₃ = b₂ . b₅ & b₁ . b₄ = b₂ . b₆ ) by Lemma9;

theorem Th17: :: CONVEX2:17

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being Subset of b₁ st b₃ c= Carrier b₂ holds
ex b₄ being Linear_Combination of b₁ st Carrier b₄ = b₃ by Lemma10;