let V be non empty RealUnitarySpace-like UNITSTR ; :: thesis: 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

let M be Subset of V; :: thesis: 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

let F be FinSequence of the carrier of V; :: thesis: 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

let B be FinSequence of REAL ; :: thesis: ( 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 ) } implies M is convex )

assume A1: 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 ) } ; :: thesis: M is convex

let u1, v1 be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for b_{1} being object holds

( b_{1} <= 0 or 1 <= b_{1} or not u1 in M or not v1 in M or (b_{1} * u1) + ((1 - b_{1}) * v1) in M )

let r be Real; :: thesis: ( r <= 0 or 1 <= r or not u1 in M or not v1 in M or (r * u1) + ((1 - r) * v1) in M )

assume that

A2: 0 < r and

A3: r < 1 and

A4: u1 in M and

A5: v1 in M ; :: thesis: (r * u1) + ((1 - r) * v1) in M

consider v9 being VECTOR of V such that

A6: v1 = v9 and

A7: for i being Element of NAT st i in (dom F) /\ (dom B) holds

ex v being VECTOR of V st

( v = F . i & v9 .|. v <= B . i ) by A1, A5;

consider u9 being VECTOR of V such that

A8: u1 = u9 and

A9: for i being Element of NAT st i in (dom F) /\ (dom B) holds

ex v being VECTOR of V st

( v = F . i & u9 .|. v <= B . i ) by A1, A4;

for i being Element of NAT st i in (dom F) /\ (dom B) holds

ex v being VECTOR of V st

( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )

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

let M be Subset of V; :: thesis: 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

let F be FinSequence of the carrier of V; :: thesis: 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

let B be FinSequence of REAL ; :: thesis: ( 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 ) } implies M is convex )

assume A1: 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 ) } ; :: thesis: M is convex

let u1, v1 be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for b

( b

let r be Real; :: thesis: ( r <= 0 or 1 <= r or not u1 in M or not v1 in M or (r * u1) + ((1 - r) * v1) in M )

assume that

A2: 0 < r and

A3: r < 1 and

A4: u1 in M and

A5: v1 in M ; :: thesis: (r * u1) + ((1 - r) * v1) in M

consider v9 being VECTOR of V such that

A6: v1 = v9 and

A7: for i being Element of NAT st i in (dom F) /\ (dom B) holds

ex v being VECTOR of V st

( v = F . i & v9 .|. v <= B . i ) by A1, A5;

consider u9 being VECTOR of V such that

A8: u1 = u9 and

A9: for i being Element of NAT st i in (dom F) /\ (dom B) holds

ex v being VECTOR of V st

( v = F . i & u9 .|. v <= B . i ) by A1, A4;

for i being Element of NAT st i in (dom F) /\ (dom B) holds

ex v being VECTOR of V st

( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )

proof

hence
(r * u1) + ((1 - r) * v1) in M
by A1; :: thesis: verum
0 + r < 1
by A3;

then A10: 1 - r > 0 by XREAL_1:20;

let i be Element of NAT ; :: thesis: ( i in (dom F) /\ (dom B) implies ex v being VECTOR of V st

( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i ) )

assume A11: i in (dom F) /\ (dom B) ; :: thesis: ex v being VECTOR of V st

( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )

reconsider b = B . i as Real ;

consider x being VECTOR of V such that

A12: x = F . i and

A13: u9 .|. x <= b by A9, A11;

take v = x; :: thesis: ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )

A14: ((r * u1) + ((1 - r) * v1)) .|. v = ((r * u1) .|. v) + (((1 - r) * v1) .|. v) by BHSP_1:def 2

.= (r * (u1 .|. v)) + (((1 - r) * v1) .|. v) by BHSP_1:def 2

.= (r * (u1 .|. v)) + ((1 - r) * (v1 .|. v)) by BHSP_1:def 2 ;

r * (u1 .|. v) <= r * b by A2, A8, A13, XREAL_1:64;

then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:6;

then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * (v1 .|. v) by XREAL_1:20;

ex y being VECTOR of V st

( y = F . i & v9 .|. y <= b ) by A7, A11;

then (1 - r) * (v1 .|. v) <= (1 - r) * b by A6, A12, A10, XREAL_1:64;

then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * b by A15, XXREAL_0:2;

then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * b) by XREAL_1:20;

hence ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i ) by A12; :: thesis: verum

end;then A10: 1 - r > 0 by XREAL_1:20;

let i be Element of NAT ; :: thesis: ( i in (dom F) /\ (dom B) implies ex v being VECTOR of V st

( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i ) )

assume A11: i in (dom F) /\ (dom B) ; :: thesis: ex v being VECTOR of V st

( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )

reconsider b = B . i as Real ;

consider x being VECTOR of V such that

A12: x = F . i and

A13: u9 .|. x <= b by A9, A11;

take v = x; :: thesis: ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i )

A14: ((r * u1) + ((1 - r) * v1)) .|. v = ((r * u1) .|. v) + (((1 - r) * v1) .|. v) by BHSP_1:def 2

.= (r * (u1 .|. v)) + (((1 - r) * v1) .|. v) by BHSP_1:def 2

.= (r * (u1 .|. v)) + ((1 - r) * (v1 .|. v)) by BHSP_1:def 2 ;

r * (u1 .|. v) <= r * b by A2, A8, A13, XREAL_1:64;

then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:6;

then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * (v1 .|. v) by XREAL_1:20;

ex y being VECTOR of V st

( y = F . i & v9 .|. y <= b ) by A7, A11;

then (1 - r) * (v1 .|. v) <= (1 - r) * b by A6, A12, A10, XREAL_1:64;

then (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) <= (1 - r) * b by A15, XXREAL_0:2;

then ((r * u1) + ((1 - r) * v1)) .|. v <= (r * b) + ((1 - r) * b) by XREAL_1:20;

hence ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v <= B . i ) by A12; :: thesis: verum