let V be non empty ComplexUnitarySpace-like CUNITSTR ; :: 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 CONVEX4:def 23 :: thesis: for z being Complex st ex r being Real st
( z = r & 0 < r & r < 1 ) & x in M & y in M holds
(z * x) + ((1r - z) * y) in M
let s be Complex; :: thesis: ( ex r being Real st
( s = r & 0 < r & r < 1 ) & x in M & y in M implies (s * x) + ((1r - s) * y) in M )
assume that
A2: ex p being Real st
( s = p & 0 < p & p < 1 ) and
A3: x in M and
A4: y in M ; :: thesis: (s * x) + ((1r - s) * y) in M
consider p being Real such that
A5: s = p and
A6: 0 < p and
A7: p < 1 by A2;
A8: 1 - p > 0 by A7, XREAL_1:50;
ex u2 being VECTOR of V st
( y = u2 & |.(u2 .|. v).| <= r ) by A1, A4;
then A9: (1 - p) * |.(y .|. v).| <= (1 - p) * r by A8, XREAL_1:64;
ex u1 being VECTOR of V st
( x = u1 & |.(u1 .|. v).| <= r ) by A1, A3;
then p * |.(x .|. v).| <= p * r by A6, XREAL_1:64;
then A10: (p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|) <= (p * r) + ((1 - p) * r) by A9, XREAL_1:7;
( |.(s * (x .|. v)).| = p * |.(x .|. v).| & |.((1r - s) * (y .|. v)).| = (1 - p) * |.(y .|. v).| ) by A5, A6, A7, Th44;
then A11: |.((s * (x .|. v)) + ((1r - s) * (y .|. v))).| <= (p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|) by COMPLEX1:56;
|.(((s * x) + ((1r - s) * y)) .|. v).| = |.(((s * x) .|. v) + (((1r - s) * y) .|. v)).| by CSSPACE:def 13
.= |.((s * (x .|. v)) + (((1r - s) * y) .|. v)).| by CSSPACE:def 13
.= |.((s * (x .|. v)) + ((1r - s) * (y .|. v))).| by CSSPACE:def 13 ;
then |.(((s * x) + ((1r - s) * y)) .|. v).| <= r by A11, A10, XXREAL_0:2;
hence (s * x) + ((1r - s) * y) in M by A1; :: thesis: verum