let V be non empty RealUnitarySpace-like UNITSTR ; :: thesis: for M being Subset of V
for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds
M is convex
let M be Subset of V; :: thesis: for v being VECTOR of V
for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds
M is convex
let v be VECTOR of V; :: thesis: for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds
M is convex
let r be Real; :: thesis: ( M = { u where u is VECTOR of V : u .|. v <= r } implies M is convex )
assume A1: M = { u where u is VECTOR of V : u .|. v <= r } ; :: thesis: M is convex
let x, y be VECTOR of V; :: according to CONVEX1:def 2 :: thesis: for r being Real st 0 < r & r < 1 & x in M & y in M holds
(r * x) + ((1 - r) * y) in M
let p be Real; :: thesis: ( 0 < p & p < 1 & x in M & y in M implies (p * x) + ((1 - p) * y) in M )
assume that
A2: ( 0 < p & p < 1 ) and
A3: ( x in M & y in M ) ; :: thesis: (p * x) + ((1 - p) * y) in M
consider u1 being VECTOR of V such that
A4: ( x = u1 & u1 .|. v <= r ) by A1, A3;
consider u2 being VECTOR of V such that
A5: ( y = u2 & u2 .|. v <= r ) by A1, A3;
(p * x) .|. v = p * (u1 .|. v) by A4, BHSP_1:def 2;
then A6: (p * x) .|. v <= p * r by A2, A4, XREAL_1:66;
0 + p < 1 by A2;
then A7: 0 < 1 - p by XREAL_1:22;
((1 - p) * y) .|. v = (1 - p) * (u2 .|. v) by A5, BHSP_1:def 2;
then A8: ((1 - p) * y) .|. v <= (1 - p) * r by A5, A7, XREAL_1:66;
((p * x) + ((1 - p) * y)) .|. v = ((p * x) .|. v) + (((1 - p) * y) .|. v) by BHSP_1:def 2;
then ((p * x) + ((1 - p) * y)) .|. v <= (p * r) + ((1 - p) * r) by A6, A8, XREAL_1:9;
hence (p * x) + ((1 - p) * y) in M by A1; :: thesis: verum