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

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

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

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

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

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

definition

let V be RealLinearSpace;

let M be Subset of V;

defpred S_{1}[ object ] means $1 is Linear_Combination of M;

ex b_{1} being set st

for L being object holds

( L in b_{1} iff L is Linear_Combination of M )

for b_{1}, b_{2} being set st ( for L being object holds

( L in b_{1} iff L is Linear_Combination of M ) ) & ( for L being object holds

( L in b_{2} iff L is Linear_Combination of M ) ) holds

b_{1} = b_{2}

end;
let M be Subset of V;

defpred S

func LinComb M -> set means :: CONVEX2:def 1

for L being object holds

( L in it iff L is Linear_Combination of M );

existence for L being object holds

( L in it iff L is Linear_Combination of M );

ex b

for L being object holds

( L in b

proof end;

uniqueness for b

( L in b

( L in b

b

proof end;

:: deftheorem defines LinComb CONVEX2:def 1 :

for V being RealLinearSpace

for M being Subset of V

for b_{3} being set holds

( b_{3} = LinComb M iff for L being object holds

( L in b_{3} iff L is Linear_Combination of M ) );

for V being RealLinearSpace

for M being Subset of V

for b

( b

( L in b

registration

let V be RealLinearSpace;

ex b_{1} being Linear_Combination of V st b_{1} is convex

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

existence ex b

proof end;

definition
end;

registration

let V be RealLinearSpace;

let M be non empty Subset of V;

ex b_{1} being Linear_Combination of M st b_{1} is convex

end;
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;

existence ex b

proof 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;
let M be non empty Subset of V;

mode Convex_Combination of M is convex Linear_Combination of M;

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

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

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

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

theorem :: CONVEX2:11

theorem :: CONVEX2:12

theorem :: CONVEX2:13

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;

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;