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

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