CONVEX2: Some Properties for Convex Combinations

:: Some Properties for Convex Combinations
:: by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

reconsider rr = 1 as Element of REAL by XREAL_0:def 1;

set ff = <*rr*>;

theorem :: CONVEX2:1

for V being non empty RLSStruct
for M, N being convex Subset of V holds M /\ N is convex ;

theorem :: CONVEX2:2

for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v <= B . i ) } holds
M is convex

proof end;

theorem :: CONVEX2:3

for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v < B . i ) } holds
M is convex

proof end;

theorem :: CONVEX2:4

for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v >= B . i ) } holds
M is convex

proof end;

theorem :: CONVEX2:5

for V being non empty RealUnitarySpace-like UNITSTR
for M being Subset of V
for F being FinSequence of the carrier of V
for B being FinSequence of REAL st M = { u where u is VECTOR of V : for i being Element of NAT st i in (dom F) /\ (dom B) holds
ex v being VECTOR of V st
( v = F . i & u .|. v > B . i ) } holds
M is convex

proof end;

Lm1: for V being RealLinearSpace
for M being convex Subset of V
for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M

proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

Lm2: for V being RealLinearSpace
for M being Subset of V st ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) holds
M is convex

proof end;

theorem :: CONVEX2:6

for V being RealLinearSpace
for M being Subset of V holds
( ( for N being Subset of V
for L being Linear_Combination of N st L is convex & N c= M holds
Sum L in M ) iff M is convex ) by Lm1, Lm2;

definition

let V be RealLinearSpace;
let M be Subset of V;
defpred S₁[ object ] means $1 is Linear_Combination of M;

func LinComb M -> set means :: CONVEX2:def 1
for L being object holds
( L in it iff L is Linear_Combination of M );

proof end;

proof end;

end;

:: deftheorem defines LinComb CONVEX2:def 1 :

registration

let V be RealLinearSpace;

cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V130() V131() V132() convex for Linear_Combination of V;

proof end;

end;

definition

let V be RealLinearSpace;
mode Convex_Combination of V is convex Linear_Combination of V;

end;

registration

let V be RealLinearSpace;
let M be non empty Subset of V;

cluster Relation-like the carrier of V -defined REAL -valued Function-like quasi_total V130() V131() V132() convex for Linear_Combination of M;

proof end;

end;

definition

let V be RealLinearSpace;
let M be non empty Subset of V;
mode Convex_Combination of M is convex Linear_Combination of M;

end;

Lm3: for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2)

proof end;

Lm4: for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2)

proof end;

theorem :: CONVEX2:7

for V being RealLinearSpace
for M being Subset of V holds Convex-Family M <> {} ;

Lm5: for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2))

proof end;

Lm6: for F, G being Function st F,G are_fiberwise_equipotent holds
for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 )

proof end;

Lm7: for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A

proof end;

theorem Th8: :: CONVEX2:8

for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of V

proof end;

theorem :: CONVEX2:9

for V being RealLinearSpace
for M being non empty Subset of V
for L1, L2 being Convex_Combination of M
for r being Real st 0 < r & r < 1 holds
(r * L1) + ((1 - r) * L2) is Convex_Combination of M

proof end;

theorem :: CONVEX2:10

for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2) by Lm3;

theorem :: CONVEX2:11

for V being RealLinearSpace
for W1, W2 being Subspace of V holds Up (W1 /\ W2) = (Up W1) /\ (Up W2) by Lm4;

theorem :: CONVEX2:12

for V being RealLinearSpace
for L1, L2 being Convex_Combination of V
for a, b being Real st a * b > 0 holds
Carrier ((a * L1) + (b * L2)) = (Carrier (a * L1)) \/ (Carrier (b * L2)) by Lm5;

theorem :: CONVEX2:13

for F, G being Function st F,G are_fiberwise_equipotent holds
for x1, x2 being set st x1 in dom F & x2 in dom F & x1 <> x2 holds
ex z1, z2 being set st
( z1 in dom G & z2 in dom G & z1 <> z2 & F . x1 = G . z1 & F . x2 = G . z2 ) by Lm6;

theorem :: CONVEX2:14

for V being RealLinearSpace
for L being Linear_Combination of V
for A being Subset of V st A c= Carrier L holds
ex L1 being Linear_Combination of V st Carrier L1 = A by Lm7;