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₁ being object holds
( b₁ <= 0 or 1 <= b₁ or not u1 in M or not v1 in M or (b₁ * u1) + ((1 - b₁) * 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 )

proof

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:68;
then ((r * u1) + ((1 - r) * v1)) .|. v < (r * b) + ((1 - r) * (v1 .|. v)) by A14, XREAL_1:8;
then A15: (((r * u1) + ((1 - r) * v1)) .|. v) - (r * b) < (1 - r) * (v1 .|. v) by XREAL_1:19;
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:19;
hence ( v = F . i & ((r * u1) + ((1 - r) * v1)) .|. v < B . i ) by A12; :: thesis: verum

end;

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