let V be non empty RealUnitarySpace-like UNITSTR ; 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; 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; for r being Real st M = { u where u is VECTOR of V : u .|. v <= r } holds
M is convex
let r be Real; ( 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 }
; M is convex
let x, y be VECTOR of V; CONVEX1:def 2 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; ( 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
; (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; verum