let V be 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
let M be 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 F be 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 B be FinSequence of REAL ; ( 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 ) }
; M is convex
let u1, v1 be VECTOR of V; CONVEX1:def 2 for b1 being object holds
( b1 <= 0 or 1 <= b1 or not u1 in M or not v1 in M or (b1 * u1) + ((1 - b1) * v1) in M )
let r be Real; ( 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
; (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 ;
( 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)
;
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;
( 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: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;
verum
end;
hence
(r * u1) + ((1 - r) * v1) in M
by A1; verum