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 and
A3: p < 1 and
A4: x in M and
A5: y in M ; :: thesis: (p * x) + ((1 - p) * y) in M
0 + p < 1 by A3;
then A6: 0 < 1 - p by XREAL_1:20;
consider u2 being VECTOR of V such that
A7: y = u2 and
A8: u2 .|. v <= r by A1, A5;
((1 - p) * y) .|. v = (1 - p) * (u2 .|. v) by A7, BHSP_1:def 2;
then A9: ((1 - p) * y) .|. v <= (1 - p) * r by A8, A6, XREAL_1:64;
consider u1 being VECTOR of V such that
A10: x = u1 and
A11: u1 .|. v <= r by A1, A4;
(p * x) .|. v = p * (u1 .|. v) by A10, BHSP_1:def 2;
then A12: (p * x) .|. v <= p * r by A2, A11, XREAL_1:64;
((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 A12, A9, XREAL_1:7;
hence (p * x) + ((1 - p) * y) in M by A1; :: thesis: verum