:: CONVEX1 semantic presentation

definition

let c₁ be non empty RLSStruct ;
let c₂ be Subset of c₁;
let c₃ be Real;
func c₃ * c₂ -> Subset of a₁ equals :: CONVEX1:def 1
{ (a₃ * b₁) where B is Element of a₁ : b₁ in a₂ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines * CONVEX1:def 1 :

definition

let c₁ be non empty RLSStruct ;
let c₂ be Subset of c₁;
attr a₂ is convex means :Def2: :: CONVEX1:def 2
for b₁, b₂ being VECTOR of a₁
for b₃ being Real st 0 < b₃ & b₃ < 1 & b₁ in a₂ & b₂ in a₂ holds
(b₃ * b₁) + ((1 - b₃) * b₂) in a₂;

end;

:: deftheorem Def2 defines convex CONVEX1:def 2 :

theorem Th1: :: CONVEX1:1

for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂ being Subset of b₁
for b₃ being Real st b₂ is convex holds
b₃ * b₂ is convex

proof end;

theorem Th2: :: CONVEX1:2

for b₁ being non empty Abelian add-associative RealLinearSpace-like RLSStruct
for b₂, b₃ being Subset of b₁ st b₂ is convex & b₃ is convex holds
b₂ + b₃ is convex

proof end;

theorem Th3: :: CONVEX1:3

for b₁ being RealLinearSpace
for b₂, b₃ being Subset of b₁ st b₂ is convex & b₃ is convex holds
b₂ - b₃ is convex

proof end;

theorem Th4: :: CONVEX1:4

for b₁ being non empty RLSStruct
for b₂ being Subset of b₁ holds
( b₂ is convex iff for b₃ being Real st 0 < b₃ & b₃ < 1 holds
(b₃ * b₂) + ((1 - b₃) * b₂) c= b₂ )

proof end;

theorem Th5: :: CONVEX1:5

for b₁ being non empty Abelian RLSStruct
for b₂ being Subset of b₁ st b₂ is convex holds
for b₃ being Real st 0 < b₃ & b₃ < 1 holds
((1 - b₃) * b₂) + (b₃ * b₂) c= b₂

proof end;

theorem Th6: :: CONVEX1:6

for b₁ being non empty Abelian add-associative RealLinearSpace-like RLSStruct
for b₂, b₃ being Subset of b₁ st b₂ is convex & b₃ is convex holds
for b₄ being Real holds (b₄ * b₂) + ((1 - b₄) * b₃) is convex

proof end;

Lemma3: for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂ being Subset of b₁ holds 1 * b₂ = b₂

proof end;

Lemma4: for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ holds 0 * b₂ = {(0. b₁)}

proof end;

Lemma5: for b₁ being non empty add-associative LoopStr
for b₂, b₃, b₄ being Subset of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

Lemma6: for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂ being Subset of b₁
for b₃, b₄ being Real holds b₃ * (b₄ * b₂) = (b₃ * b₄) * b₂

proof end;

Lemma7: for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂, b₃ being Subset of b₁
for b₄ being Real holds b₄ * (b₂ + b₃) = (b₄ * b₂) + (b₄ * b₃)

proof end;

theorem Th7: :: CONVEX1:7

for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃ being VECTOR of b₁ holds
( b₂ is convex iff b₃ + b₂ is convex )

proof end;

theorem Th8: :: CONVEX1:8

for b₁ being RealLinearSpace holds Up ((0). b₁) is convex

proof end;

theorem Th9: :: CONVEX1:9

for b₁ being RealLinearSpace holds Up ((Omega). b₁) is convex

proof end;

theorem Th10: :: CONVEX1:10

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

proof end;

theorem Th11: :: CONVEX1:11

for b₁ being non empty Abelian add-associative RealLinearSpace-like RLSStruct
for b₂, b₃ being Subset of b₁
for b₄, b₅ being Real st b₂ is convex & b₃ is convex holds
(b₄ * b₂) + (b₅ * b₃) is convex

proof end;

theorem Th12: :: CONVEX1:12

for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂ being Subset of b₁
for b₃, b₄ being Real holds (b₃ + b₄) * b₂ c= (b₃ * b₂) + (b₄ * b₂)

proof end;

Lemma11: for b₁ being non empty RLSStruct
for b₂, b₃ being Subset of b₁
for b₄ being Real st b₂ c= b₃ holds
b₄ * b₂ c= b₄ * b₃

proof end;

Lemma12: for b₁ being non empty RLSStruct
for b₂ being empty Subset of b₁
for b₃ being Real holds b₃ * b₂ = {}

proof end;

Lemma13: for b₁ being non empty LoopStr
for b₂ being empty Subset of b₁
for b₃ being Subset of b₁ holds b₂ + b₃ = {}

proof end;

Lemma14: for b₁ being non empty right_zeroed LoopStr
for b₂ being Subset of b₁ holds b₂ + {(0. b₁)} = b₂

proof end;

Lemma15: for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃, b₄ being Real st b₃ >= 0 & b₄ >= 0 & b₂ is convex holds
(b₃ * b₂) + (b₄ * b₂) c= (b₃ + b₄) * b₂

proof end;

theorem Th13: :: CONVEX1:13

for b₁ being RealLinearSpace
for b₂ being Subset of b₁
for b₃, b₄ being Real st b₃ >= 0 & b₄ >= 0 & b₂ is convex holds
(b₃ * b₂) + (b₄ * b₂) = (b₃ + b₄) * b₂

proof end;

theorem Th14: :: CONVEX1:14

for b₁ being non empty Abelian add-associative RealLinearSpace-like RLSStruct
for b₂, b₃, b₄ being Subset of b₁
for b₅, b₆, b₇ being Real st b₂ is convex & b₃ is convex & b₄ is convex holds
((b₅ * b₂) + (b₆ * b₃)) + (b₇ * b₄) is convex

proof end;

theorem Th15: :: CONVEX1:15

for b₁ being non empty RLSStruct
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is convex ) holds
meet b₂ is convex

proof end;

theorem Th16: :: CONVEX1:16

for b₁ being non empty RLSStruct
for b₂ being Subset of b₁ st b₂ is Affine holds
b₂ is convex

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

theorem Th17: :: CONVEX1:17

for b₁ being non empty RealUnitarySpace-like UNITSTR
for b₂ being Subset of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₂ = { b₅ where B is VECTOR of b₁ : b₅ .|. b₃ >= b₄ } holds
b₂ is convex

proof end;

theorem Th18: :: CONVEX1:18

for b₁ being non empty RealUnitarySpace-like UNITSTR
for b₂ being Subset of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₂ = { b₅ where B is VECTOR of b₁ : b₅ .|. b₃ > b₄ } holds
b₂ is convex

proof end;

theorem Th19: :: CONVEX1:19

for b₁ being non empty RealUnitarySpace-like UNITSTR
for b₂ being Subset of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₂ = { b₅ where B is VECTOR of b₁ : b₅ .|. b₃ <= b₄ } holds
b₂ is convex

proof end;

theorem Th20: :: CONVEX1:20

for b₁ being non empty RealUnitarySpace-like UNITSTR
for b₂ being Subset of b₁
for b₃ being VECTOR of b₁
for b₄ being Real st b₂ = { b₅ where B is VECTOR of b₁ : b₅ .|. b₃ < b₄ } holds
b₂ is convex

proof end;

definition

let c₁ be RealLinearSpace;
let c₂ be Linear_Combination of c₁;
attr a₂ is convex means :Def3: :: CONVEX1:def 3
ex b₁ being FinSequence of the carrier of a₁ st
( b₁ is one-to-one & rng b₁ = Carrier a₂ & ex b₂ being FinSequence of REAL st
( len b₂ = len b₁ & Sum b₂ = 1 & ( for b₃ being Nat st b₃ in dom b₂ holds
( b₂ . b₃ = a₂ . (b₁ . b₃) & b₂ . b₃ >= 0 ) ) ) );

end;

:: deftheorem Def3 defines convex CONVEX1:def 3 :

theorem Th21: :: CONVEX1:21

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ st b₂ is convex holds
Carrier b₂ <> {}

proof end;

theorem Th22: :: CONVEX1:22

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁
for b₃ being VECTOR of b₁ st b₂ is convex & b₂ . b₃ <= 0 holds
not b₃ in Carrier b₂

proof end;

theorem Th23: :: CONVEX1:23

for b₁ being RealLinearSpace
for b₂ being Linear_Combination of b₁ st b₂ is convex holds
b₂ <> ZeroLC b₁

proof end;

Lemma20: for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Linear_Combination of b₁ st b₃ is convex & Carrier b₃ = {b₂} holds
( b₃ . b₂ = 1 & Sum b₃ = (b₃ . b₂) * b₂ )

proof end;

Lemma21: for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Linear_Combination of b₁ st b₄ is convex & Carrier b₄ = {b₂,b₃} & b₂ <> b₃ holds
( (b₄ . b₂) + (b₄ . b₃) = 1 & b₄ . b₂ >= 0 & b₄ . b₃ >= 0 & Sum b₄ = ((b₄ . b₂) * b₂) + ((b₄ . b₃) * b₃) )

proof end;

Lemma22: for b₁ being FinSequence
for b₂, b₃, b₄ being set st b₁ is one-to-one & rng b₁ = {b₂,b₃,b₄} & b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ & not b₁ = <*b₂,b₃,b₄*> & not b₁ = <*b₂,b₄,b₃*> & not b₁ = <*b₃,b₂,b₄*> & not b₁ = <*b₃,b₄,b₂*> & not b₁ = <*b₄,b₂,b₃*> holds
b₁ = <*b₄,b₃,b₂*>

proof end;

Lemma23: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Linear_Combination of {b₂,b₃,b₄} st b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ holds
Sum b₅ = (((b₅ . b₂) * b₂) + ((b₅ . b₃) * b₃)) + ((b₅ . b₄) * b₄)

proof end;

Lemma24: for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Linear_Combination of b₁ st b₅ is convex & Carrier b₅ = {b₂,b₃,b₄} & b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ holds
( ((b₅ . b₂) + (b₅ . b₃)) + (b₅ . b₄) = 1 & b₅ . b₂ >= 0 & b₅ . b₃ >= 0 & b₅ . b₄ >= 0 & Sum b₅ = (((b₅ . b₂) * b₂) + ((b₅ . b₃) * b₃)) + ((b₅ . b₄) * b₄) )

proof end;

theorem Th24: :: CONVEX1:24

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Linear_Combination of {b₂} st b₃ is convex holds
( b₃ . b₂ = 1 & Sum b₃ = (b₃ . b₂) * b₂ )

proof end;

theorem Th25: :: CONVEX1:25

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Linear_Combination of {b₂,b₃} st b₂ <> b₃ & b₄ is convex holds
( (b₄ . b₂) + (b₄ . b₃) = 1 & b₄ . b₂ >= 0 & b₄ . b₃ >= 0 & Sum b₄ = ((b₄ . b₂) * b₂) + ((b₄ . b₃) * b₃) )

proof end;

theorem Th26: :: CONVEX1:26

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Linear_Combination of {b₂,b₃,b₄} st b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ & b₅ is convex holds
( ((b₅ . b₂) + (b₅ . b₃)) + (b₅ . b₄) = 1 & b₅ . b₂ >= 0 & b₅ . b₃ >= 0 & b₅ . b₄ >= 0 & Sum b₅ = (((b₅ . b₂) * b₂) + ((b₅ . b₃) * b₃)) + ((b₅ . b₄) * b₄) )

proof end;

theorem Th27: :: CONVEX1:27

for b₁ being RealLinearSpace
for b₂ being VECTOR of b₁
for b₃ being Linear_Combination of b₁ st b₃ is convex & Carrier b₃ = {b₂} holds
b₃ . b₂ = 1 by Lemma20;

theorem Th28: :: CONVEX1:28

for b₁ being RealLinearSpace
for b₂, b₃ being VECTOR of b₁
for b₄ being Linear_Combination of b₁ st b₄ is convex & Carrier b₄ = {b₂,b₃} & b₂ <> b₃ holds
( (b₄ . b₂) + (b₄ . b₃) = 1 & b₄ . b₂ >= 0 & b₄ . b₃ >= 0 ) by Lemma21;

theorem Th29: :: CONVEX1:29

for b₁ being RealLinearSpace
for b₂, b₃, b₄ being VECTOR of b₁
for b₅ being Linear_Combination of b₁ st b₅ is convex & Carrier b₅ = {b₂,b₃,b₄} & b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ holds
( ((b₅ . b₂) + (b₅ . b₃)) + (b₅ . b₄) = 1 & b₅ . b₂ >= 0 & b₅ . b₃ >= 0 & b₅ . b₄ >= 0 & Sum b₅ = (((b₅ . b₂) * b₂) + ((b₅ . b₃) * b₃)) + ((b₅ . b₄) * b₄) ) by Lemma24;

definition

let c₁ be non empty RLSStruct ;
let c₂ be Subset of c₁;
func Convex-Family c₂ -> Subset-Family of a₁ means :Def4: :: CONVEX1:def 4
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ( b₁ is convex & a₂ c= b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Convex-Family CONVEX1:def 4 :

definition

let c₁ be non empty RLSStruct ;
let c₂ be Subset of c₁;
func conv c₂ -> convex Subset of a₁ equals :: CONVEX1:def 5
meet (Convex-Family a₂);
coherence

proof end;

end;

:: deftheorem Def5 defines conv CONVEX1:def 5 :

theorem Th30: :: CONVEX1:30

for b₁ being non empty RLSStruct
for b₂ being Subset of b₁
for b₃ being convex Subset of b₁ st b₂ c= b₃ holds
conv b₂ c= b₃

proof end;

theorem Th31: :: CONVEX1:31

for b₁ being FinSequence
for b₂, b₃, b₄ being set st b₁ is one-to-one & rng b₁ = {b₂,b₃,b₄} & b₂ <> b₃ & b₃ <> b₄ & b₄ <> b₂ & not b₁ = <*b₂,b₃,b₄*> & not b₁ = <*b₂,b₄,b₃*> & not b₁ = <*b₃,b₂,b₄*> & not b₁ = <*b₃,b₄,b₂*> & not b₁ = <*b₄,b₂,b₃*> holds
b₁ = <*b₄,b₃,b₂*> by Lemma22;

theorem Th32: :: CONVEX1:32

for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂ being Subset of b₁ holds 1 * b₂ = b₂ by Lemma3;

theorem Th33: :: CONVEX1:33

for b₁ being non empty RLSStruct
for b₂ being empty Subset of b₁
for b₃ being Real holds b₃ * b₂ = {} by Lemma12;

theorem Th34: :: CONVEX1:34

for b₁ being RealLinearSpace
for b₂ being non empty Subset of b₁ holds 0 * b₂ = {(0. b₁)} by Lemma4;

theorem Th35: :: CONVEX1:35

for b₁ being non empty right_zeroed LoopStr
for b₂ being Subset of b₁ holds b₂ + {(0. b₁)} = b₂ by Lemma14;

theorem Th36: :: CONVEX1:36

for b₁ being non empty add-associative LoopStr
for b₂, b₃, b₄ being Subset of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄) by Lemma5;

theorem Th37: :: CONVEX1:37

for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂ being Subset of b₁
for b₃, b₄ being Real holds b₃ * (b₄ * b₂) = (b₃ * b₄) * b₂ by Lemma6;

theorem Th38: :: CONVEX1:38

for b₁ being non empty RealLinearSpace-like RLSStruct
for b₂, b₃ being Subset of b₁
for b₄ being Real holds b₄ * (b₂ + b₃) = (b₄ * b₂) + (b₄ * b₃) by Lemma7;

theorem Th39: :: CONVEX1:39

for b₁ being non empty RLSStruct
for b₂, b₃ being Subset of b₁
for b₄ being Real st b₂ c= b₃ holds
b₄ * b₂ c= b₄ * b₃ by Lemma11;

theorem Th40: :: CONVEX1:40

for b₁ being non empty LoopStr
for b₂ being empty Subset of b₁
for b₃ being Subset of b₁ holds b₂ + b₃ = {} by Lemma13;