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 & y in M ) ; :: thesis: (s * x) + ((1r - s) * y) in M
consider p being Real such that
A4: ( s = p & 0 < p & p < 1 ) by A2;
ex u1 being VECTOR of V st
( x = u1 & |.(u1 .|. v).| < r ) by A1, A3;
then A12: p * |.(x .|. v).| < p * r by A4, XREAL_1:70;
A6: ex u2 being VECTOR of V st
( y = u2 & |.(u2 .|. v).| < r ) by A1, A3;
A7: |.(((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 ;
( |.(s * (x .|. v)).| = p * |.(x .|. v).| & |.((1r - s) * (y .|. v)).| = (1 - p) * |.(y .|. v).| ) by A4, Th103;
then A11: |.((s * (x .|. v)) + ((1r - s) * (y .|. v))).| <= (p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|) by COMPLEX1:142;
1 - p > 0 by A4, XREAL_1:52;
then (1 - p) * |.(y .|. v).| < (1 - p) * r by A6, XREAL_1:70;
then (p * |.(x .|. v).|) + ((1 - p) * |.(y .|. v).|) < (p * r) + ((1 - p) * r) by A12, XREAL_1:10;
then |.(((s * x) + ((1r - s) * y)) .|. v).| < r by A7, A11, XXREAL_0:2;
hence (s * x) + ((1r - s) * y) in M by A1; :: thesis: verum